Theorems · Theorem · real analysis

BoxIntegral.hasIntegral_GP_pderiv

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [CompleteSpace E]
  (I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E)
  (s : Set (Fin (n + 1) → ℝ)),
  s.Countable →
    (∀ x ∈ s, ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) →
      (∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) →
        ∀ (i : Fin (n + 1)),
          BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => (f' x) (Pi.single i 1))
            BoxIntegral.BoxAdditiveMap.volume
            (BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x))
                BoxIntegral.BoxAdditiveMap.volume -
              BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x))
                BoxIntegral.BoxAdditiveMap.volume)

If f : ℝⁿ⁺¹ → E is differentiable on a closed rectangular box I with derivative f', then the partial derivative fun x ↦ f' x (Pi.single i 1) is Henstock-Kurzweil integrable with integral equal to the difference of integrals of f over the faces x i = I.upper i and x i = I.lower i. More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and we allow f to be non-differentiable (but still continuous) at a countable set of points. TODO: If n > 0, then the condition at x ∈ s can be replaced by a much weaker estimate but this requires either better integrability theorems, or usage of a filter depending on the countable set s (we need to ensure that none of the faces of a partition contain a point from s).

Defined in

Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Cited by

1 results in Mathlib

Foundations

Depth 251 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace