Bump mathlib

LeanAPAP.lean

@@ -5,6 +5,7 @@ import LeanAPAP.Mathlib.Algebra.BigOperators.Ring
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Analysis.Complex.Circle
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Data.Rat.Cast.Defs
 import LeanAPAP.Mathlib.Data.Rat.Cast.Lemmas
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
@@ -46,5 +47,4 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
 import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
-import LeanAPAP.Prereqs.Multinomial
 import LeanAPAP.Prereqs.Rudin

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean

@@ -1,7 +1,6 @@
 import Mathlib.Analysis.SpecialFunctions.Complex.Circle
-import LeanAPAP.Mathlib.Analysis.Complex.Circle
 
-open AddChar Multiplicative Real
+open Multiplicative Real
 open scoped ComplexConjugate Real
 
 namespace Circle
@@ -19,32 +18,4 @@ lemma exp_eq_one : expMapCircle r = 1 ↔ ∃ n : ℤ, r = n * (2 * π) := by
   simp [Subtype.ext_iff, Complex.exp_eq_one_iff, ←mul_assoc, Complex.I_ne_zero, ←
     Complex.ofReal_inj]
 
-noncomputable def e : AddChar ℝ circle where
-  toFun r := expMapCircle (2 * π * r)
-  map_zero_eq_one' := by simp
-  map_add_eq_mul' := by simp [mul_add, Complex.exp_add]
-
-lemma e_apply (r : ℝ) : e r = expMapCircle (2 * π * r) := rfl
-
-@[simp, norm_cast] lemma coe_e (r : ℝ) : ↑(e r) = Complex.exp ((2 * π * r : ℝ) * Complex.I) := rfl
-
-@[simp] lemma e_int (z : ℤ) : e z = 1 := exp_two_pi_mul_int _
-@[simp] lemma e_one : e 1 = 1 := by simpa using e_int 1
-@[simp] lemma e_add_int {z : ℤ} : e (r + z) = e r := by rw [map_add_eq_mul, e_int, mul_one]
-@[simp] lemma e_sub_int {z : ℤ} : e (r - z) = e r := by rw [map_sub_eq_div, e_int, div_one]
-@[simp] lemma e_fract (r : ℝ) : e (Int.fract r) = e r := by rw [Int.fract, e_sub_int]
-
-@[simp] lemma e_mod_div {m : ℤ} {n : ℕ} : e ((m % n : ℤ) / n) = e (m / n) := by
-  obtain hn | hn := eq_or_ne (n : ℝ) 0
-  · rw [hn, div_zero, div_zero]
-  · rw [Int.emod_def, Int.cast_sub, sub_div, Int.cast_mul, Int.cast_natCast,
-      mul_div_cancel_left₀ _ hn, e_sub_int]
-
-lemma e_eq_one : e r = 1 ↔ ∃ n : ℤ, r = n := by
-  simp [e_apply, exp_eq_one, mul_comm (2 * π), pi_ne_zero]
-
-lemma e_inj : e r = e s ↔ r ≡ s [PMOD 1] := by
-  simp [AddCommGroup.ModEq, ←e_eq_one, div_eq_one, map_sub_eq_div, eq_comm (b := 1),
-    eq_comm (a := e r)]
-
 end Circle

LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean

@@ -0,0 +1,39 @@
+import Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
+import LeanAPAP.Mathlib.Analysis.Complex.Circle
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
+
+open AddChar Multiplicative Real
+open scoped ComplexConjugate Real
+
+namespace Circle
+variable {r s : ℝ}
+
+noncomputable def e : AddChar ℝ circle where
+  toFun r := expMapCircle (2 * π * r)
+  map_zero_eq_one' := by simp
+  map_add_eq_mul' := by simp [mul_add, Complex.exp_add]
+
+lemma e_apply (r : ℝ) : e r = expMapCircle (2 * π * r) := rfl
+
+@[simp, norm_cast] lemma coe_e (r : ℝ) : ↑(e r) = Complex.exp ((2 * π * r : ℝ) * Complex.I) := rfl
+
+@[simp] lemma e_int (z : ℤ) : e z = 1 := exp_two_pi_mul_int _
+@[simp] lemma e_one : e 1 = 1 := by simpa using e_int 1
+@[simp] lemma e_add_int {z : ℤ} : e (r + z) = e r := by rw [map_add_eq_mul, e_int, mul_one]
+@[simp] lemma e_sub_int {z : ℤ} : e (r - z) = e r := by rw [map_sub_eq_div, e_int, div_one]
+@[simp] lemma e_fract (r : ℝ) : e (Int.fract r) = e r := by rw [Int.fract, e_sub_int]
+
+@[simp] lemma e_mod_div {m : ℤ} {n : ℕ} : e ((m % n : ℤ) / n) = e (m / n) := by
+  obtain hn | hn := eq_or_ne (n : ℝ) 0
+  · rw [hn, div_zero, div_zero]
+  · rw [Int.emod_def, Int.cast_sub, sub_div, Int.cast_mul, Int.cast_natCast,
+      mul_div_cancel_left₀ _ hn, e_sub_int]
+
+lemma e_eq_one : e r = 1 ↔ ∃ n : ℤ, r = n := by
+  simp [e_apply, exp_eq_one, mul_comm (2 * π), pi_ne_zero]
+
+lemma e_inj : e r = e s ↔ r ≡ s [PMOD 1] := by
+  simp [AddCommGroup.ModEq, ←e_eq_one, div_eq_one, map_sub_eq_div, eq_comm (b := 1),
+    eq_comm (a := e r)]
+
+end Circle

LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean

@@ -1,5 +1,5 @@
 import Mathlib.GroupTheory.FiniteAbelian
-import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
+import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Prereqs.AddChar.Basic
 
 /-!

LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean

@@ -1,5 +1,5 @@
 import Mathlib.Analysis.MeanInequalitiesPow
-import LeanAPAP.Prereqs.Multinomial
+import Mathlib.Data.Nat.Choose.Multinomial
 
 open Finset Fintype Nat Real
 variable {G : Type*} {A : Finset G} {m n : ℕ}
@@ -128,7 +128,7 @@ private lemma step_six {f : G → ℝ} {a b : Fin n → G} :
   simp only [←mul_assoc, pow_mul]
   refine mul_le_mul_of_nonneg_right ?_ (prod_nonneg fun i _ ↦ by positivity)
   norm_cast
-  refine double_multinomial.trans ?_
+  refine multinomial_two_mul_le_mul_multinomial.trans ?_
   rw [hk.1]
 
 private lemma step_seven {f : G → ℝ} {a b : Fin n → G} :

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3dfb59cffd1fdeaa41a92588c0d57e9a70cba8b6",
+   "rev": "41bc768e2224d6c75128a877f1d6e198859b3178",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c66fa5071dba9578bb20a3bade04bcc15c57fc2",
+   "rev": "209712c78b16c795453b6da7f7adbda4589a8f21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
+   "rev": "e7e90d90a62e6d12cbb27cbbfc31c094ee4ecc58",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "09e1ab33b2621aba98326aee36572a878b092875",
+   "rev": "19f233e7bbffce214c7b8df1f1a693958c243c77",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
+   "rev": "5e95f4776be5e048364f325c7e9d619bb56fb005",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f93115d0209de6db335725dee900d379f40c0317",
+   "rev": "5c11428272fe190b7e726ebe448f93437d057b74",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
+   "rev": "32c52a4b35ba8a3d261056e0d264de7bb94c062e",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.10.0-rc2
+leanprover/lean4:v4.10.0