Bump mathlib

LeanAPAP.lean

@@ -2,7 +2,7 @@ import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
+import LeanAPAP.Mathlib.Data.Complex.BigOperators
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.Tactic.Positivity

LeanAPAP/Extras/BSG.lean

@@ -124,7 +124,7 @@ lemma claim_two :
     rw [Real.sq_sqrt]
     exact dconv_nonneg (R := ℝ) indicate_nonneg indicate_nonneg s -- why do I need the annotation??
   have := sum_mul_sq_le_sq_mul_sq univ f (fun s ↦ f s * (A ∩ (s +ᵥ B)).card)
-  refine div_le_of_nonneg_of_le_mul (by positivity) ?_ ?_
+  refine div_le_of_le_mul₀ (by positivity) ?_ ?_
   · refine sum_nonneg fun i _ ↦ ?_
     -- indicate nonneg should be a positivity lemma
     exact mul_nonneg (dconv_nonneg indicate_nonneg indicate_nonneg _) (by positivity)

LeanAPAP/FiniteField.lean

@@ -1,5 +1,5 @@
 import Mathlib.FieldTheory.Finite.Basic
-import LeanAPAP.Prereqs.Balance.Complex
+import LeanAPAP.Mathlib.Data.Complex.BigOperators
 import LeanAPAP.Prereqs.Chang
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.FourierTransform.Convolution
@@ -16,7 +16,7 @@ set_option linter.haveLet 0
 
 attribute [-simp] Real.log_inv
 
-open FiniteDimensional Fintype Function MeasureTheory RCLike Real
+open Fintype Function MeasureTheory Module RCLike Real
 open Finset hiding card
 open scoped ENNReal NNReal BigOperators Combinatorics.Additive Pointwise
 
@@ -143,7 +143,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
   have hA₂ : A₂.Nonempty := by simpa using hα₀.trans_le hαA₂
   have hα₁ : α ≤ 1 := hαA₁.trans $ mod_cast A₁.dens_le_one
   have : 0 ≤ log α⁻¹ := log_nonneg $ one_le_inv hα₀ hα₁
-  have : 0 ≤ log (ε * α)⁻¹ := log_nonneg $ one_le_inv (by positivity) $ mul_le_one hε₁ hα₀.le hα₁
+  have : 0 ≤ log (ε * α)⁻¹ := log_nonneg $ one_le_inv (by positivity) $ mul_le_one₀ hε₁ hα₀.le hα₁
   obtain rfl | hS := S.eq_empty_or_nonempty
   · exact ⟨⊤, inferInstance, by simp [hε₀.le]; positivity⟩
   have hA₁ : σ[A₁, univ] ≤ α⁻¹ :=
@@ -186,7 +186,7 @@ lemma ap_in_ff (hα₀ : 0 < α) (hα₂ : α ≤ 2⁻¹) (hε₀ : 0 < ε) (hε
                 Nat.ceil_le_two_mul <| two_inv_lt_one.le.trans <| one_le_curlog (by positivity) sorry
               _ ≤ 2 * (4 * 𝓛 (ε * α)) := by
                 gcongr
-                exact curlog_div_le (by positivity) (mul_le_one hε₁ hα₀.le hα₁) (by norm_num)
+                exact curlog_div_le (by positivity) (mul_le_one₀ hε₁ hα₀.le hα₁) (by norm_num)
               _ = 2 ^ 3 * 𝓛 (ε * α) := by ring
         _ = 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring_nf
     calc
@@ -250,7 +250,7 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
     ∃ p' : ℕ, p' ≤ 2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p ∧
       1 + ε / 2 / 2 ≤ ‖card G • (f ○ f) + 1‖_[p', μ univ] := by
     refine unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ.le hγ₁).ne')
-      (ε / 2) (by positivity) (div_le_one_of_le (hε₁.le.trans $ by norm_num) $ by norm_num)
+      (ε / 2) (by positivity) (div_le_one_of_le₀ (hε₁.le.trans $ by norm_num) $ by norm_num)
       (card G • (balance (μ A) ○ balance (μ A))) (sqrt (card G) • balance (μ A)) (μ univ) ?_ ?_ ?_
     · ext a : 1
       simp [smul_dconv, dconv_smul, smul_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow]
@@ -362,8 +362,8 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q)
       _ ≤ 2 ^ 32 * (8 * q' * 𝓛 α) ^ 2 *
           (2 ^ 8 * q' * 𝓛 α / ε) ^ 2 * (ε / 32)⁻¹ ^ 2 := by
         have : α ^ (2 * q') ≤ 1 := pow_le_one₀ hα₀.le hα₁
-        have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one (by norm_num) (by positivity) ‹_›
-        have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one (by linarith) (by positivity) ‹_›
+        have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one₀ (by norm_num) (by positivity) ‹_›
+        have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one₀ (by linarith) (by positivity) ‹_›
         have : 0 ≤ log (ε / 32 * (4⁻¹ * α ^ (2 * q')))⁻¹ :=
           log_nonneg $ one_le_inv (by positivity) ‹_›
         have : 0 ≤ log (4⁻¹ * α ^ (2 * q'))⁻¹ := log_nonneg $ one_le_inv (by positivity) ‹_›
@@ -525,7 +525,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
     calc
       _ ≤ (1 : ℝ) := mod_cast dens_le_one
       _ < _ := ?_
-    rw [← inv_pos_lt_iff_one_lt_mul, lt_pow_iff_log_lt, ← div_lt_iff₀]
+    rw [← inv_lt_iff_one_lt_mul₀, lt_pow_iff_log_lt, ← div_lt_iff₀]
     calc
       log α⁻¹ / log (65 / 64)
         < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _

LeanAPAP/Mathlib/Data/Complex/BigOperators.lean

@@ -0,0 +1,11 @@
+import Mathlib.Data.Complex.BigOperators
+
+open Fintype
+
+namespace Complex
+variable {ι : Type*}
+
+@[simp] lemma ofReal'_comp_balance [Fintype ι] (f : ι → ℝ) :
+    ofReal' ∘ balance f = balance (ofReal' ∘ f) := ofReal_comp_balance _
+
+end Complex

LeanAPAP/Mathlib/MeasureTheory/Function/EssSup.lean

@@ -7,31 +7,7 @@ open scoped ENNReal
 variable {α β : Type*} {m : MeasurableSpace α} [ConditionallyCompleteLattice β]
   {μ : Measure α} {f : α → β}
 
-section SMul
-variable {R : Type*} [Zero R] [SMulWithZero R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞]
-  [NoZeroSMulDivisors R ℝ≥0∞] {c : ℝ≥0∞}
-
--- TODO: Replace in mathlib
-@[simp] lemma essSup_smul_measure' {f : α → β} {c : ℝ≥0∞} (hc : c ≠ 0) :
-    essSup f (c • μ) = essSup f μ := by simp_rw [essSup, Measure.ae_smul_measure_eq hc]
-
-end SMul
-
-variable [Nonempty α]
-
-lemma essSup_eq_ciSup (hμ : ∀ a, μ {a} ≠ 0) (hf : BddAbove (Set.range f)) :
-    essSup f μ = ⨆ a, f a := by rw [essSup, ae_eq_top.2 hμ, limsup_top_eq_ciSup hf]
-
-lemma essInf_eq_ciInf (hμ : ∀ a, μ {a} ≠ 0) (hf : BddBelow (Set.range f)) :
-    essInf f μ = ⨅ a, f a := by rw [essInf, ae_eq_top.2 hμ, liminf_top_eq_ciInf hf]
-
-variable [MeasurableSingletonClass α]
-
-@[simp] lemma essSup_count_eq_ciSup (hf : BddAbove (Set.range f)) :
-    essSup f .count = ⨆ a, f a := essSup_eq_ciSup (by simp) hf
-
-@[simp] lemma essInf_count_eq_ciInf (hf : BddBelow (Set.range f)) :
-    essInf f .count = ⨅ a, f a := essInf_eq_ciInf (by simp) hf
+variable [Nonempty α] [MeasurableSingletonClass α]
 
 @[simp] lemma essSup_cond_count_eq_ciSup [Finite α] (hf : BddAbove (Set.range f)) :
     essSup f .count[|.univ] = ⨆ a, f a := essSup_eq_ciSup (by simp [cond_apply, Set.finite_univ]) hf

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -433,7 +433,7 @@ theorem linfty_almost_periodicity (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤
   have hm₀ : 0 < m := curlog_pos (by positivity)
   have hm₁ : 1 ≤ ⌈m⌉₊ := Nat.one_le_iff_ne_zero.2 $ by positivity
   obtain ⟨T, hKT, hT⟩ := almost_periodicity (ε / exp 1) (by positivity)
-    (div_le_one_of_le (hε₁.trans $ one_le_exp zero_le_one) $ by positivity) ⌈m⌉₊ (𝟭 B) hK₂ hK
+    (div_le_one_of_le₀ (hε₁.trans $ one_le_exp zero_le_one) $ by positivity) ⌈m⌉₊ (𝟭 B) hK₂ hK
   norm_cast at hT
   set M : ℕ := 2 * ⌈m⌉₊
   have hM₀ : (M : ℝ≥0) ≠ 0 := by positivity
@@ -499,7 +499,7 @@ theorem linfty_almost_periodicity_boosted (ε : ℝ) (hε₀ : 0 < ε) (hε₁ :
       K ^ (-4096 * ⌈𝓛 (C.card / B.card)⌉ * k ^ 2/ ε ^ 2) * S.card ≤ T.card ∧
       ‖μ T ∗^ k ∗ (μ_[ℂ] A ∗ 𝟭 B ∗ μ C) - μ A ∗ 𝟭 B ∗ μ C‖_[∞] ≤ ε := by
   obtain ⟨T, hKT, hT⟩ := linfty_almost_periodicity (ε / k) (by positivity)
-    (div_le_one_of_le (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK
+    (div_le_one_of_le₀ (hε₁.trans $ mod_cast Nat.one_le_iff_ne_zero.2 hk) $ by positivity) hK₂ hK
     _ _ hB hC
   refine ⟨T, by simpa only [div_pow, div_div_eq_mul_div] using hKT, ?_⟩
   set F := μ_[ℂ] A ∗ 𝟭 B ∗ μ C

LeanAPAP/Physics/DRC.lean

@@ -126,7 +126,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         mul_div_right_comm] using h
       positivity
     refine ⟨(lt_of_mul_lt_mul_left (hs.trans_eq' ?_) $ hg s).le, this.trans $ mul_le_of_le_one_right
-      ?_ $ div_le_one_of_le ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le ?_ ?_⟩
+      ?_ $ div_le_one_of_le₀ ?_ ?_, this.trans $ mul_le_of_le_one_left ?_ $ div_le_one_of_le₀ ?_ ?_⟩
     · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, ← Nat.cast_smul_eq_nsmul ℝ,
         wInner_smul_left, star_trivial, mul_assoc]
     any_goals positivity
@@ -223,7 +223,7 @@ lemma sifting (B₁ B₂ : Finset G) (hε : 0 < ε) (hε₁ : ε ≤ 1) (hδ : 0
         := ?_
     _ ≤ _ :=
       mul_le_of_le_one_left (mul_nonneg (hp.pow_nonneg _) $ hp.pow_nonneg _) $
-        mul_le_one dL1Norm_mu_le_one (NNReal.coe_nonneg _) dL1Norm_mu_le_one
+        mul_le_one₀ dL1Norm_mu_le_one (NNReal.coe_nonneg _) dL1Norm_mu_le_one
     _ ≤ _ := mul_le_mul_of_nonneg_right ?_ $ hp.pow_nonneg _
   · have : 0 ≤ μ_[ℝ] B₁ ○ μ B₂ := dconv_nonneg mu_nonneg mu_nonneg
     simp_rw [← NNReal.coe_mul, ← dL1Norm_dconv mu_nonneg mu_nonneg, dL1Norm_eq_sum_nnnorm,

LeanAPAP/Prereqs/AddChar/Basic.lean

@@ -71,7 +71,7 @@ noncomputable instance instFintype [Finite G] : Fintype (AddChar G R) :=
   @Fintype.ofFinite _ (AddChar.linearIndependent G R).finite
 
 @[simp] lemma card_addChar_le [Fintype G] : card (AddChar G R) ≤ card G := by
-  simpa only [FiniteDimensional.finrank_fintype_fun_eq_card] using
+  simpa only [Module.finrank_fintype_fun_eq_card] using
     (AddChar.linearIndependent G R).fintype_card_le_finrank
 
 end RCLike

LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean

@@ -142,7 +142,7 @@ variable (α) [Finite α]
 /-- Complex-valued characters of a finite abelian group `α` form a basis of `α → ℂ`. -/
 def complexBasis : Basis (AddChar α ℂ) ℂ (α → ℂ) :=
   basisOfLinearIndependentOfCardEqFinrank (AddChar.linearIndependent _ _) $ by
-    cases nonempty_fintype α; rw [card_eq, FiniteDimensional.finrank_fintype_fun_eq_card]
+    cases nonempty_fintype α; rw [card_eq, Module.finrank_fintype_fun_eq_card]
 
 @[simp, norm_cast]
 lemma coe_complexBasis : ⇑(complexBasis α) = ((⇑) : AddChar α ℂ → α → ℂ) := by

LeanAPAP/Prereqs/Balance/Complex.lean

@@ -1,31 +1,11 @@
-import Mathlib.Algebra.BigOperators.Balance
-import Mathlib.Analysis.RCLike.Basic
 import Mathlib.Data.Complex.BigOperators
 
 open Fintype
-open scoped NNReal
 
 namespace Complex
 variable {ι : Type*}
 
-@[simp] lemma ofReal_comp_balance [Fintype ι] (f : ι → ℝ) :
-    ofReal ∘ balance f = balance (ofReal ∘ f) := by simp [balance]
-
 @[simp] lemma ofReal'_comp_balance [Fintype ι] (f : ι → ℝ) :
     ofReal' ∘ balance f = balance (ofReal' ∘ f) := ofReal_comp_balance _
 
 end Complex
-
-namespace RCLike
-variable {ι 𝕜 : Type*} [RCLike 𝕜] [Fintype ι] (f : ι → ℝ) (a : ι)
-
-@[simp, norm_cast]
-lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_balance (algebraMap ..) ..
-
-@[simp] lemma coe_comp_balance : ((↑) : ℝ → 𝕜) ∘ balance f = balance ((↑) ∘ f) :=
-  funext $ coe_balance _
-
-@[simp] lemma ofReal_comp_balance : ofReal ∘ balance f = balance (ofReal ∘ f : ι → 𝕜) := by
-  simp [balance]
-
-end RCLike

LeanAPAP/Prereqs/Chang.lean

@@ -1,6 +1,5 @@
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalities
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.Energy
 import LeanAPAP.Prereqs.LargeSpec
 import LeanAPAP.Prereqs.Rudin
@@ -80,7 +79,7 @@ local notation:70 s:70 " ^^ " n:71 => Fintype.piFinset fun _ : Fin n ↦ s
 variable [MeasurableSpace G] [DiscreteMeasurableSpace G]
 
 private lemma α_le_one (f : G → ℂ) : ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G ≤ 1 := by
-  refine div_le_one_of_le (div_le_of_nonneg_of_le_mul ?_ ?_ ?_) ?_
+  refine div_le_one_of_le₀ (div_le_of_le_mul₀ ?_ ?_ ?_) ?_
   any_goals positivity
   rw [dL1Norm_eq_sum_nnnorm, dL2Norm_sq_eq_sum_nnnorm, ← NNReal.coe_le_coe]
   push_cast
@@ -190,7 +189,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
       rw [div_self hη.ne', one_pow, one_mul]
     _ = _ := by ring
   refine le_mul_of_one_le_right (by positivity) ?_
-  rw [← inv_pos_le_iff_one_le_mul']
+  rw [← inv_le_iff_one_le_mul₀']
   calc
     α⁻¹ = exp (0 + log α⁻¹) := by rw [zero_add, exp_log]; norm_cast; positivity
     _ ≤ exp ⌈0 + log α⁻¹⌉₊ := by gcongr; exact Nat.le_ceil _

LeanAPAP/Prereqs/LpNorm/Compact.lean

@@ -1,11 +1,8 @@
-import Mathlib.Algebra.Order.BigOperators.Expect
 import Mathlib.Algebra.Star.Conjneg
-import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
-import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
+import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.NNLpNorm
 
 /-!

LeanAPAP/Prereqs/Rudin.lean

@@ -1,6 +1,5 @@
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
-import LeanAPAP.Mathlib.Data.ENNReal.Basic
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.Randomisation
 
@@ -83,7 +82,7 @@ private lemma rudin_ineq_aux (hp : 2 ≤ p) (f : α → ℂ) (hf : AddDissociate
       _ ≤ 𝔼 a, |(f a).re| ^ p / p ! := by gcongr; norm_cast; exact p.factorial_le_pow
       _ ≤ 𝔼 a, exp |(f a).re| := by gcongr; exact pow_div_factorial_le_exp _ (abs_nonneg _) _
       _ ≤ _ := rudin_exp_abs_ineq f hf
-      _ ≤ 2 ^ p * exp (‖f‖ₙ_[2] ^ 2 / 2) := by gcongr; exact le_self_pow one_le_two hp₀
+      _ ≤ 2 ^ p * exp (‖f‖ₙ_[2] ^ 2 / 2) := by gcongr; exact le_self_pow₀ one_le_two hp₀
       _ = (2 * exp 2⁻¹) ^ p := by
           rw [hfp, sq_sqrt, mul_pow, ← exp_nsmul, nsmul_eq_mul, div_eq_mul_inv]; positivity
   refine le_of_pow_le_pow_left hp₀ (by positivity) ?_

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f274aed7ae8d1addd3e70adaf3183ccc6e1ed43d",
+   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
+   "rev": "2b2f6d7fbe9d917fc010e9054c1ce11774c9088b",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
+   "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
+   "rev": "4b61d4abc1659f15ffda5ec24fdebc229d51d066",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d369bba55fcefeb0d7600e9c2e4856ac9bbece72",
+   "rev": "3693fb294c1201f0b69ba48e98d083d2bb3e630d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0-rc3