From c49d34509662666c14c7f5a7539226526f73c60a Mon Sep 17 00:00:00 2001 From: Etienne Marion Date: Thu, 21 May 2026 09:03:09 +0200 Subject: [PATCH 1/3] feat: the identity function is a.e.-strongly measurable w.r.t. the map by an a.e.-strongly measurable function --- .../AEStronglyMeasurable.lean | 51 +++++++++++++++---- 1 file changed, 41 insertions(+), 10 deletions(-) diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean index 188d6c0503ddab..197eeddc910bb6 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean @@ -135,6 +135,27 @@ theorem aestronglyMeasurable_zero_measure (f : α → β) : theorem SimpleFunc.aestronglyMeasurable (f : α →ₛ β) : AEStronglyMeasurable f μ := f.stronglyMeasurable.aestronglyMeasurable +/-- In a pseudometrizable space, if a measure `μ` is supported on +a separable set then the identity function is `AEStronglyMeasurable` with respect to `μ`. -/ +lemma aestronglyMeasurable_id_of_isSeparable [TopologicalSpace α] + [TopologicalSpace.PseudoMetrizableSpace α] [OpensMeasurableSpace α] + {s : Set α} (h1 : TopologicalSpace.IsSeparable s) (h2 : μ sᶜ = 0) (h3 : MeasurableSet s) : + AEStronglyMeasurable id μ := by + nontriviality α + obtain ⟨a, -⟩ := exists_pair_ne α + classical + refine ⟨s.piecewise id (fun _ ↦ a), ?_, Filter.mem_of_superset h2 (fun x hx ↦ by simp [hx])⟩ + have h : StronglyMeasurable ((↑) : s → α) := by + have := h1.secondCountableTopology + exact continuous_subtype_val.stronglyMeasurable + have : s.piecewise id (fun _ ↦ a) = ((↑) : s → α).extend ((↑) : s → α) (fun _ ↦ a) := by + ext x + by_cases hx : x ∈ s + · simp [Function.extend_val_apply, hx] + · simp [hx] + rw [this] + exact (MeasurableEmbedding.subtype_coe h3).stronglyMeasurable_extend h stronglyMeasurable_const + namespace AEStronglyMeasurable @[fun_prop] @@ -379,8 +400,7 @@ section Monoid variable {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M] --- TODO: `fun_prop` cannot use lemmas with a condition quantifying over the function -@[to_additive (attr := fun_prop)] +@[to_additive (attr := fun_prop, measurability)] theorem _root_.List.aestronglyMeasurable_prod (l : List (α → M)) (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable l.prod μ := by induction l with @@ -390,7 +410,7 @@ theorem _root_.List.aestronglyMeasurable_prod (l : List (α → M)) rw [List.prod_cons] exact hl.1.mul (ihl hl.2) -@[to_additive (attr := fun_prop)] +@[to_additive (attr := fun_prop, measurability)] theorem _root_.List.aestronglyMeasurable_fun_prod (l : List (α → M)) (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x => (l.map fun f : α → M => f x).prod) μ := by @@ -402,26 +422,26 @@ section CommMonoid variable {M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] -@[to_additive (attr := fun_prop)] +@[to_additive (attr := fun_prop, measurability)] theorem _root_.Multiset.aestronglyMeasurable_prod (l : Multiset (α → M)) (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable l.prod μ := by rcases l with ⟨l⟩ simpa using l.aestronglyMeasurable_prod (by simpa using hl) -@[to_additive (attr := fun_prop)] +@[to_additive (attr := fun_prop, measurability)] theorem _root_.Multiset.aestronglyMeasurable_fun_prod (s : Multiset (α → M)) (hs : ∀ f ∈ s, AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x => (s.map fun f : α → M => f x).prod) μ := by simpa only [← Pi.multiset_prod_apply] using s.aestronglyMeasurable_prod hs -@[to_additive (attr := fun_prop)] +@[to_additive (attr := fun_prop, measurability)] theorem _root_.Finset.aestronglyMeasurable_prod {ι : Type*} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (∏ i ∈ s, f i) μ := Multiset.aestronglyMeasurable_prod _ fun _g hg => let ⟨_i, hi, hg⟩ := Multiset.mem_map.1 hg hg ▸ hf _ hi -@[to_additive (attr := fun_prop)] +@[to_additive (attr := fun_prop, measurability)] theorem _root_.Finset.aestronglyMeasurable_fun_prod {ι : Type*} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ := by @@ -585,6 +605,17 @@ theorem isSeparable_ae_range (hf : AEStronglyMeasurable f μ) : filter_upwards [hf.ae_eq_mk] with x hx simp [hx] +/-- If `μ : Measure α` and `f : α → β` is `AEStronglyMeasurable` where `β` is a pseudometrizable +space and a Borel space, then the identity is a.e.-strongly measurable w.r.t. `μ.map f`. -/ +lemma aestronglyMeasurable_id_map {mβ : MeasurableSpace β} + [TopologicalSpace.PseudoMetrizableSpace β] [BorelSpace β] + {f : α → β} (hf : AEStronglyMeasurable f μ) : + AEStronglyMeasurable id (μ.map f) := by + obtain ⟨t, ht1, ht2⟩ := hf.isSeparable_ae_range + refine aestronglyMeasurable_id_of_isSeparable ht1.closure ?_ isClosed_closure.measurableSet + refine ae_map_iff hf.aemeasurable isClosed_closure.measurableSet |>.2 ?_ + filter_upwards [ht2] with ω hω using subset_closure hω + /-- A function is almost everywhere strongly measurable if and only if it is almost everywhere measurable, and up to a zero measure set its range is contained in a separable set. -/ theorem _root_.aestronglyMeasurable_iff_aemeasurable_separable [PseudoMetrizableSpace β] @@ -739,13 +770,13 @@ theorem _root_.aestronglyMeasurable_add_measure_iff [PseudoMetrizableSpace β] { rw [← sum_cond, aestronglyMeasurable_sum_measure_iff, Bool.forall_bool, and_comm] rfl -@[fun_prop] +@[fun_prop, measurability] theorem add_measure [PseudoMetrizableSpace β] {ν : Measure α} {f : α → β} (hμ : AEStronglyMeasurable f μ) (hν : AEStronglyMeasurable f ν) : AEStronglyMeasurable f (μ + ν) := aestronglyMeasurable_add_measure_iff.2 ⟨hμ, hν⟩ -@[fun_prop] +@[fun_prop, measurability] protected theorem iUnion [PseudoMetrizableSpace β] {s : ι → Set α} (h : ∀ i, AEStronglyMeasurable f (μ.restrict (s i))) : AEStronglyMeasurable f (μ.restrict (⋃ i, s i)) := @@ -771,7 +802,7 @@ theorem aestronglyMeasurable_uIoc_iff [LinearOrder α] [PseudoMetrizableSpace β AEStronglyMeasurable f (μ.restrict <| Ioc b a) := by rw [uIoc_eq_union, aestronglyMeasurable_union_iff] -@[fun_prop] +@[fun_prop, measurability] theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : AEStronglyMeasurable f μ) (c : R) : AEStronglyMeasurable f (c • μ) := ⟨h.mk f, h.stronglyMeasurable_mk, ae_smul_measure h.ae_eq_mk c⟩ From 53ff5b93956fdf9b45b03918561ac5e489da132e Mon Sep 17 00:00:00 2001 From: Etienne Marion Date: Thu, 21 May 2026 09:07:21 +0200 Subject: [PATCH 2/3] fix --- .../AEStronglyMeasurable.lean | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean index 197eeddc910bb6..99dfd740ac338b 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean @@ -400,7 +400,8 @@ section Monoid variable {M : Type*} [Monoid M] [TopologicalSpace M] [ContinuousMul M] -@[to_additive (attr := fun_prop, measurability)] +-- TODO: `fun_prop` cannot use lemmas with a condition quantifying over the function +@[to_additive (attr := fun_prop)] theorem _root_.List.aestronglyMeasurable_prod (l : List (α → M)) (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable l.prod μ := by induction l with @@ -410,7 +411,7 @@ theorem _root_.List.aestronglyMeasurable_prod (l : List (α → M)) rw [List.prod_cons] exact hl.1.mul (ihl hl.2) -@[to_additive (attr := fun_prop, measurability)] +@[to_additive (attr := fun_prop)] theorem _root_.List.aestronglyMeasurable_fun_prod (l : List (α → M)) (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x => (l.map fun f : α → M => f x).prod) μ := by @@ -422,26 +423,26 @@ section CommMonoid variable {M : Type*} [CommMonoid M] [TopologicalSpace M] [ContinuousMul M] -@[to_additive (attr := fun_prop, measurability)] +@[to_additive (attr := fun_prop)] theorem _root_.Multiset.aestronglyMeasurable_prod (l : Multiset (α → M)) (hl : ∀ f ∈ l, AEStronglyMeasurable f μ) : AEStronglyMeasurable l.prod μ := by rcases l with ⟨l⟩ simpa using l.aestronglyMeasurable_prod (by simpa using hl) -@[to_additive (attr := fun_prop, measurability)] +@[to_additive (attr := fun_prop)] theorem _root_.Multiset.aestronglyMeasurable_fun_prod (s : Multiset (α → M)) (hs : ∀ f ∈ s, AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun x => (s.map fun f : α → M => f x).prod) μ := by simpa only [← Pi.multiset_prod_apply] using s.aestronglyMeasurable_prod hs -@[to_additive (attr := fun_prop, measurability)] +@[to_additive (attr := fun_prop)] theorem _root_.Finset.aestronglyMeasurable_prod {ι : Type*} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (∏ i ∈ s, f i) μ := Multiset.aestronglyMeasurable_prod _ fun _g hg => let ⟨_i, hi, hg⟩ := Multiset.mem_map.1 hg hg ▸ hf _ hi -@[to_additive (attr := fun_prop, measurability)] +@[to_additive (attr := fun_prop)] theorem _root_.Finset.aestronglyMeasurable_fun_prod {ι : Type*} {f : ι → α → M} (s : Finset ι) (hf : ∀ i ∈ s, AEStronglyMeasurable (f i) μ) : AEStronglyMeasurable (fun a => ∏ i ∈ s, f i a) μ := by @@ -770,13 +771,13 @@ theorem _root_.aestronglyMeasurable_add_measure_iff [PseudoMetrizableSpace β] { rw [← sum_cond, aestronglyMeasurable_sum_measure_iff, Bool.forall_bool, and_comm] rfl -@[fun_prop, measurability] +@[fun_prop] theorem add_measure [PseudoMetrizableSpace β] {ν : Measure α} {f : α → β} (hμ : AEStronglyMeasurable f μ) (hν : AEStronglyMeasurable f ν) : AEStronglyMeasurable f (μ + ν) := aestronglyMeasurable_add_measure_iff.2 ⟨hμ, hν⟩ -@[fun_prop, measurability] +@[fun_prop] protected theorem iUnion [PseudoMetrizableSpace β] {s : ι → Set α} (h : ∀ i, AEStronglyMeasurable f (μ.restrict (s i))) : AEStronglyMeasurable f (μ.restrict (⋃ i, s i)) := @@ -802,7 +803,7 @@ theorem aestronglyMeasurable_uIoc_iff [LinearOrder α] [PseudoMetrizableSpace β AEStronglyMeasurable f (μ.restrict <| Ioc b a) := by rw [uIoc_eq_union, aestronglyMeasurable_union_iff] -@[fun_prop, measurability] +@[fun_prop] theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] (h : AEStronglyMeasurable f μ) (c : R) : AEStronglyMeasurable f (c • μ) := ⟨h.mk f, h.stronglyMeasurable_mk, ae_smul_measure h.ae_eq_mk c⟩ From 605d3215ac5dd30c588b67390408e219b25e0b9b Mon Sep 17 00:00:00 2001 From: Etienne Marion Date: Thu, 21 May 2026 10:11:30 +0200 Subject: [PATCH 3/3] remove measurability hypothesis --- .../AEStronglyMeasurable.lean | 19 +++++++++++-------- 1 file changed, 11 insertions(+), 8 deletions(-) diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean index 99dfd740ac338b..08bbe788dc7299 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean +++ b/Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean @@ -139,22 +139,25 @@ theorem SimpleFunc.aestronglyMeasurable (f : α →ₛ β) : AEStronglyMeasurabl a separable set then the identity function is `AEStronglyMeasurable` with respect to `μ`. -/ lemma aestronglyMeasurable_id_of_isSeparable [TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] [OpensMeasurableSpace α] - {s : Set α} (h1 : TopologicalSpace.IsSeparable s) (h2 : μ sᶜ = 0) (h3 : MeasurableSet s) : + {s : Set α} (h1 : TopologicalSpace.IsSeparable s) (h2 : μ sᶜ = 0) : AEStronglyMeasurable id μ := by nontriviality α obtain ⟨a, -⟩ := exists_pair_ne α classical - refine ⟨s.piecewise id (fun _ ↦ a), ?_, Filter.mem_of_superset h2 (fun x hx ↦ by simp [hx])⟩ - have h : StronglyMeasurable ((↑) : s → α) := by - have := h1.secondCountableTopology + refine ⟨(closure s).piecewise id (fun _ ↦ a), ?_, + Filter.mem_of_superset h2 (fun x hx ↦ by simp [subset_closure hx])⟩ + have h : StronglyMeasurable ((↑) : closure s → α) := by + have := h1.closure.secondCountableTopology exact continuous_subtype_val.stronglyMeasurable - have : s.piecewise id (fun _ ↦ a) = ((↑) : s → α).extend ((↑) : s → α) (fun _ ↦ a) := by + have : (closure s).piecewise id (fun _ ↦ a) = + ((↑) : closure s → α).extend ((↑) : closure s → α) (fun _ ↦ a) := by ext x - by_cases hx : x ∈ s + by_cases hx : x ∈ closure s · simp [Function.extend_val_apply, hx] · simp [hx] rw [this] - exact (MeasurableEmbedding.subtype_coe h3).stronglyMeasurable_extend h stronglyMeasurable_const + exact (MeasurableEmbedding.subtype_coe isClosed_closure.measurableSet).stronglyMeasurable_extend + h stronglyMeasurable_const namespace AEStronglyMeasurable @@ -613,7 +616,7 @@ lemma aestronglyMeasurable_id_map {mβ : MeasurableSpace β} {f : α → β} (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable id (μ.map f) := by obtain ⟨t, ht1, ht2⟩ := hf.isSeparable_ae_range - refine aestronglyMeasurable_id_of_isSeparable ht1.closure ?_ isClosed_closure.measurableSet + refine aestronglyMeasurable_id_of_isSeparable ht1.closure ?_ refine ae_map_iff hf.aemeasurable isClosed_closure.measurableSet |>.2 ?_ filter_upwards [ht2] with ω hω using subset_closure hω