From 62dd6e8069f081c2f5c3e3a77bc1be924ebfe355 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 24 Jun 2024 02:35:28 +0200 Subject: [PATCH 1/5] Update IdentDistrib.lean Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com> --- PFR/Mathlib/Probability/IdentDistrib.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/PFR/Mathlib/Probability/IdentDistrib.lean b/PFR/Mathlib/Probability/IdentDistrib.lean index 1fb99824..5f8282ba 100644 --- a/PFR/Mathlib/Probability/IdentDistrib.lean +++ b/PFR/Mathlib/Probability/IdentDistrib.lean @@ -147,7 +147,8 @@ lemma identDistrib_ulift_self {X : Ω → α} (hX : Measurable X) : change MeasurableSet (ULift.down ⁻¹' (ULift.down '' s)) rwa [Set.preimage_image_eq _ ULift.down_injective] -/-- To show identical distribution of two random variables on a mixture of probability measures, it suffices to do so on each non-trivial component. -/ +/-- To show identical distribution of two random variables on a mixture of probability measures, +it suffices to do so on each non-trivial component. -/ -- in fact this is an if and only if lemma identDistrib_of_sum {X : Ω → α} {Y : Ω' → α} {μ : T → Measure Ω} {μ' : T → Measure Ω'} {w : T → ENNReal} (s : Finset T) (hX : Measurable X) (hY : Measurable Y) From 2afd5d35696c1f21d32b834e19f1d6b882510165 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 24 Jun 2024 02:37:39 +0200 Subject: [PATCH 2/5] Update IdentDistrib.lean Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com> --- PFR/Mathlib/Probability/IdentDistrib.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/PFR/Mathlib/Probability/IdentDistrib.lean b/PFR/Mathlib/Probability/IdentDistrib.lean index 5f8282ba..60241897 100644 --- a/PFR/Mathlib/Probability/IdentDistrib.lean +++ b/PFR/Mathlib/Probability/IdentDistrib.lean @@ -166,6 +166,25 @@ lemma identDistrib_of_sum {X : Ω → α} {Y : Ω' → α} {μ : T → Measure rw [Measure.mapₗ_apply_of_measurable hX, Measure.mapₗ_apply_of_measurable hY] exact (h_ident y hy).map_eq +-- [TODO] +-- theorem IdentDistrib.comp' {m : ℕ} {α : (i : Fin m) → Type*} {hα : (i : Fin m) → MeasurableSpace (α i)} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i)) +-- (hΩ': (i : Fin m) → MeasureSpace (Ω' i)) (f : (i : Fin m) → (Ω i) → (α i)) (g : (i : Fin m) → (Ω' i) → (α i)) +-- (hident : ∀ i, IdentDistrib (f i) (g i)) {u : ((i : Fin m) → α i) → β} +-- (hu : Measurable u) : IdentDistrib (u ∘ (fun i ↦ )) (u ∘ g) μ ν := sorry + +-- { aemeasurable_fst := hu.comp_aemeasurable h.aemeasurable_fst +-- aemeasurable_snd := by rw [h.map_eq] at hu; exact hu.comp_aemeasurable h.aemeasurable_snd +-- map_eq := by +-- rw [← AEMeasurable.map_map_of_aemeasurable hu h.aemeasurable_fst, ← +-- AEMeasurable.map_map_of_aemeasurable _ h.aemeasurable_snd, h.map_eq] +-- rwa [← h.map_eq] } +-- #align probability_theory.ident_distrib.comp_of_ae_measurable ProbabilityTheory.IdentDistrib.comp_of_aemeasurable + +-- protected theorem comp {u : γ → δ} (h : IdentDistrib f g μ ν) (hu : Measurable u) : +-- IdentDistrib (u ∘ f) (u ∘ g) μ ν := +-- h.comp_of_aemeasurable hu.aemeasurable +-- #align probability_theory.ident_distrib.comp ProbabilityTheory.IdentDistrib.comp + /-- A random variable is identically distributed to its lift to a product space (in the first factor). -/ lemma identDistrib_comp_fst {X : Ω → α} (hX : Measurable X) (μ : Measure Ω) (μ' : Measure Ω') [IsProbabilityMeasure μ'] : IdentDistrib (X ∘ Prod.fst) X (μ.prod μ') μ where From 2346a749595cf02e74ced098eb188b032dabb6f9 Mon Sep 17 00:00:00 2001 From: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> Date: Mon, 24 Jun 2024 02:38:17 +0200 Subject: [PATCH 3/5] Progress on A.3 Co-Authored-By: Lorenzo Luccioli <71074618+LorenzoLuccioli@users.noreply.github.com> --- PFR/MoreRuzsaDist.lean | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/PFR/MoreRuzsaDist.lean b/PFR/MoreRuzsaDist.lean index eb768d7c..c8c4d03d 100644 --- a/PFR/MoreRuzsaDist.lean +++ b/PFR/MoreRuzsaDist.lean @@ -239,7 +239,7 @@ lemma rdist_of_neg_le [IsProbabilityMeasure μ] [IsProbabilityMeasure μ'] (hX : calc _ = H[⟨⟨X₃ - Y₂, ⟨X₁ - Y₃, ⟨X₂, Y₁⟩⟩⟩, (X₃ - Y₂) - (X₁ - Y₃) + X₂ + Y₁⟩ ; ν₀] := by refine IdentDistrib.entropy_eq <| - IdentDistrib.of_ae_eq (meas321321.prod_mk <| mX₃.add mY₃).aemeasurable ?_ + IdentDistrib.of_ae_eq (meas321321.prod_mk <| mX₃.add mY₃).aemeasurable ?_ filter_upwards [eq4] with ω h simp only [Prod.mk.injEq, h, Pi.add_apply, Pi.sub_apply, and_self] _ = _ := by @@ -737,15 +737,23 @@ Then we define `D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i']`, where the `X_i' of the `X_i`.-/ noncomputable def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i)) - (X : (i : Fin m) → (Ω i) → G) : ℝ := H[ fun ω ↦ ∑ i, (X i) (ω i); .pi (fun i ↦ (hΩ i).volume)] - (m:ℝ)⁻¹ * ∑ i, H[X i] + (X : (i : Fin m) → (Ω i) → G) : ℝ := + H[fun ω ↦ ∑ i, (X i) (ω i); .pi (fun i ↦ (hΩ i).volume)] - (m:ℝ)⁻¹ * ∑ i, H[X i] @[inherit_doc multiDist] notation3:max "D[" X " ; " hΩ "]" => multiDist hΩ X +#check IdentDistrib.entropy_eq + /-- If `X_i` has the same distribution as `Y_i` for each `i`, then `D[X_[m]] = D[Y_[m]]`. -/ -lemma multiDist_copy {m :ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i)) +lemma multiDist_copy {m : ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i)) (hΩ': (i : Fin m) → MeasureSpace (Ω' i)) (X : (i : Fin m) → (Ω i) → G) (X' : (i : Fin m) → (Ω' i) → G) - (hident : ∀ i, IdentDistrib (X i) (X' i) ) : - D[X ; hΩ] = D[X' ; hΩ'] := by sorry + (hident : ∀ i, IdentDistrib (X i) (X' i)) : + D[X ; hΩ] = D[X' ; hΩ'] := by + simp_rw [multiDist, IdentDistrib.entropy_eq (hident _)] + simp only [sub_left_inj] + refine IdentDistrib.entropy_eq ?_ + refine ?_ + sorry /-- If `X_i` are independent, then `D[X_[m]] = D[Y_[m]]`. -/ lemma multiDist_indep {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) (X : Fin m → Ω → G) From 5a6c4f467d537959106c2627155262439db994f6 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 2 Jul 2024 23:39:45 +0200 Subject: [PATCH 4/5] modify definition of `multiDist` Co-authored-by: Pietro Monticone --- PFR/MoreRuzsaDist.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/PFR/MoreRuzsaDist.lean b/PFR/MoreRuzsaDist.lean index c8c4d03d..1933329d 100644 --- a/PFR/MoreRuzsaDist.lean +++ b/PFR/MoreRuzsaDist.lean @@ -737,13 +737,11 @@ Then we define `D[X_[m]] = H[∑ i, X_i'] - 1/m*∑ i, H[X_i']`, where the `X_i' of the `X_i`.-/ noncomputable def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i)) - (X : (i : Fin m) → (Ω i) → G) : ℝ := - H[fun ω ↦ ∑ i, (X i) (ω i); .pi (fun i ↦ (hΩ i).volume)] - (m:ℝ)⁻¹ * ∑ i, H[X i] + (X : (i : Fin m) → (Ω i) → G) : ℝ := + H[fun x ↦ ∑ i, x i; .pi (fun i ↦ (hΩ i).volume.map (X i))] - (m:ℝ)⁻¹ * ∑ i, H[X i] @[inherit_doc multiDist] notation3:max "D[" X " ; " hΩ "]" => multiDist hΩ X -#check IdentDistrib.entropy_eq - /-- If `X_i` has the same distribution as `Y_i` for each `i`, then `D[X_[m]] = D[Y_[m]]`. -/ lemma multiDist_copy {m : ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i)) (hΩ': (i : Fin m) → MeasureSpace (Ω' i)) (X : (i : Fin m) → (Ω i) → G) (X' : (i : Fin m) → (Ω' i) → G) From 315ea54197bff4f2f9ffd2dd8e4d9ea9322f8c88 Mon Sep 17 00:00:00 2001 From: Lorenzo Luccioli Date: Tue, 2 Jul 2024 23:41:01 +0200 Subject: [PATCH 5/5] proof of `multiDist_copy` Co-authored-by: Pietro Monticone <38562595+pitmonticone@users.noreply.github.com> --- PFR/MoreRuzsaDist.lean | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/PFR/MoreRuzsaDist.lean b/PFR/MoreRuzsaDist.lean index 1933329d..7930a753 100644 --- a/PFR/MoreRuzsaDist.lean +++ b/PFR/MoreRuzsaDist.lean @@ -743,15 +743,12 @@ def multiDist {m : ℕ} {Ω : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpa @[inherit_doc multiDist] notation3:max "D[" X " ; " hΩ "]" => multiDist hΩ X /-- If `X_i` has the same distribution as `Y_i` for each `i`, then `D[X_[m]] = D[Y_[m]]`. -/ -lemma multiDist_copy {m : ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i)) - (hΩ': (i : Fin m) → MeasureSpace (Ω' i)) (X : (i : Fin m) → (Ω i) → G) (X' : (i : Fin m) → (Ω' i) → G) +lemma multiDist_copy {m : ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} + (hΩ : (i : Fin m) → MeasureSpace (Ω i)) (hΩ': (i : Fin m) → MeasureSpace (Ω' i)) + (X : (i : Fin m) → (Ω i) → G) (X' : (i : Fin m) → (Ω' i) → G) (hident : ∀ i, IdentDistrib (X i) (X' i)) : D[X ; hΩ] = D[X' ; hΩ'] := by - simp_rw [multiDist, IdentDistrib.entropy_eq (hident _)] - simp only [sub_left_inj] - refine IdentDistrib.entropy_eq ?_ - refine ?_ - sorry + simp_rw [multiDist, IdentDistrib.entropy_eq (hident _), (hident _).map_eq] /-- If `X_i` are independent, then `D[X_[m]] = D[Y_[m]]`. -/ lemma multiDist_indep {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) (X : Fin m → Ω → G)