Exact source: Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
Pinned GitHub source · Raw UTF-8 source
Back to Zero integral of a compactly supported divergence
1/-2Copyright (c) 2021 Yury Kudryashov. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Yury Kudryashov5-/6module78public import Mathlib.Analysis.BoxIntegral.DivergenceTheorem9public import Mathlib.Analysis.BoxIntegral.Integrability10public import Mathlib.Analysis.Calculus.Deriv.Basic11public import Mathlib.Analysis.Calculus.FDeriv.Equiv12public import Mathlib.MeasureTheory.Integral.Prod13public import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic1415/-!16# Divergence theorem for Bochner integral1718In this file we prove the Divergence theorem for Bochner integral on a box in19`ℝⁿ⁺¹ = Fin (n + 1) → ℝ`. More precisely, we prove the following theorem.2021Let `E` be a complete normed space. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is22continuous on a rectangular box `[a, b] : Set ℝⁿ⁺¹`, `a ≤ b`, differentiable on its interior with23derivative `f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹`, and the divergence `fun x ↦ ∑ i, f' x eᵢ i`24is integrable on `[a, b]`, where `eᵢ = Pi.single i 1` is the `i`-th basis vector,25then its integral is equal to the sum of integrals of `f` over the faces of `[a, b]`,26taken with appropriate signs. Moreover, the same27is true if the function is not differentiable at countably many points of the interior of `[a, b]`.2829Once we prove the general theorem, we deduce corollaries for functions `ℝ → E` and pairs of30functions `(ℝ × ℝ) → E`.3132## Notation3334We use the following local notation to make the statement more readable. Note that the documentation35website shows the actual terms, not those abbreviated using local notations.3637* `ℝⁿ`, `ℝⁿ⁺¹`, `Eⁿ⁺¹`: `Fin n → ℝ`, `Fin (n + 1) → ℝ`, `Fin (n + 1) → E`;38* `face i`: the `i`-th face of the box `[a, b]` as a closed segment in `ℝⁿ`, namely39 `[a ∘ Fin.succAbove i, b ∘ Fin.succAbove i]`;40* `e i` : `i`-th basis vector `Pi.single i 1`;41* `frontFace i`, `backFace i`: embeddings `ℝⁿ → ℝⁿ⁺¹` corresponding to the front face42 `{x | x i = b i}` and back face `{x | x i = a i}` of the box `[a, b]`, respectively.43 They are given by `Fin.insertNth i (b i)` and `Fin.insertNth i (a i)`.4445## TODO4647* Add a version that assumes existence and integrability of partial derivatives.4849## Tags5051divergence theorem, Bochner integral52-/5354public section555657open Set Finset TopologicalSpace Function BoxIntegral MeasureTheory Filter5859open scoped Topology Interval6061universe u6263namespace MeasureTheory6465variable {E : Type u} [NormedAddCommGroup E] [NormedSpace ℝ E]6667section6869variable {n : ℕ}7071local macro:arg t:term:max noWs "ⁿ" : term => `(Fin n → $t)7273local macro:arg t:term:max noWs "ⁿ⁺¹" : term => `(Fin (n + 1) → $t)7475local notation "e " i => Pi.single i 17677section7879/-!80### Divergence theorem for functions on `ℝⁿ⁺¹ = Fin (n + 1) → ℝ`.8182In this section we use the divergence theorem for a Henstock-Kurzweil-like integral83`BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt` to prove the divergence84theorem for Bochner integral. The divergence theorem for Bochner integral85`MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable` assumes that the function86itself is continuous on a closed box, differentiable at all but countably many points of its87interior, and the divergence is integrable on the box.8889This statement differs from `BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt`90in several aspects.9192* We use Bochner integral instead of a Henstock-Kurzweil integral. This modification is done in93 `MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁`. As a side effect94 of this change, we need to assume that the divergence is integrable.9596* We don't assume differentiability on the boundary of the box. This modification is done in97 `MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable_aux₂`. To prove it, we98 choose an increasing sequence of smaller boxes that cover the interior of the original box, then99 apply the previous lemma to these smaller boxes and take the limit of both sides of the equation.100101* We assume `a ≤ b` instead of `∀ i, a i < b i`. This is the last step of the proof, and it is done102 in the main theorem `MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable`.103-/104105/-- An auxiliary lemma for106`MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable`. This is exactly107`BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt` reformulated for the108Bochner integral. -/109private theorem integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ (I : Box (Fin (n + 1)))110 (f : ℝⁿ⁺¹ → Eⁿ⁺¹)111 (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : Set ℝⁿ⁺¹)112 (hs : s.Countable) (Hc : ContinuousOn f (Box.Icc I))113 (Hd : ∀ x ∈ (Box.Icc I) \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x)114 (Hi : IntegrableOn (fun x => ∑ i, f' x (e i) i) (Box.Icc I)) :115 (∫ x in Box.Icc I, ∑ i, f' x (e i) i) =116 ∑ i : Fin (n + 1),117 ((∫ x in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -118 ∫ x in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i) := by119 wlog hE : CompleteSpace E generalizing120 · simp [integral, hE]121 simp only [← setIntegral_congr_set (Box.coe_ae_eq_Icc _)]122 have A := (Hi.mono_set Box.coe_subset_Icc).hasBoxIntegral ⊥ rfl123 have B :=124 hasIntegral_GP_divergence_of_forall_hasDerivWithinAt I f f' (s ∩ Box.Icc I)125 (hs.mono inter_subset_left) (fun x hx => Hc _ hx.2) fun x hx =>126 Hd _ ⟨hx.1, fun h => hx.2 ⟨h, hx.1⟩⟩127 rw [continuousOn_pi] at Hc128 refine (A.unique B).trans (sum_congr rfl fun i _ => ?_)129 refine congr_arg₂ Sub.sub ?_ ?_130 · have := Box.continuousOn_face_Icc (Hc i) (Set.right_mem_Icc.2 (I.lower_le_upper i))131 have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set132 Box.coe_subset_Icc133 exact (this.hasBoxIntegral ⊥ rfl).integral_eq134 · have := Box.continuousOn_face_Icc (Hc i) (Set.left_mem_Icc.2 (I.lower_le_upper i))135 have := (this.integrableOn_compact (μ := volume) (Box.isCompact_Icc _)).mono_set136 Box.coe_subset_Icc137 exact (this.hasBoxIntegral ⊥ rfl).integral_eq138139/-- An auxiliary lemma for140`MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable`. Compared to the previous141lemma, here we drop the assumption of differentiability on the boundary of the box. -/142private theorem integral_divergence_of_hasFDerivAt_off_countable_aux₂ (I : Box (Fin (n + 1)))143 (f : ℝⁿ⁺¹ → Eⁿ⁺¹)144 (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹)145 (s : Set ℝⁿ⁺¹) (hs : s.Countable) (Hc : ContinuousOn f (Box.Icc I))146 (Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x)147 (Hi : IntegrableOn (∑ i, f' · (e i) i) (Box.Icc I)) :148 (∫ x in Box.Icc I, ∑ i, f' x (e i) i) =149 ∑ i : Fin (n + 1),150 ((∫ x in Box.Icc (I.face i), f (i.insertNth (I.upper i) x) i) -151 ∫ x in Box.Icc (I.face i), f (i.insertNth (I.lower i) x) i) := by152 /- Choose a monotone sequence `J k` of subboxes that cover the interior of `I` and prove that153 these boxes satisfy the assumptions of the previous lemma. -/154 rcases I.exists_seq_mono_tendsto with ⟨J, hJ_sub, hJl, hJu⟩155 have hJ_sub' : ∀ k, Box.Icc (J k) ⊆ Box.Icc I := fun k => (hJ_sub k).trans I.Ioo_subset_Icc156 have hJ_le : ∀ k, J k ≤ I := fun k => Box.le_iff_Icc.2 (hJ_sub' k)157 have HcJ : ∀ k, ContinuousOn f (Box.Icc (J k)) := fun k => Hc.mono (hJ_sub' k)158 have HdJ : ∀ (k), ∀ x ∈ (Box.Icc (J k)) \ s, HasFDerivWithinAt f (f' x) (Box.Icc (J k)) x :=159 fun k x hx => (Hd x ⟨hJ_sub k hx.1, hx.2⟩).hasFDerivWithinAt160 have HiJ : ∀ k, IntegrableOn (∑ i, f' · (e i) i) (Box.Icc (J k)) volume := fun k =>161 Hi.mono_set (hJ_sub' k)162 -- Apply the previous lemma to `J k`.163 have HJ_eq := fun k =>164 integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ (J k) f f' s hs (HcJ k) (HdJ k)165 (HiJ k)166 -- Note that the LHS of `HJ_eq k` tends to the LHS of the goal as `k → ∞`.167 have hI_tendsto :168 Tendsto (fun k => ∫ x in Box.Icc (J k), ∑ i, f' x (e i) i) atTop169 (𝓝 (∫ x in Box.Icc I, ∑ i, f' x (e i) i)) := by170 simp only [IntegrableOn, ← Measure.restrict_congr_set (Box.Ioo_ae_eq_Icc _)] at Hi ⊢171 rw [← Box.iUnion_Ioo_of_tendsto J.monotone hJl hJu] at Hi ⊢172 exact tendsto_setIntegral_of_monotone (fun k => (J k).measurableSet_Ioo)173 (Box.Ioo.comp J).monotone Hi174 -- Thus it suffices to prove the same about the RHS.175 refine tendsto_nhds_unique_of_eventuallyEq hI_tendsto ?_ (Eventually.of_forall HJ_eq)176 clear hI_tendsto177 rw [tendsto_pi_nhds] at hJl hJu178 /- We'll need to prove a similar statement about the integrals over the front sides and the179 integrals over the back sides. In order to avoid repeating ourselves, we formulate a lemma. -/180 suffices ∀ (i : Fin (n + 1)) (c : ℕ → ℝ) (d), (∀ k, c k ∈ Icc (I.lower i) (I.upper i)) →181 Tendsto c atTop (𝓝 d) →182 Tendsto (fun k => ∫ x in Box.Icc ((J k).face i), f (i.insertNth (c k) x) i) atTop183 (𝓝 <| ∫ x in Box.Icc (I.face i), f (i.insertNth d x) i) by184 rw [Box.Icc_eq_pi] at hJ_sub'185 refine tendsto_finsetSum _ fun i _ => (this _ _ _ ?_ (hJu _)).sub (this _ _ _ ?_ (hJl _))186 exacts [fun k => hJ_sub' k (J k).upper_mem_Icc _ trivial, fun k =>187 hJ_sub' k (J k).lower_mem_Icc _ trivial]188 intro i c d hc hcd189 /- First we prove that the integrals of the restriction of `f` to `{x | x i = d}` over increasing190 boxes `((J k).face i).Icc` tend to the desired limit. The proof mostly repeats the one above. -/191 have hd : d ∈ Icc (I.lower i) (I.upper i) :=192 isClosed_Icc.mem_of_tendsto hcd (Eventually.of_forall hc)193 have Hic : ∀ k, IntegrableOn (fun x => f (i.insertNth (c k) x) i) (Box.Icc (I.face i)) := fun k =>194 (Box.continuousOn_face_Icc ((continuous_apply i).comp_continuousOn Hc) (hc k)).integrableOn_Icc195 have Hid : IntegrableOn (fun x => f (i.insertNth d x) i) (Box.Icc (I.face i)) :=196 (Box.continuousOn_face_Icc ((continuous_apply i).comp_continuousOn Hc) hd).integrableOn_Icc197 have H :198 Tendsto (fun k => ∫ x in Box.Icc ((J k).face i), f (i.insertNth d x) i) atTop199 (𝓝 <| ∫ x in Box.Icc (I.face i), f (i.insertNth d x) i) := by200 have hIoo : (⋃ k, Box.Ioo ((J k).face i)) = Box.Ioo (I.face i) :=201 Box.iUnion_Ioo_of_tendsto ((Box.monotone_face i).comp J.monotone)202 (tendsto_pi_nhds.2 fun _ => hJl _) (tendsto_pi_nhds.2 fun _ => hJu _)203 simp only [IntegrableOn, ← Measure.restrict_congr_set (Box.Ioo_ae_eq_Icc _), ← hIoo] at Hid ⊢204 exact tendsto_setIntegral_of_monotone (fun k => ((J k).face i).measurableSet_Ioo)205 (Box.Ioo.monotone.comp ((Box.monotone_face i).comp J.monotone)) Hid206 /- Thus it suffices to show that the distance between the integrals of the restrictions of `f` to207 `{x | x i = c k}` and `{x | x i = d}` over `((J k).face i).Icc` tends to zero as `k → ∞`. Choose208 `ε > 0`. -/209 refine H.congr_dist (Metric.nhds_basis_closedBall.tendsto_right_iff.2 fun ε εpos => ?_)210 have hvol_pos : ∀ J : Box (Fin n), 0 < ∏ j, (J.upper j - J.lower j) := fun J =>211 prod_pos fun j hj => sub_pos.2 <| J.lower_lt_upper _212 /- Choose `δ > 0` such that for any `x y ∈ I.Icc` at distance at most `δ`, the distance between213 `f x` and `f y` is at most `ε / volume (I.face i).Icc`, then the distance between the integrals214 is at most `(ε / volume (I.face i).Icc) * volume ((J k).face i).Icc ≤ ε`. -/215 rcases Metric.uniformContinuousOn_iff_le.1 (I.isCompact_Icc.uniformContinuousOn_of_continuous Hc)216 (ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)) (div_pos εpos (hvol_pos (I.face i)))217 with ⟨δ, δpos, hδ⟩218 refine (hcd.eventually (Metric.ball_mem_nhds _ δpos)).mono fun k hk => ?_219 have Hsub : Box.Icc ((J k).face i) ⊆ Box.Icc (I.face i) :=220 Box.le_iff_Icc.1 (Box.face_mono (hJ_le _) i)221 rw [mem_closedBall_zero_iff, Real.norm_eq_abs, abs_of_nonneg dist_nonneg, dist_eq_norm,222 ← integral_sub (Hid.mono_set Hsub) ((Hic _).mono_set Hsub)]223 calc224 ‖∫ x in Box.Icc ((J k).face i), f (i.insertNth d x) i - f (i.insertNth (c k) x) i‖ ≤225 (ε / ∏ j, ((I.face i).upper j - (I.face i).lower j)) *226 (volume (Box.Icc ((J k).face i))).toReal := by227 refine norm_setIntegral_le_of_norm_le_const (((J k).face i).measure_Icc_lt_top _)228 fun x hx => ?_229 rw [← dist_eq_norm]230 calc231 dist (f (i.insertNth d x) i) (f (i.insertNth (c k) x) i) ≤232 dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) :=233 dist_le_pi_dist (f (i.insertNth d x)) (f (i.insertNth (c k) x)) i234 _ ≤ ε / ∏ j, ((I.face i).upper j - (I.face i).lower j) :=235 hδ _ (I.mapsTo_insertNth_face_Icc hd <| Hsub hx) _236 (I.mapsTo_insertNth_face_Icc (hc _) <| Hsub hx) ?_237 rw [Fin.dist_insertNth_insertNth, dist_self, dist_comm]238 exact max_le hk.le δpos.lt.le239 _ ≤ ε := by240 rw [Box.Icc_def, Real.volume_Icc_pi_toReal ((J k).face i).lower_le_upper,241 ← le_div_iff₀ (hvol_pos _)]242 gcongr243 exacts [hvol_pos _, fun _ _ ↦ sub_nonneg.2 (Box.lower_le_upper _ _),244 (hJ_sub' _ (J _).upper_mem_Icc).2 _, (hJ_sub' _ (J _).lower_mem_Icc).1 _]245246variable (a b : Fin (n + 1) → ℝ)247248local notation "face " i => Set.Icc (a ∘ Fin.succAbove i) (b ∘ Fin.succAbove i)249local notation:max "frontFace " i:arg => Fin.insertNth i (b i)250local notation:max "backFace " i:arg => Fin.insertNth i (a i)251252/-- **Divergence theorem** for Bochner integral. If `f : ℝⁿ⁺¹ → Eⁿ⁺¹` is continuous on a rectangular253box `[a, b] : Set ℝⁿ⁺¹`, `a ≤ b`, is differentiable on its interior with derivative254`f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹` and the divergence `fun x ↦ ∑ i, f' x eᵢ i` is integrable on `[a, b]`,255where `eᵢ = Pi.single i 1` is the `i`-th basis vector, then its integral is equal to the sum of256integrals of `f` over the faces of `[a, b]`, taken with appropriate signs.257258Moreover, the same is true if the function is not differentiable at countably many259points of the interior of `[a, b]`.260261We represent both faces `x i = a i` and `x i = b i` as the box262`face i = [a ∘ Fin.succAbove i, b ∘ Fin.succAbove i]` in `ℝⁿ`, where263`Fin.succAbove : Fin n ↪o Fin (n + 1)` is the order embedding with range `{i}ᶜ`. The restrictions264of `f : ℝⁿ⁺¹ → Eⁿ⁺¹` to these faces are given by `f ∘ backFace i` and `f ∘ frontFace i`, where265`backFace i = Fin.insertNth i (a i)` and `frontFace i = Fin.insertNth i (b i)` are embeddings266`ℝⁿ → ℝⁿ⁺¹` that take `y : ℝⁿ` and insert `a i` (resp., `b i`) as `i`-th coordinate. -/267theorem integral_divergence_of_hasFDerivAt_off_countable (hle : a ≤ b)268 (f : ℝⁿ⁺¹ → Eⁿ⁺¹) (f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹)269 (s : Set ℝⁿ⁺¹) (hs : s.Countable) (Hc : ContinuousOn f (Icc a b))270 (Hd : ∀ x ∈ (Set.pi univ fun i => Ioo (a i) (b i)) \ s, HasFDerivAt f (f' x) x)271 (Hi : IntegrableOn (fun x => ∑ i, f' x (e i) i) (Icc a b)) :272 (∫ x in Icc a b, ∑ i, f' x (e i) i) =273 ∑ i : Fin (n + 1),274 ((∫ x in face i, f (frontFace i x) i) - ∫ x in face i, f (backFace i x) i) := by275 rcases em (∃ i, a i = b i) with (⟨i, hi⟩ | hne)276 · -- First we sort out the trivial case `∃ i, a i = b i`.277 rw [volume_pi, ← setIntegral_congr_set Measure.univ_pi_Ioc_ae_eq_Icc]278 have hi' : Ioc (a i) (b i) = ∅ := Ioc_eq_empty hi.not_lt279 have : (pi Set.univ fun j => Ioc (a j) (b j)) = ∅ := univ_pi_eq_empty hi'280 rw [this, setIntegral_empty, sum_eq_zero]281 rintro j -282 rcases eq_or_ne i j with (rfl | hne)283 · simp [hi]284 · rcases Fin.exists_succAbove_eq hne with ⟨i, rfl⟩285 have : Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] (∅ : Set ℝⁿ) := by286 rw [ae_eq_empty, Real.volume_Icc_pi, prod_eq_zero (Finset.mem_univ i)]287 simp [hi]288 rw [setIntegral_congr_set this, setIntegral_congr_set this, setIntegral_empty,289 setIntegral_empty, sub_self]290 · -- In the non-trivial case `∀ i, a i < b i`, we apply a lemma we proved above.291 have hlt : ∀ i, a i < b i := fun i => (hle i).lt_of_ne fun hi => hne ⟨i, hi⟩292 exact integral_divergence_of_hasFDerivAt_off_countable_aux₂ ⟨a, b, hlt⟩ f f' s hs Hc Hd Hi293294/-- **Divergence theorem** for a family of functions `f : Fin (n + 1) → ℝⁿ⁺¹ → E`. See also295`MeasureTheory.integral_divergence_of_hasFDerivAt_off_countable'` for a version formulated296in terms of a vector-valued function `f : ℝⁿ⁺¹ → Eⁿ⁺¹`. -/297theorem integral_divergence_of_hasFDerivAt_off_countable' (hle : a ≤ b)298 (f : Fin (n + 1) → ℝⁿ⁺¹ → E)299 (f' : Fin (n + 1) → ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] E) (s : Set ℝⁿ⁺¹)300 (hs : s.Countable) (Hc : ∀ i, ContinuousOn (f i) (Icc a b))301 (Hd : ∀ x ∈ (pi Set.univ fun i => Ioo (a i) (b i)) \ s, ∀ (i), HasFDerivAt (f i) (f' i x) x)302 (Hi : IntegrableOn (fun x => ∑ i, f' i x (e i)) (Icc a b)) :303 (∫ x in Icc a b, ∑ i, f' i x (e i)) =304 ∑ i : Fin (n + 1), ((∫ x in face i, f i (frontFace i x)) -305 ∫ x in face i, f i (backFace i x)) :=306 integral_divergence_of_hasFDerivAt_off_countable a b hle (fun x i => f i x)307 (fun x => ContinuousLinearMap.pi fun i => f' i x) s hs (continuousOn_pi.2 Hc)308 (fun x hx => hasFDerivAt_pi.2 (Hd x hx)) Hi309310end311312/-- An auxiliary lemma that is used to specialize the general divergence theorem to spaces that do313not have the form `Fin n → ℝ`. -/314theorem integral_divergence_of_hasFDerivAt_off_countable_of_equiv {F : Type*}315 [NormedAddCommGroup F] [NormedSpace ℝ F] [Preorder F] [MeasureSpace F] [BorelSpace F]316 (eL : F ≃L[ℝ] ℝⁿ⁺¹) (he_ord : ∀ x y, eL x ≤ eL y ↔ x ≤ y)317 (he_vol : MeasurePreserving eL volume volume) (f : Fin (n + 1) → F → E)318 (f' : Fin (n + 1) → F → F →L[ℝ] E) (s : Set F) (hs : s.Countable) (a b : F) (hle : a ≤ b)319 (Hc : ∀ i, ContinuousOn (f i) (Icc a b))320 (Hd : ∀ x ∈ interior (Icc a b) \ s, ∀ (i), HasFDerivAt (f i) (f' i x) x) (DF : F → E)321 (hDF : ∀ x, DF x = ∑ i, f' i x (eL.symm <| e i)) (Hi : IntegrableOn DF (Icc a b)) :322 ∫ x in Icc a b, DF x =323 ∑ i : Fin (n + 1),324 ((∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),325 f i (eL.symm <| i.insertNth (eL b i) x)) -326 ∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),327 f i (eL.symm <| i.insertNth (eL a i) x)) :=328 have he_emb : MeasurableEmbedding eL := eL.toHomeomorph.measurableEmbedding329 have hIcc : eL ⁻¹' Icc (eL a) (eL b) = Icc a b := by330 ext1 x; simp only [Set.mem_preimage, Set.mem_Icc, he_ord]331 have hIcc' : Icc (eL a) (eL b) = eL.symm ⁻¹' Icc a b := by rw [← hIcc, eL.symm_preimage_preimage]332 calc333 ∫ x in Icc a b, DF x = ∫ x in Icc a b, ∑ i, f' i x (eL.symm <| e i) := by simp only [hDF]334 _ = ∫ x in Icc (eL a) (eL b), ∑ i, f' i (eL.symm x) (eL.symm <| e i) := by335 rw [← he_vol.setIntegral_preimage_emb he_emb]336 simp only [hIcc, eL.symm_apply_apply]337 _ = ∑ i : Fin (n + 1),338 ((∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),339 f i (eL.symm <| i.insertNth (eL b i) x)) -340 ∫ x in Icc (eL a ∘ i.succAbove) (eL b ∘ i.succAbove),341 f i (eL.symm <| i.insertNth (eL a i) x)) := by342 refine integral_divergence_of_hasFDerivAt_off_countable' (eL a) (eL b)343 ((he_ord _ _).2 hle) (fun i x => f i (eL.symm x))344 (fun i x => f' i (eL.symm x) ∘L (eL.symm : ℝⁿ⁺¹ →L[ℝ] F)) (eL.symm ⁻¹' s)345 (hs.preimage eL.symm.injective) ?_ ?_ ?_346 · exact fun i => (Hc i).comp eL.symm.continuousOn hIcc'.subset347 · refine fun x hx i => (Hd (eL.symm x) ⟨?_, hx.2⟩ i).comp x eL.symm.hasFDerivAt348 rw [← hIcc]349 refine preimage_interior_subset_interior_preimage eL.continuous ?_350 simpa only [Set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc,351 interior_pi_set (@finite_univ (Fin _) _), interior_Icc] using hx.1352 · rw [← he_vol.integrableOn_comp_preimage he_emb, hIcc]353 simp [← hDF, Function.comp_def, Hi]354355end356357open scoped Interval358359open ContinuousLinearMap (smulRight)360361362local macro:arg t:term:max noWs "¹" : term => `(Fin 1 → $t)363local macro:arg t:term:max noWs "²" : term => `(Fin 2 → $t)364365/-- **Fundamental theorem of calculus, part 2**. This version assumes that `f` is continuous on the366interval and is differentiable off a countable set `s`.367368See also369370* `intervalIntegral.integral_eq_sub_of_hasDeriv_right_of_le` for a version that only assumes right371 differentiability of `f`;372* `MeasureTheory.integral_eq_of_hasDerivWithinAt_off_countable` for a version that works both373 for `a ≤ b` and `b ≤ a` at the expense of using unordered intervals instead of `Set.Icc`. -/374theorem integral_eq_of_hasDerivAt_off_countable_of_le [CompleteSpace E] (f f' : ℝ → E)375 {a b : ℝ} (hle : a ≤ b) {s : Set ℝ} (hs : s.Countable) (Hc : ContinuousOn f (Icc a b))376 (Hd : ∀ x ∈ Ioo a b \ s, HasDerivAt f (f' x) x) (Hi : IntervalIntegrable f' volume a b) :377 ∫ x in a..b, f' x = f b - f a := by378 set e : ℝ ≃L[ℝ] ℝ¹ := (ContinuousLinearEquiv.funUnique (Fin 1) ℝ ℝ).symm379 set F' : ℝ → ℝ →L[ℝ] E := fun x => smulRight (1 : ℝ →L[ℝ] ℝ) (f' x)380 calc381 ∫ x in a..b, f' x = ∫ x in Icc a b, f' x := by382 rw [intervalIntegral.integral_of_le hle, setIntegral_congr_set Ioc_ae_eq_Icc]383 _ = ∑ i : Fin 1,384 ((∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),385 f (e.symm <| i.insertNth (e b i) x)) -386 ∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),387 f (e.symm <| i.insertNth (e a i) x)) := by388 simp only [← interior_Icc] at Hd389 refine390 integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ (fun _ => f)391 (fun _ => F') s hs a b hle (fun _ => Hc) (fun x hx _ => Hd x hx) _ ?_ ?_392 · exact fun x y => (OrderIso.funUnique (Fin 1) ℝ).symm.le_iff_le393 · exact (volume_preserving_funUnique (Fin 1) ℝ).symm _394 · simp [F', e]395 · rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hle] at Hi396 exact Hi.congr_set_ae Ioc_ae_eq_Icc.symm397 _ = f b - f a := by398 simp [e, Subsingleton.elim (const (Fin 0) _) isEmptyElim, volume_pi,399 Measure.pi_of_empty fun _ : Fin 0 ↦ _]400401/-- **Fundamental theorem of calculus, part 2**. This version assumes that `f` is continuous on the402interval and is differentiable off a countable set `s`.403404See also `intervalIntegral.integral_eq_sub_of_hasDeriv_right` for a version that405only assumes right differentiability of `f`.406-/407theorem integral_eq_of_hasDerivAt_off_countable [CompleteSpace E] (f f' : ℝ → E) {a b : ℝ}408 {s : Set ℝ} (hs : s.Countable) (Hc : ContinuousOn f [[a, b]])409 (Hd : ∀ x ∈ Ioo (min a b) (max a b) \ s, HasDerivAt f (f' x) x)410 (Hi : IntervalIntegrable f' volume a b) : ∫ x in a..b, f' x = f b - f a := by411 rcases le_total a b with hab | hab412 · simp only [uIcc_of_le hab, min_eq_left hab, max_eq_right hab] at *413 exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi414 · simp only [uIcc_of_ge hab, min_eq_right hab, max_eq_left hab] at *415 rw [intervalIntegral.integral_symm, neg_eq_iff_eq_neg, neg_sub]416 exact integral_eq_of_hasDerivAt_off_countable_of_le f f' hab hs Hc Hd Hi.symm417418/-- **Divergence theorem** for functions on the plane along rectangles. It is formulated in terms of419two functions `f g : ℝ × ℝ → E` and an integral over `Icc a b = [a.1, b.1] × [a.2, b.2]`, where420`a b : ℝ × ℝ`, `a ≤ b`. When thinking of `f` and `g` as the two coordinates of a single function421`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the422divergence of `F` inside the rectangle equals the integral of the normal derivative of `F` along the423boundary.424425See also `MeasureTheory.integral2_divergence_prod_of_hasFDerivAt_off_countable` for a426version that does not assume `a ≤ b` and uses iterated interval integral instead of the integral427over `Icc a b`. -/428theorem integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le (f g : ℝ × ℝ → E)429 (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a b : ℝ × ℝ) (hle : a ≤ b) (s : Set (ℝ × ℝ)) (hs : s.Countable)430 (Hcf : ContinuousOn f (Icc a b)) (Hcg : ContinuousOn g (Icc a b))431 (Hdf : ∀ x ∈ Ioo a.1 b.1 ×ˢ Ioo a.2 b.2 \ s, HasFDerivAt f (f' x) x)432 (Hdg : ∀ x ∈ Ioo a.1 b.1 ×ˢ Ioo a.2 b.2 \ s, HasFDerivAt g (g' x) x)433 (Hi : IntegrableOn (fun x => f' x (1, 0) + g' x (0, 1)) (Icc a b)) :434 (∫ x in Icc a b, f' x (1, 0) + g' x (0, 1)) =435 (((∫ x in a.1..b.1, g (x, b.2)) - ∫ x in a.1..b.1, g (x, a.2)) +436 ∫ y in a.2..b.2, f (b.1, y)) -437 ∫ y in a.2..b.2, f (a.1, y) :=438 let e : (ℝ × ℝ) ≃L[ℝ] ℝ² := (ContinuousLinearEquiv.finTwoArrow ℝ ℝ).symm439 calc440 (∫ x in Icc a b, f' x (1, 0) + g' x (0, 1)) =441 ∑ i : Fin 2,442 ((∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),443 ![f, g] i (e.symm <| i.insertNth (e b i) x)) -444 ∫ x in Icc (e a ∘ i.succAbove) (e b ∘ i.succAbove),445 ![f, g] i (e.symm <| i.insertNth (e a i) x)) := by446 refine integral_divergence_of_hasFDerivAt_off_countable_of_equiv e ?_ ?_ ![f, g]447 ![f', g'] s hs a b hle ?_ (fun x hx => ?_) _ ?_ Hi448 · exact fun x y => (OrderIso.finTwoArrowIso ℝ).symm.le_iff_le449 · exact (volume_preserving_finTwoArrow ℝ).symm _450 · exact Fin.forall_fin_two.2 ⟨Hcf, Hcg⟩451 · rw [Icc_prod_eq, interior_prod_eq, interior_Icc, interior_Icc] at hx452 exact Fin.forall_fin_two.2 ⟨Hdf x hx, Hdg x hx⟩453 · intro x; rw [Fin.sum_univ_two]; rfl454 _ = ((∫ y in Icc a.2 b.2, f (b.1, y)) - ∫ y in Icc a.2 b.2, f (a.1, y)) +455 ((∫ x in Icc a.1 b.1, g (x, b.2)) - ∫ x in Icc a.1 b.1, g (x, a.2)) := by456 have : ∀ (a b : ℝ¹) (f : ℝ¹ → E),457 ∫ x in Icc a b, f x = ∫ x in Icc (a 0) (b 0), f fun _ => x := fun a b f ↦ by458 convert!459 (((volume_preserving_funUnique (Fin 1) ℝ).symm _).setIntegral_preimage_emb460 (MeasurableEquiv.measurableEmbedding _) f _).symm461 exact ((OrderIso.funUnique (Fin 1) ℝ).symm.preimage_Icc a b).symm462 simp only [Fin.sum_univ_two, this]463 rfl464 _ = (((∫ x in a.1..b.1, g (x, b.2)) - ∫ x in a.1..b.1, g (x, a.2)) +465 ∫ y in a.2..b.2, f (b.1, y)) - ∫ y in a.2..b.2, f (a.1, y) := by466 simp only [intervalIntegral.integral_of_le hle.1, intervalIntegral.integral_of_le hle.2,467 setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]468 abel469470/-- **Divergence theorem** for functions on the plane along rectangles. It is formulated in terms of471two functions `f g : ℝ × ℝ → E` and an integral over `Icc a b = [a.1, b.1] × [a.2, b.2]`, where472`a b : ℝ × ℝ`, `a ≤ b`. When thinking of `f` and `g` as the two coordinates of a single function473`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the474divergence of `F` inside the rectangle equals the integral of the normal derivative of `F` along the475boundary.476477See also `MeasureTheory.integral2_divergence_prod_of_hasFDerivAt` for a478version that does not assume `a ≤ b` and uses iterated interval integral instead of the integral479over `Icc a b`.480481See also `integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le`482for a version that assumes differentiability out of a countable set. -/483theorem integral_divergence_prod_Icc_of_hasFDerivAt_of_le (f g : ℝ × ℝ → E)484 (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a b : ℝ × ℝ) (hle : a ≤ b)485 (Hcf : ContinuousOn f (Icc a b)) (Hcg : ContinuousOn g (Icc a b))486 (Hdf : ∀ x ∈ Ioo a.1 b.1 ×ˢ Ioo a.2 b.2, HasFDerivAt f (f' x) x)487 (Hdg : ∀ x ∈ Ioo a.1 b.1 ×ˢ Ioo a.2 b.2, HasFDerivAt g (g' x) x)488 (Hi : IntegrableOn (fun x => f' x (1, 0) + g' x (0, 1)) (Icc a b)) :489 (∫ x in Icc a b, f' x (1, 0) + g' x (0, 1)) =490 (((∫ x in a.1..b.1, g (x, b.2)) - ∫ x in a.1..b.1, g (x, a.2)) +491 ∫ y in a.2..b.2, f (b.1, y)) - ∫ y in a.2..b.2, f (a.1, y) :=492 integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le f g f' g' a b hle ∅493 (by simp) Hcf Hcg (by simpa only [sdiff_empty]) (by simpa only [sdiff_empty]) Hi494495/-- **Divergence theorem** for functions on the plane. It is formulated in terms of two functions496`f g : ℝ × ℝ → E` and iterated integral `∫ x in a₁..b₁, ∫ y in a₂..b₂, _`, where497`a₁ a₂ b₁ b₂ : ℝ`. When thinking of `f` and `g` as the two coordinates of a single function498`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the499divergence of `F` inside the rectangle with vertices `(aᵢ, bⱼ)`, `i, j =1,2`, equals the integral of500the normal derivative of `F` along the boundary.501502See also `MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le`503for a version that uses an integral over `Icc a b`, where `a b : ℝ × ℝ`, `a ≤ b`. -/504theorem integral2_divergence_prod_of_hasFDerivAt_off_countable (f g : ℝ × ℝ → E)505 (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ) (s : Set (ℝ × ℝ)) (hs : s.Countable)506 (Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))507 (Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))508 (Hdf : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂) \ s,509 HasFDerivAt f (f' x) x)510 (Hdg : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂) \ s,511 HasFDerivAt g (g' x) x)512 (Hi : IntegrableOn (fun x => f' x (1, 0) + g' x (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]])) :513 (∫ x in a₁..b₁, ∫ y in a₂..b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1)) =514 (((∫ x in a₁..b₁, g (x, b₂)) - ∫ x in a₁..b₁, g (x, a₂)) + ∫ y in a₂..b₂, f (b₁, y)) -515 ∫ y in a₂..b₂, f (a₁, y) := by516 wlog h₁ : a₁ ≤ b₁ generalizing a₁ b₁517 · specialize this b₁ a₁518 rw [uIcc_comm b₁ a₁, min_comm b₁ a₁, max_comm b₁ a₁] at this519 simp only [intervalIntegral.integral_symm b₁ a₁]520 refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₁))).trans ?_; abel521 wlog h₂ : a₂ ≤ b₂ generalizing a₂ b₂522 · specialize this b₂ a₂523 rw [uIcc_comm b₂ a₂, min_comm b₂ a₂, max_comm b₂ a₂] at this524 simp only [intervalIntegral.integral_symm b₂ a₂, intervalIntegral.integral_neg]525 refine (congr_arg Neg.neg (this Hcf Hcg Hdf Hdg Hi (le_of_not_ge h₂))).trans ?_; abel526 simp only [uIcc_of_le h₁, uIcc_of_le h₂, min_eq_left, max_eq_right, h₁, h₂] at Hcf Hcg Hdf Hdg Hi527 calc528 (∫ x in a₁..b₁, ∫ y in a₂..b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1)) =529 ∫ x in Icc a₁ b₁, ∫ y in Icc a₂ b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1) := by530 simp only [intervalIntegral.integral_of_le, h₁, h₂,531 setIntegral_congr_set (Ioc_ae_eq_Icc (α := ℝ) (μ := volume))]532 _ = ∫ x in Icc a₁ b₁ ×ˢ Icc a₂ b₂, f' x (1, 0) + g' x (0, 1) := (setIntegral_prod _ Hi).symm533 _ = (((∫ x in a₁..b₁, g (x, b₂)) - ∫ x in a₁..b₁, g (x, a₂)) + ∫ y in a₂..b₂, f (b₁, y)) -534 ∫ y in a₂..b₂, f (a₁, y) := by535 rw [Icc_prod_Icc] at *536 apply integral_divergence_prod_Icc_of_hasFDerivAt_off_countable_of_le f g f' g'537 (a₁, a₂) (b₁, b₂) ⟨h₁, h₂⟩ s <;> assumption538539/-- **Divergence theorem** for functions on the plane. It is formulated in terms of two functions540`f g : ℝ × ℝ → E` and iterated integral `∫ x in a₁..b₁, ∫ y in a₂..b₂, _`, where541`a₁ a₂ b₁ b₂ : ℝ`. When thinking of `f` and `g` as the two coordinates of a single function542`F : ℝ × ℝ → E × E` and when `E = ℝ`, this is the usual statement that the integral of the543divergence of `F` inside the rectangle with vertices `(aᵢ, bⱼ)`, `i, j = 1, 2`,544equals the integral of the normal derivative of `F` along the boundary.545546See also `MeasureTheory.integral_divergence_prod_Icc_of_hasFDerivAt_of_le`547for a version that uses an integral over `Icc a b`, where `a b : ℝ × ℝ`, `a ≤ b`.548549See also `integral2_divergence_prod_of_hasFDerivAt_off_countable`550for a version that assumes differentiability outside of a countable set. -/551theorem integral2_divergence_prod_of_hasFDerivAt (f g : ℝ × ℝ → E)552 (f' g' : ℝ × ℝ → ℝ × ℝ →L[ℝ] E) (a₁ a₂ b₁ b₂ : ℝ)553 (Hcf : ContinuousOn f ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))554 (Hcg : ContinuousOn g ([[a₁, b₁]] ×ˢ [[a₂, b₂]]))555 (Hdf : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂),556 HasFDerivAt f (f' x) x)557 (Hdg : ∀ x ∈ Ioo (min a₁ b₁) (max a₁ b₁) ×ˢ Ioo (min a₂ b₂) (max a₂ b₂),558 HasFDerivAt g (g' x) x)559 (Hi : IntegrableOn (fun x => f' x (1, 0) + g' x (0, 1)) ([[a₁, b₁]] ×ˢ [[a₂, b₂]])) :560 (∫ x in a₁..b₁, ∫ y in a₂..b₂, f' (x, y) (1, 0) + g' (x, y) (0, 1)) =561 (((∫ x in a₁..b₁, g (x, b₂)) - ∫ x in a₁..b₁, g (x, a₂)) + ∫ y in a₂..b₂, f (b₁, y)) -562 ∫ y in a₂..b₂, f (a₁, y) :=563 integral2_divergence_prod_of_hasFDerivAt_off_countable f g f' g' a₁ a₂ b₁ b₂ ∅ countable_empty564 Hcf Hcg (fun x hx ↦ Hdf x hx.1) (fun x hx ↦ Hdg x hx.1) Hi565566end MeasureTheory