Bump mathlib

LeanAPAP.lean

@@ -1,14 +1,11 @@
 import LeanAPAP.Extras.BSG
 import LeanAPAP.FiniteField.Basic
-import LeanAPAP.Mathlib.Algebra.Algebra.Rat
 import LeanAPAP.Mathlib.Algebra.Group.AddChar
 import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Mathlib.Analysis.Normed.Field.Basic
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
 import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup
 import LeanAPAP.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanAPAP.Mathlib.Order.ConditionallyCompleteLattice.Basic
@@ -50,4 +47,5 @@ import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.LpNorm.Weighted
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 import LeanAPAP.Prereqs.NNLpNorm
+import LeanAPAP.Prereqs.Randomisation
 import LeanAPAP.Prereqs.Rudin

LeanAPAP/Physics/AlmostPeriodicity.lean

@@ -4,6 +4,7 @@ import Mathlib.Data.Complex.ExponentialBounds
 import LeanAPAP.Prereqs.Convolution.Discrete.Basic
 import LeanAPAP.Prereqs.Convolution.Norm
 import LeanAPAP.Prereqs.Curlog
+import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.MarcinkiewiczZygmund
 
 /-!

LeanAPAP/Physics/Unbalancing.lean

@@ -1,6 +1,6 @@
 import Mathlib.Algebra.Order.Group.PosPart
 import Mathlib.Data.Complex.ExponentialBounds
-import LeanAPAP.Prereqs.Convolution.Discrete.Basic
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.LpNorm.Weighted
 

LeanAPAP/Prereqs/Bohr/Basic.lean

@@ -1,6 +1,5 @@
 import Mathlib.Analysis.Complex.Basic
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
-import LeanAPAP.Prereqs.Function.Translate
 
 open AddChar Function
 open scoped NNReal ENNReal

LeanAPAP/Prereqs/Convolution/Norm.lean

@@ -1,8 +1,7 @@
 import Mathlib.Data.Real.StarOrdered
 import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
-import LeanAPAP.Prereqs.Convolution.Order
-import LeanAPAP.Prereqs.LpNorm.Compact.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 
 /-!
 # Norm of a convolution

LeanAPAP/Prereqs/FourierTransform/Discrete.lean

@@ -1,8 +1,9 @@
 import LeanAPAP.Prereqs.AddChar.MeasurableSpace
 import LeanAPAP.Prereqs.AddChar.PontryaginDuality
+import LeanAPAP.Prereqs.Convolution.Discrete.Defs
+import LeanAPAP.Prereqs.Function.Indicator.Defs
 import LeanAPAP.Prereqs.LpNorm.Compact.Inner
 import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
-import LeanAPAP.Prereqs.Convolution.Discrete.Defs
 
 /-!
 # Discrete Fourier transform

LeanAPAP/Prereqs/LpNorm/Compact/Defs.lean

@@ -1,8 +1,7 @@
 import Mathlib.Data.Finset.Density
 import Mathlib.Probability.ConditionalProbability
-import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
-import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 import LeanAPAP.Prereqs.Expect.Complex
+import LeanAPAP.Prereqs.NNLpNorm
 
 /-!
 # Normalised Lp norms

LeanAPAP/Prereqs/LpNorm/Compact/Inner.lean

@@ -1,8 +1,8 @@
 import Mathlib.Analysis.InnerProductSpace.PiL2
-import LeanAPAP.Mathlib.Algebra.Algebra.Rat
 import LeanAPAP.Mathlib.Algebra.Star.Rat
 import LeanAPAP.Prereqs.Expect.Complex
 import LeanAPAP.Prereqs.LpNorm.Compact.Defs
+import LeanAPAP.Prereqs.LpNorm.Discrete.Inner
 
 /-! # Inner product -/
 

LeanAPAP/Prereqs/LpNorm/Weighted.lean

@@ -1,4 +1,5 @@
-import LeanAPAP.Prereqs.LpNorm.Discrete.Basic
+import LeanAPAP.Prereqs.Function.Translate
+import LeanAPAP.Prereqs.LpNorm.Discrete.Defs
 
 /-!
 # Lp norms

LeanAPAP/Prereqs/Randomisation.lean

@@ -0,0 +1,38 @@
+import Mathlib.Combinatorics.Additive.Dissociation
+import LeanAPAP.Prereqs.AddChar.Basic
+import LeanAPAP.Prereqs.Expect.Complex
+
+/-!
+# Randomisation
+-/
+
+open Finset
+open scoped BigOperators ComplexConjugate
+
+variable {α : Type*} [Fintype α] [AddCommGroup α] {p : ℕ}
+
+/-- A function of dissociated support can be randomised. -/
+lemma AddDissociated.randomisation (c : AddChar α ℂ → ℝ) (d : AddChar α ℂ → ℂ)
+    (hcd : AddDissociated {ψ | d ψ ≠ 0}) : 𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re) = ∏ ψ, c ψ := by
+  refine Complex.ofReal_injective ?_
+  push_cast
+  calc
+    _ = ∑ t, (𝔼 a, ∏ ψ ∈ t, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, (c ψ : ℂ) := by
+        simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
+          Complex.re_eq_add_conj]
+    _ = (𝔼 a, ∏ ψ ∈ ∅, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ ∅ᶜ, (c ψ : ℂ) :=
+        Fintype.sum_eq_single ∅ fun t ht ↦ mul_eq_zero_of_left ?_ _
+    _ = _ := by simp
+  simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm,
+    div_eq_zero_iff, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero, compl_eq_empty_iff,
+    false_and, or_false]
+  refine sum_eq_zero fun u _ ↦ ?_
+  calc
+    𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, conj (d ψ) * conj (ψ a)
+      = ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, conj (d ψ)) * 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a := by
+        simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
+          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
+    _ = 0 := ?_
+  rw [mul_eq_zero, AddChar.expect_eq_zero_iff_ne_zero, sub_ne_zero, or_iff_not_imp_left, ← Ne,
+    mul_ne_zero_iff, prod_ne_zero_iff, prod_ne_zero_iff]
+  exact fun h ↦ hcd.ne h.1 (by simpa only [map_ne_zero] using h.2) (sdiff_ne_right.2 $ .inl ht).symm

LeanAPAP/Prereqs/Rudin.lean

@@ -1,9 +1,8 @@
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.Series
-import Mathlib.Combinatorics.Additive.Dissociation
 import LeanAPAP.Mathlib.Analysis.Complex.Basic
-import LeanAPAP.Mathlib.Data.Real.Sqrt
 import LeanAPAP.Prereqs.FourierTransform.Compact
+import LeanAPAP.Prereqs.Randomisation
 
 /-!
 # Rudin's inequality
@@ -19,32 +18,6 @@ open scoped BigOperators Nat NNReal ENNReal ComplexConjugate ComplexOrder
 
 variable {α : Type*} [Fintype α] [AddCommGroup α] {p : ℕ}
 
-/-- A function of dissociated support can be randomised. -/
-lemma AddDissociated.randomisation (c : AddChar α ℂ → ℝ) (d : AddChar α ℂ → ℂ)
-    (hcd : AddDissociated {ψ | d ψ ≠ 0}) : 𝔼 a, ∏ ψ, (c ψ + (d ψ * ψ a).re) = ∏ ψ, c ψ := by
-  refine Complex.ofReal_injective ?_
-  push_cast
-  calc
-    _ = ∑ t, (𝔼 a, ∏ ψ ∈ t, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ tᶜ, (c ψ : ℂ) := by
-        simp_rw [expect_mul, ← expect_sum_comm, ← Fintype.prod_add, add_comm,
-          Complex.re_eq_add_conj]
-    _ = (𝔼 a, ∏ ψ ∈ ∅, ((d ψ * ψ a) + conj (d ψ * ψ a)) / 2) * ∏ ψ ∈ ∅ᶜ, (c ψ : ℂ) :=
-        Fintype.sum_eq_single ∅ fun t ht ↦ mul_eq_zero_of_left ?_ _
-    _ = _ := by simp
-  simp only [map_mul, prod_div_distrib, prod_add, prod_const, ← expect_div, expect_sum_comm,
-    div_eq_zero_iff, pow_eq_zero_iff', OfNat.ofNat_ne_zero, ne_eq, card_eq_zero, compl_eq_empty_iff,
-    false_and, or_false]
-  refine sum_eq_zero fun u _ ↦ ?_
-  calc
-    𝔼 a, (∏ ψ ∈ u, d ψ * ψ a) * ∏ ψ ∈ t \ u, conj (d ψ) * conj (ψ a)
-      = ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, conj (d ψ)) * 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a := by
-        simp_rw [mul_expect, AddChar.sub_apply, AddChar.sum_apply, mul_mul_mul_comm,
-          ← prod_mul_distrib, AddChar.map_neg_eq_conj]
-    _ = 0 := ?_
-  rw [mul_eq_zero, AddChar.expect_eq_zero_iff_ne_zero, sub_ne_zero, or_iff_not_imp_left, ← Ne,
-    mul_ne_zero_iff, prod_ne_zero_iff, prod_ne_zero_iff]
-  exact fun h ↦ hcd.ne h.1 (by simpa only [map_ne_zero] using h.2) (sdiff_ne_right.2 $ .inl ht).symm
-
 variable [MeasurableSpace α] [DiscreteMeasurableSpace α]
 
 /-- **Rudin's inequality**, exponential form. -/

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a7fd140a94bbbfa40cf10839227bbb9e8492be2d",
+   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d38fb94558af9957b8f479e350841ce65a1ec42c",
+   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6c89b6765913a0d727c1066493c3f5dc51c9713e",
+   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0a756018b736ef4f4bc3c9a45fc03cf97a0b1a0c",
+   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "63cced2a6b7c4ed2afb8e6cdf7443d6dbcc975e0",
+   "rev": "00df099f8ed42c12b35cdedcfbf1fde6c7413662",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9447739fe9714f8a091192bad5cd5e7b5a8ae1e4",
+   "rev": "929690af200efb291babee737b087d244a70c3c3",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "83f718b9055972dce4f92f5b3917426b91a0d2fe",
+   "rev": "e490631b72a43a6a82b4ddd3a2d020b2029491d0",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0-rc3
+leanprover/lean4:v4.11.0