Merge pull request #218 from LorenzoLuccioli/task-a3

Task A.3

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)
@@ -165,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

PFR/MoreRuzsaDist.lean

@@ -246,7 +246,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
@@ -744,15 +744,18 @@ 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
 
 /-- 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)
-    (hident : ∀ i, IdentDistrib (X i) (X' i) ) :
-    D[X ; hΩ] = D[X' ; hΩ'] := by sorry
+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 _), (hident _).map_eq]
 
 /-- If `X_i` are independent, then `D[X_{[m]}] = H[∑_{i=1}^m X_i] - \frac{1}{m} \sum_{i=1}^m H[X_i]`. -/
 lemma multiDist_indep {m : ℕ} {Ω : Type*} (hΩ : MeasureSpace Ω) (X : Fin m → Ω → G)