Bump mathlib

LeanAPAP.lean

@@ -6,9 +6,7 @@ import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled
 import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
-import LeanAPAP.Mathlib.Data.Complex.Basic
 import LeanAPAP.Mathlib.Data.ENNReal.Basic
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
 import LeanAPAP.Mathlib.Data.ENNReal.Real
 import LeanAPAP.Mathlib.Data.Real.ConjExponents
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
@@ -35,7 +33,6 @@ import LeanAPAP.Prereqs.Convolution.Order
 import LeanAPAP.Prereqs.Convolution.ThreeAP
 import LeanAPAP.Prereqs.Convolution.WithConv
 import LeanAPAP.Prereqs.Energy
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Compact
 import LeanAPAP.Prereqs.FourierTransform.Convolution
 import LeanAPAP.Prereqs.FourierTransform.Discrete

LeanAPAP/Mathlib/Data/Real/ConjExponents.lean

@@ -1,6 +1,5 @@
 import Mathlib.Data.ENNReal.Inv
 import Mathlib.Data.Real.ConjExponents
-import LeanAPAP.Mathlib.Data.ENNReal.Operations
 
 open scoped NNReal
 

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -3,7 +3,6 @@ import Mathlib.Combinatorics.Additive.DoublingConst
 import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Inner.Hoelder.Discrete
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 

LeanAPAP/Prereqs/Balance/Complex.lean

@@ -1,5 +1,6 @@
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Complex.BigOperators
 import LeanAPAP.Prereqs.Balance.Defs
-import LeanAPAP.Prereqs.Expect.Complex
 
 open Finset
 open scoped BigOperators NNReal
@@ -28,4 +29,3 @@ lemma coe_balance : (↑(balance f a) : 𝕜) = balance ((↑) ∘ f) a := map_b
   simp [balance]
 
 end RCLike
-

LeanAPAP/Prereqs/Convolution/Compact.lean

@@ -1,6 +1,5 @@
 import LeanAPAP.Prereqs.Balance.Defs
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 
 /-!
@@ -393,11 +392,11 @@ end Field
 namespace RCLike
 variable {𝕜 : Type} [RCLike 𝕜] (f g : G → ℝ) (a : G)
 
-@[simp, norm_cast]
-lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a := map_cconv (algebraMap ℝ 𝕜) _ _ _
+@[simp, norm_cast] lemma coe_cconv : (f ∗ₙ g) a = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) a :=
+  map_cconv (algebraMap ℝ 𝕜) ..
 
-@[simp, norm_cast]
-lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by simp [cdconv_apply, coe_expect]
+@[simp, norm_cast] lemma coe_cdconv : (f ○ₙ g) a = ((↑) ∘ f ○ₙ (↑) ∘ g : G → 𝕜) a := by
+  simp [cdconv_apply, ofReal_expect]
 
 @[simp]
 lemma coe_comp_cconv : ofReal ∘ (f ∗ₙ g) = ((↑) ∘ f ∗ₙ (↑) ∘ g : G → 𝕜) := funext $ coe_cconv _ _

LeanAPAP/Prereqs/Energy.lean

@@ -1,6 +1,5 @@
 import LeanAPAP.Prereqs.AddChar.Basic
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.FourierTransform.Discrete
 import LeanAPAP.Prereqs.Function.Indicator.Complex
 

LeanAPAP/Prereqs/LpNorm/Compact.lean

@@ -4,7 +4,6 @@ import Mathlib.Data.Finset.Density
 import Mathlib.Data.Fintype.Order
 import Mathlib.Probability.ConditionalProbability
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
-import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.Function.Translate
 import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.NNLpNorm

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -3,6 +3,7 @@ Copyright (c) 2023 Yaël Dillies, Bhavik Mehta. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
+import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Analysis.MeanInequalitiesPow
 import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Tactic.Positivity.Finset
@@ -39,7 +40,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
     _ = (∑ b in B, |∑ i, (f (a i) - f (b i))|) ^ (m + 1) / B.card ^ m / B.card := by
       rw [div_div, ← _root_.pow_succ]
     _ ≤ (∑ b in B, |∑ i, (f (a i) - f (b i))| ^ (m + 1)) / B.card := by
-      gcongr; exact pow_sum_div_card_le_sum_pow _ _ fun _ _ ↦ abs_nonneg _
+      gcongr; exact pow_sum_div_card_le_sum_pow (fun _ _ ↦ abs_nonneg _) _
     _ = _ := by simp [B]
 
 private lemma step_one' (hA : A.Nonempty) (f : ι → ℝ) (hf : ∀ i, ∑ a in A ^^ n, f (a i) = 0) (m : ℕ)
@@ -227,7 +228,7 @@ theorem marcinkiewicz_zygmund (hm : m ≠ 0) (f : ι → ℝ) (hf : ∀ i, ∑ a
       simp_rw [mul_assoc, mul_sum]; rfl
   gcongr with a
   rw [← div_le_iff₀']
-  have := Real.pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) univ m fun i _ ↦ ?_
+  have := pow_sum_div_card_le_sum_pow (f := fun i ↦ f (a i) ^ 2) (s := univ) (fun i _ ↦ ?_) m
   simpa only [Finset.card_fin, pow_mul] using this
   all_goals { positivity }
 

LeanAPAP/Prereqs/Randomisation.lean

@@ -1,6 +1,5 @@
 import Mathlib.Combinatorics.Additive.Dissociation
 import LeanAPAP.Prereqs.AddChar.Basic
-import LeanAPAP.Prereqs.Expect.Complex
 
 /-!
 # Randomisation

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bf12ff6041cbab6eba6b54d9467baed807bb2bfd",
+   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "50aaaf78b7db5bd635c19c660d59ed31b9bc9b5a",
+   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "rev": "781beceb959c68b36d3d96205b3531e341879d2c",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "eed3300c27c9f168d53e13bb198a92a147b671d0",
+   "rev": "d902abe2c36d37eb76fddd9e43290bcef3bcb6e8",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7afce91e4fcee25c1ed06dca8d71b82bed396776",
+   "rev": "6d2e06515f1ed1f74208d5a1da3a9cc26c60a7a0",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "0a294fe9bf23b396c5cc955054c50b9b652ec5ad",
+   "rev": "85e1e7143dd4cfa2b551826c27867bada60858e8",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -115,7 +115,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "1b0072fea2aa6a0ef8ef8b506ec5223b184cb4d0",
+   "rev": "5119580cd7510a440d54f67834c9024cc03a3e32",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0-rc1
+leanprover/lean4:v4.12.0