From b619bd601c7705c9fd96d91c7c0692958d1ab2e5 Mon Sep 17 00:00:00 2001 From: Thomas Zhu Date: Tue, 24 Sep 2024 21:17:18 -0400 Subject: [PATCH] Bump Lean version, finish separating points proof --- Clt/CharFun.lean | 40 ++++++++++++-------------- Clt/ExpPoly.lean | 67 +++++++++++++++++++++++------------------- Clt/Tight.lean | 2 +- lake-manifest.json | 72 ++++++++++++++++++++-------------------------- lakefile.lean | 2 +- lean-toolchain | 2 +- 6 files changed, 91 insertions(+), 94 deletions(-) diff --git a/Clt/CharFun.lean b/Clt/CharFun.lean index 0a9651c..b400bc0 100644 --- a/Clt/CharFun.lean +++ b/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 diff --git a/Clt/ExpPoly.lean b/Clt/ExpPoly.lean index a956cbd..6b39663 100644 --- a/Clt/ExpPoly.lean +++ b/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,7 +19,10 @@ These functions are a star-subalgebra of `E →ᵇ ℂ` (see `expPoly`). -/ -open scoped BigOperators + +noncomputable section + +open scoped RealInnerProductSpace open BoundedContinuousFunction Complex @@ -25,20 +30,19 @@ 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,31 +51,30 @@ 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 @@ -79,23 +82,20 @@ def expPoly : StarSubalgebra ℝ (E →ᵇ ℂ) where 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 diff --git a/Clt/Tight.lean b/Clt/Tight.lean index 8cc8300..86d25dd 100644 --- a/Clt/Tight.lean +++ b/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 => diff --git a/lake-manifest.json b/lake-manifest.json index 7e62dc1..bec225f 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,11 +1,12 @@ -{"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, @@ -13,7 +14,8 @@ {"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", diff --git a/lakefile.lean b/lakefile.lean index 29e72c2..203383e 100644 --- a/lakefile.lean +++ b/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" diff --git a/lean-toolchain b/lean-toolchain index 3f21e50..98556ba 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.5.0-rc1 +leanprover/lean4:v4.12.0-rc1