Bump mathlib to v4.18.0

Author: YaelDillies

PFR/Endgame.lean

@@ -120,7 +120,7 @@ lemma I₃_eq [IsProbabilityMeasure (ℙ : Measure Ω)] : I[V : W | S] = I₂ :=
   have hS : Measurable S := by fun_prop
   rw [condMutualInfo_eq hV hW hS, condMutualInfo_eq hU hW hS, chain_rule'' ℙ hU hS,
     chain_rule'' ℙ hV hS, chain_rule'' ℙ hW hS, chain_rule'' ℙ _ hS, chain_rule'' ℙ _ hS,
-    IdentDistrib.entropy_eq hUVS, IdentDistrib.entropy_eq hUVWS]
+    hUVS.entropy_congr, hUVWS.entropy_congr]
   · exact Measurable.prod hU hW
   · exact Measurable.prod hV hW
 
@@ -153,7 +153,7 @@ local notation3:max "c[" A " | " B " # " C " | " D "]" =>
 
 include h_indep h₁ h₂ in
 lemma hU [IsProbabilityMeasure (ℙ : Measure Ω)] : H[U] = H[X₁' + X₂'] :=
-  IdentDistrib.entropy_eq (h₁.add h₂
+  IdentDistrib.entropy_congr (h₁.add h₂
     (h_indep.indepFun (show (0 : Fin 4) ≠ 1 by norm_cast))
      (h_indep.indepFun (show (2 : Fin 4) ≠ 3 by norm_cast)))
 
@@ -165,7 +165,7 @@ lemma independenceCondition1 :
 
 include h₁ h₂ h_indep in
 lemma hV [IsProbabilityMeasure (ℙ : Measure Ω)] : H[V] = H[X₁ + X₂'] :=
-  IdentDistrib.entropy_eq (h₁.symm.add h₂
+  IdentDistrib.entropy_congr (h₁.symm.add h₂
     (h_indep.indepFun (show (2 : Fin 4) ≠ 1 by norm_cast))
     (h_indep.indepFun (show (0 : Fin 4) ≠ 3 by norm_cast)))
 
@@ -240,9 +240,8 @@ lemma sum_dist_diff_le [IsProbabilityMeasure (ℙ : Measure Ω)] [Module (ZMod 2
       (independenceCondition3 hX₁ hX₂ hX₁' hX₂' h_indep)
 
     have aux1 : H[S] + H[V] - H[X₁'] - H[X₁ + X₂'] = H[S ; ℙ] - H[X₁ ; ℙ] := by
-      rw [hV X₁ X₂ X₁' X₂' h₁ h₂ h_indep, h₁.entropy_eq]; ring
-    rw [← ProbabilityTheory.IdentDistrib.rdist_eq (IdentDistrib.refl p.hmeas1.aemeasurable) h₁,
-      V_add_eq, aux1] at aux2
+      rw [hV X₁ X₂ X₁' X₂' h₁ h₂ h_indep, h₁.entropy_congr]; ring
+    rw [← h₁.rdist_congr_right p.hmeas1.aemeasurable, V_add_eq, aux1] at aux2
     linarith [aux2]
 
   have ineq4 : d[X₀₂ # V | S] - d[X₀₂ # X₂] ≤ (H[S ; ℙ] - H[X₂ ; ℙ])/2 := by
@@ -341,7 +340,7 @@ lemma cond_c_eq_integral [IsProbabilityMeasure (ℙ : Measure Ω')]
   rw [← condRuzsaDist'_eq_integral _ hY hZ, ← condRuzsaDist'_eq_integral _ hY hZ, integral_const,
     integral_const]
   have : IsProbabilityMeasure (Measure.map Z ℙ) := isProbabilityMeasure_map hZ.aemeasurable
-  simp only [measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul]
+  simp only [measure_univ, ENNReal.toReal_one, smul_eq_mul, one_mul]
 
 variable {T₁ T₂ T₃ : Ω' → G} (hT : T₁+T₂+T₃ = 0)
 variable (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃)
@@ -391,7 +390,7 @@ lemma construct_good_prelim :
   have h2 : p.η * sum2 ≤ p.η * (d[p.X₀₁ # T₁] - d[p.X₀₁ # X₁] + I[T₁ : T₃] / 2) := by
     have : sum2 = d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁] := by
       simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ,
-        ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum2]
+        ENNReal.toReal_one, smul_eq_mul, one_mul, sub_left_inj, sum2]
       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]
@@ -402,7 +401,7 @@ lemma construct_good_prelim :
   have h3 : p.η * sum3 ≤ p.η * (d[p.X₀₂ # T₂] - d[p.X₀₂ # X₂] + I[T₂ : T₃] / 2) := by
     have : sum3 = d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂] := by
       simp only [integral_sub .of_finite .of_finite, integral_const, measure_univ,
-        ENNReal.one_toReal, smul_eq_mul, one_mul, sub_left_inj, sum3]
+        ENNReal.toReal_one, smul_eq_mul, one_mul, sub_left_inj, sum3]
       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]

PFR/EntropyPFR.lean

@@ -34,7 +34,7 @@ theorem tau_strictly_decreases (h_min : tau_minimizes p X₁ X₂) (hpη : p.η
     d[X₁ # X₂] = 0 := by
   let ⟨A, mA, μ, Y₁, Y₂, Y₁', Y₂', hμ, h_indep, hY₁, hY₂, hY₁', hY₂', h_id1, h_id2, h_id1', h_id2'⟩
     := independent_copies4_nondep hX₁ hX₂ hX₁ hX₂ ℙ ℙ ℙ ℙ
-  rw [← h_id1.rdist_eq h_id2]
+  rw [← h_id1.rdist_congr h_id2]
   let _ : MeasureSpace A := ⟨μ⟩
   have : IsProbabilityMeasure (ℙ : Measure A) := hμ
   rw [← h_id1.tau_minimizes p h_id2] at h_min

PFR/Examples.lean

@@ -167,7 +167,8 @@ variable (X : Ω → G) (hX : Measurable X) (Y : Ω → G) (hY : Measurable Y) (
 example (h : IndepFun X Y) : d[X # Y] = H[X-Y] - H[X]/2 - H[Y]/2 := h.rdist_eq hX hY
 
 /-- `d[X # Y]` depends only on the distribution of `X` and `Y`.-/
-example (h1 : IdentDistrib X X') (h2 : IdentDistrib Y Y') : d[X # Y] = d[X' # Y'] := h1.rdist_eq h2
+example (h1 : IdentDistrib X X') (h2 : IdentDistrib Y Y') : d[X # Y] = d[X' # Y'] :=
+  h1.rdist_congr h2
 
 /-- The Ruzsa triangle inequality. -/
 example : d[X # Z] ≤ d[X # Y] + d[Y # Z] := rdist_triangle hX hY hZ

PFR/Fibring.lean

@@ -67,7 +67,7 @@ lemma rdist_le_sum_fibre {Z_1 : Ω → H} {Z_2 : Ω' → H}
   have hφ : Measurable (fun x ↦ (x, π x)) := .of_discrete
   have hπ1 : IdentDistrib (⟨Z_1, π ∘ Z_1⟩) (⟨W_1, π ∘ W_1⟩) μ ν := hi1.symm.comp hφ
   have hπ2 : IdentDistrib (⟨Z_2, π ∘ Z_2⟩) (⟨W_2, π ∘ W_2⟩) μ' ν := hi2.symm.comp hφ
-  rw [← hi1.rdist_eq hi2, ← (hi1.comp hπ).rdist_eq (hi2.comp hπ),
+  rw [← hi1.rdist_congr hi2, ← (hi1.comp hπ).rdist_congr (hi2.comp hπ),
     rdist_of_indep_eq_sum_fibre π hi m1 m2,
     condRuzsaDist_of_copy h1 (hπ.comp h1) h2 (hπ.comp h2) m1 (hπ.comp m1) m2 (hπ.comp m2) hπ1 hπ2]
   exact le_add_of_nonneg_right (condMutualInfo_nonneg (by fun_prop) (by fun_prop))

PFR/FirstEstimate.lean

@@ -62,7 +62,7 @@ lemma rdist_add_rdist_add_condMutual_eq [Module (ZMod 2) G] :
   rw [h0, h1, h2, h3] at h
   have heq : d[X₂' # X₁'] = k := by
     rw [rdist_symm]
-    apply h₁.symm.rdist_eq h₂.symm
+    apply h₁.symm.rdist_congr h₂.symm
   rw [heq] at h
   convert h.symm using 1
   · congr 2 <;> abel
@@ -95,8 +95,8 @@ lemma diff_rdist_le_1 [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] :
     d[p.X₀₁ # X₁ + X₂'] - d[p.X₀₁ # X₁] ≤ k/2 + H[X₂]/4 - H[X₁]/4 := by
   have h : IndepFun X₁ X₂' := by simpa using h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide)
   convert condRuzsaDist_diff_le' ℙ p.hmeas1 hX₁ hX₂' h using 4
-  · exact (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂
-  · exact h₂.entropy_eq
+  · exact h₂.rdist_congr_right hX₁.aemeasurable
+  · exact h₂.entropy_congr
 
 include hX₁' hX₂ h_indep h₁ in
 /-- $$ d[X^0_2;X_2+\tilde X_1] - d[X^0_2; X_2] \leq \tfrac{1}{2} k + \tfrac{1}{4} \mathbb{H}[X_1] - \tfrac{1}{4} \mathbb{H}[X_2].$$ -/
@@ -105,8 +105,8 @@ lemma diff_rdist_le_2 [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
   have h : IndepFun X₂ X₁' := by simpa using h_indep.indepFun (show (1 : Fin 4) ≠ 3 by decide)
   convert condRuzsaDist_diff_le' ℙ p.hmeas2 hX₂ hX₁' h using 4
   · rw [rdist_symm]
-    exact (IdentDistrib.refl hX₂.aemeasurable).rdist_eq h₁
-  · exact h₁.entropy_eq
+    exact h₁.rdist_congr_right hX₂.aemeasurable
+  · exact h₁.entropy_congr
 
 include h_indep hX₁ hX₂' h₂ in
 /-- $$ d[X_1^0;X_1|X_1+\tilde X_2] - d[X_1^0;X_1] \leq
@@ -115,8 +115,8 @@ lemma diff_rdist_le_3 [IsProbabilityMeasure (ℙ : Measure Ω₀₁)] :
     d[p.X₀₁ # X₁ | X₁ + X₂'] - d[p.X₀₁ # X₁] ≤ k/2 + H[X₁]/4 - H[X₂]/4 := by
   have h : IndepFun X₁ X₂' := by simpa using h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide)
   convert condRuzsaDist_diff_le''' ℙ p.hmeas1 hX₁ hX₂' h using 3
-  · rw [(IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂]
-  · apply h₂.entropy_eq
+  · rw [h₂.rdist_congr_right hX₁.aemeasurable]
+  · apply h₂.entropy_congr
 
 include h_indep hX₂ hX₁' h₁
 /-- $$ d[X_2^0; X_2|X_2+\tilde X_1] - d[X_2^0; X_2] \leq
@@ -125,8 +125,8 @@ lemma diff_rdist_le_4 [IsProbabilityMeasure (ℙ : Measure Ω₀₂)] :
     d[p.X₀₂ # X₂ | X₂ + X₁'] - d[p.X₀₂ # X₂] ≤ k/2 + H[X₂]/4 - H[X₁]/4 := by
   have h : IndepFun X₂ X₁' := by simpa using h_indep.indepFun (show (1 : Fin 4) ≠ 3 by decide)
   convert condRuzsaDist_diff_le''' ℙ p.hmeas2 hX₂ hX₁' h using 3
-  · rw [rdist_symm, (IdentDistrib.refl hX₂.aemeasurable).rdist_eq h₁]
-  · apply h₁.entropy_eq
+  · rw [rdist_symm, h₁.rdist_congr_right hX₂.aemeasurable]
+  · apply h₁.entropy_congr
 
 include hX₁ hX₂ hX₁' hX₂' h₁ h₂ h_min in
 /-- We have $I_1 \leq 2 \eta k$ -/
@@ -188,7 +188,7 @@ lemma ent_ofsum_le
     have HX₂_eq : H[X₂] = H[X₂'] :=
       congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₂.map_eq
     have k_eq : k = H[X₁ - X₂'] - H[X₁] / 2 - H[X₂'] / 2 := by
-      have k_eq_aux : k = d[X₁ # X₂'] := (IdentDistrib.refl hX₁.aemeasurable).rdist_eq h₂
+      have k_eq_aux : k = d[X₁ # X₂'] := h₂.rdist_congr_right hX₁.aemeasurable
       rw [k_eq_aux]
       exact (h_indep.indepFun (show (0 : Fin 4) ≠ 2 by decide)).rdist_eq hX₁ hX₂'
     rw [k_eq, ← ZModModule.sub_eq_add, ← HX₂_eq]
@@ -197,10 +197,9 @@ lemma ent_ofsum_le
     have HX₁_eq : H[X₁] = H[X₁'] :=
       congr_arg (fun (μ : Measure G) ↦ measureEntropy (μ := μ)) h₁.map_eq
     have k_eq' : k = H[X₁' - X₂] - H[X₁'] / 2 - H[X₂] / 2 := by
-      have k_eq_aux : k = d[X₁' # X₂] :=
-        IdentDistrib.rdist_eq h₁ (IdentDistrib.refl hX₂.aemeasurable)
+      have k_eq_aux : k = d[X₁' # X₂] := h₁.rdist_congr_left hX₂.aemeasurable
       rw [k_eq_aux]
-      exact IndepFun.rdist_eq (h_indep.indepFun (show (3 : Fin 4) ≠ 1 by decide)) hX₁' hX₂
+      exact (h_indep.indepFun (show (3 : Fin 4) ≠ 1 by decide)).rdist_eq hX₁' hX₂
     rw [add_comm X₂ X₁', k_eq', ← ZModModule.sub_eq_add, ← HX₁_eq]
     ring
   calc H[X₁ + X₂ + X₁' + X₂']

PFR/ForMathlib/CompactProb.lean

@@ -67,7 +67,7 @@ noncomputable def probabilityMeasureEquivStdSimplex [Fintype X] [MeasurableSingl
       measure_univ, smul_eq_mul, mul_one]
     rw [← ENNReal.toReal_eq_toReal (by simp [ENNReal.sum_eq_top]) ENNReal.one_ne_top,
         ENNReal.toReal_sum (by simp)]
-    simp_rw [ENNReal.toReal_ofReal (p.2.1 _), p.2.2, ENNReal.one_toReal]
+    simp_rw [ENNReal.toReal_ofReal (p.2.1 _), p.2.2, ENNReal.toReal_one]
   left_inv := by
     intro μ
     ext s _hs

PFR/ForMathlib/Entropy/Basic.lean

@@ -55,7 +55,7 @@ lemma entropy_def (X : Ω → S) (μ : Measure Ω) : entropy X μ = Hm[μ.map X]
 lemma entropy_eq_kernel_entropy (X : Ω → S) (μ : Measure Ω) :
     H[X ; μ] = Hk[Kernel.const Unit (μ.map X), Measure.dirac ()] := by
   simp only [Kernel.entropy, Kernel.const_apply, integral_const, MeasurableSpace.measurableSet_top,
-    Measure.dirac_apply', Set.mem_univ, Set.indicator_of_mem, Pi.one_apply, ENNReal.one_toReal,
+    Measure.dirac_apply', Set.mem_univ, Set.indicator_of_mem, Pi.one_apply, ENNReal.toReal_one,
     smul_eq_mul, one_mul]
   rfl
 
@@ -71,7 +71,7 @@ lemma entropy_congr {X X' : Ω → S} (h : X =ᵐ[μ] X') : H[X ; μ] = H[X' ; 
 lemma entropy_nonneg (X : Ω → S) (μ : Measure Ω) : 0 ≤ entropy X μ := measureEntropy_nonneg _
 
 /-- Two variables that have the same distribution, have the same entropy. -/
-lemma IdentDistrib.entropy_eq {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'} {X' : Ω' → S}
+lemma IdentDistrib.entropy_congr {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Measure Ω'} {X' : Ω' → S}
     (h : IdentDistrib X X' μ μ') : H[X ; μ] = H[X' ; μ'] := by
   simp [entropy_def, h.map_eq]
 
@@ -113,7 +113,7 @@ lemma entropy_eq_sum_finset {μ : Measure Ω} [IsZeroOrProbabilityMeasure μ]
   convert tsum_eq_sum ?_
   intro s hs
   convert negMulLog_zero
-  convert ENNReal.zero_toReal
+  convert ENNReal.toReal_zero
   convert measure_mono_null ?_ hA
   simp [hs]
 
@@ -190,7 +190,7 @@ lemma IsUniform.entropy_eq [DiscreteMeasurableSpace S] {H : Finset S} {X : Ω 
   rw [Measure.map_apply hX' (by measurability)]
   exact hX.measure_preimage_compl
 
-/-- Variant of `IsUniform.entropy_eq` where `H` is a finite `Set` rather than `Finset`. -/
+/-- Variant of `IsUniform.entropy_congr` where `H` is a finite `Set` rather than `Finset`. -/
 lemma IsUniform.entropy_eq' [DiscreteMeasurableSpace S]
     {H : Set S} (hH : H.Finite) {X : Ω → S} {μ : Measure Ω} [IsProbabilityMeasure μ]
     (hX : IsUniform H X μ) (hX' : Measurable X) : H[X ; μ] = log (Nat.card H) := by
@@ -271,7 +271,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.one_toReal]
+      Finset.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
@@ -602,7 +602,7 @@ lemma IdentDistrib.condEntropy_eq {Ω' : Type*} [MeasurableSpace Ω'] {X : Ω 
     [FiniteRange Y'] :
     H[X | Y ; μ] = H[X' | Y' ; μ'] := by
   have : IdentDistrib Y Y' μ μ' := h.comp measurable_snd
-  rw [chain_rule'' _ hX hY, chain_rule'' _ hX' hY', h.entropy_eq, this.entropy_eq]
+  rw [chain_rule'' _ hX hY, chain_rule'' _ hX' hY', h.entropy_congr, this.entropy_congr]
 
 variable [Countable U] [MeasurableSingletonClass U]
 
@@ -704,7 +704,7 @@ lemma IdentDistrib.mutualInfo_eq {Ω' : Type*} [MeasurableSpace Ω'] {μ' : Meas
       I[X : Y ; μ] = I[X' : Y' ; μ'] := by
   have hX : IdentDistrib X X' μ μ' := hXY.comp measurable_fst
   have hY : IdentDistrib Y Y' μ μ' := hXY.comp measurable_snd
-  simp_rw [mutualInfo_def,hX.entropy_eq,hY.entropy_eq,hXY.entropy_eq]
+  simp_rw [mutualInfo_def,hX.entropy_congr,hY.entropy_congr,hXY.entropy_congr]
 
 /-- The conditional mutual information `I[X : Y| Z]` is the mutual information of `X| Z=z` and
 `Y| Z=z`, integrated over `z`. -/

PFR/ForMathlib/Entropy/Kernel/Basic.lean

@@ -358,7 +358,7 @@ lemma entropy_prodMkRight [Countable S] [MeasurableSingletonClass S] [Countable
     Hk[prodMkRight S η, μ ⊗ₘ κ] = Hk[η, μ] := by
   simp_rw [entropy, prodMkRight_apply]
   rw [Measure.integral_compProd]
-  · simp only [MeasureTheory.integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul]
+  · simp only [MeasureTheory.integral_const, measure_univ, ENNReal.toReal_one, smul_eq_mul, one_mul]
   · have := finiteSupport_of_compProd hκ (μ := μ)
     exact integrable_of_finiteSupport (μ ⊗ₘ κ)
 

PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean

@@ -105,7 +105,7 @@ lemma rdist_symm {κ : Kernel T G} {η : Kernel T' G} [IsFiniteKernel κ] [IsFin
     [FiniteSupport μ] [FiniteSupport ν] :
     dk[κ ; μ # const T' (Measure.dirac 0) ; ν] = Hk[κ, μ] / 2 := by
   rw [rdist_eq']
-  simp only [entropy_const, measure_univ, ENNReal.one_toReal, measureEntropy_dirac, mul_zero,
+  simp only [entropy_const, measure_univ, ENNReal.toReal_one, measureEntropy_dirac, mul_zero,
     zero_div, sub_zero]
   rw [sub_eq_iff_eq_add]
   ring_nf
@@ -340,7 +340,7 @@ lemma rdist_triangle_aux2 (η : Kernel T' G) (ξ : Kernel T'' G)
     simp
   simp_rw [this, ← Finset.sum_mul, Finset.sum_toReal_measure_singleton,
     measure_of_measure_compl_eq_zero (measure_compl_support μ),
-    measure_univ, ENNReal.one_toReal, one_mul, ← mul_assoc, mul_comm _ (μ'' {z}).toReal, mul_assoc,
+    measure_univ, ENNReal.toReal_one, one_mul, ← mul_assoc, mul_comm _ (μ'' {z}).toReal, mul_assoc,
     ← Finset.mul_sum]
   congr with y
   congr 2 with s _hs