English
If f ω satisfy differentiability on interior away from a countable set and appropriate integrability, then the integral of the divergence equals the sum of boundary face integrals.
Русский
Если функции удовлетворяют условиям дивергенции (с дифференцируемостью внутри и интегрируемостью), то интеграл дивергенции равен сумме поверхностей границы.
LaTeX
$$$\\int_{Icc} \\text{div}(f) = \\sum_{i} \\text{boundary faces}(f_i)$$$
Lean4
/-- **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. -/
theorem integral_divergence_of_hasFDerivAt_off_countable (hle : a ≤ b) (f : ℝⁿ⁺¹ → Eⁿ⁺¹) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹)
(s : Set ℝⁿ⁺¹) (hs : s.Countable) (Hc : ContinuousOn f (Icc a b))
(Hd : ∀ x ∈ (Set.pi univ fun i => Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x)
(Hi : IntegrableOn (fun x => ∑ i, f' x (e i) i) (Icc a b)) :
(∫ x in Icc a b, ∑ i, f' x (e i) i) =
∑ i : Fin (n + 1), ((∫ x in face i, f (frontFace i x) i) - ∫ x in face i, f (backFace i x) i) :=
by
rcases em (∃ i, a i = b i) with (⟨i, hi⟩ | hne)
· -- First we sort out the trivial case `∃ i, a i = b i`.
rw [volume_pi, ← setIntegral_congr_set Measure.univ_pi_Ioc_ae_eq_Icc]
have hi' : Ioc (a i) (b i) = ∅ := Ioc_eq_empty hi.not_lt
have : (pi Set.univ fun j => Ioc (a j) (b j)) = ∅ := univ_pi_eq_empty hi'
rw [this, setIntegral_empty, sum_eq_zero]
rintro j -
rcases eq_or_ne i j with (rfl | hne)
· simp [hi]
· rcases Fin.exists_succAbove_eq hne with ⟨i, rfl⟩
have : Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] (∅ : Set ℝⁿ) :=
by
rw [ae_eq_empty, Real.volume_Icc_pi, prod_eq_zero (Finset.mem_univ i)]
simp [hi]
rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty, setIntegral_empty, sub_self]
· -- In the non-trivial case `∀ i, a i < b i`, we apply a lemma we proved above.
have hlt : ∀ i, a i < b i := fun i => (hle i).lt_of_ne fun hi => hne ⟨i, hi⟩
exact integral_divergence_of_hasFDerivAt_off_countable_aux₂ ⟨a, b, hlt⟩ f f' s hs Hc Hd Hi
