Theorems · Theorem · real analysis

MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable

∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} (a b : Fin (n + 1) → ℝ),
  a ≤ b →
    ∀ (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 →
        ContinuousOn f (Set.Icc a b) →
          (∀ x ∈ (Set.univ.pi fun i => Set.Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x) →
            MeasureTheory.IntegrableOn (fun x => ∑ i, (f' x) (Pi.single i 1) i) (Set.Icc a b) MeasureTheory.volume →
              ∫ (x : Fin (n + 1) → ℝ) in Set.Icc a b, ∑ i, (f' x) (Pi.single i 1) i =
                ∑ i,
                  ((∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (b i) x) i) -
                    ∫ (x : Fin n → ℝ) in Set.Icc (a ∘ i.succAbove) (b ∘ i.succAbove), f (i.insertNth (a i) x) i)

Divergence theorem for Bochner integral. If f : ℝⁿ⁺¹ → Eⁿ⁺¹ is continuous on a rectangular box [a, b] : Set ℝⁿ⁺¹, a ≤ b, is differentiable on its interior with derivative f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹ and the divergence fun x ↦ ∑ i, f' x eᵢ i is integrable on [a, b], where eᵢ = Pi.single i 1 is the i-th basis vector, then its integral is equal to the sum of integrals of f over the faces of [a, b], taken with appropriate signs. Moreover, the same is true if the function is not differentiable at countably many points of the interior of [a, b]. We represent both faces x i = a i and x i = b i as the box face i = [a ∘ Fin.succAbove i, b ∘ Fin.succAbove i] in ℝⁿ, where Fin.succAbove : Fin n ↪o Fin (n + 1) is the order embedding with range {i}ᶜ. The restrictions of f : ℝⁿ⁺¹ → Eⁿ⁺¹ to these faces are given by f ∘ backFace i and f ∘ frontFace i, where backFace i = Fin.insertNth i (a i) and frontFace i = Fin.insertNth i (b i) are embeddings ℝⁿ → ℝⁿ⁺¹ that take y : ℝⁿ and insert a i (resp., b i) as i-th coordinate.

Defined in

Mathlib.MeasureTheory.Integral.DivergenceTheorem

Cited by

1 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace