From 1ec32f704f80dd4fdd367a61097a3d7dc764e474 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Wed, 22 Apr 2026 08:57:26 +0800 Subject: [PATCH 1/3] refactor(MeasureTheory): golf Pi construction --- Mathlib/MeasureTheory/Constructions/Pi.lean | 23 ++++++--------------- 1 file changed, 6 insertions(+), 17 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 5f0f7f9209e3a2..1ad00cb7d6a5b2 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -450,23 +450,6 @@ theorem ae_eq_set_pi {I : Set ι} {s t : ∀ i, Set (α i)} (h : ∀ i ∈ I, s Set.pi I s =ᵐ[Measure.pi μ] Set.pi I t := (ae_le_set_pi fun i hi => (h i hi).le).antisymm (ae_le_set_pi fun i hi => (h i hi).symm.le) -lemma pi_map_piCongrLeft [hι' : Fintype ι'] (e : ι ≃ ι') {β : ι' → Type*} - [∀ i, MeasurableSpace (β i)] (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] : - (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e) - = Measure.pi μ := by - let e_meas : ((b : ι) → β (e b)) ≃ᵐ ((a : ι') → β a) := - MeasurableEquiv.piCongrLeft (fun i ↦ β i) e - refine Measure.pi_eq (fun s _ ↦ ?_) |>.symm - rw [e_meas.measurableEmbedding.map_apply] - let s' : (i : ι) → Set (β (e i)) := fun i ↦ s (e i) - have : e_meas ⁻¹' pi univ s = pi univ s' := by - ext x - simp only [mem_preimage, Set.mem_pi, mem_univ, forall_true_left, s'] - refine (e.forall_congr ?_).symm - intro i - rw [MeasurableEquiv.piCongrLeft_apply_apply e x i] - simpa [this] using Fintype.prod_equiv _ (fun _ ↦ (μ _) (s' _)) _ (congrFun rfl) - lemma pi_map_piOptionEquivProd {β : Option ι → Type*} [∀ i, MeasurableSpace (β i)] (μ : (i : Option ι) → Measure (β i)) [∀ (i : Option ι), SigmaFinite (μ i)] : ((Measure.pi fun i ↦ μ (some i)).prod (μ none)).map @@ -755,6 +738,12 @@ theorem volume_measurePreserving_piCongrLeft (α : ι → Type*) (f : ι' ≃ ι MeasurePreserving (MeasurableEquiv.piCongrLeft α f) volume volume := measurePreserving_piCongrLeft (fun _ ↦ volume) f +lemma pi_map_piCongrLeft (e : ι ≃ ι') {β : ι' → Type*} [∀ i, MeasurableSpace (β i)] + (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] : + (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e) = + Measure.pi μ := + (measurePreserving_piCongrLeft (α := fun i ↦ β i) (μ := μ) e).map_eq + theorem measurePreserving_arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α] [MeasurableSpace β] [Fintype γ] (μ : γ → Measure α) (ν : γ → Measure β) [∀ i, SigmaFinite (μ i)] [∀ i, SigmaFinite (ν i)] : From 35ff69a0f7e3ccb7da74baa7f4ac553b8f424b96 Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Wed, 22 Apr 2026 09:20:24 +0800 Subject: [PATCH 2/3] fix ci --- Mathlib/MeasureTheory/Constructions/Pi.lean | 2 +- Mathlib/Probability/ProductMeasure.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index 1ad00cb7d6a5b2..a7030a5dab285d 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -742,7 +742,7 @@ lemma pi_map_piCongrLeft (e : ι ≃ ι') {β : ι' → Type*} [∀ i, Measurabl (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] : (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e) = Measure.pi μ := - (measurePreserving_piCongrLeft (α := fun i ↦ β i) (μ := μ) e).map_eq + (measurePreserving_piCongrLeft (α := fun i ↦ β i) μ e).map_eq theorem measurePreserving_arrowProdEquivProdArrow (α β γ : Type*) [MeasurableSpace α] [MeasurableSpace β] [Fintype γ] (μ : γ → Measure α) (ν : γ → Measure β) [∀ i, SigmaFinite (μ i)] diff --git a/Mathlib/Probability/ProductMeasure.lean b/Mathlib/Probability/ProductMeasure.lean index 49333de91686c9..9a1e464c9ede56 100644 --- a/Mathlib/Probability/ProductMeasure.lean +++ b/Mathlib/Probability/ProductMeasure.lean @@ -89,7 +89,7 @@ theorem piContent_eq_measure_pi [Fintype ι] {s : Set (Π i, X i)} (hs : Measura have : s = cylinder univ (MeasurableEquiv.piCongrLeft X e ⁻¹' s) := rfl nth_rw 1 [this] dsimp [e] - rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← Measure.pi_map_piCongrLeft e, + rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← MeasureTheory.pi_map_piCongrLeft e, ← Measure.map_apply (by fun_prop) hs]; rfl end Preliminaries From 0b21b6726868b3beb3a4f3e199aa74c9e56fa8cd Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Fri, 24 Apr 2026 18:22:28 +0800 Subject: [PATCH 3/3] golf --- Mathlib/MeasureTheory/Constructions/Pi.lean | 2 +- Mathlib/Probability/ProductMeasure.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/Pi.lean b/Mathlib/MeasureTheory/Constructions/Pi.lean index a7030a5dab285d..232c8330843009 100644 --- a/Mathlib/MeasureTheory/Constructions/Pi.lean +++ b/Mathlib/MeasureTheory/Constructions/Pi.lean @@ -738,7 +738,7 @@ theorem volume_measurePreserving_piCongrLeft (α : ι → Type*) (f : ι' ≃ ι MeasurePreserving (MeasurableEquiv.piCongrLeft α f) volume volume := measurePreserving_piCongrLeft (fun _ ↦ volume) f -lemma pi_map_piCongrLeft (e : ι ≃ ι') {β : ι' → Type*} [∀ i, MeasurableSpace (β i)] +lemma Measure.pi_map_piCongrLeft (e : ι ≃ ι') {β : ι' → Type*} [∀ i, MeasurableSpace (β i)] (μ : (i : ι') → Measure (β i)) [∀ i, SigmaFinite (μ i)] : (Measure.pi fun i ↦ μ (e i)).map (MeasurableEquiv.piCongrLeft (fun i ↦ β i) e) = Measure.pi μ := diff --git a/Mathlib/Probability/ProductMeasure.lean b/Mathlib/Probability/ProductMeasure.lean index 9a1e464c9ede56..49333de91686c9 100644 --- a/Mathlib/Probability/ProductMeasure.lean +++ b/Mathlib/Probability/ProductMeasure.lean @@ -89,7 +89,7 @@ theorem piContent_eq_measure_pi [Fintype ι] {s : Set (Π i, X i)} (hs : Measura have : s = cylinder univ (MeasurableEquiv.piCongrLeft X e ⁻¹' s) := rfl nth_rw 1 [this] dsimp [e] - rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← MeasureTheory.pi_map_piCongrLeft e, + rw [piContent_cylinder _ (hs.preimage (by fun_prop)), ← Measure.pi_map_piCongrLeft e, ← Measure.map_apply (by fun_prop) hs]; rfl end Preliminaries