update to v4.34

StatsMLlib/Analysis/FiniteSample.lean

@@ -6,7 +6,7 @@ Authors: Sho Sonoda, Kei Tsukamoto
 import Mathlib.Algebra.BigOperators.Field
 import Mathlib.Algebra.Order.BigOperators.Group.Finset
 import Mathlib.Data.Fintype.Order
-import Mathlib.Data.Real.Basic
+import Mathlib.Basic.Real.Basic
 import Mathlib.Tactic.FieldSimp
 import Mathlib.Tactic.GCongr
 import Mathlib.Tactic.Ring

StatsMLlib/Analysis/MetricEntropy/Basic.lean

@@ -1513,11 +1513,11 @@ redundant because `Real.log 0 = Real.log 1 = 0`. -/
 lemma metricEntropyOfNat_eq_log (n : ℕ) : metricEntropyOfNat n = Real.log n := by
   unfold metricEntropyOfNat
   by_cases h : n ≤ 1
-  · rw [if_pos h]
+  · rw [ite_eq_left h]
     interval_cases n
     · simp
     · simp
-  · rw [if_neg h]
+  · rw [ite_eq_right h]
 
 /-- On a totally bounded set at a positive radius, the metric entropy is the logarithm
 of the natural-valued covering number. -/

StatsMLlib/Analysis/NormedSpace/CoveringNumber/LipschitzBall.lean

@@ -159,7 +159,7 @@ lemma abs_signVector_le_one (n : ℕ) (β : Fin n → Bool) (i : ℕ) :
 
 lemma signVector_of_lt {n : ℕ} (β : Fin n → Bool) {i : ℕ} (h : i < n) :
     signVector n β i = if β ⟨i, h⟩ then 1 else -1 := by
-  rw [signVector, dif_pos h]
+  rw [signVector, dite_eq_left h]
 
 lemma signVector_congr {n : ℕ} {β β' : Fin n → Bool} {i : ℕ} (h : i < n)
     (hβ : β ⟨i, h⟩ = β' ⟨i, h⟩) : signVector n β i = signVector n β' i := by

StatsMLlib/LearningTheory/FunctionClass/HilbertPredictor.lean

@@ -110,7 +110,7 @@ private lemma rademacher_sum_norm_sq_average
               (σ k : ℝ) ^ 2 = |(σ k : ℝ)| ^ 2 := (sq_abs _).symm
               _ = 1 := by rw [abs_sigma]; norm_num
           _ = Fintype.card (Signs n) := by simp
-      simpa only [if_true] using hdiag
+      simpa only [ite_true] using hdiag
     · simpa [hkl] using rademacher_orthogonality n k l hkl
   calc
     (Fintype.card (Signs n) : ℝ)⁻¹ *

StatsMLlib/LearningTheory/Rademacher/Complexity.lean

@@ -130,8 +130,6 @@ lemma symmetrization_signed_sup_le_add
             apply abs_signed_sum_le_card_mul_bound hf'
         intro i
         convert abs_sub _ _
-        · rfl
-        · rfl
         · rw [←Finset.sum_sub_distrib]
           congr
           ext k

StatsMLlib/LearningTheory/Rademacher/Symmetrization.lean

@@ -74,19 +74,19 @@ theorem Signs.apply_abs' (σ : Signs n) (k : Fin n) : (|σ k| : ℝ) = 1 := by
 
 theorem measurable_snocEquiv:
   @Measurable (Ω × (Fin n → Ω)) (Fin (n + 1) → Ω) Prod.instMeasurableSpace MeasurableSpace.pi fun f ↦ Fin.snoc f.2 f.1 := by
-  apply measurable_pi_lambda
+  apply Measurable.of_eval
   intro i
   dsimp [Fin.snoc]
   if h : i.1 < n then
     have : (fun c : Ω × (Fin n → Ω) ↦ if h : ↑i < n then c.2 (i.castLT h) else c.1) = fun c ↦ c.2 (i.castLT h) := by
       ext c
-      rw [dif_pos h]
+      rw [dite_eq_left h]
     rw [this]
     exact Measurable.eval measurable_snd
   else
     have : (fun c : Ω × (Fin n → Ω)↦ if h : ↑i < n then c.2 (i.castLT h) else c.1) = fun c ↦ c.1 := by
       ext c
-      rw [dif_neg h]
+      rw [dite_eq_right h]
     rw [this]
     exact measurable_fst
 
@@ -114,10 +114,10 @@ lemma measure_equiv : (MeasureTheory.Measure.pi (fun _ ↦ μ) : Measure (Fin n.
     · rintro ⟨h₁, h₂⟩ i
       dsimp [Fin.snoc]
       if h : i.1 < n then
-        rw [dif_pos]
+        rw [dite_eq_left]
         exact h₂ (i.castLT h)
       else
-        rw [dif_neg h]
+        rw [dite_eq_right h]
         have : i = Fin.last n := Fin.eq_last_of_not_lt h
         rw [this]
         exact h₁
@@ -230,7 +230,7 @@ lemma inineq (ω : Ω × Ω) (ω': Fin n → Ω × Ω) {c : ι → ℝ}:
     _ = _ := by
       rw [sigma_eq]
       simp only [inv_pow, Int.reduceNeg,
-        mul_eq_mul_left_iff, inv_eq_zero, ne_eq, AddLeftCancelMonoid.add_eq_zero, one_ne_zero,
+        mul_eq_mul_left_iff, inv_eq_zero, ne_eq, Nat.add_eq_zero_iff, one_ne_zero,
         and_false, not_false_eq_true, pow_eq_zero_iff, OfNat.ofNat_ne_zero, or_false]
       rfl
 
@@ -653,9 +653,9 @@ lemma aux₃ [Countable ι] [Nonempty ι] (h𝓕 : ∀ I : ι, Measurable (f I 
           ext i
           dsimp [Fin.snoc]
           if h : i.1 < n then
-            rw [dif_pos h, dif_pos h]
+            rw [dite_eq_left h, dite_eq_left h]
           else
-            rw [dif_neg h, dif_neg h]
+            rw [dite_eq_right h, dite_eq_right h]
             congr
             simp only [not_lt] at h
             exact Fin.last_le_iff.mp h
@@ -696,10 +696,10 @@ lemma sup_abs_lemma [Nonempty ι] {V : (Z → ℝ) → ℝ} (hV₀: ∀ f, V (-f
     rw [←eq]
     dsimp
     if h : s.1 == 0 then
-      rw [if_pos h]
+      rw [ite_eq_left h]
       exact le_of_max_le_left hax
     else
-      rw [if_neg h, hV₀]
+      rw [ite_eq_right h, hV₀]
       exact le_of_max_le_right hax
   apply le_antisymm
   · apply ciSup_le
@@ -713,10 +713,10 @@ lemma sup_abs_lemma [Nonempty ι] {V : (Z → ℝ) → ℝ} (hV₀: ∀ f, V (-f
     rintro ⟨s,i⟩
     apply le_trans _ (le_ciSup hV₁ i)
     if h : s.1 == 0 then
-      rw [if_pos h]
+      rw [ite_eq_left h]
       exact le_abs_self (V (f i))
     else
-      rw [if_neg h, hV₀]
+      rw [ite_eq_right h, hV₀]
       exact neg_le_abs (V (f i))
 
 theorem abs_symmetrization_equation [Countable ι] [Nonempty ι] (h𝓕 : ∀ I : ι, Measurable (f I ∘ X))
@@ -753,21 +753,21 @@ theorem abs_symmetrization_equation [Countable ι] [Nonempty ι] (h𝓕 : ∀ I
         dsimp [f']
         rintro ⟨s, I⟩
         if h : s.1 == 0 then
-          rw [if_pos h]
+          rw [ite_eq_left h]
           dsimp
           exact h𝓕 I
         else
-          rw [if_neg h]
+          rw [ite_eq_right h]
           dsimp
           exact (h𝓕 I).neg
       have h𝓕'₂: ∀ I, ∀ z : Z, |f' I z| ≤ b := by
         rintro ⟨s,I⟩ z
         dsimp [f']
         if h : s.1 == 0 then
-          rw [if_pos h]
+          rw [ite_eq_left h]
           exact h𝓕' I z
         else
-          rw [if_neg h]
+          rw [ite_eq_right h]
           simp only [Pi.neg_apply, abs_neg]
           exact h𝓕' I z
       exact symmetrization_equation h𝓕₂ h𝓕'₂

StatsMLlib/LinearAlgebra/Matrix/Lieb.lean

@@ -77,7 +77,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 theorem rayleighQuotient_mono_of_le {A B : E →ₗ[ℝ] E} (hAB : A ≤ B) {x : E}
     (hx : x ≠ 0) :
     rayleighQuotient A x ≤ rayleighQuotient B x := by
-  have hpos : (B - A).IsPositive := (LinearMap.le_def A B).mp hAB
+  have hpos : (B - A).IsPositive := LinearMap.le_def.mp hAB
   have hinner : 0 ≤ inner ℝ ((B - A) x) x := hpos.inner_nonneg_left x
   have hden : 0 < ‖x‖ ^ 2 := sq_pos_of_pos (norm_pos_iff.mpr hx)
   unfold rayleighQuotient
@@ -114,7 +114,7 @@ functional-calculus theorem for logarithm.
 -/
 noncomputable def realMatrixToCStarMatrixStarAlgHom :
     Matrix n n ℝ →⋆ₐ[ℝ] CStarMatrix n n ℂ :=
-  (((CStarMatrix.ofMatrixStarAlgEquiv (n := n) (A := ℂ) :
+  ((((CStarMatrix.ofMatrixStarAlgEquiv (n := n) (A := ℂ)).toStarAlgHom :
       Matrix n n ℂ →⋆ₐ[ℂ] CStarMatrix n n ℂ).restrictScalars ℝ).comp
     (realMatrixToComplexMatrixStarAlgHom (n := n)))
 

StatsMLlib/LinearAlgebra/Matrix/SingularValue.lean

@@ -282,7 +282,7 @@ theorem orthonormal_leftSingularVector_of_singularValues_ne_zero
   intro i j
   by_cases hij : i = j
   · subst j
-    rw [if_pos rfl, inner_self_eq_norm_sq_to_K,
+    rw [ite_eq_left rfl, inner_self_eq_norm_sq_to_K,
       A.norm_leftSingularVector_of_singularValues_ne_zero i.property]
     norm_num
   · have hne : (i : Fin (Fintype.card n)) ≠ (j : Fin (Fintype.card n)) := by
@@ -304,7 +304,7 @@ theorem orthonormal_leftSingularVector_of_singularValues_ne_zero
         _ = 0 := by
           rw [inner_smul_left]
           simp [A.rightSingularVectorBasis.inner_eq_zero hne]
-    rw [if_neg hij]
+    rw [ite_eq_right hij]
     unfold leftSingularVector
     rw [inner_smul_left, inner_smul_right, hmap]
     simp

StatsMLlib/MeasureTheory/Function/L1Subsequence.lean

@@ -14,13 +14,11 @@ variable {α E : Type*} {m : MeasurableSpace α} {mu : Measure α}
 /-- Convergence in L^1 yields an a.e.-convergent subsequence. -/
 theorem exists_seq_tendsto_ae_of_tendsto_eLpNorm_one
     [NormedAddCommGroup E] {f : ℕ → α → E} {g : α → E}
-    (hf : ∀ n, AEStronglyMeasurable (f n) mu)
-    (hg : AEStronglyMeasurable g mu)
     (hfg : Tendsto (fun n => eLpNorm (f n - g) (1 : ENNReal) mu) atTop (nhds 0)) :
     ∃ ns : ℕ → ℕ, StrictMono ns ∧
       ∀ᵐ x ∂mu, Tendsto (fun i => f (ns i) x) atTop (nhds (g x)) := by
   have h_in_measure : TendstoInMeasure mu f atTop g :=
-    tendstoInMeasure_of_tendsto_eLpNorm (p := (1 : ENNReal)) (by simp) hf hg hfg
+    tendstoInMeasure_of_tendsto_eLpNorm (p := (1 : ENNReal)) (by simp) hfg
   exact h_in_measure.exists_seq_tendsto_ae
 
 end MeasureTheory

StatsMLlib/Probability/Concentration/EfronStein.lean

@@ -62,7 +62,7 @@ lemma condExpExceptCoord_stronglyMeasurable (hf : StronglyMeasurable f) :
     StronglyMeasurable (condExpExceptCoord (μs := μs) i f) := by
   unfold condExpExceptCoord
   apply StronglyMeasurable.integral_prod_right
-  exact hf.comp_measurable (measurable_pi_lambda _ (fun j => by
+  exact hf.comp_measurable (Measurable.of_eval (fun j => by
     by_cases h : j = i
     · subst h
       simp only [Function.update_self]
@@ -1000,7 +1000,7 @@ lemma memLp_condExpExceptCoord (i : Fin n) (f : (Fin n → Ω) → ℝ) (hf : Me
       -- f = mk f on μˢ-a.e., so f ∘ update = (mk f) ∘ update on (μˢ × μ)-a.e.
       have hae_prod : (fun p : (Fin n → Ω) × Ω => f (Function.update p.1 i p.2)) =ᶠ[ae (μˢ.prod (μs i))]
                       (fun p => hf.aestronglyMeasurable.mk f (Function.update p.1 i p.2)) := by
-        have := hmp.quasiMeasurePreserving.ae_eq hae
+        have := hmp.quasiMeasurePreserving.ae_eq_comp hae
         filter_upwards [this] with p hp
         exact hp
       -- By Fubini: for μˢ-a.e. x, the slice functions are μ-a.e. equal

StatsMLlib/Probability/Concentration/HansonWright.lean

@@ -66,7 +66,9 @@ lemma mgf_innerSL_stdGaussian {E : Type*} [NormedAddCommGroup E] [InnerProductSp
   have hmap : (stdGaussian E).map L =
       gaussianReal ((stdGaussian E)[L]) Var[L; stdGaussian E].toNNReal :=
     IsGaussian.map_eq_gaussianReal L
-  have hmgf := mgf_gaussianReal hmap t
+  have hlaw : HasLaw (⇑L) (gaussianReal ((stdGaussian E)[L])
+      Var[L; stdGaussian E].toNNReal) (stdGaussian E) := ⟨by fun_prop, hmap⟩
+  have hmgf := mgf_gaussianReal hlaw t
   have hmean : (stdGaussian E)[L] = 0 := integral_strongDual_stdGaussian L
   have hvar : (Var[L; stdGaussian E].toNNReal : ℝ) = ‖v‖ ^ 2 := by
     rw [variance_dual_stdGaussian L]
@@ -161,7 +163,7 @@ lemma randomVector_aemeasurable {μ : Measure Ω} {n : ℕ} {X : Fin n → Ω 
     (hX_meas : ∀ i, AEMeasurable (X i) μ) :
     AEMeasurable (randomVector X) μ := by
   exact (MeasurableEquiv.toLp 2 (Fin n → ℝ)).measurable.comp_aemeasurable
-    (aemeasurable_pi_lambda _ hX_meas)
+    (AEMeasurable.of_eval hX_meas)
 
 omit [MeasurableSpace Ω] in
 lemma measure_map_prod_map_of_aemeasurable {α β γ δ : Type*}
@@ -241,7 +243,7 @@ lemma subtypeMask_apply {n : ℕ} (s : Finset (Fin n)) (x : s → ℝ) (i : Fin
 lemma measurable_subtypeMask {n : ℕ} (s : Finset (Fin n)) :
     Measurable (subtypeMask (n := n) s) := by
   exact (MeasurableEquiv.toLp 2 (Fin n → ℝ)).measurable.comp
-    (measurable_pi_lambda _ fun i => by
+    (Measurable.of_eval fun i => by
       by_cases hi : i ∈ s
       · simpa [hi] using
           (measurable_pi_apply (⟨i, hi⟩ : s) : Measurable fun x : s → ℝ => x ⟨i, hi⟩)
@@ -262,7 +264,7 @@ lemma coordinateMask_aemeasurable {μ : Measure Ω} {n : ℕ} (s : Finset (Fin n
     AEMeasurable (fun ω => coordinateMask s (randomVector X ω)) μ := by
   rw [← subtypeMask_subtype_randomVector s X]
   exact (measurable_subtypeMask s).aemeasurable.comp_aemeasurable
-    (aemeasurable_pi_lambda _ fun i => hX_meas i)
+    (AEMeasurable.of_eval fun i => hX_meas i)
 
 lemma coordinateMask_indepFun_compl {μ : Measure Ω} {n : ℕ} {X : Fin n → Ω → ℝ}
     (h_indep : iIndepFun X μ) (hX_meas : ∀ i, AEMeasurable (X i) μ)
@@ -1535,7 +1537,7 @@ lemma integral_exp_quadratic_stdGaussian_le {E : Type*} [NormedAddCommGroup E]
             (μ := fun _ => gaussianReal 0 1))
     _ ≤ ∏ i : Fin (Module.finrank ℝ E),
           exp (2 * exp 1 * ((θ * lam i) * 1 * exp 1)) := by
-          apply Finset.prod_le_prod
+          apply Finset.prod_le_prod₀
           · intro i _
             exact integral_nonneg_of_ae (ae_of_all _ fun x => exp_nonneg _)
           · intro i _
@@ -2387,10 +2389,6 @@ lemma integrable_exp_mul_prod_of_indepFun_hasSubgaussianMGF_of_le
   have hg : AEStronglyMeasurable g (μ.map φ) := by
     dsimp [g]
     fun_prop
-  have : IsProbabilityMeasure (μ.map X) :=
-    MeasureTheory.Measure.isProbabilityMeasure_map hX.aemeasurable
-  have : IsProbabilityMeasure (μ.map Y) :=
-    MeasureTheory.Measure.isProbabilityMeasure_map hY.aemeasurable
   have hprod_int :
       Integrable g ((μ.map Y).prod (μ.map X)) :=
     integrable_exp_mul_snd_fst_prod_of_hasSubgaussianMGF_of_le
@@ -2422,10 +2420,6 @@ lemma integral_exp_mul_prod_le_of_indepFun_hasSubgaussianMGF_of_le
   have hg : AEStronglyMeasurable g (μ.map φ) := by
     dsimp [g]
     fun_prop
-  have : IsProbabilityMeasure (μ.map X) :=
-    MeasureTheory.Measure.isProbabilityMeasure_map hX.aemeasurable
-  have : IsProbabilityMeasure (μ.map Y) :=
-    MeasureTheory.Measure.isProbabilityMeasure_map hY.aemeasurable
   have hmap_eq :
       μ.map φ = (μ.map Y).prod (μ.map X) := by
     simpa [φ] using (h_indep.symm.map_prod_eq_prod_map_map hY.aemeasurable hX.aemeasurable)
@@ -2873,7 +2867,7 @@ lemma quadraticForm_eq_diag_add_offDiagonal {n : ℕ}
                   by_cases hij : i = j
                   · subst j
                     simp
-                  · rw [if_neg hij, if_neg hij]
+                  · rw [ite_eq_right hij, ite_eq_right hij]
                     ring
             _ = A i i * x i ^ 2 +
                     ∑ j, (if i = j then 0 else A i j) * x i * x j := by

StatsMLlib/Probability/Concentration/Hoeffding.lean

@@ -79,7 +79,6 @@ theorem cgf_le_quadratic_of_nonneg [IsProbabilityMeasure μ] (t a b : ℝ) {X :
       · rw [← (by ring : 0 - f' x + (f' x - f'' x * (t - x)) = - f'' x * (t - x))]
         apply ((hasDerivAt_const x _).sub (cgf_deriv_one a b hX h x)).add
         convert (cgf_deriv_two a b hX h x).mul ((hasDerivAt_id' x).add_const (-t)) using 1
-        · rfl
         · funext y
           simp only [Pi.mul_apply]
           ring

StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean

@@ -133,11 +133,11 @@ theorem bernoulli_flip_invariance (j : Fin n) :
     by_cases h : i = j
     · subst h; simp only [update_self, Bool.not_not]
     · rw [update_of_ne h, update_of_ne h]
-  rw [Measure.map_smul]
+  have hmeas : Measurable (flipCoord j) := measurable_of_finite _
+  rw [Measure.map_smul _ hmeas.aemeasurable]
   congr 1
   -- Show count measure is invariant under bijection
   ext s hs
-  have hmeas : Measurable (flipCoord j) := measurable_of_finite _
   rw [Measure.map_apply hmeas hs]
   have hs1 : (flipCoord j ⁻¹' s).Finite := Set.toFinite _
   have hs2 : s.Finite := Set.toFinite _
@@ -1004,9 +1004,9 @@ theorem twoPointEntropyCoord_castSucc_eq_slice {n : ℕ} (j : Fin n)
   cases b
   · -- false case: if false = true then ... else ... becomes sliceFalse
     simp only [twoPointEntropyCoord, flipCoord_castSucc_snoc, sliceFalse,
-               Bool.false_eq_true, if_false]
+               Bool.false_eq_true, ite_false]
   · -- true case: if true = true then ... else ... becomes sliceTrue
-    simp only [twoPointEntropyCoord, flipCoord_castSucc_snoc, sliceTrue, if_true]
+    simp only [twoPointEntropyCoord, flipCoord_castSucc_snoc, sliceTrue, ite_true]
 
 /-- Average of twoPointEntropyCoord at castSucc j equals average of slices -/
 theorem avg_twoPointEntropyCoord_castSucc {n : ℕ} (j : Fin n)
@@ -1016,7 +1016,7 @@ theorem avg_twoPointEntropyCoord_castSucc {n : ℕ} (j : Fin n)
     (twoPointEntropyCoord j (sliceTrue h) ε' + twoPointEntropyCoord j (sliceFalse h) ε') / 2 := by
   rw [twoPointEntropyCoord_castSucc_eq_slice j h ε' true]
   rw [twoPointEntropyCoord_castSucc_eq_slice j h ε' false]
-  simp only [if_true, Bool.false_eq_true, if_false]
+  simp only [ite_true, Bool.false_eq_true, ite_false]
 
 /-- The conditional mean sqrt function: g such that g² = condMeanLast h² -/
 def condMeanSqrt {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ) : (Fin n → Bool) → ℝ :=
@@ -1273,8 +1273,8 @@ theorem toRademacher_flipCoord {n : ℕ} (j : Fin n) (ε : Fin n → Bool) :
   simp only [toRademacher, Function.update]
   by_cases h : i = j
   · subst h
-    simp only [flipCoord_same, signValue_not, dif_pos]
-  · simp only [dif_neg h]
+    simp only [flipCoord_same, signValue_not, dite_eq_left]
+  · simp only [dite_eq_right h]
     rw [flipCoord_noteq j i ε h]
 
 /-- The Rademacher sum after coordinate flip equals the shifted sum -/