From 33cbed4e8217343d126991aea95915e437be3977 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Thu, 16 Apr 2026 16:19:59 +0800 Subject: [PATCH 1/5] refactor: golf SimpleFunc, LpSeminorm/Basic, Polish/Basic --- .../Constructions/Polish/Basic.lean | 12 ++---- .../Function/LpSeminorm/Basic.lean | 26 ++++--------- .../MeasureTheory/Function/SimpleFunc.lean | 38 +------------------ 3 files changed, 13 insertions(+), 63 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean index d013f8556c1ebb..839012f57c07d2 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean @@ -838,14 +838,10 @@ theorem MeasurableSet.image_of_measurable_injOn {f : γ → α} obtain ⟨t', t't, f_cont, t'_polish⟩ : ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' := f_meas.exists_continuous - have M : MeasurableSet[@borel γ t'] s := - @Continuous.measurable γ γ t' (@borel γ t') - (@BorelSpace.opensMeasurable γ t' (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl)) - tγ _ _ _ (continuous_id_of_le t't) s hs - exact - @MeasurableSet.image_of_continuousOn_injOn γ - _ _ _ _ s f _ t' t'_polish (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl) - M (@Continuous.continuousOn γ _ t' _ f s f_cont) f_inj + have hs' := (borel_anti t't s) <| by rwa [← eq_borel_upgradeStandardBorel γ] + letI : MeasurableSpace γ := @borel γ t' + letI : BorelSpace γ := ⟨rfl⟩ + exact hs'.image_of_continuousOn_injOn f_cont.continuousOn f_inj /-- An injective continuous function on a Polish space is a measurable embedding. -/ theorem Continuous.measurableEmbedding [BorelSpace β] diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index e0a122dd1bc6d0..264378743af347 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -278,12 +278,8 @@ lemma eLpNorm'_mono_enorm_ae {f : α → ε} {g : α → ε'} (hq : 0 ≤ q) (h gcongr lemma eLpNorm'_mono_nnnorm_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : - eLpNorm' f q μ ≤ eLpNorm' g q μ := by - simp only [eLpNorm'_eq_lintegral_enorm] - gcongr ?_ ^ (1 / q) - refine lintegral_mono_ae (h.mono fun x hx => ?_) - dsimp [enorm] - gcongr + eLpNorm' f q μ ≤ eLpNorm' g q μ := + eLpNorm'_mono_enorm_ae hq <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx theorem eLpNorm'_mono_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : eLpNorm' f q μ ≤ eLpNorm' g q μ := @@ -327,12 +323,8 @@ theorem eLpNorm_mono_enorm_ae {f : α → ε} {g : α → ε'} (h : ∀ᵐ x ∂ · exact eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h theorem eLpNorm_mono_nnnorm_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : - eLpNorm f p μ ≤ eLpNorm g p μ := by - simp only [eLpNorm] - split_ifs - · exact le_rfl - · exact essSup_mono_ae (h.mono fun x hx => ENNReal.coe_le_coe.mpr hx) - · exact eLpNorm'_mono_nnnorm_ae ENNReal.toReal_nonneg h + eLpNorm f p μ ≤ eLpNorm g p μ := + eLpNorm_mono_enorm_ae <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx theorem eLpNorm_mono_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : eLpNorm f p μ ≤ eLpNorm g p μ := @@ -401,13 +393,9 @@ theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddM theorem eLpNorm_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) : eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := by - rcases eq_zero_or_neZero μ with rfl | hμ - · simp - by_cases hp : p = 0 - · simp [hp] - have : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖(C : ℝ)‖₊ := hfC.mono fun x hx => hx.trans_eq C.nnnorm_eq.symm - refine (eLpNorm_mono_ae this).trans_eq ?_ - rw [eLpNorm_const _ hp (NeZero.ne μ), C.enorm_eq, one_div, ENNReal.smul_def, smul_eq_mul] + simpa [C.enorm_eq, ENNReal.smul_def, smul_eq_mul] using + (eLpNorm_le_of_ae_enorm_bound (f := f) (C := (C : ℝ≥0∞)) + (hfC.mono fun _ hx => by simpa using hx)) theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C := by diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean index 91bbff2ab208d1..6786252a3f4191 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFunc.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFunc.lean @@ -1328,24 +1328,7 @@ theorem _root_.Measurable.add_simpleFunc {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E] {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : Measurable (g + (f : α → E)) := by - classical - induction f using SimpleFunc.induction with - | @const c s hs => - simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, - SimpleFunc.coe_zero] - rw [← s.piecewise_same g, ← piecewise_add] - exact Measurable.piecewise hs (hg.add_const _) (hg.add_const _) - | @add f f' hff' hf hf' => - have : (g + ↑(f + f')) = (Function.support f).piecewise (g + (f : α → E)) (g + f') := by - ext x - by_cases hx : x ∈ Function.support f - · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not, - Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_right_inj, add_eq_left] - using Set.disjoint_left.1 hff' hx - · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not, - Set.piecewise_eq_of_notMem _ _ _ hx, _root_.add_right_inj, add_eq_right] using hx - rw [this] - exact Measurable.piecewise f.measurableSet_support hf hf' + simpa using f.measurable_bind (fun b a => g a + b) fun b => hg.add_const b /-- In a topological vector space, the addition of a simple function and a measurable function is measurable. -/ @@ -1353,24 +1336,7 @@ theorem _root_.Measurable.simpleFunc_add {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E] {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : Measurable ((f : α → E) + g) := by - classical - induction f using SimpleFunc.induction with - | @const c s hs => - simp only [SimpleFunc.const_zero, SimpleFunc.coe_piecewise, SimpleFunc.coe_const, - SimpleFunc.coe_zero] - rw [← s.piecewise_same g, ← piecewise_add] - exact Measurable.piecewise hs (hg.const_add _) (hg.const_add _) - | @add f f' hff' hf hf' => - have : (↑(f + f') + g) = (Function.support f).piecewise ((f : α → E) + g) (f' + g) := by - ext x - by_cases hx : x ∈ Function.support f - · simpa only [coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not, - Set.piecewise_eq_of_mem _ _ _ hx, _root_.add_left_inj, add_eq_left] - using Set.disjoint_left.1 hff' hx - · simpa only [SimpleFunc.coe_add, Pi.add_apply, Function.mem_support, ne_eq, not_not, - Set.piecewise_eq_of_notMem _ _ _ hx, _root_.add_left_inj, add_eq_right] using hx - rw [this] - exact Measurable.piecewise f.measurableSet_support hf hf' + simpa using f.measurable_bind (fun b a => b + g a) fun b => hg.const_add b end SimpleFunc From 79fe631e349691a8411b44bc853f52c7e2eb5ef9 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Thu, 16 Apr 2026 20:40:09 +0800 Subject: [PATCH 2/5] Apply suggestions from code review Co-authored-by: Michael Rothgang Co-authored-by: Etienne Marion <66847262+EtienneC30@users.noreply.github.com> --- Mathlib/MeasureTheory/Constructions/Polish/Basic.lean | 2 +- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean | 8 ++++---- Mathlib/MeasureTheory/Function/SimpleFunc.lean | 2 +- 3 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean index 839012f57c07d2..084a984abd2ae6 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean @@ -840,7 +840,7 @@ theorem MeasurableSet.image_of_measurable_injOn {f : γ → α} f_meas.exists_continuous have hs' := (borel_anti t't s) <| by rwa [← eq_borel_upgradeStandardBorel γ] letI : MeasurableSpace γ := @borel γ t' - letI : BorelSpace γ := ⟨rfl⟩ + haveI : BorelSpace γ := ⟨rfl⟩ exact hs'.image_of_continuousOn_injOn f_cont.continuousOn f_inj /-- An injective continuous function on a Polish space is a measurable embedding. -/ diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index 264378743af347..5d70d0679bdc0c 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -279,7 +279,7 @@ lemma eLpNorm'_mono_enorm_ae {f : α → ε} {g : α → ε'} (hq : 0 ≤ q) (h lemma eLpNorm'_mono_nnnorm_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : eLpNorm' f q μ ≤ eLpNorm' g q μ := - eLpNorm'_mono_enorm_ae hq <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx + eLpNorm'_mono_enorm_ae hq <| h.mono fun _ hx ↦ ENNReal.coe_le_coe.mpr hx theorem eLpNorm'_mono_ae {f : α → F} {g : α → G} (hq : 0 ≤ q) (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : eLpNorm' f q μ ≤ eLpNorm' g q μ := @@ -324,7 +324,7 @@ theorem eLpNorm_mono_enorm_ae {f : α → ε} {g : α → ε'} (h : ∀ᵐ x ∂ theorem eLpNorm_mono_nnnorm_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) : eLpNorm f p μ ≤ eLpNorm g p μ := - eLpNorm_mono_enorm_ae <| h.mono fun _ hx => ENNReal.coe_le_coe.mpr hx + eLpNorm_mono_enorm_ae <| h.mono fun _ hx ↦ ENNReal.coe_le_coe.mpr hx theorem eLpNorm_mono_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : eLpNorm f p μ ≤ eLpNorm g p μ := @@ -394,8 +394,8 @@ theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddM theorem eLpNorm_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) : eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := by simpa [C.enorm_eq, ENNReal.smul_def, smul_eq_mul] using - (eLpNorm_le_of_ae_enorm_bound (f := f) (C := (C : ℝ≥0∞)) - (hfC.mono fun _ hx => by simpa using hx)) + (eLpNorm_le_of_ae_enorm_bound (f := f) (C := C.toENNReal) + (hfC.mono fun _ hx ↦ by simpa using hx)) theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C := by diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean index 6786252a3f4191..492ca41f721f7e 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFunc.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFunc.lean @@ -1328,7 +1328,7 @@ theorem _root_.Measurable.add_simpleFunc {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E] {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : Measurable (g + (f : α → E)) := by - simpa using f.measurable_bind (fun b a => g a + b) fun b => hg.add_const b + simpa using f.measurable_bind (fun b a ↦ g a + b) fun b ↦ hg.add_const b /-- In a topological vector space, the addition of a simple function and a measurable function is measurable. -/ From 38d9fdcd3cf0c10ca31e33222a78bb1403e39a03 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 18 Apr 2026 16:32:59 +0800 Subject: [PATCH 3/5] apply suggestions --- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean | 4 +--- Mathlib/MeasureTheory/Function/SimpleFunc.lean | 10 ++++------ 2 files changed, 5 insertions(+), 9 deletions(-) diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index 5d70d0679bdc0c..662e2e185593d0 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -393,9 +393,7 @@ theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddM theorem eLpNorm_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) : eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := by - simpa [C.enorm_eq, ENNReal.smul_def, smul_eq_mul] using - (eLpNorm_le_of_ae_enorm_bound (f := f) (C := C.toENNReal) - (hfC.mono fun _ hx ↦ by simpa using hx)) + simpa [C.enorm_eq] using eLpNorm_le_of_ae_enorm_bound (hfC.mono fun _ hx ↦ enorm_le_coe.mpr hx) theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C := by diff --git a/Mathlib/MeasureTheory/Function/SimpleFunc.lean b/Mathlib/MeasureTheory/Function/SimpleFunc.lean index 492ca41f721f7e..d1f82cbcf13532 100644 --- a/Mathlib/MeasureTheory/Function/SimpleFunc.lean +++ b/Mathlib/MeasureTheory/Function/SimpleFunc.lean @@ -1326,17 +1326,15 @@ protected theorem induction' {α γ} [MeasurableSpace α] [Nonempty γ] {P : Sim measurable. -/ theorem _root_.Measurable.add_simpleFunc {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E] - {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : - Measurable (g + (f : α → E)) := by - simpa using f.measurable_bind (fun b a ↦ g a + b) fun b ↦ hg.add_const b + {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : Measurable (g + (f : α → E)) := + f.measurable_bind (fun b a ↦ g a + b) fun b ↦ hg.add_const b /-- In a topological vector space, the addition of a simple function and a measurable function is measurable. -/ theorem _root_.Measurable.simpleFunc_add {E : Type*} {_ : MeasurableSpace α} [MeasurableSpace E] [AddCancelMonoid E] [MeasurableAdd E] - {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : - Measurable ((f : α → E) + g) := by - simpa using f.measurable_bind (fun b a => b + g a) fun b => hg.const_add b + {g : α → E} (hg : Measurable g) (f : SimpleFunc α E) : Measurable ((f : α → E) + g) := + f.measurable_bind (fun b a => b + g a) fun b => hg.const_add b end SimpleFunc From fa5009ddbe725442db61c820c765f4adab6c2ab7 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 18 Apr 2026 16:34:43 +0800 Subject: [PATCH 4/5] apply suggestions --- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean index 662e2e185593d0..38ab3d89344b00 100644 --- a/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean +++ b/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean @@ -393,7 +393,9 @@ theorem eLpNorm_le_of_ae_enorm_bound {ε} [TopologicalSpace ε] [ESeminormedAddM theorem eLpNorm_le_of_ae_nnnorm_bound {f : α → F} {C : ℝ≥0} (hfC : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ C) : eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := by - simpa [C.enorm_eq] using eLpNorm_le_of_ae_enorm_bound (hfC.mono fun _ hx ↦ enorm_le_coe.mpr hx) + have : eLpNorm f p μ ≤ C • μ Set.univ ^ p.toReal⁻¹ := + eLpNorm_le_of_ae_enorm_bound (hfC.mono fun _ hx ↦ enorm_le_coe.mpr hx) + simpa [C.enorm_eq] theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) : eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C := by From 991dfa844ea8affa2fc1fc9fd26452a574c06fa2 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Sat, 18 Apr 2026 16:35:36 +0800 Subject: [PATCH 5/5] Update Basic.lean --- .../MeasureTheory/Constructions/Polish/Basic.lean | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean index 084a984abd2ae6..d013f8556c1ebb 100644 --- a/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean +++ b/Mathlib/MeasureTheory/Constructions/Polish/Basic.lean @@ -838,10 +838,14 @@ theorem MeasurableSet.image_of_measurable_injOn {f : γ → α} obtain ⟨t', t't, f_cont, t'_polish⟩ : ∃ t' : TopologicalSpace γ, t' ≤ tγ ∧ @Continuous γ _ t' _ f ∧ @PolishSpace γ t' := f_meas.exists_continuous - have hs' := (borel_anti t't s) <| by rwa [← eq_borel_upgradeStandardBorel γ] - letI : MeasurableSpace γ := @borel γ t' - haveI : BorelSpace γ := ⟨rfl⟩ - exact hs'.image_of_continuousOn_injOn f_cont.continuousOn f_inj + have M : MeasurableSet[@borel γ t'] s := + @Continuous.measurable γ γ t' (@borel γ t') + (@BorelSpace.opensMeasurable γ t' (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl)) + tγ _ _ _ (continuous_id_of_le t't) s hs + exact + @MeasurableSet.image_of_continuousOn_injOn γ + _ _ _ _ s f _ t' t'_polish (@borel γ t') (@BorelSpace.mk _ _ (borel γ) rfl) + M (@Continuous.continuousOn γ _ t' _ f s f_cont) f_inj /-- An injective continuous function on a Polish space is a measurable embedding. -/ theorem Continuous.measurableEmbedding [BorelSpace β]