Theorems · Theorem · real analysis

BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [CompleteSpace E]
  (I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → Fin (n + 1) → E)
  (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] Fin (n + 1) → 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) →
        BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => ∑ i, (f' x) (Pi.single i 1) i)
          BoxIntegral.BoxAdditiveMap.volume
          (∑ i,
            (BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x) i)
                BoxIntegral.BoxAdditiveMap.volume -
              BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP
                (fun x => f (i.insertNth (I.lower i) x) i) BoxIntegral.BoxAdditiveMap.volume))

Divergence theorem for a Henstock-Kurzweil style integral. If f : ℝⁿ⁺¹ → Eⁿ⁺¹ is differentiable on a closed rectangular box I with derivative f', then the divergence ∑ i, f' x (Pi.single i 1) i is Henstock-Kurzweil integrable with integral equal to the sum of integrals of f over the faces of I taken with appropriate signs. 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.

Defined in

Mathlib.Analysis.BoxIntegral.DivergenceTheorem

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace