Bump mathlib (#239)

Author: YaelDillies

PFR.lean

@@ -23,9 +23,6 @@ import PFR.ForMathlib.FiniteRange.ConditionalProbability
 import PFR.ForMathlib.FiniteRange.Defs
 import PFR.ForMathlib.FiniteRange.IdentDistrib
 import PFR.ForMathlib.FourVariables
-import PFR.ForMathlib.MeasureReal.Defs
-import PFR.ForMathlib.MeasureReal.Indep
-import PFR.ForMathlib.MeasureReal.UniformOn
 import PFR.ForMathlib.Pair
 import PFR.ForMathlib.ProbabilityMeasureProdCont
 import PFR.ForMathlib.ThreeVariables
@@ -42,9 +39,17 @@ import PFR.Mathlib.LinearAlgebra.Basis.VectorSpace
 import PFR.Mathlib.LinearAlgebra.Dimension.Finrank
 import PFR.Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
 import PFR.Mathlib.MeasureTheory.Constructions.Pi
-import PFR.Mathlib.MeasureTheory.Integral.Lebesgue
-import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
+import PFR.Mathlib.MeasureTheory.Integral.Bochner.Basic
+import PFR.Mathlib.MeasureTheory.Integral.Bochner.Set
+import PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Basic
+import PFR.Mathlib.MeasureTheory.Integral.Lebesgue.Countable
+import PFR.Mathlib.MeasureTheory.Measure.Dirac
+import PFR.Mathlib.MeasureTheory.Measure.MeasureSpace
+import PFR.Mathlib.MeasureTheory.Measure.MeasureSpaceDef
 import PFR.Mathlib.MeasureTheory.Measure.Prod
+import PFR.Mathlib.MeasureTheory.Measure.Real
+import PFR.Mathlib.MeasureTheory.Measure.Typeclasses.Probability
+import PFR.Mathlib.Probability.ConditionalProbability
 import PFR.Mathlib.Probability.IdentDistrib
 import PFR.Mathlib.Probability.Independence.Basic
 import PFR.Mathlib.Probability.Independence.Kernel

PFR/BoundingMutual.lean

@@ -26,7 +26,7 @@ $$ {\mathcal I} := \bbI[ \bigl(\sum_{i=1}^m X_{i,j}\bigr)_{j =1}^{m}
  Then ${\mathcal I} \leq 4 m^2 \eta k.$
 -/
 lemma mutual_information_le {G Ωₒ : Type u} [MeasureableFinGroup G] [MeasureSpace Ωₒ]
-  (p : multiRefPackage G Ωₒ) (Ω : Type u) [hΩ: MeasureSpace Ω] (X : ∀ i, Ω → G)
+  (p : multiRefPackage G Ωₒ) (Ω : Type u) [hΩ : MeasureSpace Ω] (X : ∀ i, Ω → G)
   (h_indep : iIndepFun X)
   (h_min : multiTauMinimizes p (fun _ ↦ Ω) (fun _ ↦ hΩ) X) (Ω' : Type*) [MeasureSpace Ω']
   (X' : Fin p.m × Fin p.m → Ω' → G) (h_indep': iIndepFun X')

PFR/Endgame.lean

@@ -394,6 +394,7 @@ lemma construct_good_prelim :
       simp_rw [condRuzsaDist'_eq_sum hT₁ hT₃,
         integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset,
         Measure.map_apply hT₃ (.singleton _), smul_eq_mul]
+      rfl
 
     gcongr
     linarith [condRuzsaDist_le' ℙ ℙ p.hmeas1 hT₁ hT₃]
@@ -405,6 +406,7 @@ lemma construct_good_prelim :
       simp_rw [condRuzsaDist'_eq_sum hT₂ hT₃,
         integral_eq_setIntegral (FiniteRange.null_of_compl _ T₃), integral_finset _ _ IntegrableOn.finset,
         Measure.map_apply hT₃ (.singleton _), smul_eq_mul]
+      rfl
     gcongr
     linarith [condRuzsaDist_le' ℙ ℙ p.hmeas2 hT₂ hT₃]
 

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/ForMathlib/Entropy/Basic.lean

@@ -1,6 +1,8 @@
 import PFR.ForMathlib.ConditionalIndependence
 import PFR.ForMathlib.Entropy.Kernel.MutualInfo
 import PFR.ForMathlib.Uniform
+import PFR.Mathlib.MeasureTheory.Integral.Bochner.Basic
+import PFR.Mathlib.Probability.ConditionalProbability
 
 /-!
 # Entropy and conditional entropy
@@ -99,7 +101,7 @@ lemma entropy_le_log_card_of_mem_finite [DiscreteMeasurableSpace S]
 
 /-- `H[X] = ∑ₛ P[X=s] log 1 / P[X=s]`. -/
 lemma entropy_eq_sum (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] :
-    entropy X μ = ∑' x, negMulLog (μ.map X {x}).toReal := by
+    entropy X μ = ∑' x, negMulLog ((μ.map X).real {x}) := by
   rw [entropy_def, measureEntropy_of_isProbabilityMeasure]
 
 lemma entropy_eq_sum' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] :
@@ -108,11 +110,12 @@ lemma entropy_eq_sum' (μ : Measure Ω) [IsZeroOrProbabilityMeasure μ] :
 
 lemma entropy_eq_sum_finset {μ : Measure Ω} [IsZeroOrProbabilityMeasure μ]
     {A : Finset S} (hA : (μ.map X) Aᶜ = 0):
-    entropy X μ = ∑ x ∈ A, negMulLog (μ.map X {x}).toReal := by
+    entropy X μ = ∑ x ∈ A, negMulLog ((μ.map X).real {x}) := by
   rw [entropy_eq_sum]
   convert tsum_eq_sum ?_
   intro s hs
   convert negMulLog_zero
+  rw [Measure.real]
   convert ENNReal.toReal_zero
   convert measure_mono_null ?_ hA
   simp [hs]
@@ -124,7 +127,7 @@ lemma entropy_eq_sum_finset' {μ : Measure Ω} [IsZeroOrProbabilityMeasure μ]
 
 lemma entropy_eq_sum_finiteRange [MeasurableSingletonClass S]
     (hX : Measurable X) {μ : Measure Ω} [IsZeroOrProbabilityMeasure μ] [FiniteRange X]:
-    entropy X μ = ∑ x ∈ FiniteRange.toFinset X, negMulLog (μ.map X {x}).toReal :=
+    entropy X μ = ∑ x ∈ FiniteRange.toFinset X, negMulLog ((μ.map X).real {x}) :=
   entropy_eq_sum_finset (A := FiniteRange.toFinset X) (full_measure_of_finiteRange hX)
 
 lemma entropy_eq_sum_finiteRange' [MeasurableSingletonClass S] (hX : Measurable X) {μ : Measure Ω}
@@ -134,15 +137,15 @@ lemma entropy_eq_sum_finiteRange' [MeasurableSingletonClass S] (hX : Measurable
 
 /-- `H[X | Y=y] = ∑_s P[X=s | Y=y] log 1/(P[X=s | Y=y])`. -/
 lemma entropy_cond_eq_sum (μ : Measure Ω) (y : T) :
-    H[X | Y ← y ; μ] = ∑' x, negMulLog ((μ[|Y ← y]).map X {x}).toReal := by
+    H[X | Y ← y ; μ] = ∑' x, negMulLog (((μ[|Y ← y]).map X).real {x}) := by
   by_cases hy : μ (Y ⁻¹' {y}) = 0
   · rw [entropy_def, cond_eq_zero_of_meas_eq_zero hy]
     simp
   · rw [entropy_eq_sum]
 
 lemma entropy_cond_eq_sum_finiteRange [MeasurableSingletonClass S]
     (hX : Measurable X) (μ : Measure Ω) (y : T) [FiniteRange X]:
-    H[X | Y ← y ; μ] = ∑ x ∈ FiniteRange.toFinset X, negMulLog ((μ[|Y ← y]).map X {x}).toReal := by
+    H[X | Y ← y ; μ] = ∑ x ∈ FiniteRange.toFinset X, negMulLog (((μ[|Y ← y]).map X).real {x}) := by
   by_cases hy : μ (Y ⁻¹' {y}) = 0
   · rw [entropy_def, cond_eq_zero_of_meas_eq_zero hy]
     simp
@@ -212,10 +215,12 @@ lemma entropy_eq_log_card {X : Ω → S} [Fintype S] [MeasurableSingletonClass S
   simp
 
 /-- If `X` is an `S`-valued random variable, then there exists `s ∈ S` such that
-`P[X = s] ≥ \exp(- H[X])`. TODO: remove the probability measure hypothesis, which is unncessary here. -/
+`P[X = s] ≥ \exp(- H[X])`.
+
+TODO: remove the probability measure hypothesis, which is unnecessary here. -/
 lemma prob_ge_exp_neg_entropy [MeasurableSingletonClass S] (X : Ω → S) (μ : Measure Ω)
     [IsProbabilityMeasure μ] (hX : Measurable X) [hX': FiniteRange X] :
-    ∃ s : S, μ.map X {s} ≥ (μ Set.univ) * (rexp (- H[X ; μ])).toNNReal := by
+    ∃ s : S, μ Set.univ * (rexp (- H[X ; μ])).toNNReal ≤ μ.map X {s} := by
   have : Nonempty Ω := μ.nonempty_of_neZero
   have : Nonempty S := Nonempty.map X (by infer_instance)
   let μS := μ.map X
@@ -237,7 +242,7 @@ lemma prob_ge_exp_neg_entropy [MeasurableSingletonClass S] (X : Ω → S) (μ :
   rcases Finset.eq_empty_or_nonempty S_nonzero with h_empty | h_nonempty
   · have h_norm_zero : μ Set.univ = 0 := by
       have h : ∀ s ∈ A, μs s ≠ 0 → μs s ≠ 0 := fun _ _ h ↦ h
-      rw [← h_norm, rw_norm, ← Finset.sum_measure_singleton, ← Finset.sum_filter_of_ne h,
+      rw [← h_norm, rw_norm, ← sum_measure_singleton, ← Finset.sum_filter_of_ne h,
         show Finset.filter _ _ = S_nonzero from rfl, h_empty, show Finset.sum ∅ μs = 0 from rfl]
     use Classical.arbitrary (α := S)
     rw [h_norm_zero, zero_mul]
@@ -256,7 +261,7 @@ lemma prob_ge_exp_neg_entropy [MeasurableSingletonClass S] (X : Ω → S) (μ :
     rw [h_norm, Measure.measure_univ_pos]
     exact NeZero.ne μ
   have h_norm_finite : norm < ∞ := by
-    rw [rw_norm, ← Finset.sum_measure_singleton]
+    rw [rw_norm, ← sum_measure_singleton]
     exact ENNReal.sum_lt_top.2 (fun s _ ↦ Ne.lt_top (h_finite s))
   have h_invinvnorm_finite : norm⁻¹⁻¹ ≠ ∞ := by
     rw [inv_inv]
@@ -271,7 +276,7 @@ lemma prob_ge_exp_neg_entropy [MeasurableSingletonClass S] (X : Ω → S) (μ :
     ENNReal.mul_inv_cancel (ne_zero_of_lt h_norm_pos) (LT.lt.ne_top h_norm_finite)
   have h_pdf1 : (∑ s ∈ A, pdf s) = 1 := by
     rw [← ENNReal.toReal_sum (fun s _ ↦ h_pdf_finite s), ← Finset.mul_sum,
-      Finset.sum_measure_singleton, mul_comm, h_norm_cancel, ENNReal.toReal_one]
+      sum_measure_singleton, mul_comm, h_norm_cancel, ENNReal.toReal_one]
 
   let ⟨s_max, hs, h_min⟩ := Finset.exists_min_image S_nonzero neg_log_pdf h_nonempty
   have h_pdf_s_max_pos : 0 < pdf s_max := by
@@ -296,7 +301,7 @@ lemma prob_ge_exp_neg_entropy [MeasurableSingletonClass S] (X : Ω → S) (μ :
     congr with s
     simp only [negMulLog, neg_mul, ENNReal.toReal_mul, neg_inj, g_rhs, pdf, pdf_nn]
     simp at h_norm
-    simp [h_norm, μs, μS]
+    simp [h_norm, μs, μS, Measure.real]
   have h_lhs : ∀ s, μs s = 0 → g_lhs s = 0 := by {intros _ h; simp [g_lhs, pdf, pdf_nn, h]}
   have h_rhs : ∀ s, μs s = 0 → g_rhs s = 0 := by {intros _ h; simp [g_rhs, pdf, pdf_nn, h]}
   rw [← Finset.sum_filter_of_ne (fun s _ ↦ (h_lhs s).mt),
@@ -314,7 +319,7 @@ lemma prob_ge_exp_neg_entropy' [MeasurableSingletonClass S]
     ∃ s : S, rexp (- H[X ; μ]) ≤ μ.real (X ⁻¹' {s}) := by
   obtain ⟨s, hs⟩ := prob_ge_exp_neg_entropy X μ hX
   use s
-  rwa [IsProbabilityMeasure.measure_univ, one_mul, ge_iff_le,
+  rwa [IsProbabilityMeasure.measure_univ, one_mul,
     (show ENNReal.ofNNReal _ = ENNReal.ofReal _ from rfl),
     ENNReal.ofReal_le_iff_le_toReal (measure_ne_top _ _), ← Measure.real,
     map_measureReal_apply hX (MeasurableSet.singleton s)] at hs
@@ -327,7 +332,7 @@ lemma const_of_nonpos_entropy [MeasurableSingletonClass S]
     rcases prob_ge_exp_neg_entropy' (μ := μ) X hX with ⟨ s, hs ⟩
     use s
     apply LE.le.antisymm
-    · rw [← IsProbabilityMeasure.measureReal_univ (μ := μ)]
+    · rw [← measureReal_univ_eq_one (μ := μ)]
       exact measureReal_mono (subset_univ _) (by finiteness)
     refine le_trans ?_ hs
     simp [hent]
@@ -381,10 +386,10 @@ section
 variable [MeasurableSingletonClass T]
 
 lemma condEntropy_eq_zero (hY : Measurable Y) (μ : Measure Ω) [IsFiniteMeasure μ] (t : T)
-    (ht : (μ.map Y {t}).toReal = 0) : H[X | Y ← t ; μ] = 0 := by
+    (ht : (μ.map Y).real {t} = 0) : H[X | Y ← t ; μ] = 0 := by
   convert entropy_zero_measure X
   apply cond_eq_zero_of_meas_eq_zero
-  rw [Measure.map_apply hY (MeasurableSet.singleton t)] at ht
+  rw [map_measureReal_apply hY (.singleton t)] at ht
   rw [← measureReal_eq_zero_iff]
   exact ht
 
@@ -443,39 +448,39 @@ lemma condEntropy_le_log_card [MeasurableSingletonClass S] [Fintype S]
 /-- `H[X|Y] = ∑_y P[Y=y] H[X|Y=y]`.-/
 lemma condEntropy_eq_sum [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω)
     [IsFiniteMeasure μ] (hY : Measurable Y) [FiniteRange Y]:
-    H[X | Y ; μ] = ∑ y ∈ FiniteRange.toFinset Y, (μ.map Y {y}).toReal * H[X | Y ← y ; μ] := by
-  rw [condEntropy_def, integral_eq_setIntegral (full_measure_of_finiteRange hY), integral_finset _ _ IntegrableOn.finset]
+    H[X | Y ; μ] = ∑ y ∈ FiniteRange.toFinset Y, ((μ.map Y).real {y}) * H[X | Y ← y ; μ] := by
+  rw [condEntropy_def, integral_eq_setIntegral (full_measure_of_finiteRange hY),
+    integral_finset' _ .finset]
   simp_rw [smul_eq_mul]
 
 /-- `H[X|Y] = ∑_y P[Y=y] H[X|Y=y]`$.-/
 lemma condEntropy_eq_sum_fintype
     [MeasurableSingletonClass T] (X : Ω → S) (Y : Ω → T) (μ : Measure Ω)
     [IsFiniteMeasure μ] (hY : Measurable Y) [Fintype T] :
-    H[X | Y ; μ] = ∑ y, (μ (Y ⁻¹' {y})).toReal * H[X | Y ← y ; μ] := by
-  rw [condEntropy_def, integral_fintype _ .of_finite]
-  simp_rw [smul_eq_mul, Measure.map_apply hY (.singleton _)]
+    H[X | Y ; μ] = ∑ y, μ.real (Y ⁻¹' {y}) * H[X | Y ← y ; μ] := by
+  rw [condEntropy_def, integral_fintype' .of_finite]
+  simp_rw [smul_eq_mul, map_measureReal_apply hY (.singleton _)]
 
 variable [MeasurableSingletonClass T]
 
 lemma condEntropy_prod_eq_sum {X : Ω → S} {Y : Ω → T} {Z : Ω → T'} [MeasurableSpace T']
     [MeasurableSingletonClass T']
     (μ : Measure Ω) (hY : Measurable Y) (hZ : Measurable Z)
     [IsFiniteMeasure μ] [Fintype T] [Fintype T'] :
-    H[X | ⟨Y, Z⟩ ; μ]
-      = ∑ z, (μ (Z ⁻¹' {z})).toReal * H[X | Y ; μ[|Z ⁻¹' {z}]] := by
+    H[X | ⟨Y, Z⟩ ; μ] = ∑ z, μ.real (Z ⁻¹' {z}) * H[X | Y ; μ[|Z ⁻¹' {z}]] := by
   simp_rw [condEntropy_eq_sum_fintype _ _ _ (hY.prodMk hZ), condEntropy_eq_sum_fintype _ _ _ hY,
-    Fintype.sum_prod_type_right, Finset.mul_sum, ← mul_assoc, ← ENNReal.toReal_mul]
+    Fintype.sum_prod_type_right, Finset.mul_sum, ← mul_assoc]
   congr with y
   congr with x
   have A : (fun a ↦ (Y a, Z a)) ⁻¹' {(x, y)} = Z ⁻¹' {y} ∩ Y ⁻¹' {x} := by
     ext p; simp [and_comm]
   congr 2
-  · rw [cond_apply (hZ (.singleton y)), ← mul_assoc, A]
-    rcases eq_or_ne (μ (Z ⁻¹' {y})) 0 with hy|hy
-    · have : μ (Z ⁻¹' {y} ∩ Y ⁻¹' {x}) = 0 :=
-        le_antisymm ((measure_mono Set.inter_subset_left).trans hy.le) bot_le
+  · rw [cond_real_apply (hZ (.singleton y)), A]
+    obtain hy | hy := eq_or_ne (μ.real (Z ⁻¹' {y})) 0
+    · have : μ.real (Z ⁻¹' {y} ∩ Y ⁻¹' {x}) = 0 :=
+        measureReal_mono_null Set.inter_subset_left hy (by finiteness)
       simp [this, hy]
-    · rw [ENNReal.mul_inv_cancel hy (by finiteness), one_mul]
+    · rw [mul_inv_cancel_left₀ hy]
   · rw [A, cond_cond_eq_cond_inter (hZ (.singleton y)) (hY (.singleton x))]
 
 variable [MeasurableSingletonClass S]
@@ -485,7 +490,7 @@ lemma condEntropy_eq_sum_sum (hX : Measurable X) {Y : Ω → T} (hY : Measurable
     (μ : Measure Ω) [IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y] :
     H[X | Y ; μ]
       = ∑ y ∈ FiniteRange.toFinset Y, ∑ x ∈ FiniteRange.toFinset X,
-        (μ.map Y {y}).toReal * negMulLog ((μ[|Y ← y]).map X {x}).toReal := by
+        ((μ.map Y).real {y}) * negMulLog (((μ[|Y ← y]).map X).real {x}) := by
   rw [condEntropy_eq_sum _ _ _ hY]
   congr with y
   rw [entropy_cond_eq_sum_finiteRange hX, Finset.mul_sum]
@@ -494,19 +499,17 @@ omit [MeasurableSingletonClass S] in
 /-- `H[X|Y] = ∑_y ∑_x P[Y=y] P[X=x|Y=y] log ⧸(P[X=x|Y=y])`$.-/
 lemma condEntropy_eq_sum_sum_fintype {Y : Ω → T} (hY : Measurable Y)
     (μ : Measure Ω) [IsProbabilityMeasure μ] [Fintype S] [Fintype T] :
-    H[X | Y ; μ] = ∑ y, ∑ x,
-        (μ.map Y {y}).toReal * negMulLog ((μ[|Y ← y]).map X {x}).toReal := by
+    H[X | Y ; μ] = ∑ y, ∑ x, (μ.map Y).real {y} * negMulLog (((μ[|Y ← y]).map X).real {x}) := by
   rw [condEntropy_eq_sum_fintype _ _ _ hY]
   congr with y
-  rw [entropy_cond_eq_sum, tsum_fintype, Finset.mul_sum,
-    Measure.map_apply hY (measurableSet_singleton _)]
+  rw [entropy_cond_eq_sum, tsum_fintype, Finset.mul_sum, map_measureReal_apply hY (.singleton _)]
 
 /-- Same as previous lemma, but with a sum over a product space rather than a double sum. -/
 lemma condEntropy_eq_sum_prod (hX : Measurable X) {Y : Ω → T}
     (hY : Measurable Y)
     (μ : Measure Ω) [IsProbabilityMeasure μ] [FiniteRange X] [FiniteRange Y]:
     H[X | Y ; μ] = ∑ p ∈ (FiniteRange.toFinset X) ×ˢ (FiniteRange.toFinset Y),
-      (μ.map Y {p.2}).toReal * negMulLog ((μ[|Y ⁻¹' {p.2}]).map X {p.1}).toReal := by
+      (μ.map Y).real {p.2} * negMulLog (((μ[|Y ⁻¹' {p.2}]).map X).real {p.1}) := by
   rw [condEntropy_eq_sum_sum hX hY, Finset.sum_product_right]
 
 variable [Countable S]
@@ -865,7 +868,7 @@ end
 lemma condMutualInfo_eq_sum [MeasurableSingletonClass U] [IsFiniteMeasure μ]
     (hZ : Measurable Z) [FiniteRange Z] :
     I[X : Y | Z ; μ] = ∑ z ∈ FiniteRange.toFinset Z,
-      (μ (Z ⁻¹' {z})).toReal * I[X : Y ; (μ[|Z ← z])] := by
+      μ.real (Z ⁻¹' {z}) * I[X : Y ; (μ[|Z ← z])] := by
   rw [condMutualInfo_eq_integral_mutualInfo,
     integral_eq_setIntegral (FiniteRange.null_of_compl _ Z), integral_finset _ _ IntegrableOn.finset]
   congr 1 with z
@@ -875,7 +878,7 @@ lemma condMutualInfo_eq_sum [MeasurableSingletonClass U] [IsFiniteMeasure μ]
 /-- A variant of `condMutualInfo_eq_sum` when `Z` has finite codomain. -/
 lemma condMutualInfo_eq_sum' [MeasurableSingletonClass U] [IsFiniteMeasure μ]
     (hZ : Measurable Z) [Fintype U] :
-    I[X : Y | Z ; μ] = ∑ z, (μ (Z ⁻¹' {z})).toReal * I[X : Y ; (μ[|Z ← z])] := by
+    I[X : Y | Z ; μ] = ∑ z, μ.real (Z ⁻¹' {z}) * I[X : Y ; (μ[|Z ← z])] := by
   rw [condMutualInfo_eq_sum hZ]
   apply Finset.sum_subset
   · simp
@@ -961,12 +964,12 @@ lemma condEntropy_prod_eq_of_indepFun [Fintype T] [Fintype U] [IsZeroOrProbabili
   rcases eq_zero_or_isProbabilityMeasure μ with rfl | hμ
   · simp
   rw [condEntropy_prod_eq_sum _ hY hZ]
-  have : H[X | Y ; μ] = ∑ z, (μ (Z ⁻¹' {z})).toReal * H[X | Y ; μ] := by
-    rw [← Finset.sum_mul, sum_measure_preimage_singleton' μ hZ, one_mul]
+  have : H[X | Y ; μ] = ∑ z, (μ.real (Z ⁻¹' {z})) * H[X | Y ; μ] := by
+    rw [← Finset.sum_mul, sum_measureReal_preimage_singleton _ fun z _ ↦ hZ <| .singleton z]; simp
   rw [this]
   congr with w
   rcases eq_or_ne (μ (Z ⁻¹' {w})) 0 with hw|hw
-  · simp [hw]
+  · simp [hw, Measure.real]
   congr 1
   have : IsProbabilityMeasure (μ[|Z ⁻¹' {w}]) := cond_isProbabilityMeasure hw
   apply IdentDistrib.condEntropy_eq hX hY hX hY

PFR/ForMathlib/Entropy/Kernel/Basic.lean

@@ -1,6 +1,6 @@
 import Mathlib.MeasureTheory.Integral.Prod
 import PFR.ForMathlib.Entropy.Measure
-import PFR.Mathlib.MeasureTheory.Integral.SetIntegral
+import PFR.Mathlib.MeasureTheory.Integral.Bochner.Set
 import PFR.Mathlib.Probability.Kernel.Disintegration
 
 /-!
@@ -113,7 +113,7 @@ lemma entropy_le_log_card
   · simp
 
 lemma entropy_eq_integral_sum (κ : Kernel T S) [IsZeroOrMarkovKernel κ] (μ : Measure T) :
-    Hk[κ, μ] = μ[fun y ↦ ∑' x, negMulLog (κ y {x}).toReal] := by
+    Hk[κ, μ] = μ[fun y ↦ ∑' x, negMulLog ((κ y).real {x})] := by
   simp_rw [entropy, measureEntropy_of_isProbabilityMeasure]
 
 -- entropy_map_of_injective is a special case of this (see def of map)
@@ -246,14 +246,14 @@ lemma entropy_compProd_aux [MeasurableSingletonClass S] [MeasurableSingletonClas
       simp at hu ⊢
       exact hu hs
     exact MeasurableSet.compl (Finset.measurableSet _)
-  rw [measureEntropy_def_finite' hκη, measureEntropy_def_finite' (hB t ht),
+  rw [measureEntropy_eq_sum hκη, measureEntropy_eq_sum (hB t ht),
     integral_finset _ _ IntegrableOn.finset,
     ← Finset.sum_add_distrib, Finset.sum_product]
   apply Finset.sum_congr rfl
   intro s hs
   simp
   have hts : (t, s) ∈ A ×ˢ B := by simp [ht, hs]
-  rw [measureEntropy_def_finite' (hC (t, s) hts)]
+  rw [measureEntropy_eq_sum (hC (t, s) hts)]
   simp
   have : negMulLog ((κ t).real {s}) = ∑ u ∈ C, negMulLog ((κ t).real {s}) *
       ((comap η (Prod.mk t) measurable_prodMk_left) s).real {u} := by