feat(measure_theory/integral): Divergence theorem for Bochner integral (

#9811)

src/measure_theory/integral/divergence_theorem.lean

@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2021 Yury Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury Kudryashov
+-/
+import analysis.box_integral.divergence_theorem
+import analysis.box_integral.integrability
+import measure_theory.integral.interval_integral
+
+/-!
+# Divergence theorem for Bochner integral
+
+In this file we prove the Divergence theorem for Bochner integral on a box in
+`ℝⁿ⁺¹ = fin (n + 1) → ℝ`. More precisely, we prove the following theorem.
+
+Let `E` be a complete normed space with second countably topology. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is
+differentiable on a rectangular box `[a, b] : set ℝⁿ⁺¹`, `a ≤ b`, with derivative
+`f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹` and the divergence `λ 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 appropriat signs. Moreover, the same is true
+if the function is not differentiable but continuous at countably many points of `[a, b]`.
+
+## Notations
+
+We use the following local notation to make the statement more readable. Note that the documentation
+website shows the actual terms, not those abbreviated using local notations.
+
+* `ℝⁿ`, `ℝⁿ⁺¹`, `Eⁿ⁺¹`: `fin n → ℝ`, `fin (n + 1) → ℝ`, `fin (n + 1) → E`;
+* `face i`: the `i`-th face of the box `[a, b]` as a closed segment in `ℝⁿ`, namely `[a ∘
+  fin.succ_above i, b ∘ fin.succ_above i]`;
+* `e i` : `i`-th basis vector `pi.single i 1`;
+* `front_face i`, `back_face i`: embeddings `ℝⁿ → ℝⁿ⁺¹` corresponding to the front face
+  `{x | x i = b i}` and back face `{x | x i = a i}` of the box `[a, b]`, respectively.
+  They are given by `fin.insert_nth i (b i)` and `fin.insert_nth i (a i)`.
+
+## TODO
+
+* Deduce corollaries about integrals in `ℝ × ℝ` and interval integral.
+* Add a version that assumes existence and integrability of partial derivatives.
+
+## Tags
+
+divergence theorem, Bochner integral
+-/
+
+open set finset topological_space function box_integral
+open_locale big_operators classical
+
+namespace measure_theory
+
+universes u
+variables {E : Type u} [normed_group E] [normed_space ℝ E] [measurable_space E] [borel_space E]
+  [second_countable_topology E] [complete_space E]
+
+section
+variables {n : ℕ}
+
+local notation `ℝⁿ` := fin n → ℝ
+local notation `ℝⁿ⁺¹` := fin (n + 1) → ℝ
+local notation `Eⁿ⁺¹` := fin (n + 1) → E
+
+variables (a b : ℝⁿ⁺¹)
+
+local notation `face` i := set.Icc (a ∘ fin.succ_above i) (b ∘ fin.succ_above i)
+local notation `e` i := pi.single i 1
+local notation `front_face` i:2000 := fin.insert_nth i (b i)
+local notation `back_face` i:2000 := fin.insert_nth i (a i)
+
+/-- **Divergence theorem** for Bochner integral. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is differentiable on a
+rectangular box `[a, b] : set ℝⁿ⁺¹`, `a ≤ b`, with derivative `f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹` and the
+divergence `λ 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 appropriat signs.
+
+Moreover, the same is true if the function is not differentiable but continuous at countably many
+points of `[a, b]`.
+
+We represent both faces `x i = a i` and `x i = b i` as the box
+`face i = [a ∘ fin.succ_above i, b ∘ fin.succ_above i]` in `ℝⁿ`, where
+`fin.succ_above : 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 ∘ back_face i` and `f ∘ front_face i`, where
+`back_face i = fin.insert_nth i (a i)` and `front_face i = fin.insert_nth i (b i)` are embeddings
+`ℝⁿ → ℝⁿ⁺¹` that take `y : ℝⁿ` and insert `a i` (resp., `b i`) as `i`-th coordinate. -/
+lemma integral_divergence_of_has_fderiv_within_at_off_countable (hle : a ≤ b) (f : ℝⁿ⁺¹ → Eⁿ⁺¹)
+  (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : set ℝⁿ⁺¹) (hs : countable s)
+  (Hc : ∀ x ∈ s, continuous_within_at f (Icc a b) x)
+  (Hd : ∀ x ∈ Icc a b \ s, has_fderiv_within_at f (f' x) (Icc a b) x)
+  (Hi : integrable_on (λ x, ∑ i, f' x (pi.single i 1) i) (Icc a b)) :
+  ∫ x in Icc a b, ∑ i, f' x (e i) i =
+    ∑ i : fin (n + 1),
+      ((∫ x in face i, f (front_face i x) i) - ∫ x in face i, f (back_face i x) i) :=
+begin
+  simp only [volume_pi, ← set_integral_congr_set_ae measure.univ_pi_Ioc_ae_eq_Icc],
+  by_cases heq : ∃ i, a i = b i,
+  { rcases heq with ⟨i, hi⟩,
+    have hi' : Ioc (a i) (b i) = ∅ := Ioc_eq_empty hi.not_lt,
+    have : pi set.univ (λ j, Ioc (a j) (b j)) = ∅, from univ_pi_eq_empty hi',
+    rw [this, integral_empty, sum_eq_zero],
+    rintro j -,
+    rcases eq_or_ne i j with rfl|hne,
+    { simp [hi] },
+    { rcases fin.exists_succ_above_eq hne with ⟨i, rfl⟩,
+      have : pi set.univ (λ k : fin n, Ioc (a $ j.succ_above k) (b $ j.succ_above k)) = ∅,
+        from univ_pi_eq_empty hi',
+      rw [this, integral_empty, integral_empty, sub_self] } },
+  { push_neg at heq,
+    obtain ⟨I, rfl, rfl⟩ : ∃ I : box_integral.box (fin (n + 1)), I.lower = a ∧ I.upper = b,
+      from ⟨⟨a, b, λ i, (hle i).lt_of_ne (heq i)⟩, rfl, rfl⟩,
+    simp only [← box.coe_eq_pi, ← box.face_lower, ← box.face_upper],
+    have A := ((Hi.mono_set box.coe_subset_Icc).has_box_integral ⊥ rfl),
+    have B := has_integral_bot_divergence_of_forall_has_deriv_within_at I f f' s hs Hc Hd,
+    have Hc : continuous_on f I.Icc,
+    { intros x hx,
+      by_cases hxs : x ∈ s,
+      exacts [Hc x hxs, (Hd x ⟨hx, hxs⟩).continuous_within_at] },
+    rw continuous_on_pi at Hc,
+    refine (A.unique B).trans (sum_congr rfl $ λ i hi, _),
+    refine congr_arg2 has_sub.sub _ _,
+    { have := box.continuous_on_face_Icc (Hc i) (right_mem_Icc.2 (hle i)),
+      have := (this.integrable_on_compact (box.is_compact_Icc _)).mono_set box.coe_subset_Icc,
+      exact (this.has_box_integral ⊥ rfl).integral_eq, apply_instance },
+    { have := box.continuous_on_face_Icc (Hc i) (left_mem_Icc.2 (hle i)),
+      have := (this.integrable_on_compact (box.is_compact_Icc _)).mono_set box.coe_subset_Icc,
+      exact (this.has_box_integral ⊥ rfl).integral_eq, apply_instance } }
+end
+
+end
+
+end measure_theory