fix

Author: sgouezel

PFR/Examples.lean

@@ -119,7 +119,7 @@ variable (X : Ω → S) (hX : Measurable X) (Y : Ω → T) (hY : Measurable Y) (
 
 /-- $H[X]$ is the Shannon entropy of $X$. -/
 example : H[X] =
-    - ∑ x, ((ℙ : Measure Ω).map X {x}).toReal * Real.log ((ℙ : Measure Ω).map X {x}).toReal := by
+    - ∑ x, ((ℙ : Measure Ω).map X).real {x} * Real.log (((ℙ : Measure Ω).map X).real {x}) := by
   rw [entropy_eq_sum ℙ, ← Finset.sum_neg_distrib, tsum_eq_sum]
   · congr with x
     unfold Real.negMulLog

PFR/ImprovedPFR.lean

@@ -133,38 +133,40 @@ lemma gen_ineq_aux2 :
         ext p; simp
       rw [this]
       have J : IndepFun (Z₁ + Z₃) (Z₂ + Z₄) := by exact I.comp measurable_add measurable_add
-      rw [J.measureReal_inter_preimage_eq_mul (.singleton x) (.singleton y), ENNReal.toReal_mul]
-      rcases eq_or_ne (ℙ ((Z₁ + Z₃) ⁻¹' {x})) 0 with h1|h1
+      rw [J.measureReal_inter_preimage_eq_mul (.singleton x) (.singleton y)]
+      rcases eq_or_ne (Measure.real ℙ ((Z₁ + Z₃) ⁻¹' {x})) 0 with h1|h1
       · simp [h1]
-      rcases eq_or_ne (ℙ ((Z₂ + Z₄) ⁻¹' {y})) 0 with h2|h2
+      rcases eq_or_ne (Measure.real ℙ ((Z₂ + Z₄) ⁻¹' {y})) 0 with h2|h2
       · simp [h2]
       congr 1
       have A : IdentDistrib Z₁ Z₁ (ℙ[|(Z₁ + Z₃) ⁻¹' {x} ∩ (Z₂ + Z₄) ⁻¹' {y}])
           (ℙ[|(Z₁ + Z₃) ⁻¹' {x}]) := by
         rw [← cond_cond_eq_cond_inter']
-        have : IsProbabilityMeasure (ℙ[|(Z₁ + Z₃) ⁻¹' {x}]) := cond_isProbabilityMeasure h1
+        have : IsProbabilityMeasure (ℙ[|(Z₁ + Z₃) ⁻¹' {x}]) := cond_isProbabilityMeasure_of_real h1
         apply (IndepFun.identDistrib_cond _ (.singleton _) hZ₁ (by fun_prop) _).symm
         · have : IndepFun (⟨Z₁, Z₃⟩) (⟨Z₂, Z₄⟩) (ℙ[|(⟨Z₁, Z₃⟩) ⁻¹' {p | p.1 + p.2 = x}]) :=
             I.cond_left (measurable_add (.singleton x))
               (hZ₁.prodMk hZ₃)
           exact this.comp measurable_fst measurable_add
         · rw [cond_apply, J.measure_inter_preimage_eq_mul _ _ (.singleton x) (.singleton y)]
-          simp [h1, h2]
+          · simp only [ne_eq, measure_ne_top, not_false_eq_true, measureReal_eq_zero_iff] at h1 h2
+            simp [h1, h2]
           · exact hZ₁.add hZ₃ (.singleton _)
         · exact hZ₁.add hZ₃ (.singleton _)
         · exact hZ₂.add hZ₄ (.singleton _)
         · finiteness
       have B : IdentDistrib Z₂ Z₂ (ℙ[|(Z₁ + Z₃) ⁻¹' {x} ∩ (Z₂ + Z₄) ⁻¹' {y}])
           (ℙ[|(Z₂ + Z₄) ⁻¹' {y}]) := by
         rw [Set.inter_comm, ← cond_cond_eq_cond_inter']
-        have : IsProbabilityMeasure (ℙ[|(Z₂ + Z₄) ⁻¹' {y}]) := cond_isProbabilityMeasure h2
+        have : IsProbabilityMeasure (ℙ[|(Z₂ + Z₄) ⁻¹' {y}]) := cond_isProbabilityMeasure_of_real h2
         apply (IndepFun.identDistrib_cond _ (.singleton _) hZ₂ (hZ₁.add hZ₃) _).symm
         · have : IndepFun (⟨Z₂, Z₄⟩) (⟨Z₁, Z₃⟩) (ℙ[|(⟨Z₂, Z₄⟩) ⁻¹' {p | p.1 + p.2 = y}]) :=
             I.symm.cond_left (measurable_add (.singleton y))
               (hZ₂.prodMk hZ₄)
           exact this.comp measurable_fst measurable_add
         · rw [Pi.add_def, cond_apply (hZ₂.add hZ₄ (.singleton y)), ← Pi.add_def, ← Pi.add_def,
             J.symm.measure_inter_preimage_eq_mul _ _ (.singleton _) (.singleton _)]
+          simp only [ne_eq, measure_ne_top, not_false_eq_true, measureReal_eq_zero_iff] at h1 h2
           simp [h1, h2]
         · exact hZ₂.add hZ₄ (.singleton _)
         · exact hZ₁.add hZ₃ (.singleton _)

PFR/Kullback.lean

@@ -115,7 +115,7 @@ lemma KLDiv_eq_zero_iff_identDistrib [Fintype G] [MeasurableSingletonClass G]
 and ${\bf P}(X=x) = \sum_{s\in S} w_s {\bf P}(X_s=x)$, ${\bf P}(Y=x) =
   \sum_{s\in S} w_s {\bf P}(Y_s=x)$ for all $x$, then
 $$D_{KL}(X\Vert Y) \le \sum_{s\in S} w_s D_{KL}(X_s\Vert Y_s).$$ -/
-lemma KLDiv_of_convex [Fintype G] [IsFiniteMeasure μ''']
+lemma KLDiv_of_convex [Fintype G]
     {ι : Type*} {S : Finset ι} {w : ι → ℝ} (hw : ∀ s ∈ S, 0 ≤ w s)
     (X' : ι → Ω'' → G) (Y' : ι → Ω''' → G)
     (hconvex : ∀ x, (μ.map X).real {x} = ∑ s ∈ S, w s * (μ''.map (X' s)).real {x})
@@ -244,6 +244,16 @@ lemma ProbabilityTheory.IndepFun.map_add_singleton_eq_sum
   simp
   abel
 
+lemma ProbabilityTheory.IndepFun.real_map_add_eq_sum [IsFiniteMeasure μ]
+    [Fintype G] [AddCommGroup G] [DiscreteMeasurableSpace G]
+    {X Z : Ω → G} (h_indep : IndepFun X Z μ)
+    (hX : Measurable X) (hZ : Measurable Z) (S : Set G) :
+    (μ.map (X + Z)).real S = ∑ s, (μ.map Z).real {s} * (μ.map X).real ({-s} + S) := by
+  rw [measureReal_def, h_indep.map_add_eq_sum hX hZ, ENNReal.toReal_sum (by finiteness)]
+  congr with s
+  simp only [singleton_add, image_add_left, neg_neg, ENNReal.toReal_mul]
+  rfl
+
 lemma ProbabilityTheory.IndepFun.real_map_add_singleton_eq_sum
     [Fintype G] [AddCommGroup G] [DiscreteMeasurableSpace G] [IsFiniteMeasure μ]
     {X Z : Ω → G} (h_indep : IndepFun X Z μ)

PFR/Mathlib/Probability/UniformOn.lean

@@ -1,4 +1,5 @@
 import Mathlib.Probability.UniformOn
+import Mathlib.MeasureTheory.Measure.Real
 
 open Function MeasureTheory Measure
 
@@ -13,9 +14,17 @@ lemma uniformOn_apply_singleton_of_mem (hx : x ∈ s) (hs : s.Finite) :
     this, Measure.count_singleton', smul_eq_mul, mul_one, one_div, inv_inj]
   rw [Measure.count_apply_finite _ hs, Nat.card_eq_card_finite_toFinset hs]
 
+lemma real_uniformOn_apply_singleton_of_mem (hx : x ∈ s) (hs : s.Finite) :
+    (uniformOn s).real {x} = 1 / Nat.card s := by
+  simp [measureReal_def, uniformOn_apply_singleton_of_mem hx hs]
+
 lemma uniformOn_apply_singleton_of_not_mem (hx : x ∉ s) : uniformOn s {x} = 0 := by
   simp [uniformOn, cond, hx]
 
+lemma real_uniformOn_apply_singleton_of_not_mem (hx : x ∉ s) :
+    (uniformOn s).real {x} = 0 := by
+  simp [measureReal_def, uniformOn_apply_singleton_of_not_mem hx]
+
 theorem uniformOn_apply_eq_zero (hst : s ∩ t = ∅) : uniformOn s t = 0 := by
   rcases Set.finite_or_infinite s with hs | hs
   · exact (uniformOn_eq_zero_iff hs).mpr hst