Bump mathlib

LeanAPAP.lean

@@ -1,8 +1,6 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField
 import LeanAPAP.Integer
-import LeanAPAP.Mathlib.MeasureTheory.Function.LpSpace
-import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner
 import LeanAPAP.Physics.AlmostPeriodicity
 import LeanAPAP.Physics.DRC
 import LeanAPAP.Physics.Unbalancing

LeanAPAP/FiniteField.lean

@@ -461,8 +461,8 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
       (B.dens < (65 / 64 : ℝ) ^ i * α →
         2⁻¹ ≤ card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
     induction' i with i ih hi
-    · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp, hA,
-        by simp, by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
+    · exact ⟨G, inferInstance, inferInstance, inferInstance, inferInstance, A, by simp [n], hA,
+        by simp [α], by simp [α, nnratCast_dens, Fintype.card_subtype, subset_iff]⟩
     obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ih
     obtain hB' | hB' := le_or_lt 2⁻¹ (card V * ⟪μ_[ℝ] B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ])
     · exact ⟨V, inferInstance, inferInstance, inferInstance, inferInstance, B,
@@ -486,7 +486,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hA₀ : A.Nonempty) (hA : ThreeAPFr
         _ ≤ ‖(𝟭_[ℝ] B ∗ μ (V' : Set V).toFinset) x‖ := hx
         _ = B'.dens := ?_
       rw [mu, conv_smul, Pi.smul_apply, indicate_conv_indicate_eq_card_vadd_inter_neg,
-        norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div]
+        Real.norm_of_nonneg (by positivity), nnratCast_dens, card_preimage, smul_eq_mul, inv_mul_eq_div]
       congr 2
       · congr 1 with x
         simp

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -138,7 +138,7 @@ lemma lemma28_part_one (hm : 1 ≤ m) (x : G) :
     simp only [boole_mul, indicate_apply]
     rw [← sum_filter, filter_mem_eq_inter, univ_inter, sub_self, smul_zero]
   congr with a : 1
-  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin]
+  simp only [sum_sub_distrib, Pi.smul_apply, sum_const, card_fin, f']
 
 lemma big_shifts_step2 (L : Finset (Fin k → G)) (hk : k ≠ 0) :
     (∑ x ∈ L + S.piDiag (Fin k), ∑ l ∈ L, ∑ s ∈ S.piDiag (Fin k), ite (l + s = x) (1 : ℝ) 0) ^ 2

LeanAPAP/Physics/DRC.lean

@@ -128,7 +128,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
     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₀ ?_ ?_⟩
     · simp_rw [A₁, A₂, g, ← card_smul_mu, smul_dconv, dconv_smul, ← Nat.cast_smul_eq_nsmul ℝ,
-        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc]
+        wInner_smul_left, smul_eq_mul, star_trivial, mul_assoc, A₁, A₂]
     any_goals positivity
     all_goals exact Nat.cast_le.2 $ card_mono inter_subset_left
   rw [← sum_mul, lemma_0, nsmul_eq_mul, Nat.cast_mul, ← sum_mul, mul_right_comm, ← hgB,
@@ -156,7 +156,7 @@ lemma drc (hp₂ : 2 ≤ p) (f : G → ℝ≥0) (hf : ∃ x, x ∈ B₁ - B₂ 
         := sum_lt_sum_of_nonempty ⟨s, mem_filter.2 ⟨mem_univ _, hs.symm⟩⟩ ?_
     _ ≤ ∑ s, M * sqrt (g s) := sum_le_univ_sum_of_nonneg fun s ↦ by positivity
     _ = M * (∑ s, sqrt #(A₁ s) * sqrt #(A₂ s))
-        := by simp_rw [mul_sum, sqrt_mul $ Nat.cast_nonneg _]
+        := by simp_rw [mul_sum, g, sqrt_mul $ Nat.cast_nonneg _]
     _ ≤ M * (sqrt (∑ s, #(A₁ s)) * sqrt (∑ s, #(A₂ s))) := by
       gcongr; exact sum_sqrt_mul_sqrt_le _ fun i ↦ by positivity fun i ↦ by positivity
     _ = _ := ?_

LeanAPAP/Prereqs/Chang.lean

@@ -170,7 +170,7 @@ lemma chang (hf : f ≠ 0) (hη : 0 < η) :
       #Δ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G)⌉₊ / η ^ 2⌉₊ ∧
       largeSpec f η ⊆ Δ.addSpan := by
   refine exists_subset_addSpan_card_le_of_forall_addDissociated fun Δ hΔη hΔ ↦ ?_
-  obtain hΔ' | hΔ' := @eq_zero_or_pos _ _ #Δ
+  obtain hΔ' | hΔ' := eq_zero_or_pos #Δ
   · simp [hΔ']
   let α := ‖f‖_[1] ^ 2 / ‖f‖_[2] ^ 2 / card G
   have : 0 < α := by positivity

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -27,7 +27,7 @@ private lemma step_one (hA : A.Nonempty) (f : ι → ℝ) (a : Fin n → ι)
   calc
     |∑ i, f (a i)| ^ (m + 1)
       = |∑ i, (f (a i) - (∑ b ∈ B, f (b i)) / #B)| ^ (m + 1) := by
-      simp only [hf, sub_zero, zero_div]
+      simp only [B, hf, sub_zero, zero_div]
     _ = |(∑ b ∈ B, ∑ i, (f (a i) - f (b i))) / #B| ^ (m + 1) := by
       simp only [sum_sub_distrib]
       rw [sum_const, sub_div, sum_comm, sum_div, nsmul_eq_mul, card_piFinset, prod_const,
@@ -72,18 +72,18 @@ private lemma step_two_aux (A : Finset ι) (f : ι → ℝ) (ε : Fin n → ℝ)
     intro xy
     exact (fun i ↦ if ε i = 1 then xy.1 i else xy.2 i, fun i ↦ if ε i = 1 then xy.2 i else xy.1 i)
   have h₁ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper a ∈ (A ^^ n) ×ˢ (A ^^ n) := by
-    simp only [mem_product, and_imp, mem_piFinset, ← forall_and]
+    simp only [mem_product, and_imp, mem_piFinset, ← forall_and, swapper]
     intro a h i
     split_ifs
     · exact h i
     · exact (h i).symm
   have h₂ : ∀ a ∈ (A ^^ n) ×ˢ (A ^^ n), swapper (swapper a) = a := fun a _ ↦ by
-    ext <;> simp only <;> split_ifs <;> rfl
+    ext <;> simp only [swapper] <;> split_ifs <;> rfl
   refine sum_nbij' swapper swapper h₁ h₁ h₂ h₂ ?_
   · rintro ⟨a, b⟩ _
     congr with i : 1
-    simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply]
     simp only [mem_piFinset, mem_insert, mem_singleton] at hε
+    simp only [Pi.mul_apply, Pi.sub_apply, Function.comp_apply, swapper]
     split_ifs with h
     · simp [h]
     rw [(hε i).resolve_right h]
@@ -171,6 +171,7 @@ private lemma end_step {f : ι → ℝ} (hm : 1 ≤ m) (hA : A.Nonempty) :
         add_assoc, Nat.sub_add_cancel hm, pow_add, ← mul_pow, ← mul_pow, card_piFinset, prod_const,
         Finset.card_univ, Fintype.card_fin, Nat.cast_pow, mul_div_cancel_left₀]
       norm_num
+      dsimp [B]
       positivity
 
 namespace Real

LeanAPAP/Prereqs/NewMarcinkiewiczZygmund.lean

@@ -5,7 +5,6 @@ Authors: Yaël Dillies, Bhavik Mehta
 -/
 import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Probability.IdentDistrib
-import LeanAPAP.Mathlib.MeasureTheory.Integral.Bochner
 
 /-!
 # The Marcinkiewicz-Zygmund inequality

docbuild/lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0291556f04e89d46cd2999f0f4c1164c81778207",
+   "rev": "e9d995eaa95a4e3c880ffe94c416c34113e0f251",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"type": "path",
@@ -32,7 +32,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "470c41643209208d325a5a7315116f293c7443fb",
+   "rev": "b64b8eab8cfcf24c398e84b11c77b6555b61095a",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -42,7 +42,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
+   "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -52,7 +52,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e",
+   "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -62,7 +62,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9082fa7b9f7bcad5b4b6052a629eb9347580073a",
+   "rev": "02a6cbce220609dc6a9e5a686afa01a463643d9d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -72,10 +72,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -92,47 +92,47 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
+   "rev": "383137545783429af1317226778fd44869a711e2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

docbuild/lakefile.toml

@@ -10,4 +10,4 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.15.0"
+rev = "main"

docbuild/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.16.0-rc2

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "02a6cbce220609dc6a9e5a686afa01a463643d9d",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": null,
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,30 +35,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "383137545783429af1317226778fd44869a711e2",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -91,5 +91,5 @@
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
- "name": "LeanCamCombi",
+ "name": "LeanAPAP",
  "lakeDir": ".lake"}

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0
+leanprover/lean4:v4.16.0-rc2