Skip to content

Commit

Permalink
fix: restore notations in MeasureTheory.Integral.DivergenceTheorem (#…
Browse files Browse the repository at this point in the history 
…4841)
  • Loading branch information
@digama0
digama0 committed Jun 8, 2023
1 parent 840194b commit 7c2a6d5
Showing 1 changed file with 23 additions and 31 deletions.
54 changes: 23 additions & 31 deletions Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean
View file
Expand Up @@ -71,15 +71,10 @@ section

variable {n : ℕ}

-- local notation "ℝⁿ" => Fin n → ℝ
local macro:arg t:term:max noWs "ⁿ" : term => `(Fin n → $t)

-- set_option quotPrecheck false in
-- local notation:200 "ℝⁿ⁺¹" => Fin (n + 1) → ℝ
local macro:arg t:term:max noWs "ⁿ⁺¹" : term => `(Fin (n + 1) → $t)

-- set_option quotPrecheck false in
-- local notation:200 "Eⁿ⁺¹" => Fin (n + 1) → E

-- -- mathport name: «expre »
local notation "e " i => Pi.single i 1

section
Expand Down Expand Up @@ -115,8 +110,8 @@ in several aspects.
`BoxIntegral.hasIntegral_GP_divergence_of_forall_hasDerivWithinAt` reformulated for the
Bochner integral. -/
theorem integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ (I : 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) → ℝ))
(f : ℝⁿ⁺¹ → Eⁿ⁺¹)
(f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹) (s : Set ℝⁿ⁺¹)
(hs : s.Countable) (Hc : ContinuousOn f (Box.Icc I))
(Hd : ∀ x ∈ (Box.Icc I) \ s, HasFDerivWithinAt f (f' x) (Box.Icc I) x)
(Hi : IntegrableOn (fun x => ∑ i, f' x (e i) i) (Box.Icc I)) :
Expand Down Expand Up @@ -147,9 +142,9 @@ theorem integral_divergence_of_hasFDerivWithinAt_off_countable_aux₁ (I : Box (
`MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable`. Compared to the previous
lemma, here we drop the assumption of differentiability on the boundary of the box. -/
theorem integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ (I : 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) → ℝ)) (hs : s.Countable) (Hc : ContinuousOn f (Box.Icc I))
(f : ℝⁿ⁺¹ → Eⁿ⁺¹)
(f' : ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] Eⁿ⁺¹)
(s : Set ℝⁿ⁺¹) (hs : s.Countable) (Hc : ContinuousOn f (Box.Icc I))
(Hd : ∀ x ∈ Box.Ioo I \ s, HasFDerivAt f (f' x) x)
(Hi : IntegrableOn (∑ i, f' · (e i) i) (Box.Icc I)) :
(∫ x in Box.Icc I, ∑ i, f' x (e i) i) =
Expand Down Expand Up @@ -255,8 +250,8 @@ theorem integral_divergence_of_hasFDerivWithinAt_off_countable_aux₂ (I : Box (
variable (a b : Fin (n + 1) → ℝ)

local notation "face " i => Set.Icc (a ∘ Fin.succAbove i) (b ∘ Fin.succAbove i)
-- local notation "frontFace " i:2000 => Fin.insertNth i (b i)
-- local notation "backFace " i:2000 => Fin.insertNth i (a i)
local notation:max "frontFace " i:arg => Fin.insertNth i (b i)
local notation:max "backFace " i:arg => Fin.insertNth i (a 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
Expand All @@ -274,14 +269,14 @@ of `f : ℝⁿ⁺¹ → Eⁿ⁺¹` to these faces are given by `f ∘ backFace i
`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_hasFDerivWithinAt_off_countable (hle : 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) → ℝ)) (hs : s.Countable) (Hc : ContinuousOn f (Icc 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 (i.insertNth (b i) x) i) -
∫ x in face i, f (i.insertNth (a i) x) i) := by
∑ 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, ← set_integral_congr_set_ae Measure.univ_pi_Ioc_ae_eq_Icc]
Expand All @@ -292,7 +287,7 @@ theorem integral_divergence_of_hasFDerivWithinAt_off_countable (hle : a ≤ b)
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 (Fin n → ℝ))
have : Icc (a ∘ j.succAbove) (b ∘ j.succAbove) =ᵐ[volume] (∅ : Set ℝⁿ)
· rw [ae_eq_empty, Real.volume_Icc_pi, prod_eq_zero (Finset.mem_univ i)]
simp [hi]
rw [set_integral_congr_set_ae this, set_integral_congr_set_ae this, integral_empty,
Expand All @@ -307,14 +302,14 @@ theorem integral_divergence_of_hasFDerivWithinAt_off_countable (hle : a ≤ b)
`MeasureTheory.integral_divergence_of_hasFDerivWithinAt_off_countable'` for a version formulated
in terms of a vector-valued function `f : ℝⁿ⁺¹ → Eⁿ⁺¹`. -/
theorem integral_divergence_of_hasFDerivWithinAt_off_countable' (hle : a ≤ b)
(f : Fin (n + 1) → (Fin (n + 1) → ℝ) → E)
(f' : Fin (n + 1) → (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E) (s : Set (Fin (n + 1) → ℝ))
(f : Fin (n + 1) → ℝⁿ⁺¹ → E)
(f' : Fin (n + 1) → ℝⁿ⁺¹ → ℝⁿ⁺¹ →L[ℝ] E) (s : Set ℝⁿ⁺¹)
(hs : s.Countable) (Hc : ∀ i, ContinuousOn (f i) (Icc a b))
(Hd : ∀ x ∈ (pi Set.univ fun i => Ioo (a i) (b i)) \ s, ∀ (i), HasFDerivAt (f i) (f' i x) x)
(Hi : IntegrableOn (fun x => ∑ i, f' i x (e i)) (Icc a b)) :
(∫ x in Icc a b, ∑ i, f' i x (e i)) =
∑ i : Fin (n + 1), ((∫ x in face i, f i (i.insertNth (b i) x)) -
∫ x in face i, f i (i.insertNth (a i) x)) :=
∑ i : Fin (n + 1), ((∫ x in face i, f i (frontFace i x)) -
∫ x in face i, f i (backFace i x)) :=
integral_divergence_of_hasFDerivWithinAt_off_countable a b hle (fun x i => f i x)
(fun x => ContinuousLinearMap.pi fun i => f' i x) s hs (continuousOn_pi.2 Hc)
(fun x hx => hasFDerivAt_pi.2 (Hd x hx)) Hi
Expand All @@ -326,7 +321,7 @@ end
not have the form `Fin n → ℝ`. -/
theorem integral_divergence_of_hasFDerivWithinAt_off_countable_of_equiv {F : Type _}
[NormedAddCommGroup F] [NormedSpace ℝ F] [PartialOrder F] [MeasureSpace F] [BorelSpace F]
(eL : F ≃L[ℝ] (Fin (n + 1) → ℝ)) (he_ord : ∀ x y, eL x ≤ eL y ↔ x ≤ y)
(eL : F ≃L[ℝ] ℝⁿ⁺¹) (he_ord : ∀ x y, eL x ≤ eL y ↔ x ≤ y)
(he_vol : MeasurePreserving eL volume volume) (f : Fin (n + 1) → F → E)
(f' : Fin (n + 1) → F → F →L[ℝ] E) (s : Set F) (hs : s.Countable) (a b : F) (hle : a ≤ b)
(Hc : ∀ i, ContinuousOn (f i) (Icc a b))
Expand Down Expand Up @@ -354,7 +349,7 @@ theorem integral_divergence_of_hasFDerivWithinAt_off_countable_of_equiv {F : Typ
f i (eL.symm <| i.insertNth (eL a i) x)) := by
refine integral_divergence_of_hasFDerivWithinAt_off_countable' (eL a) (eL b)
((he_ord _ _).2 hle) (fun i x => f i (eL.symm x))
(fun i x => f' i (eL.symm x) ∘L (eL.symm : (Fin (n + 1) → ℝ) →L[ℝ] F)) (eL.symm ⁻¹' s)
(fun i x => f' i (eL.symm x) ∘L (eL.symm : ℝⁿ⁺¹ →L[ℝ] F)) (eL.symm ⁻¹' s)
(hs.preimage eL.symm.injective) ?_ ?_ ?_
· exact fun i => (Hc i).comp eL.symm.continuousOn hIcc'.subset
· refine' fun x hx i => (Hd (eL.symm x) ⟨_, hx.2⟩ i).comp x eL.symm.hasFDerivAt
Expand All @@ -373,10 +368,8 @@ open scoped Interval
open ContinuousLinearMap (smulRight)


local notation "ℝ¹" => Fin 1 → ℝ
local notation "ℝ²" => Fin 2 → ℝ
local notation "E¹" => Fin 1 → E
local notation "E²" => Fin 2 → E
local macro:arg t:term:max noWs "¹" : term => `(Fin 1 → $t)
local macro:arg t:term:max noWs "²" : term => `(Fin 2 → $t)

/-- **Fundamental theorem of calculus, part 2**. This version assumes that `f` is continuous on the
interval and is differentiable off a countable set `s`.
Expand Down Expand Up @@ -535,4 +528,3 @@ theorem integral2_divergence_prod_of_hasFDerivWithinAt_off_countable (f g : ℝ
#align measure_theory.integral2_divergence_prod_of_has_fderiv_within_at_off_countable MeasureTheory.integral2_divergence_prod_of_hasFDerivWithinAt_off_countable

end MeasureTheory

0 comments on commit 7c2a6d5

Please sign in to comment.