diff --git a/LeanAPAP.lean b/LeanAPAP.lean index db550b977d..7e56b179cb 100644 --- a/LeanAPAP.lean +++ b/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 diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean index 19e4509ce7..87a07d3b17 100644 --- a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean +++ b/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 diff --git a/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean b/LeanAPAP/Mathlib/Analysis/SpecialFunctions/Complex/CircleAddChar.lean new file mode 100644 index 0000000000..d20c81c131 --- /dev/null +++ b/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 diff --git a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean b/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean index 9635024b71..9a563f8687 100644 --- a/LeanAPAP/Prereqs/AddChar/PontryaginDuality.lean +++ b/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 /-! diff --git a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean b/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean index 83b0d5628a..d60f8e6c3e 100644 --- a/LeanAPAP/Prereqs/MarcinkiewiczZygmund.lean +++ b/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} : diff --git a/LeanAPAP/Prereqs/Multinomial.lean b/LeanAPAP/Prereqs/Multinomial.lean deleted file mode 100644 index c85bb51f81..0000000000 --- a/LeanAPAP/Prereqs/Multinomial.lean +++ /dev/null @@ -1,25 +0,0 @@ -import Mathlib.Data.Nat.Choose.Multinomial -import Mathlib.Data.Nat.Factorial.DoubleFactorial - -open Finset - -variable {K : Type*} {s : Finset K} {f f' : K → ℕ} -namespace Nat - -lemma double_multinomial : - (multinomial s fun i ↦ 2 * f i) ≤ ((∑ i in s, f i) ^ ∑ i in s, f i) * multinomial s f := by - rw [multinomial, multinomial, ←mul_sum] - refine Nat.div_le_of_le_mul' ?_ - rw [←mul_assoc, ←Nat.mul_div_assoc _ (prod_factorial_dvd_factorial_sum _ _), - Nat.le_div_iff_mul_le] - swap - · exact prod_pos fun i _ ↦ by positivity - refine (Nat.mul_le_mul_right _ $ factorial_two_mul_le _).trans ?_ - rw [mul_pow, mul_comm, ←mul_assoc, ←mul_assoc] - refine Nat.mul_le_mul_right _ (Nat.mul_le_mul_right _ ?_) - rw [←Finset.prod_pow_eq_pow_sum, ←prod_mul_distrib] - refine prod_le_prod' fun i _ ↦ ?_ - rw [mul_comm, ←doubleFactorial_two_mul] - exact doubleFactorial_le_factorial _ - -end Nat diff --git a/lake-manifest.json b/lake-manifest.json index fca0319862..56ad1b7806 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lean-toolchain b/lean-toolchain index 6a4259fa56..7f0ea50aaa 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0-rc2 +leanprover/lean4:v4.10.0