Merge pull request #5 from hanwenzhu/master

Bump Lean version, finish separating points proof

Clt/CharFun.lean

@@ -28,40 +28,41 @@ import Mathlib.Probability.Notation
 -/
 
 
+noncomputable section
+
 open MeasureTheory ComplexConjugate Complex
 
 open scoped RealInnerProductSpace
 
-section character
+section Character
 
 open scoped FourierTransform Real
 
 /-- The additive character of `ℝ` given by `fun x ↦ exp (- x * I)`. -/
-noncomputable
-def probFourierChar : Multiplicative ℝ →* circle where
-  toFun z := expMapCircle (- Multiplicative.toAdd z)
-  map_one' := by simp only; rw [toAdd_one, neg_zero, expMapCircle_zero]
-  map_mul' x y := by simp only; rw [toAdd_mul, neg_add, expMapCircle_add]
+def probFourierChar : AddChar ℝ Circle where
+  toFun x := .exp (-x)
+  map_zero_eq_one' := by beta_reduce; rw [neg_zero, Circle.exp_zero]
+  map_add_eq_mul' x y := by beta_reduce; rw [neg_add, Circle.exp_add]
 
-theorem probFourierChar_apply' (x : ℝ) : probFourierChar[x] = exp (↑(-x) * I) := rfl
+theorem probFourierChar_apply' (x : ℝ) : probFourierChar x = exp (↑(-x) * I) := rfl
 
-theorem probFourierChar_apply (x : ℝ) : probFourierChar[x] = exp (- ↑x * I) := by
+theorem probFourierChar_apply (x : ℝ) : probFourierChar x = exp (- ↑x * I) := by
   simp only [probFourierChar_apply', ofReal_neg]
 
 @[continuity]
 theorem continuous_probFourierChar : Continuous probFourierChar :=
-  (map_continuous expMapCircle).comp continuous_toAdd.neg
+  Circle.exp.continuous.comp continuous_neg
 
-variable {E : Type _} [NormedAddCommGroup E] [CompleteSpace E] [NormedSpace ℂ E]
+variable {E : Type _} [NormedAddCommGroup E] [NormedSpace ℂ E]
 
 theorem fourierIntegral_probFourierChar_eq_integral_exp {V : Type _} [AddCommGroup V] [Module ℝ V]
     [MeasurableSpace V] {W : Type _} [AddCommGroup W] [Module ℝ W] (L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ)
     (μ : Measure V) (f : V → E) (w : W) :
     VectorFourier.fourierIntegral probFourierChar μ L f w =
       ∫ v : V, exp (↑(L v w) * I) • f v ∂μ := by
-  simp_rw [VectorFourier.fourierIntegral, probFourierChar_apply, ofReal_neg, neg_neg]
+  simp_rw [VectorFourier.fourierIntegral, Circle.smul_def, probFourierChar_apply, ofReal_neg, neg_neg]
 
-end character
+end Character
 
 open scoped ProbabilityTheory
 
@@ -70,16 +71,14 @@ namespace ProbabilityTheory
 variable {E : Type*} [MeasurableSpace E]
 
 /-- The characteristic function of a measure. -/
-noncomputable
 def charFun [Inner ℝ E] (μ : Measure E) (t : E) : ℂ := ∫ x, exp (⟪t, x⟫ • I) ∂μ
 
 variable [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
 lemma charFun_eq_fourierIntegral (μ : Measure E) (t : E) :
-    charFun μ t = VectorFourier.fourierIntegral probFourierChar μ sesqFormOfInner
-      (fun _ ↦ (1 : ℂ)) t := by
-  simp only [charFun, fourierIntegral_probFourierChar_eq_integral_exp, real_smul, smul_eq_mul,
-    mul_one]
+    charFun μ t = VectorFourier.fourierIntegral probFourierChar μ sesqFormOfInner 1 t := by
+  simp only [charFun, real_smul, fourierIntegral_probFourierChar_eq_integral_exp, Pi.one_apply,
+    smul_eq_mul, mul_one]
   congr
 
 @[simp]
@@ -88,13 +87,12 @@ lemma charFun_zero (μ : Measure E) [IsProbabilityMeasure μ] : charFun μ 0 = 1
     ENNReal.one_toReal, one_smul]
 
 lemma charFun_neg (μ : Measure E) (t : E) : charFun μ (-t) = conj (charFun μ t) := by
-  simp [charFun, ← integral_conj, ← exp_conj, conj_ofReal]
-  -- todo: conj_ofReal should be simp
+  simp [charFun, ← integral_conj, ← exp_conj]
 
 lemma norm_charFun_le_one (μ : Measure E) [IsProbabilityMeasure μ] (t : E) : ‖charFun μ t‖ ≤ 1 := by
   rw [charFun_eq_fourierIntegral]
   refine (VectorFourier.norm_fourierIntegral_le_integral_norm _ _ _ _ _).trans_eq ?_
-  simp only [CstarRing.norm_one, integral_const, smul_eq_mul, mul_one, measure_univ,
-    ENNReal.one_toReal]
+  simp only [Pi.one_apply, norm_one, integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul,
+    mul_one]
 
 end ProbabilityTheory

Clt/ExpPoly.lean

@@ -7,6 +7,8 @@ import Mathlib.Analysis.InnerProductSpace.Basic
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.Topology.ContinuousFunction.Compact
 import Mathlib.Analysis.Fourier.FourierTransform
+import Mathlib.Data.Real.Irrational
+import Mathlib.Topology.ContinuousFunction.StoneWeierstrass
 
 /-!
 # Exponential polynomials
@@ -17,28 +19,30 @@ These functions are a star-subalgebra of `E →ᵇ ℂ` (see `expPoly`).
 
 -/
 
-open scoped BigOperators
+
+noncomputable section
+
+open scoped RealInnerProductSpace
 
 open BoundedContinuousFunction Complex
 
 namespace Clt
 
 @[simp]
 lemma conj_exp_mul_I (x : ℝ) : starRingEnd ℂ (exp (x * I)) = exp (- x * I) := by
-  have h := coe_inv_circle_eq_conj ⟨exp (x * I), ?_⟩
-  · simp only [coe_inv_unitSphere] at h
+  have h := Circle.coe_inv_eq_conj ⟨exp (x * I), ?_⟩
+  · simp only [Circle.coe_inv] at h
     rw [← h, neg_mul, exp_neg]
-  · simp [exp_mul_I, abs_cos_add_sin_mul_I]
+  · simp [exp_mul_I, abs_cos_add_sin_mul_I, Submonoid.unitSphere]
 
 variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
 
-noncomputable
 def expInnerMulI : Multiplicative E →* (E →ᵇ ℂ) where
   toFun := fun u ↦
-    { toFun := fun x ↦ expMapCircle ⟪Multiplicative.toAdd u, x⟫_ℝ
+    { toFun := fun x ↦ Circle.exp ⟪Multiplicative.toAdd u, x⟫
       continuous_toFun := by
         -- `continuity` fails
-        refine continuous_induced_dom.comp (expMapCircle.continuous.comp ?_)
+        refine continuous_induced_dom.comp (Circle.exp.continuous.comp ?_)
         exact continuous_const.inner continuous_id
       map_bounded' := by
         refine ⟨2, fun x y ↦ ?_⟩
@@ -47,55 +51,51 @@ def expInnerMulI : Multiplicative E →* (E →ᵇ ℂ) where
         _ ≤ 1 + 1 := add_le_add (by simp) (by simp)
         _ = 2 := by ring }
   map_one' := by
-    simp only [toAdd_one, inner_zero_left, expMapCircle_zero, OneMemClass.coe_one]
+    simp only [toAdd_one, inner_zero_left, Circle.exp_zero, OneMemClass.coe_one]
     rfl
   map_mul' := fun x y ↦ by
-    simp only [toAdd_mul, expMapCircle_apply, inner_add_left, ofReal_add, add_mul, exp_add]
+    simp only [toAdd_mul, inner_add_left, Circle.exp_add, Circle.coe_mul, Circle.coe_exp]
     rfl
 
-lemma expInnerMulI_apply (u : Multiplicative E) (x : E) :
-    expInnerMulI u x = exp (⟪Multiplicative.toAdd u, x⟫_ℝ * I) := by
-  simp only [expInnerMulI, expMapCircle_apply, MonoidHom.coe_mk, OneHom.coe_mk]
+lemma expInnerMulI_apply (u x : E) :
+    expInnerMulI u x = exp (⟪u, x⟫ * I) := by
+  simp only [expInnerMulI, Circle.coe_exp, AddChar.coe_mk]
   rfl
 
-noncomputable
 def expInnerMulIₐ : AddMonoidAlgebra ℝ E →ₐ[ℝ] (E →ᵇ ℂ) :=
   AddMonoidAlgebra.lift ℝ E (E →ᵇ ℂ) expInnerMulI
 
 lemma expInnerMulIₐ_apply (x : AddMonoidAlgebra ℝ E) (v : E) :
-    expInnerMulIₐ x v = ∑ a in x.support, x a * exp (⟪a, v⟫_ℝ * I) := by
-  simp only [expInnerMulIₐ, AddMonoidAlgebra.lift_apply, expMapCircle_apply, expInnerMulI_apply]
+    expInnerMulIₐ x v = ∑ a in x.support, x a * exp (⟪a, v⟫ * I) := by
+  simp only [expInnerMulIₐ, AddMonoidAlgebra.lift_apply, Circle.exp, expInnerMulI_apply]
   rw [Finsupp.sum_of_support_subset x subset_rfl]
   · simp [expInnerMulI_apply]
+    rfl
   · simp
 
 variable (E) in
 /-- The star-subalgebra of exponential polynomials. -/
-noncomputable
 def expPoly : StarSubalgebra ℝ (E →ᵇ ℂ) where
   toSubalgebra := AlgHom.range expInnerMulIₐ
   star_mem' := by
     intro x hx
     simp only [Subsemiring.coe_carrier_toSubmonoid, Subalgebra.coe_toSubsemiring,
       AlgHom.coe_range, Set.mem_range] at hx ⊢
     obtain ⟨y, rfl⟩ := hx
-    let f : E ↪ E := ⟨fun x ↦ -x, (fun _ _ ↦ neg_inj.mp)⟩
+    set f : E ↪ E := ⟨fun x ↦ -x, (fun _ _ ↦ neg_inj.mp)⟩ with hf
     refine ⟨y.embDomain f, ?_⟩
     ext1 u
-    simp only [star_apply, IsROrC.star_def, expInnerMulIₐ_apply, Finsupp.support_embDomain,
-      Finset.sum_map, Function.Embedding.coeFn_mk, inner_neg_left, ofReal_neg, neg_mul]
-    rw [map_sum]
+    simp [expInnerMulIₐ_apply, Finsupp.support_embDomain, Finset.sum_map,
+      Finsupp.embDomain_apply, star_apply, star_sum, star_mul', RCLike.star_def, conj_ofReal,
+      conj_exp_mul_I]
     congr
     ext1 v
-    simp only [map_mul]
     congr
-    · change y.embDomain f (f v) = starRingEnd ℂ (y v)
-      rw [Finsupp.embDomain_apply, conj_ofReal] -- why is `conj_ofReal` not simp?
-    · rw [conj_exp_mul_I, neg_mul]
+    simp only [hf, Function.Embedding.coeFn_mk, inner_neg_left, ofReal_neg, neg_mul]
 
 lemma mem_expPoly (f : E →ᵇ ℂ) :
     f ∈ expPoly E
-      ↔ ∃ y : AddMonoidAlgebra ℝ E, f = fun x ↦ ∑ a in y.support, y a * exp (⟪a, x⟫_ℝ * I) := by
+      ↔ ∃ y : AddMonoidAlgebra ℝ E, f = fun x ↦ ∑ a in y.support, y a * exp (⟪a, x⟫ * I) := by
   change f ∈ AlgHom.range expInnerMulIₐ ↔ _
   simp only [AlgHom.mem_range]
   constructor
@@ -129,14 +129,23 @@ lemma expPoly_separatesPoints : ((expPoly E).map (toContinuousFunₐ E)).Separat
     exact hxy_ne (ext_inner_left ℝ h)
   obtain ⟨r, hr_ne⟩ : ∃ r : ℝ,
       cexp (((inner (r • v) x : ℝ) : ℂ) * I) ≠ cexp (((inner (r • v) y : ℝ) : ℂ) * I) := by
-    simp_rw [inner_smul_left, IsROrC.conj_to_real, ofReal_mul]
-    sorry
-  let u := AddMonoidAlgebra.single (r • v) (1 : ℝ)
+    simp_rw [inner_smul_left, RCLike.conj_to_real, ofReal_mul, ne_eq, Complex.exp_eq_exp_iff_exists_int]
+    -- use (inner v x - inner v y)⁻¹ would suffice, if we knew pi was irrational (#6718)
+    use √2 * Real.pi * (inner v x - inner v y)⁻¹
+    push_neg
+    intro n hn
+    apply irrational_sqrt_two.ne_int (n * 2)
+    rw [← sub_eq_iff_eq_add', ← sub_mul, ← mul_sub, ← mul_assoc] at hn
+    simp only [mul_eq_mul_right_iff, I_ne_zero, or_false] at hn
+    norm_cast at hn
+    rw [inv_mul_cancel_right₀ (sub_ne_zero_of_ne hv_ne)] at hn
+    simpa [← mul_assoc, Real.pi_ne_zero] using hn
+  set u := AddMonoidAlgebra.single (r • v) (1 : ℝ) with hu
   refine ⟨expInnerMulIₐ u, ⟨u, ?_⟩, ?_⟩
   · ext x
     rw [expInnerMulIₐ_apply]
   · rw [expInnerMulIₐ_apply,expInnerMulIₐ_apply]
-    simp only [ne_eq, one_ne_zero, not_false_eq_true, Finsupp.support_single_ne_zero,
+    simp only [hu, ne_eq, one_ne_zero, not_false_eq_true, Finsupp.support_single_ne_zero,
       Finset.sum_singleton, Finsupp.single_eq_same, ofReal_one, one_mul]
     exact hr_ne
 

Clt/Tight.lean

@@ -51,7 +51,7 @@ lemma tight_singleton [T2Space α] [OpensMeasurableSpace α]
     simp
   | inr hμ =>
     let r := μ Set.univ
-    have hr : 0 < r := by simp [hμ.out]
+    have hr : 0 < r := Measure.measure_univ_pos.mpr hμ.out
     intro ε hε
     cases lt_or_ge ε r with
     | inl hεr =>

lake-manifest.json

@@ -1,19 +1,21 @@
-{"version": 7,
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "ee49cf8fada1bf5a15592c399a925c401848227f",
-   "name": "std",
+   "scope": "leanprover-community",
+   "rev": "35d1cd731ad832c9f1d860c4d8ec1c7c3ab96823",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "ccba5d35d07a448fab14c0e391c8105df6e2564c",
+   "scope": "leanprover-community",
+   "rev": "2c8ae451ce9ffc83554322b14437159c1a9703f9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,73 +24,61 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "69404390bdc1de946bf0a2e51b1a69f308e56d7a",
+   "scope": "leanprover-community",
+   "rev": "a895713f7701e295a015b1087f3113fd3d615272",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "31d41415d5782a196999d4fd8eeaef3cae386a5f",
+   "scope": "leanprover-community",
+   "rev": "eb08eee94098fe530ccd6d8751a86fe405473d4c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.24",
+   "inputRev": "v0.0.42",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "a751d21d4b68c999accb6fc5d960538af26ad5ec",
+   "scope": "",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/mathlib4.git",
-   "type": "git",
-   "subDir": null,
-   "rev": "499d53818b170da7d91a3c0a7ec2073e66dc409f",
-   "name": "mathlib",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": null,
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/xubaiw/CMark.lean",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "0077cbbaa92abf855fc1c0413e158ffd8195ec77",
-   "name": "CMark",
+   "scope": "leanprover-community",
+   "rev": "fb7841a6f4fb389ec0e47dd4677844d49906af3c",
+   "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
-   "rev": "280d75fdfe7be8eb337be7f1bf8479b4aac09f71",
-   "name": "UnicodeBasic",
+   "scope": "leanprover-community",
+   "rev": "2ba60fa2c384a94735454db11a2d523612eaabff",
+   "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/hargonix/LeanInk",
-   "type": "git",
-   "subDir": null,
-   "rev": "2447df5cc6e48eb965c3c3fba87e46d353b5e9f1",
-   "name": "leanInk",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "doc-gen",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "86d5c219a9ad7aa686c9e0e704af030e203c63a1",
-   "name": "«doc-gen4»",
+   "scope": "",
+   "rev": "6d0638698bd9e481c26abc2827b7d7a53ebbc115",
+   "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "master",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "clt",

lakefile.lean

@@ -28,7 +28,7 @@ package «clt» where
   -- add any package configuration options here
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "master"
 
 meta if get_config? env = some "dev" then -- dev is so not everyone has to build it
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

lean-toolchain

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