From 9f82b0176acb4940dbe19c0a45db32309fa56ef9 Mon Sep 17 00:00:00 2001 From: tukamilano Date: Sun, 20 Sep 2026 23:02:00 +0900 Subject: [PATCH] update to v4.34 --- StatsMLlib/Analysis/FiniteSample.lean | 2 +- StatsMLlib/Analysis/MetricEntropy/Basic.lean | 4 +- .../CoveringNumber/LipschitzBall.lean | 2 +- .../FunctionClass/HilbertPredictor.lean | 2 +- .../LearningTheory/Rademacher/Complexity.lean | 2 - .../Rademacher/Symmetrization.lean | 32 ++--- StatsMLlib/LinearAlgebra/Matrix/Lieb.lean | 4 +- .../LinearAlgebra/Matrix/SingularValue.lean | 4 +- .../MeasureTheory/Function/L1Subsequence.lean | 4 +- .../Probability/Concentration/EfronStein.lean | 4 +- .../Concentration/HansonWright.lean | 22 ++-- .../Probability/Concentration/Hoeffding.lean | 1 - .../Concentration/LogSobolev/Bernoulli.lean | 14 +- .../LogSobolev/GaussianOneDim.lean | 33 +++-- .../Probability/Concentration/Maximal.lean | 2 +- .../Probability/Concentration/McDiarmid.lean | 121 +++++++++--------- .../Entropy/Conditional/Subadditivity.lean | 76 +++++------ StatsMLlib/Probability/Entropy/Duality.lean | 2 +- .../Probability/Entropy/Variational.lean | 10 +- StatsMLlib/Probability/Gaussian/Basic.lean | 8 +- .../Gaussian/Poincare/EfronStein.lean | 11 +- .../Probability/Gaussian/Poincare/Limit.lean | 2 +- .../Probability/Gaussian/Sobolev/Cutoff.lean | 51 +++++--- .../Probability/Gaussian/Sobolev/Defs.lean | 24 ++-- .../Probability/Gaussian/Sobolev/Density.lean | 21 ++- .../Gaussian/Sobolev/Mollification.lean | 32 +++-- .../Probability/Independence/FinsetPi.lean | 10 +- StatsMLlib/Probability/Process/Dudley.lean | 15 ++- .../Probability/Process/SubGaussian.lean | 2 +- .../Probability/Process/TruncatedDudley.lean | 16 +-- .../Probability/RandomMatrix/Basic.lean | 4 +- .../Probability/RandomMatrix/Bernstein.lean | 6 +- StatsMLlib/Probability/SmallBall.lean | 2 +- .../LeastSquares/L1/CoveringBound.lean | 2 +- .../Linear/EuclideanReduction.lean | 4 +- .../LeastSquares/LocalGaussianComplexity.lean | 7 +- .../LeastSquares/SubGaussianity.lean | 5 +- .../MetricSpace/CoveringNumber/Basic.lean | 10 +- .../Topology/SeparableSpace/Supremum.lean | 2 +- lake-manifest.json | 22 ++-- lakefile.lean | 4 +- lean-toolchain | 2 +- 42 files changed, 311 insertions(+), 292 deletions(-) diff --git a/StatsMLlib/Analysis/FiniteSample.lean b/StatsMLlib/Analysis/FiniteSample.lean index 6833827..3a0c22b 100644 --- a/StatsMLlib/Analysis/FiniteSample.lean +++ b/StatsMLlib/Analysis/FiniteSample.lean @@ -6,7 +6,7 @@ Authors: Sho Sonoda, Kei Tsukamoto import Mathlib.Algebra.BigOperators.Field import Mathlib.Algebra.Order.BigOperators.Group.Finset import Mathlib.Data.Fintype.Order -import Mathlib.Data.Real.Basic +import Mathlib.Basic.Real.Basic import Mathlib.Tactic.FieldSimp import Mathlib.Tactic.GCongr import Mathlib.Tactic.Ring diff --git a/StatsMLlib/Analysis/MetricEntropy/Basic.lean b/StatsMLlib/Analysis/MetricEntropy/Basic.lean index 9c17706..c54046e 100644 --- a/StatsMLlib/Analysis/MetricEntropy/Basic.lean +++ b/StatsMLlib/Analysis/MetricEntropy/Basic.lean @@ -1513,11 +1513,11 @@ redundant because `Real.log 0 = Real.log 1 = 0`. -/ lemma metricEntropyOfNat_eq_log (n : ℕ) : metricEntropyOfNat n = Real.log n := by unfold metricEntropyOfNat by_cases h : n ≤ 1 - · rw [if_pos h] + · rw [ite_eq_left h] interval_cases n · simp · simp - · rw [if_neg h] + · rw [ite_eq_right h] /-- On a totally bounded set at a positive radius, the metric entropy is the logarithm of the natural-valued covering number. -/ diff --git a/StatsMLlib/Analysis/NormedSpace/CoveringNumber/LipschitzBall.lean b/StatsMLlib/Analysis/NormedSpace/CoveringNumber/LipschitzBall.lean index 5e784b4..e77f489 100644 --- a/StatsMLlib/Analysis/NormedSpace/CoveringNumber/LipschitzBall.lean +++ b/StatsMLlib/Analysis/NormedSpace/CoveringNumber/LipschitzBall.lean @@ -159,7 +159,7 @@ lemma abs_signVector_le_one (n : ℕ) (β : Fin n → Bool) (i : ℕ) : lemma signVector_of_lt {n : ℕ} (β : Fin n → Bool) {i : ℕ} (h : i < n) : signVector n β i = if β ⟨i, h⟩ then 1 else -1 := by - rw [signVector, dif_pos h] + rw [signVector, dite_eq_left h] lemma signVector_congr {n : ℕ} {β β' : Fin n → Bool} {i : ℕ} (h : i < n) (hβ : β ⟨i, h⟩ = β' ⟨i, h⟩) : signVector n β i = signVector n β' i := by diff --git a/StatsMLlib/LearningTheory/FunctionClass/HilbertPredictor.lean b/StatsMLlib/LearningTheory/FunctionClass/HilbertPredictor.lean index a7ae6c0..877f5c5 100644 --- a/StatsMLlib/LearningTheory/FunctionClass/HilbertPredictor.lean +++ b/StatsMLlib/LearningTheory/FunctionClass/HilbertPredictor.lean @@ -110,7 +110,7 @@ private lemma rademacher_sum_norm_sq_average (σ k : ℝ) ^ 2 = |(σ k : ℝ)| ^ 2 := (sq_abs _).symm _ = 1 := by rw [abs_sigma]; norm_num _ = Fintype.card (Signs n) := by simp - simpa only [if_true] using hdiag + simpa only [ite_true] using hdiag · simpa [hkl] using rademacher_orthogonality n k l hkl calc (Fintype.card (Signs n) : ℝ)⁻¹ * diff --git a/StatsMLlib/LearningTheory/Rademacher/Complexity.lean b/StatsMLlib/LearningTheory/Rademacher/Complexity.lean index a7d1ab8..c08ff78 100644 --- a/StatsMLlib/LearningTheory/Rademacher/Complexity.lean +++ b/StatsMLlib/LearningTheory/Rademacher/Complexity.lean @@ -130,8 +130,6 @@ lemma symmetrization_signed_sup_le_add apply abs_signed_sum_le_card_mul_bound hf' intro i convert abs_sub _ _ - · rfl - · rfl · rw [←Finset.sum_sub_distrib] congr ext k diff --git a/StatsMLlib/LearningTheory/Rademacher/Symmetrization.lean b/StatsMLlib/LearningTheory/Rademacher/Symmetrization.lean index 82af86e..e7bb61a 100644 --- a/StatsMLlib/LearningTheory/Rademacher/Symmetrization.lean +++ b/StatsMLlib/LearningTheory/Rademacher/Symmetrization.lean @@ -74,19 +74,19 @@ theorem Signs.apply_abs' (σ : Signs n) (k : Fin n) : (|σ k| : ℝ) = 1 := by theorem measurable_snocEquiv: @Measurable (Ω × (Fin n → Ω)) (Fin (n + 1) → Ω) Prod.instMeasurableSpace MeasurableSpace.pi fun f ↦ Fin.snoc f.2 f.1 := by - apply measurable_pi_lambda + apply Measurable.of_eval intro i dsimp [Fin.snoc] if h : i.1 < n then have : (fun c : Ω × (Fin n → Ω) ↦ if h : ↑i < n then c.2 (i.castLT h) else c.1) = fun c ↦ c.2 (i.castLT h) := by ext c - rw [dif_pos h] + rw [dite_eq_left h] rw [this] exact Measurable.eval measurable_snd else have : (fun c : Ω × (Fin n → Ω)↦ if h : ↑i < n then c.2 (i.castLT h) else c.1) = fun c ↦ c.1 := by ext c - rw [dif_neg h] + rw [dite_eq_right h] rw [this] exact measurable_fst @@ -114,10 +114,10 @@ lemma measure_equiv : (MeasureTheory.Measure.pi (fun _ ↦ μ) : Measure (Fin n. · rintro ⟨h₁, h₂⟩ i dsimp [Fin.snoc] if h : i.1 < n then - rw [dif_pos] + rw [dite_eq_left] exact h₂ (i.castLT h) else - rw [dif_neg h] + rw [dite_eq_right h] have : i = Fin.last n := Fin.eq_last_of_not_lt h rw [this] exact h₁ @@ -230,7 +230,7 @@ lemma inineq (ω : Ω × Ω) (ω': Fin n → Ω × Ω) {c : ι → ℝ}: _ = _ := by rw [sigma_eq] simp only [inv_pow, Int.reduceNeg, - mul_eq_mul_left_iff, inv_eq_zero, ne_eq, AddLeftCancelMonoid.add_eq_zero, one_ne_zero, + mul_eq_mul_left_iff, inv_eq_zero, ne_eq, Nat.add_eq_zero_iff, one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, OfNat.ofNat_ne_zero, or_false] rfl @@ -653,9 +653,9 @@ lemma aux₃ [Countable ι] [Nonempty ι] (h𝓕 : ∀ I : ι, Measurable (f I ext i dsimp [Fin.snoc] if h : i.1 < n then - rw [dif_pos h, dif_pos h] + rw [dite_eq_left h, dite_eq_left h] else - rw [dif_neg h, dif_neg h] + rw [dite_eq_right h, dite_eq_right h] congr simp only [not_lt] at h exact Fin.last_le_iff.mp h @@ -696,10 +696,10 @@ lemma sup_abs_lemma [Nonempty ι] {V : (Z → ℝ) → ℝ} (hV₀: ∀ f, V (-f rw [←eq] dsimp if h : s.1 == 0 then - rw [if_pos h] + rw [ite_eq_left h] exact le_of_max_le_left hax else - rw [if_neg h, hV₀] + rw [ite_eq_right h, hV₀] exact le_of_max_le_right hax apply le_antisymm · apply ciSup_le @@ -713,10 +713,10 @@ lemma sup_abs_lemma [Nonempty ι] {V : (Z → ℝ) → ℝ} (hV₀: ∀ f, V (-f rintro ⟨s,i⟩ apply le_trans _ (le_ciSup hV₁ i) if h : s.1 == 0 then - rw [if_pos h] + rw [ite_eq_left h] exact le_abs_self (V (f i)) else - rw [if_neg h, hV₀] + rw [ite_eq_right h, hV₀] exact neg_le_abs (V (f i)) theorem abs_symmetrization_equation [Countable ι] [Nonempty ι] (h𝓕 : ∀ I : ι, Measurable (f I ∘ X)) @@ -753,21 +753,21 @@ theorem abs_symmetrization_equation [Countable ι] [Nonempty ι] (h𝓕 : ∀ I dsimp [f'] rintro ⟨s, I⟩ if h : s.1 == 0 then - rw [if_pos h] + rw [ite_eq_left h] dsimp exact h𝓕 I else - rw [if_neg h] + rw [ite_eq_right h] dsimp exact (h𝓕 I).neg have h𝓕'₂: ∀ I, ∀ z : Z, |f' I z| ≤ b := by rintro ⟨s,I⟩ z dsimp [f'] if h : s.1 == 0 then - rw [if_pos h] + rw [ite_eq_left h] exact h𝓕' I z else - rw [if_neg h] + rw [ite_eq_right h] simp only [Pi.neg_apply, abs_neg] exact h𝓕' I z exact symmetrization_equation h𝓕₂ h𝓕'₂ diff --git a/StatsMLlib/LinearAlgebra/Matrix/Lieb.lean b/StatsMLlib/LinearAlgebra/Matrix/Lieb.lean index 1544368..919723d 100644 --- a/StatsMLlib/LinearAlgebra/Matrix/Lieb.lean +++ b/StatsMLlib/LinearAlgebra/Matrix/Lieb.lean @@ -77,7 +77,7 @@ variable {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] theorem rayleighQuotient_mono_of_le {A B : E →ₗ[ℝ] E} (hAB : A ≤ B) {x : E} (hx : x ≠ 0) : rayleighQuotient A x ≤ rayleighQuotient B x := by - have hpos : (B - A).IsPositive := (LinearMap.le_def A B).mp hAB + have hpos : (B - A).IsPositive := LinearMap.le_def.mp hAB have hinner : 0 ≤ inner ℝ ((B - A) x) x := hpos.inner_nonneg_left x have hden : 0 < ‖x‖ ^ 2 := sq_pos_of_pos (norm_pos_iff.mpr hx) unfold rayleighQuotient @@ -114,7 +114,7 @@ functional-calculus theorem for logarithm. -/ noncomputable def realMatrixToCStarMatrixStarAlgHom : Matrix n n ℝ →⋆ₐ[ℝ] CStarMatrix n n ℂ := - (((CStarMatrix.ofMatrixStarAlgEquiv (n := n) (A := ℂ) : + ((((CStarMatrix.ofMatrixStarAlgEquiv (n := n) (A := ℂ)).toStarAlgHom : Matrix n n ℂ →⋆ₐ[ℂ] CStarMatrix n n ℂ).restrictScalars ℝ).comp (realMatrixToComplexMatrixStarAlgHom (n := n))) diff --git a/StatsMLlib/LinearAlgebra/Matrix/SingularValue.lean b/StatsMLlib/LinearAlgebra/Matrix/SingularValue.lean index 304ce55..0f17cd4 100644 --- a/StatsMLlib/LinearAlgebra/Matrix/SingularValue.lean +++ b/StatsMLlib/LinearAlgebra/Matrix/SingularValue.lean @@ -282,7 +282,7 @@ theorem orthonormal_leftSingularVector_of_singularValues_ne_zero intro i j by_cases hij : i = j · subst j - rw [if_pos rfl, inner_self_eq_norm_sq_to_K, + rw [ite_eq_left rfl, inner_self_eq_norm_sq_to_K, A.norm_leftSingularVector_of_singularValues_ne_zero i.property] norm_num · have hne : (i : Fin (Fintype.card n)) ≠ (j : Fin (Fintype.card n)) := by @@ -304,7 +304,7 @@ theorem orthonormal_leftSingularVector_of_singularValues_ne_zero _ = 0 := by rw [inner_smul_left] simp [A.rightSingularVectorBasis.inner_eq_zero hne] - rw [if_neg hij] + rw [ite_eq_right hij] unfold leftSingularVector rw [inner_smul_left, inner_smul_right, hmap] simp diff --git a/StatsMLlib/MeasureTheory/Function/L1Subsequence.lean b/StatsMLlib/MeasureTheory/Function/L1Subsequence.lean index a3dca6e..b810241 100644 --- a/StatsMLlib/MeasureTheory/Function/L1Subsequence.lean +++ b/StatsMLlib/MeasureTheory/Function/L1Subsequence.lean @@ -14,13 +14,11 @@ variable {α E : Type*} {m : MeasurableSpace α} {mu : Measure α} /-- Convergence in L^1 yields an a.e.-convergent subsequence. -/ theorem exists_seq_tendsto_ae_of_tendsto_eLpNorm_one [NormedAddCommGroup E] {f : ℕ → α → E} {g : α → E} - (hf : ∀ n, AEStronglyMeasurable (f n) mu) - (hg : AEStronglyMeasurable g mu) (hfg : Tendsto (fun n => eLpNorm (f n - g) (1 : ENNReal) mu) atTop (nhds 0)) : ∃ ns : ℕ → ℕ, StrictMono ns ∧ ∀ᵐ x ∂mu, Tendsto (fun i => f (ns i) x) atTop (nhds (g x)) := by have h_in_measure : TendstoInMeasure mu f atTop g := - tendstoInMeasure_of_tendsto_eLpNorm (p := (1 : ENNReal)) (by simp) hf hg hfg + tendstoInMeasure_of_tendsto_eLpNorm (p := (1 : ENNReal)) (by simp) hfg exact h_in_measure.exists_seq_tendsto_ae end MeasureTheory diff --git a/StatsMLlib/Probability/Concentration/EfronStein.lean b/StatsMLlib/Probability/Concentration/EfronStein.lean index c0b93fb..2d33f31 100644 --- a/StatsMLlib/Probability/Concentration/EfronStein.lean +++ b/StatsMLlib/Probability/Concentration/EfronStein.lean @@ -62,7 +62,7 @@ lemma condExpExceptCoord_stronglyMeasurable (hf : StronglyMeasurable f) : StronglyMeasurable (condExpExceptCoord (μs := μs) i f) := by unfold condExpExceptCoord apply StronglyMeasurable.integral_prod_right - exact hf.comp_measurable (measurable_pi_lambda _ (fun j => by + exact hf.comp_measurable (Measurable.of_eval (fun j => by by_cases h : j = i · subst h simp only [Function.update_self] @@ -1000,7 +1000,7 @@ lemma memLp_condExpExceptCoord (i : Fin n) (f : (Fin n → Ω) → ℝ) (hf : Me -- f = mk f on μˢ-a.e., so f ∘ update = (mk f) ∘ update on (μˢ × μ)-a.e. have hae_prod : (fun p : (Fin n → Ω) × Ω => f (Function.update p.1 i p.2)) =ᶠ[ae (μˢ.prod (μs i))] (fun p => hf.aestronglyMeasurable.mk f (Function.update p.1 i p.2)) := by - have := hmp.quasiMeasurePreserving.ae_eq hae + have := hmp.quasiMeasurePreserving.ae_eq_comp hae filter_upwards [this] with p hp exact hp -- By Fubini: for μˢ-a.e. x, the slice functions are μ-a.e. equal diff --git a/StatsMLlib/Probability/Concentration/HansonWright.lean b/StatsMLlib/Probability/Concentration/HansonWright.lean index 7a66ae5..53bd67c 100644 --- a/StatsMLlib/Probability/Concentration/HansonWright.lean +++ b/StatsMLlib/Probability/Concentration/HansonWright.lean @@ -66,7 +66,9 @@ lemma mgf_innerSL_stdGaussian {E : Type*} [NormedAddCommGroup E] [InnerProductSp have hmap : (stdGaussian E).map L = gaussianReal ((stdGaussian E)[L]) Var[L; stdGaussian E].toNNReal := IsGaussian.map_eq_gaussianReal L - have hmgf := mgf_gaussianReal hmap t + have hlaw : HasLaw (⇑L) (gaussianReal ((stdGaussian E)[L]) + Var[L; stdGaussian E].toNNReal) (stdGaussian E) := ⟨by fun_prop, hmap⟩ + have hmgf := mgf_gaussianReal hlaw t have hmean : (stdGaussian E)[L] = 0 := integral_strongDual_stdGaussian L have hvar : (Var[L; stdGaussian E].toNNReal : ℝ) = ‖v‖ ^ 2 := by rw [variance_dual_stdGaussian L] @@ -161,7 +163,7 @@ lemma randomVector_aemeasurable {μ : Measure Ω} {n : ℕ} {X : Fin n → Ω (hX_meas : ∀ i, AEMeasurable (X i) μ) : AEMeasurable (randomVector X) μ := by exact (MeasurableEquiv.toLp 2 (Fin n → ℝ)).measurable.comp_aemeasurable - (aemeasurable_pi_lambda _ hX_meas) + (AEMeasurable.of_eval hX_meas) omit [MeasurableSpace Ω] in lemma measure_map_prod_map_of_aemeasurable {α β γ δ : Type*} @@ -241,7 +243,7 @@ lemma subtypeMask_apply {n : ℕ} (s : Finset (Fin n)) (x : s → ℝ) (i : Fin lemma measurable_subtypeMask {n : ℕ} (s : Finset (Fin n)) : Measurable (subtypeMask (n := n) s) := by exact (MeasurableEquiv.toLp 2 (Fin n → ℝ)).measurable.comp - (measurable_pi_lambda _ fun i => by + (Measurable.of_eval fun i => by by_cases hi : i ∈ s · simpa [hi] using (measurable_pi_apply (⟨i, hi⟩ : s) : Measurable fun x : s → ℝ => x ⟨i, hi⟩) @@ -262,7 +264,7 @@ lemma coordinateMask_aemeasurable {μ : Measure Ω} {n : ℕ} (s : Finset (Fin n AEMeasurable (fun ω => coordinateMask s (randomVector X ω)) μ := by rw [← subtypeMask_subtype_randomVector s X] exact (measurable_subtypeMask s).aemeasurable.comp_aemeasurable - (aemeasurable_pi_lambda _ fun i => hX_meas i) + (AEMeasurable.of_eval fun i => hX_meas i) lemma coordinateMask_indepFun_compl {μ : Measure Ω} {n : ℕ} {X : Fin n → Ω → ℝ} (h_indep : iIndepFun X μ) (hX_meas : ∀ i, AEMeasurable (X i) μ) @@ -1535,7 +1537,7 @@ lemma integral_exp_quadratic_stdGaussian_le {E : Type*} [NormedAddCommGroup E] (μ := fun _ => gaussianReal 0 1)) _ ≤ ∏ i : Fin (Module.finrank ℝ E), exp (2 * exp 1 * ((θ * lam i) * 1 * exp 1)) := by - apply Finset.prod_le_prod + apply Finset.prod_le_prod₀ · intro i _ exact integral_nonneg_of_ae (ae_of_all _ fun x => exp_nonneg _) · intro i _ @@ -2387,10 +2389,6 @@ lemma integrable_exp_mul_prod_of_indepFun_hasSubgaussianMGF_of_le have hg : AEStronglyMeasurable g (μ.map φ) := by dsimp [g] fun_prop - have : IsProbabilityMeasure (μ.map X) := - MeasureTheory.Measure.isProbabilityMeasure_map hX.aemeasurable - have : IsProbabilityMeasure (μ.map Y) := - MeasureTheory.Measure.isProbabilityMeasure_map hY.aemeasurable have hprod_int : Integrable g ((μ.map Y).prod (μ.map X)) := integrable_exp_mul_snd_fst_prod_of_hasSubgaussianMGF_of_le @@ -2422,10 +2420,6 @@ lemma integral_exp_mul_prod_le_of_indepFun_hasSubgaussianMGF_of_le have hg : AEStronglyMeasurable g (μ.map φ) := by dsimp [g] fun_prop - have : IsProbabilityMeasure (μ.map X) := - MeasureTheory.Measure.isProbabilityMeasure_map hX.aemeasurable - have : IsProbabilityMeasure (μ.map Y) := - MeasureTheory.Measure.isProbabilityMeasure_map hY.aemeasurable have hmap_eq : μ.map φ = (μ.map Y).prod (μ.map X) := by simpa [φ] using (h_indep.symm.map_prod_eq_prod_map_map hY.aemeasurable hX.aemeasurable) @@ -2873,7 +2867,7 @@ lemma quadraticForm_eq_diag_add_offDiagonal {n : ℕ} by_cases hij : i = j · subst j simp - · rw [if_neg hij, if_neg hij] + · rw [ite_eq_right hij, ite_eq_right hij] ring _ = A i i * x i ^ 2 + ∑ j, (if i = j then 0 else A i j) * x i * x j := by diff --git a/StatsMLlib/Probability/Concentration/Hoeffding.lean b/StatsMLlib/Probability/Concentration/Hoeffding.lean index 65822d6..d1a3beb 100644 --- a/StatsMLlib/Probability/Concentration/Hoeffding.lean +++ b/StatsMLlib/Probability/Concentration/Hoeffding.lean @@ -79,7 +79,6 @@ theorem cgf_le_quadratic_of_nonneg [IsProbabilityMeasure μ] (t a b : ℝ) {X : · rw [← (by ring : 0 - f' x + (f' x - f'' x * (t - x)) = - f'' x * (t - x))] apply ((hasDerivAt_const x _).sub (cgf_deriv_one a b hX h x)).add convert (cgf_deriv_two a b hX h x).mul ((hasDerivAt_id' x).add_const (-t)) using 1 - · rfl · funext y simp only [Pi.mul_apply] ring diff --git a/StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean b/StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean index 9f2a0d8..829332b 100644 --- a/StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean +++ b/StatsMLlib/Probability/Concentration/LogSobolev/Bernoulli.lean @@ -133,11 +133,11 @@ theorem bernoulli_flip_invariance (j : Fin n) : by_cases h : i = j · subst h; simp only [update_self, Bool.not_not] · rw [update_of_ne h, update_of_ne h] - rw [Measure.map_smul] + have hmeas : Measurable (flipCoord j) := measurable_of_finite _ + rw [Measure.map_smul _ hmeas.aemeasurable] congr 1 -- Show count measure is invariant under bijection ext s hs - have hmeas : Measurable (flipCoord j) := measurable_of_finite _ rw [Measure.map_apply hmeas hs] have hs1 : (flipCoord j ⁻¹' s).Finite := Set.toFinite _ have hs2 : s.Finite := Set.toFinite _ @@ -1004,9 +1004,9 @@ theorem twoPointEntropyCoord_castSucc_eq_slice {n : ℕ} (j : Fin n) cases b · -- false case: if false = true then ... else ... becomes sliceFalse simp only [twoPointEntropyCoord, flipCoord_castSucc_snoc, sliceFalse, - Bool.false_eq_true, if_false] + Bool.false_eq_true, ite_false] · -- true case: if true = true then ... else ... becomes sliceTrue - simp only [twoPointEntropyCoord, flipCoord_castSucc_snoc, sliceTrue, if_true] + simp only [twoPointEntropyCoord, flipCoord_castSucc_snoc, sliceTrue, ite_true] /-- Average of twoPointEntropyCoord at castSucc j equals average of slices -/ theorem avg_twoPointEntropyCoord_castSucc {n : ℕ} (j : Fin n) @@ -1016,7 +1016,7 @@ theorem avg_twoPointEntropyCoord_castSucc {n : ℕ} (j : Fin n) (twoPointEntropyCoord j (sliceTrue h) ε' + twoPointEntropyCoord j (sliceFalse h) ε') / 2 := by rw [twoPointEntropyCoord_castSucc_eq_slice j h ε' true] rw [twoPointEntropyCoord_castSucc_eq_slice j h ε' false] - simp only [if_true, Bool.false_eq_true, if_false] + simp only [ite_true, Bool.false_eq_true, ite_false] /-- The conditional mean sqrt function: g such that g² = condMeanLast h² -/ def condMeanSqrt {n : ℕ} (h : (Fin (n+1) → Bool) → ℝ) : (Fin n → Bool) → ℝ := @@ -1273,8 +1273,8 @@ theorem toRademacher_flipCoord {n : ℕ} (j : Fin n) (ε : Fin n → Bool) : simp only [toRademacher, Function.update] by_cases h : i = j · subst h - simp only [flipCoord_same, signValue_not, dif_pos] - · simp only [dif_neg h] + simp only [flipCoord_same, signValue_not, dite_eq_left] + · simp only [dite_eq_right h] rw [flipCoord_noteq j i ε h] /-- The Rademacher sum after coordinate flip equals the shifted sum -/ diff --git a/StatsMLlib/Probability/Concentration/LogSobolev/GaussianOneDim.lean b/StatsMLlib/Probability/Concentration/LogSobolev/GaussianOneDim.lean index 6754980..5b4a950 100644 --- a/StatsMLlib/Probability/Concentration/LogSobolev/GaussianOneDim.lean +++ b/StatsMLlib/Probability/Concentration/LogSobolev/GaussianOneDim.lean @@ -150,8 +150,8 @@ lemma tendsto_eLpNorm_sq_sub_of_tendsto_L2 refine Eventually.of_forall ?_ intro x simp [norm_mul] - have h_holder' := (eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm (p := 2) (q := 2) (r := 1) - h_meas1 h_meas2 (fun a b => a * b) 1 h_bound) + have h_holder' := (eLpNorm_le_eLpNorm_mul_eLpNorm_of_norm (p := 2) (q := 2) (r := 1) + (fun a b => a * b) 1 continuous_mul h_meas1 h_meas2 h_bound) have h_eq : (fun x => (g k x)^2 - (f x)^2) = fun x => (g k x - f x) * (g k x + f x) := by ext x @@ -177,11 +177,9 @@ lemma tendsto_eLpNorm_sq_sub_of_tendsto_L2 eLpNorm (fun x => g k x + f x) 2 μ ≤ 1 + 2 * eLpNorm f 2 μ := by filter_upwards [h_eventually_small] with k hk - have h_meas1 : AEStronglyMeasurable (fun x => g k x - f x) μ := - (hg_cont k).aestronglyMeasurable.sub hf_cont.aestronglyMeasurable - have h_meas2 : AEStronglyMeasurable (fun x => (2 : ℝ) * f x) μ := - hf_cont.aestronglyMeasurable.const_mul (2 : ℝ) - have h_tri := eLpNorm_add_le h_meas1 h_meas2 (by norm_num : (1 : ℝ≥0∞) ≤ 2) + have h_tri := eLpNorm_add_le (μ := μ) (p := 2) + (f := fun x => g k x - f x) (g := fun x => (2 : ℝ) * f x) + (by norm_num : (1 : ℝ≥0∞) ≤ 2) have h_eq : (fun x => g k x + f x) = fun x => (g k x - f x) + (2 : ℝ) * f x := by funext x ring @@ -309,7 +307,9 @@ lemma tendsto_integral_norm_fderiv_sq_of_sobolev (f : ℝ → ℝ) (g : ℕ → eLpNorm (fun x => ‖fderiv ℝ f x‖ - ‖fderiv ℝ (g k) x‖) 2 μ ≤ eLpNorm (fun x => ‖fderiv ℝ f x - fderiv ℝ (g k) x‖) 2 μ := by intro k - refine eLpNorm_mono_ae ?_ + refine eLpNorm_mono_ae + (((measurable_fderiv ℝ f).norm.sub (measurable_fderiv ℝ (g k)).norm) + ).aestronglyMeasurable ?_ refine Eventually.of_forall ?_ intro x simpa [Real.norm_eq_abs] using @@ -337,8 +337,7 @@ lemma tendsto_integral_norm_fderiv_sq_of_sobolev (f : ℝ → ℝ) (g : ℕ → have h_int_g : ∀ᶠ k in atTop, Integrable (fun x => ‖fderiv ℝ (g k) x‖^2) μ := Eventually.of_forall (fun k => (hg_mem k).integrable_sq) have h_int_tend := - tendsto_integral_of_L1' (f := fun x => ‖fderiv ℝ f x‖^2) - h_int_f.aestronglyMeasurable h_int_g h_sq_tend + tendsto_integral_of_L1' (f := fun x => ‖fderiv ℝ f x‖^2) h_int_g h_sq_tend simpa using h_int_tend /-- Shifted entropy density φ(t) + 1/e ≥ 0 for t ≥ 0. -/ @@ -446,8 +445,7 @@ theorem gaussian_logSobolev_W12_real {f : ℝ → ℝ} Eventually.of_forall h_int_qk have h_m_tend : Tendsto (fun k => ∫ x, qk k x ∂μ) atTop (nhds (∫ x, q x ∂μ)) := by - have h_int_tend := tendsto_integral_of_L1' (f := q) - h_int_q.aestronglyMeasurable h_int_qk_event h_L1 + have h_int_tend := tendsto_integral_of_L1' (f := q) h_int_qk_event h_L1 simpa [q, qk] using h_int_tend have h_mlog_tend : Tendsto (fun k => @@ -538,7 +536,9 @@ theorem gaussian_logSobolev_W12_real {f : ℝ → ℝ} eLpNorm (fun x => ‖fderiv ℝ f x‖ - ‖fderiv ℝ (g k) x‖) 2 μ ≤ eLpNorm (fun x => ‖fderiv ℝ f x - fderiv ℝ (g k) x‖) 2 μ := by intro k - refine eLpNorm_mono_ae ?_ + refine eLpNorm_mono_ae + (((measurable_fderiv ℝ f).norm.sub (measurable_fderiv ℝ (g k)).norm) + ).aestronglyMeasurable ?_ refine Eventually.of_forall ?_ intro x simpa [Real.norm_eq_abs] using @@ -557,8 +557,7 @@ theorem gaussian_logSobolev_W12_real {f : ℝ → ℝ} have h_int_g : ∀ᶠ k in atTop, Integrable (fun x => ‖fderiv ℝ (g k) x‖^2) μ := Eventually.of_forall (fun k => (hg_mem k).integrable_sq) have h_int_tend := - tendsto_integral_of_L1' (f := fun x => ‖fderiv ℝ f x‖^2) - h_int_f.aestronglyMeasurable h_int_g h_norm_tend + tendsto_integral_of_L1' (f := fun x => ‖fderiv ℝ f x‖^2) h_int_g h_norm_tend simpa using h_int_tend have h_grad_bound : ∀ᶠ k in atTop, ∫ x, ‖fderiv ℝ (g k) x‖^2 ∂μ ≤ ∫ x, ‖fderiv ℝ f x‖^2 ∂μ + 1 := by @@ -668,9 +667,7 @@ theorem gaussian_logSobolev_W12_real {f : ℝ → ℝ} h_L1.comp (StrictMono.tendsto_atTop hφ_mono) obtain ⟨ns, hns_mono, h_ae_tend⟩ := exists_seq_tendsto_ae_of_tendsto_eLpNorm_one - (f := fun n x => qk (φ n) x) (g := q) - (hf := fun n => (hg_smooth (φ n)).continuous.aestronglyMeasurable.pow 2) - (hg := hf_diff.continuous.aestronglyMeasurable.pow 2) h_L1_subseq + (f := fun n x => qk (φ n) x) (g := q) h_L1_subseq let qk' : ℕ → ℝ → ℝ := fun n x => qk (φ (ns n)) x have h_ae_tend' : ∀ᵐ x ∂μ, Tendsto (fun i => qk' i x) atTop (nhds (q x)) := by diff --git a/StatsMLlib/Probability/Concentration/Maximal.lean b/StatsMLlib/Probability/Concentration/Maximal.lean index a0b320c..ece4cbb 100644 --- a/StatsMLlib/Probability/Concentration/Maximal.lean +++ b/StatsMLlib/Probability/Concentration/Maximal.lean @@ -276,7 +276,7 @@ lemma maximal_inequality_supR' simp_all only _ ≤ ∏ i ∈ s, ENNReal.ofReal (Real.exp (t ^ 2 * r i j ^ 2 / 2)) := by suffices ∀ i ∈ s, ∫⁻ (ω : Ω), ENNReal.ofReal (Real.exp (t * Y i j ω)) ∂μ ≤ ENNReal.ofReal (Real.exp (t ^ 2 * r i j ^ 2 / 2)) from by - exact Finset.prod_le_prod' this + exact Finset.prod_le_prod this intro i hi have : t ^ 2 * r i j ^ 2 / 2 = t ^ 2 * (r i j - (- r i j)) ^ 2 / 8 := by simp diff --git a/StatsMLlib/Probability/Concentration/McDiarmid.lean b/StatsMLlib/Probability/Concentration/McDiarmid.lean index fcc6d85..84008f0 100644 --- a/StatsMLlib/Probability/Concentration/McDiarmid.lean +++ b/StatsMLlib/Probability/Concentration/McDiarmid.lean @@ -93,7 +93,7 @@ theorem ProbabilityTheory.iIndepFun.comp_right have h₁ : ∀ i ∈ s, @MeasurableSet Ω (MeasurableSpace.comap (f i) (mβ i)) (f₁ i) := by intro i hi dsimp only [f₁] - rw [dif_pos hi] + rw [dite_eq_left hi] let j := invg ⟨i, hi⟩ change @MeasurableSet Ω (MeasurableSpace.comap (f i) (mβ i)) (f₁' j) have hj : g j = i := j.property.2 @@ -111,7 +111,7 @@ theorem ProbabilityTheory.iIndepFun.comp_right apply Set.mem_iInter₂_of_mem intro i hi dsimp only [f₁] - rw [dif_pos hi] + rw [dite_eq_left hi] simp only [Set.mem_iInter] at hx apply hx exact (invg ⟨i, hi⟩).2.1 @@ -121,7 +121,7 @@ theorem ProbabilityTheory.iIndepFun.comp_right Set.iInter_iInter_eq_right, Set.mem_iInter, s, f₁, invg] at hx intro i' hi' have hx := hx i' hi' - rw [dif_pos (⟨i', ⟨hi', rfl⟩⟩ : ∃ a ∈ s', g a = g i')] at hx + rw [dite_eq_left (⟨i', ⟨hi', rfl⟩⟩ : ∃ a ∈ s', g a = g i')] at hx have h₀ : g i' ∈ Finset.image g s' := (Function.Injective.mem_finset_image hg).mpr hi' have : (invg ⟨g i', h₀⟩).1 = i' := hg (invg ⟨g i', h₀⟩).2.2 rw [this] at hx @@ -141,7 +141,7 @@ theorem ProbabilityTheory.iIndepFun.comp_right apply congrArg dsimp [f₁] have : g i' ∈ s := (Function.Injective.mem_finset_image hg).mpr hi' - rw [dif_pos this] + rw [dite_eq_left this] apply congrArg apply hg exact (invg ⟨g i', this⟩).2.2.symm @@ -191,22 +191,22 @@ lemma Y_snoc_eq ext i if h : i.1 < k.1 then have : i.1<(Fin.succ k).1 := by dsimp; linarith - rw [dif_pos this, dif_pos h] - simp only [Fin.snoc, dif_pos h, cast_eq] + rw [dite_eq_left this, dite_eq_left h] + simp only [Fin.snoc, dite_eq_left h, cast_eq] exact congrArg Xk (Fin.ext rfl) else - rw [dif_neg h] + rw [dite_eq_right h] if h2 : i.1 = k.1 then have : i.1 < (Fin.succ k).1 := by dsimp; linarith - rw [dif_pos this, if_pos h2] - simp only [Fin.snoc, dif_neg h, cast_eq] + rw [dite_eq_left this, ite_eq_left h2] + simp only [Fin.snoc, dite_eq_right h, cast_eq] else have : ¬ (i.1 < (Fin.succ k).1) := by simp only [Fin.val_succ, not_lt] simp only [Fin.val_fin_lt, not_lt] at h apply Fin.val_add_one_le_of_lt exact lt_of_le_of_ne h fun a => h2 (congrArg Fin.val (id (Eq.symm a))) - rw [dif_neg this, if_neg h2] + rw [dite_eq_right this, ite_eq_right h2] variable {c' : Fin m → ℝ} @@ -227,13 +227,13 @@ lemma bound_f' ext i if hik : i.1 < k then have : i.1 < k+1 := by linarith - rw [if_pos this] + rw [ite_eq_left this] have : i ≠ ⟨k, by linarith [h']⟩:= Fin.ne_of_lt hik - rw [Function.update_of_ne this, if_pos hik] + rw [Function.update_of_ne this, ite_eq_left hik] else if hik' : i.1 = k then have : i.1 < k+1 := by linarith - rw [if_pos this] + rw [ite_eq_left this] have : i = ⟨k, by linarith [h']⟩ := Fin.eq_mk_iff_val_eq.mpr hik' rw [this, Function.update_self] else @@ -242,9 +242,9 @@ lemma bound_f' simp only [not_lt] apply Nat.succ_le_of_lt exact Nat.lt_of_le_of_ne hik (fun a ↦ hik' (id (Eq.symm a))) - rw [if_neg this] + rw [ite_eq_right this] have : i ≠ ⟨k, by linarith [h']⟩ := Fin.ne_of_val_ne hik' - rw [Function.update_of_ne this, if_neg hik] + rw [Function.update_of_ne this, ite_eq_right hik] rw [this] apply hfι have : ∑ (i : Fin (k+1)), c' ⟨i.1, by linarith [i.2, h']⟩ = (∑ (i : Fin k), c' ⟨i.1, by linarith [i.2, h']⟩) + c' ⟨k, h'⟩ := by @@ -255,7 +255,7 @@ lemma bound_f' have h' := h m (Nat.le_refl m) xi have : (fun i : Fin m ↦ if ↑i < m then x₀ else xi i) = fun _ ↦ x₀ := by ext i - rw [if_pos i.2] + rw [ite_eq_left i.2] rw [this] at h' exact h' @@ -302,13 +302,13 @@ lemma hmeasurableY = f' ∘ (fun xy : (Ω × (Fin k.1 → 𝓧)) ↦ fun (i : Fin m) ↦ if h : i.1 < k.1 then xy.2 ⟨↑i, h⟩ else X' i xy.1) := rfl rw [this] apply StronglyMeasurable.comp_measurable hf'' - apply measurable_pi_lambda + apply Measurable.of_eval intro i if h : i.1 < k.1 then have : (fun (c : Ω × (Fin k.1 → 𝓧)) ↦ if h : i.1 < k.1 then c.2 ⟨↑i, h⟩ else X' i c.1) = (fun c ↦ c ⟨i.1, h⟩) ∘ Prod.snd := by ext c - rw [dif_pos h] + rw [dite_eq_left h] simp only [Nat.succ_eq_add_one, Function.comp_apply] rw [this] apply Measurable.comp @@ -317,7 +317,7 @@ lemma hmeasurableY else have : (fun (c : Ω × (Fin k.1 → 𝓧)) ↦ if h : i.1 < k.1 then c.2 ⟨↑i, h⟩ else X' i c.1) = (X' i) ∘ Prod.fst := by ext c - rw [dif_neg h] + rw [dite_eq_right h] simp rw [this] apply Measurable.comp @@ -349,7 +349,7 @@ lemma hintegrablelefts = expressionY μ X' f' ⟨k, Nat.lt_add_one_of_le h⟩ ∘ fun x ↦ fun i ↦ X' (Fin.castLE h i) x := rfl rw [this] apply (hmeasurableY hX'' hf'' ⟨k, Nat.lt_add_one_of_le h⟩).comp - apply measurable_pi_lambda + apply Measurable.of_eval intro _ apply hX'' · let x₀ : 𝓧 := (Classical.inhabited_of_nonempty hnonempty𝓧).default @@ -380,20 +380,20 @@ lemma hintegrableAB if h₀ : i.1 < k.1 then have : (fun x_1 ↦ if h : i.1 < k.1 then Xk ⟨↑i, h⟩ else if i.1 = k.1 then x else X' i x_1) = fun _ ↦ Xk ⟨i.1, h₀⟩ := by ext x - rw [dif_pos h₀] + rw [dite_eq_left h₀] rw [this] exact measurable_const else if h₁ : i.1 = k.1 then have : (fun x_1 ↦ if h : i.1 < k.1 then Xk ⟨↑i, h⟩ else if i.1 = k.1 then x else X' i x_1) = fun _ ↦ x := by ext x - rw [dif_neg h₀, if_pos h₁] + rw [dite_eq_right h₀, ite_eq_left h₁] rw [this] exact measurable_const else have : (fun x_1 ↦ if h : i.1 < k.1 then Xk ⟨↑i, h⟩ else if i.1 = k.1 then x else X' i x_1) = fun x_1 ↦ X' i x_1 := by ext x - rw [dif_neg h₀, if_neg h₁] + rw [dite_eq_right h₀, ite_eq_right h₁] rw [this] exact hX'' i · apply MeasureTheory.HasFiniteIntegral.of_bounded _ @@ -423,16 +423,16 @@ lemma hAB ext i if h : i.1 < k.1 then have : i ≠ k := Fin.ne_of_lt h - rw [dif_pos h, Function.update_of_ne this, dif_pos h] + rw [dite_eq_left h, Function.update_of_ne this, dite_eq_left h] else - rw [dif_neg h] + rw [dite_eq_right h] if h': i.1 = k.1 then have : i=k := Fin.eq_of_val_eq h' - rw [if_pos h', this, Function.update_self] + rw [ite_eq_left h', this, Function.update_self] else - rw [if_neg h'] + rw [ite_eq_right h'] have : i ≠ k := fun a ↦ h' (congrArg Fin.val a) - rw [Function.update_of_ne this, dif_neg h, if_neg h'] + rw [Function.update_of_ne this, dite_eq_right h, ite_eq_right h'] dsimp rw [this] apply tsub_le_iff_left.mp @@ -482,26 +482,26 @@ lemma hmartingale apply congr rfl ext i if h : i.1 < k.1 then - rw [dif_pos h] + rw [dite_eq_left h] have : i.1 < k.succ := Nat.lt_succ_of_lt h - rw [dif_pos this] + rw [dite_eq_left this] dsimp - simp only [Fin.snoc, dif_pos h, Fin.castLT_mk, cast_eq] + simp only [Fin.snoc, dite_eq_left h, Fin.castLT_mk, cast_eq] else - rw [dif_neg h] + rw [dite_eq_right h] if h' : i.1 = k.1 then - rw [dif_pos h', h'] + rw [dite_eq_left h', h'] have : k.1 < k.succ := Nat.lt_add_one k.1 - rw [dif_pos this] + rw [dite_eq_left this] simp [Fin.snoc, cast_eq] rfl else - rw [dif_neg h'] + rw [dite_eq_right h'] have : ¬ i.1 < k.succ := by simp only [Fin.val_succ, not_lt] simp only [Fin.val_fin_lt, not_lt] at h exact Nat.lt_of_le_of_ne h fun a ↦ h' (id (Eq.symm a)) - rw [dif_neg this] + rw [dite_eq_right this] apply Eq.trans hlefteq have hrighteq : expressionY μ X' f' k.castSucc Xk = ∫ (ω : Ω), F ⟨(gT ω), (gS ω)⟩ ∂μ := by dsimp only [F] @@ -510,20 +510,20 @@ lemma hmartingale apply congr rfl ext i if h : i.1 < k.1 then - rw [dif_pos h] + rw [dite_eq_left h] have : i.1 < k.castSucc.1 := h - rw [dif_pos this] + rw [dite_eq_left this] else - rw [dif_neg h] + rw [dite_eq_right h] have : ¬ i.1 < k.castSucc.1 := h - rw [dif_neg this] + rw [dite_eq_right this] if h' : i.1 = k.1 then - rw [dif_pos h'] + rw [dite_eq_left h'] dsimp [gT] have : i = k := Fin.eq_of_val_eq h' rw [this] else - rw [dif_neg h'] + rw [dite_eq_right h'] apply Eq.trans _ hrighteq.symm apply double_integral_indep_eq_integral · apply StronglyMeasurable.comp_measurable hf'' @@ -533,7 +533,7 @@ lemma hmartingale have : (fun x : (T → 𝓧) × (S → 𝓧) ↦ if h : i.1 < k.1 then Xk ⟨↑i, h⟩ else if h' : i.1 = k.1 then x.1 elT else x.2 (toelS i h h')) = fun _ ↦ Xk ⟨i.1, h⟩ := by simp only [Fin.val_fin_lt] ext x - rw [dif_pos h] + rw [dite_eq_left h] rw [this] exact measurable_const else @@ -541,20 +541,20 @@ lemma hmartingale have : (fun x : (T → 𝓧) × (S → 𝓧) ↦ if h : i.1 < k.1 then Xk ⟨↑i, h⟩ else if h' : i.1 = k.1 then x.1 elT else x.2 (toelS i h h')) = fun x ↦ x.1 elT := by simp only [Fin.val_fin_lt] ext x - rw [dif_neg h, dif_pos h'] + rw [dite_eq_right h, dite_eq_left h'] rw [this] exact Measurable.eval measurable_fst else have : (fun x : (T → 𝓧) × (S → 𝓧) ↦ if h : i.1 < k.1 then Xk ⟨↑i, h⟩ else if h' : i.1 = k.1 then x.1 elT else x.2 (toelS i h h')) = fun x ↦ x.2 (toelS i h h') := by simp only [Fin.val_fin_lt] ext x - rw [dif_neg h, dif_neg h'] + rw [dite_eq_right h, dite_eq_right h'] rw [this] exact Measurable.eval measurable_snd · apply Measurable.aemeasurable - exact measurable_pi_lambda gT fun a ↦ hX'' ↑a + exact Measurable.of_eval fun a ↦ hX'' ↑a · apply Measurable.aemeasurable - exact measurable_pi_lambda gS fun a ↦ hX'' ↑a + exact Measurable.of_eval fun a ↦ hX'' ↑a · exact hindep · let x₀ : 𝓧 := (Classical.inhabited_of_nonempty hnonempty𝓧).default apply @MeasureTheory.HasFiniteIntegral.of_bounded _ _ _ _ _ _ F (|f' (fun _ ↦ x₀)| + ∑ i : Fin m, c' i) @@ -575,13 +575,13 @@ lemma hhoeffding_V let a := A k Xk - Y k.castSucc Xk let b := B k Xk - Y k.castSucc Xk have hmeasurable : Measurable (fun x ↦ Fin.snoc Xk (X' k x) : Ω → Fin (k.1+1) → 𝓧):= by - apply measurable_pi_lambda + apply Measurable.of_eval intro i if h : i.1 < k.1 then - simp only [Fin.snoc, dif_pos h, cast_eq] + simp only [Fin.snoc, dite_eq_left h, cast_eq] exact measurable_const else - simpa only [Fin.snoc, dif_neg h, cast_eq] using hX'' k + simpa only [Fin.snoc, dite_eq_right h, cast_eq] using hX'' k calc _ ≤ ((t''^2 * (b - a)^2 / 8).exp : ℝ) := by apply hoeffding μ t'' a b @@ -683,11 +683,11 @@ lemma heqind ext i if h': i.1 < k then dsimp only [Fin.snoc] - rw [dif_pos h'] + rw [dite_eq_left h'] congr else dsimp only [Fin.snoc] - rw [dif_neg h'] + rw [dite_eq_right h'] simp only [cast_eq, gT] have : i.1 = k := by simp only [Nat.succ_eq_add_one, not_lt] at h' @@ -727,7 +727,7 @@ lemma heqind = (fun x ↦ x (toelS ⟨i, h'⟩)) ∘ Prod.fst := by ext x dsimp [Fin.snoc] - rw [dif_pos h'] + rw [dite_eq_left h'] rfl rw [this] apply Measurable.comp _ measurable_fst @@ -737,14 +737,14 @@ lemma heqind = (fun x ↦ x elT) ∘ Prod.snd := by ext x dsimp [Fin.snoc] - rw [dif_neg h'] + rw [dite_eq_right h'] rw [this] apply Measurable.comp _ measurable_snd exact measurable_pi_apply elT · apply Measurable.aemeasurable - exact measurable_pi_lambda gS fun a ↦ hX'' ↑a + exact Measurable.of_eval fun a ↦ hX'' ↑a · apply Measurable.aemeasurable - exact measurable_pi_lambda gT fun a ↦ hX'' ↑a + exact Measurable.of_eval fun a ↦ hX'' ↑a · exact hindep · apply @MeasureTheory.HasFiniteIntegral.of_bounded _ _ _ _ _ _ F (t''*(bdf-E)).exp filter_upwards with ⟨a, t⟩ @@ -805,15 +805,15 @@ lemma heqind · exact measurable_const_mul t'' · apply Measurable.sub · apply (hmeasurableY hX'' hf'' (⟨k, h⟩ : Fin m).succ).comp - apply measurable_pi_lambda + apply Measurable.of_eval intro i if h' : i.1 < k then - simp only [Fin.snoc, dif_pos h', cast_eq, + simp only [Fin.snoc, dite_eq_left h', cast_eq, Fin.castLE_castSucc] change Measurable (X' _ ∘ Prod.snd) exact (hX'' _).comp measurable_snd else - simp only [Fin.snoc, dif_neg h', cast_eq] + simp only [Fin.snoc, dite_eq_right h', cast_eq] change Measurable (X' _ ∘ Prod.fst) exact (hX'' _).comp measurable_fst · have : (fun a : Ω × Ω ↦ Y (⟨k, h⟩ : Fin m).castSucc fun i ↦ X' (Fin.castLE h (Fin.castSucc i)) a.2) @@ -823,7 +823,7 @@ lemma heqind rw [this] apply (hmeasurableY hX'' hf'' (⟨k, h⟩ : Fin m).castSucc).comp apply Measurable.comp _ measurable_snd - apply measurable_pi_lambda + apply Measurable.of_eval intro i apply hX'' · filter_upwards with ω @@ -900,7 +900,6 @@ theorem mcdiarmid_inequality_aux integral_const, smul_eq_mul, Fin.val_zero, not_lt_zero, Y, expressionY, E] at hintegrable convert (ProbabilityTheory.measure_ge_le_exp_mul_mgf ε ht'' hintegrable).trans _ - · rfl · simp only [Function.comp_apply, ge_iff_le, probReal_univ, one_mul] rfl · dsimp only [mgf] diff --git a/StatsMLlib/Probability/Entropy/Conditional/Subadditivity.lean b/StatsMLlib/Probability/Entropy/Conditional/Subadditivity.lean index 008f2bc..12baf8f 100644 --- a/StatsMLlib/Probability/Entropy/Conditional/Subadditivity.lean +++ b/StatsMLlib/Probability/Entropy/Conditional/Subadditivity.lean @@ -68,11 +68,11 @@ lemma map_select_coords_prod_pi (k : Fin (n + 1)) : (fun j : Fin n => if j.val < k.val then p.1 j else p.2 j) with hφ_def -- φ is measurable have hφ_meas : Measurable φ := by - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases h : j.val < k.val - · simp only [hφ_def, if_pos h]; exact measurable_fst.eval - · simp only [hφ_def, if_neg h]; exact measurable_snd.eval + · simp only [hφ_def, ite_eq_left h]; exact measurable_fst.eval + · simp only [hφ_def, ite_eq_right h]; exact measurable_snd.eval rw [Measure.map_apply hφ_meas (MeasurableSet.univ_pi (fun j => hs j))] -- Preimage of ∏ⱼ s j under φ -- {p : p.1 j ∈ s j for j < k, p.2 j ∈ s j for j ≥ k} @@ -86,16 +86,16 @@ lemma map_select_coords_prod_pi (k : Fin (n + 1)) : constructor · intro j by_cases hj : j.val < k.val - · simp only [if_pos hj]; have := h j; simp only [if_pos hj] at this; exact this + · simp only [ite_eq_left hj]; have := h j; simp only [ite_eq_left hj] at this; exact this · simp [hj] · intro j by_cases hj : j.val < k.val · simp [hj] - · simp only [if_neg hj]; have := h j; simp only [if_neg hj] at this; exact this + · simp only [ite_eq_right hj]; have := h j; simp only [ite_eq_right hj] at this; exact this · intro ⟨hx, hy⟩ j by_cases hj : j.val < k.val - · simp only [if_pos hj]; have := hx j; simp only [if_pos hj] at this; exact this - · simp only [if_neg hj]; have := hy j; simp only [if_neg hj] at this; exact this + · simp only [ite_eq_left hj]; have := hx j; simp only [ite_eq_left hj] at this; exact this + · simp only [ite_eq_right hj]; have := hy j; simp only [ite_eq_right hj] at this; exact this rw [preimage_eq] -- Measure of product set: μˢ.prod μˢ (s₁ ×ˢ s₂) = μˢ s₁ * μˢ s₂ rw [Measure.prod_prod] @@ -106,14 +106,14 @@ lemma map_select_coords_prod_pi (k : Fin (n + 1)) : congr 1 with j by_cases hj : j.val < k.val · simp [hj] - · simp only [if_neg hj, measure_univ] + · simp only [ite_eq_right hj, measure_univ] -- Second factor: ∏ⱼ (if j < k then 1 else μs j (s j)) have factor2 : μˢ (Set.univ.pi (fun j => if j.val < k.val then Set.univ else s j)) = ∏ j : Fin n, (if j.val < k.val then 1 else μs j (s j)) := by rw [Measure.pi_pi] congr 1 with j by_cases hj : j.val < k.val - · simp only [if_pos hj, measure_univ] + · simp only [ite_eq_left hj, measure_univ] · simp [hj] rw [factor1, factor2] -- Product of factors: ∏ⱼ (if j if j.val < k.val then p.1 j else p.2 j) with hφ_def -- φ is measurable have hφ_meas : Measurable φ := by - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases h : j.val < k.val - · simp only [hφ_def, if_pos h]; exact measurable_fst.eval - · simp only [hφ_def, if_neg h]; exact measurable_snd.eval + · simp only [hφ_def, ite_eq_left h]; exact measurable_fst.eval + · simp only [hφ_def, ite_eq_right h]; exact measurable_snd.eval -- Key: φ is measure-preserving from μˢ.prod μˢ to μˢ have hφ_mp : MeasurePreserving φ (μˢ.prod μˢ) μˢ := ⟨hφ_meas, map_select_coords_prod_pi k⟩ -- f ∘ φ is integrable on μˢ.prod μˢ because f is integrable on μˢ @@ -193,11 +193,11 @@ lemma condExpFirstK_measurable (k : Fin (n + 1)) (f : (Fin n → Ω) → ℝ) (fun j : Fin n => if j.val < k.val then p.1 j else p.2 j) with hφ_def -- φ is measurable have hφ_meas' : Measurable φ := by - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases h : j.val < k.val - · simp only [hφ_def, if_pos h]; exact measurable_fst.eval - · simp only [hφ_def, if_neg h]; exact measurable_snd.eval + · simp only [hφ_def, ite_eq_left h]; exact measurable_fst.eval + · simp only [hφ_def, ite_eq_right h]; exact measurable_snd.eval -- f ∘ φ is measurable have hcomp_meas : Measurable (f ∘ φ) := hf_meas.comp hφ_meas' -- StronglyMeasurable version for the integral result @@ -237,11 +237,11 @@ lemma condExpFirstK_mul_log_integrable (k : Fin (n + 1)) (f : (Fin n → Ω) → (fun j : Fin n => if j.val < k.val then p.1 j else p.2 j) with hφ_def -- φ is measurable have hφ_meas : Measurable φ := by - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases h : j.val < k.val - · simp only [hφ_def, if_pos h]; exact measurable_fst.eval - · simp only [hφ_def, if_neg h]; exact measurable_snd.eval + · simp only [hφ_def, ite_eq_left h]; exact measurable_fst.eval + · simp only [hφ_def, ite_eq_right h]; exact measurable_snd.eval -- φ is measure-preserving have hφ_mp : MeasurePreserving φ (μˢ.prod μˢ) μˢ := ⟨hφ_meas, map_select_coords_prod_pi k⟩ -- f ∘ φ satisfies the nonnegativity condition a.e. @@ -329,11 +329,11 @@ lemma f_mul_log_condExpFirstK_integrable (k : Fin (n + 1)) (f : (Fin n → Ω) (fun j : Fin n => if j.val < k.val then p.1 j else p.2 j) with hφ_def -- φ is measurable have hφ_meas : Measurable φ := by - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases h : j.val < k.val - · simp only [hφ_def, if_pos h]; exact measurable_fst.eval - · simp only [hφ_def, if_neg h]; exact measurable_snd.eval + · simp only [hφ_def, ite_eq_left h]; exact measurable_fst.eval + · simp only [hφ_def, ite_eq_right h]; exact measurable_snd.eval -- φ is measure-preserving have hφ_mp : MeasurePreserving φ (μˢ.prod μˢ) μˢ := ⟨hφ_meas, map_select_coords_prod_pi k⟩ @@ -596,7 +596,7 @@ theorem condExpFirstK_tower_of_integrable_slice (k : Fin n) (f : (Fin n → Ω) have hG_meas : Measurable (fun p : Ω × (Fin n → Ω) => G p.1 p.2) := by simp only [G] apply hf_meas.comp - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases hj_lt : j.val < k.val · -- j < k: returns x j (constant) @@ -626,8 +626,8 @@ theorem condExpFirstK_tower_of_integrable_slice (k : Fin n) (f : (Fin n → Ω) · simp only [hj_lt, ↓reduceIte] · simp only [hj_lt, ↓reduceIte] by_cases hj_eq : j = k - · rw [hj_eq, if_pos rfl, Function.update_self] - · simp only [if_neg hj_eq, Function.update_of_ne hj_eq] + · rw [hj_eq, ite_eq_left rfl, Function.update_self] + · simp only [ite_eq_right hj_eq, Function.update_of_ne hj_eq] rw [h_eq] -- slice_func is integrable on μˢ by hslice have hslice' : Integrable slice_func μˢ := hslice @@ -676,11 +676,11 @@ theorem condExpFirstK_tower (k : Fin n) (f : (Fin n → Ω) → ℝ) -- φ is measurable have hφ_meas : Measurable φ := by - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases h : j.val < k.val - · simp only [hφ_def, if_pos h]; exact measurable_fst.eval - · simp only [hφ_def, if_neg h]; exact measurable_snd.eval + · simp only [hφ_def, ite_eq_left h]; exact measurable_fst.eval + · simp only [hφ_def, ite_eq_right h]; exact measurable_snd.eval -- Key: φ is measure-preserving from μˢ.prod μˢ to μˢ have hφ_mp : MeasurePreserving φ (μˢ.prod μˢ) μˢ := ⟨hφ_meas, map_select_coords_prod_pi k.castSucc⟩ @@ -892,11 +892,11 @@ lemma condExpFirstK_pos_on_slice_ae (i : Fin n) (f : (Fin n → Ω) → ℝ) (fun j : Fin n => if j.val < i.succ.val then p.1 j else p.2 j) with hφ_def have hφ_meas : Measurable φ := by - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases h : j.val < i.succ.val - · simp only [hφ_def, if_pos h]; exact measurable_fst.eval - · simp only [hφ_def, if_neg h]; exact measurable_snd.eval + · simp only [hφ_def, ite_eq_left h]; exact measurable_fst.eval + · simp only [hφ_def, ite_eq_right h]; exact measurable_snd.eval have hφ_mp : MeasurePreserving φ (μˢ.prod μˢ) μˢ := ⟨hφ_meas, map_select_coords_prod_pi i.succ⟩ @@ -909,8 +909,8 @@ lemma condExpFirstK_pos_on_slice_ae (i : Fin n) (f : (Fin n → Ω) → ℝ) simp only [hφ_def] congr 1 with j by_cases hj : j.val < i.succ.val - · rw [if_pos hj, if_pos hj, if_pos hj] - · rw [if_neg hj, if_neg hj] + · rw [ite_eq_left hj, ite_eq_left hj, ite_eq_left hj] + · rw [ite_eq_right hj, ite_eq_right hj] have hφ_preimage : φ ⁻¹' S = {p : (Fin n → Ω) × (Fin n → Ω) | condExpFirstK (μs := μs) i.succ f p.1 = 0 ∧ f (φ p) > 0} := by @@ -1121,7 +1121,7 @@ theorem term_le_expected_condEnt (i : Fin n) (f : (Fin n → Ω) → ℝ) have hRHS_eq : Eflogf x - Ef x * log (Ef x) = condEntExceptCoord (μs := μs) i f x := rfl have hY_meas : Measurable Y := by apply hf_meas.comp - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases hj : j = i · subst hj; simp only [Function.update_self]; exact measurable_id @@ -1133,14 +1133,14 @@ theorem term_le_expected_condEnt (i : Fin n) (f : (Fin n → Ω) → ℝ) f (fun j => if j.val < (Fin.succ i).val then w j else z j) have hg_sm : StronglyMeasurable (Function.uncurry g) := by apply StronglyMeasurable.comp_measurable hf_meas.stronglyMeasurable - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases hj : j.val < (Fin.succ i).val · simp only [hj, ↓reduceIte]; exact measurable_fst.eval · simp only [hj, ↓reduceIte]; exact measurable_snd.eval exact (hg_sm.integral_prod_right).measurable apply hT_meas.comp - apply measurable_pi_lambda + apply Measurable.of_eval intro j by_cases hj : j = i · subst hj; simp only [Function.update_self]; exact measurable_id diff --git a/StatsMLlib/Probability/Entropy/Duality.lean b/StatsMLlib/Probability/Entropy/Duality.lean index 14ef920..3d4e92e 100644 --- a/StatsMLlib/Probability/Entropy/Duality.lean +++ b/StatsMLlib/Probability/Entropy/Duality.lean @@ -371,7 +371,7 @@ lemma optimalU_in_dualEntropySet [IsProbabilityMeasure μ] filter_upwards with ω intro hY_pos show optimalU Y mean ω = ((if 0 < Y ω then log (Y ω) - log mean else 0) : ℝ) - simp only [optimalU, if_pos hY_pos] + simp only [optimalU, ite_eq_left hY_pos] · -- u * Y is integrable have h_eq : (fun ω => u ω * Y ω) =ᵐ[μ] (optimalU_mul_Y_toReal Y mean) := by filter_upwards [hY_nn] with ω hY_nn_ω diff --git a/StatsMLlib/Probability/Entropy/Variational.lean b/StatsMLlib/Probability/Entropy/Variational.lean index 2f0b434..9295a80 100644 --- a/StatsMLlib/Probability/Entropy/Variational.lean +++ b/StatsMLlib/Probability/Entropy/Variational.lean @@ -103,13 +103,13 @@ lemma integralYLogT_of_pos_on_Y (Y T : Ω → ℝ) (hT_pos_on_Y : ∀ᵐ ω ∂μ, 0 < Y ω → 0 < T ω) : integralYLogT μ Y T = ((∫ ω, Y ω * (Real.log (T ω) - Real.log (∫ ω', T ω' ∂μ)) ∂μ) : ℝ) := by - simp only [integralYLogT, if_pos hT_pos_on_Y] + simp only [integralYLogT, ite_eq_left hT_pos_on_Y] /-- When T = 0 on a set of positive measure where Y > 0, the integral is ⊥. -/ lemma integralYLogT_eq_bot (Y T : Ω → ℝ) (hT_not_pos : ¬∀ᵐ ω ∂μ, 0 < Y ω → 0 < T ω) : integralYLogT μ Y T = ⊥ := by - simp only [integralYLogT, if_neg hT_not_pos] + simp only [integralYLogT, ite_eq_right hT_not_pos] end IntegralYLogT @@ -203,14 +203,14 @@ lemma T_value_in_dualEntropySet [IsProbabilityMeasure μ] · -- U = u on {Y > 0} filter_upwards [hT_pos_on_Y] with ω hT_pos_ω intro hY_pos - simp only [U, u, if_pos (hT_pos_ω hY_pos)] + simp only [U, u, ite_eq_left (hT_pos_ω hY_pos)] · -- u * Y is integrable have h_eq : (fun ω => u ω * Y ω) =ᵐ[μ] (fun ω => Y ω * (Real.log (T ω) - Real.log mean)) := by filter_upwards [hT_nn, hY_nn, hT_pos_on_Y] with ω hT_nn_ω hY_nn_ω hT_pos_ω simp only [u] by_cases hY_pos : 0 < Y ω - · rw [if_pos (hT_pos_ω hY_pos)] + · rw [ite_eq_left (hT_pos_ω hY_pos)] ring · have hY_zero : Y ω = 0 := le_antisymm (le_of_not_gt hY_pos) hY_nn_ω simp [hY_zero] @@ -221,7 +221,7 @@ lemma T_value_in_dualEntropySet [IsProbabilityMeasure μ] filter_upwards [hT_nn, hY_nn, hT_pos_on_Y] with ω hT_nn_ω hY_nn_ω hT_pos_ω simp only [u] by_cases hY_pos : 0 < Y ω - · rw [if_pos (hT_pos_ω hY_pos)] + · rw [ite_eq_left (hT_pos_ω hY_pos)] ring · have hY_zero : Y ω = 0 := le_antisymm (le_of_not_gt hY_pos) hY_nn_ω simp [hY_zero] diff --git a/StatsMLlib/Probability/Gaussian/Basic.lean b/StatsMLlib/Probability/Gaussian/Basic.lean index 0311978..f386d7d 100644 --- a/StatsMLlib/Probability/Gaussian/Basic.lean +++ b/StatsMLlib/Probability/Gaussian/Basic.lean @@ -62,8 +62,7 @@ noncomputable def stdGaussianE (n : ℕ) : Measure (EuclideanSpace ℝ (Fin n)) /-- `stdGaussianE` is a probability measure. -/ instance stdGaussianE_isProbabilityMeasure : IsProbabilityMeasure (stdGaussianE n) := by unfold stdGaussianE - apply MeasureTheory.Measure.isProbabilityMeasure_map - exact (EuclideanSpace.equiv (Fin n) ℝ).symm.continuous.measurable.aemeasurable + infer_instance /-- Transfer of integrals: integrating f over stdGaussianE equals integrating f ∘ e.symm over stdGaussianPi. -/ lemma integral_stdGaussianE_eq (f : EuclideanSpace ℝ (Fin n) → ℝ) : @@ -91,8 +90,9 @@ lemma map_eval_stdGaussianPi (i : Fin n) : /-- MGF of coordinate projection equals standard Gaussian MGF -/ lemma mgf_eval_stdGaussianPi (i : Fin n) (t : ℝ) : mgf (fun w : Fin n → ℝ => w i) (stdGaussianPi n) t = exp (t^2 / 2) := by - have h_map : (stdGaussianPi n).map (fun w => w i) = gaussianReal 0 1 := map_eval_stdGaussianPi i - rw [mgf_gaussianReal h_map t] + have h_law : HasLaw (fun w : Fin n → ℝ => w i) (gaussianReal 0 1) (stdGaussianPi n) := + ⟨(measurable_pi_apply i).aemeasurable, map_eval_stdGaussianPi i⟩ + rw [mgf_gaussianReal h_law t] simp only [zero_mul, NNReal.coe_one, one_mul, zero_add] /-- CGF of coordinate projection equals t²/2 -/ diff --git a/StatsMLlib/Probability/Gaussian/Poincare/EfronStein.lean b/StatsMLlib/Probability/Gaussian/Poincare/EfronStein.lean index e927527..20ead97 100644 --- a/StatsMLlib/Probability/Gaussian/Poincare/EfronStein.lean +++ b/StatsMLlib/Probability/Gaussian/Poincare/EfronStein.lean @@ -322,7 +322,7 @@ open RademacherApprox /-- Rademacher random variables take values in {-1, 1} almost surely. -/ lemma rademacher_values_ae {Ω : Type*} [MeasurableSpace Ω] - {P : Measure Ω} {ε : Ω → ℝ} (hε : IsRademacher P ε) : + {P : Measure Ω} {ε : Ω → ℝ} (hmeas : AEMeasurable ε P) (hε : IsRademacher P ε) : ∀ᵐ ω ∂P, ε ω = 1 ∨ ε ω = -1 := by unfold IsRademacher at hε -- rademacherMeasure is supported on {-1, 1} @@ -338,12 +338,7 @@ lemma rademacher_values_ae {Ω : Type*} [MeasurableSpace Ω] simp } rw [← hε] at hsupp - -- ε is measurable since map ε P = rademacherMeasure ≠ 0 - have hmeas' : AEMeasurable ε P := by - apply AEMeasurable.of_map_ne_zero - rw [hε] - exact IsProbabilityMeasure.ne_zero rademacherMeasure - exact ae_of_ae_map hmeas' hsupp + exact ae_of_ae_map hmeas hsupp variable (n : ℕ) @@ -403,7 +398,7 @@ lemma aestronglyMeasurable_rademacherSumProd : /-- All coordinates are ±1 almost surely on the product space. -/ lemma coord_values_ae (i : Fin n) : ∀ᵐ x ∂(rademacherProductMeasure n), x i = 1 ∨ x i = -1 := - rademacher_values_ae (coord_isRademacher n i) + rademacher_values_ae (measurable_coord n i).aemeasurable (coord_isRademacher n i) /-- The `a⁺` function on the product space. -/ def aPlusProd (i : Fin n) (x : RademacherSpace n) : ℝ := diff --git a/StatsMLlib/Probability/Gaussian/Poincare/Limit.lean b/StatsMLlib/Probability/Gaussian/Poincare/Limit.lean index 32baf2c..a4ef8fe 100644 --- a/StatsMLlib/Probability/Gaussian/Poincare/Limit.lean +++ b/StatsMLlib/Probability/Gaussian/Poincare/Limit.lean @@ -91,7 +91,7 @@ lemma charFun_map_sum_pi_const (μ : Measure ℝ) [IsFiniteMeasure μ] (n : ℕ) This is the pushforward of `rademacherProductMeasure n` under `rademacherSumProd n`. -/ def rademacherLaw (n : ℕ) [NeZero n] : ProbabilityMeasure ℝ := ⟨(rademacherProductMeasure n).map (rademacherSumProd n), - Measure.isProbabilityMeasure_map (Measurable.aemeasurable (measurable_rademacherSumProd n))⟩ + inferInstance⟩ /-- The characteristic function of the Rademacher measure: φ(t) = cos(t). This follows from: φ(t) = (1/2)e^{it} + (1/2)e^{-it} = cos(t). -/ diff --git a/StatsMLlib/Probability/Gaussian/Sobolev/Cutoff.lean b/StatsMLlib/Probability/Gaussian/Sobolev/Cutoff.lean index abf3c9d..8642fee 100644 --- a/StatsMLlib/Probability/Gaussian/Sobolev/Cutoff.lean +++ b/StatsMLlib/Probability/Gaussian/Sobolev/Cutoff.lean @@ -203,7 +203,7 @@ lemma cutoff_L2_convergence (f : E n → ℝ) (hf : MemLp f 2 (stdGaussianE n)) have hf_sq_int : ∫⁻ x, (‖f x‖₊ : ℝ≥0∞) ^ (2 : ℝ) ∂(stdGaussianE n) < ⊤ := by have hlt := hf.eLpNorm_lt_top rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num : (2 : ℝ≥0∞) ≠ 0) - (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)] at hlt + (by norm_num : (2 : ℝ≥0∞) ≠ ⊤) hf.aestronglyMeasurable] at hlt simp only [ENNReal.toReal_ofNat, one_div, enorm_eq_nnnorm] at hlt by_contra habs push Not at habs @@ -314,8 +314,14 @@ lemma cutoff_L2_convergence (f : E n → ℝ) (hf : MemLp f 2 (stdGaussianE n)) have heLpNorm_eq : ∀ R, eLpNorm (fun x => f x * (1 - smoothCutoffR R x)) 2 (stdGaussianE n) = (∫⁻ x, F R x ∂(stdGaussianE n)) ^ (2⁻¹ : ℝ) := by intro R + have hχR_cont : Continuous (smoothCutoffR (n := n) R) := by + unfold smoothCutoffR + exact smoothCutoff_contDiff.continuous.comp (continuous_norm.div_const R) + have haesm : AEStronglyMeasurable (fun x => f x * (1 - smoothCutoffR R x)) + (stdGaussianE n) := + hf.aestronglyMeasurable.mul (continuous_const.sub hχR_cont).aestronglyMeasurable rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num : (2 : ℝ≥0∞) ≠ 0) - (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)] + (by norm_num : (2 : ℝ≥0∞) ≠ ⊤) haesm] simp only [ENNReal.toReal_ofNat, one_div, enorm_eq_nnnorm, F] simp only [heLpNorm_eq] -- rpow (1/2) is continuous, so if lintegral → 0 then lintegral^(1/2) → 0 @@ -407,7 +413,7 @@ lemma cutoff_gradient_error_bound (f : E n → ℝ) have hg_sq_int : ∫⁻ x, (‖g x‖₊ : ℝ≥0∞) ^ (2 : ℝ) ∂(stdGaussianE n) < ⊤ := by have hlt := hf_grad.eLpNorm_lt_top rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num : (2 : ℝ≥0∞) ≠ 0) - (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)] at hlt + (by norm_num : (2 : ℝ≥0∞) ≠ ⊤) hf_grad.aestronglyMeasurable] at hlt simp only [ENNReal.toReal_ofNat, one_div, enorm_eq_nnnorm, g] at hlt ⊢ by_contra habs push Not at habs @@ -466,8 +472,14 @@ lemma cutoff_gradient_error_bound (f : E n → ℝ) have heLpNorm_eq : ∀ R, eLpNorm (fun x => (1 - smoothCutoffR R x) • fderiv ℝ f x) 2 (stdGaussianE n) = (∫⁻ x, F R x ∂(stdGaussianE n)) ^ (2⁻¹ : ℝ) := by intro R + have hχR_cont : Continuous (smoothCutoffR (n := n) R) := by + unfold smoothCutoffR + exact smoothCutoff_contDiff.continuous.comp (continuous_norm.div_const R) + have haesm : AEStronglyMeasurable (fun x => (1 - smoothCutoffR R x) • g x) + (stdGaussianE n) := + (continuous_const.sub hχR_cont).aestronglyMeasurable.smul hf_grad.aestronglyMeasurable rw [MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal (by norm_num : (2 : ℝ≥0∞) ≠ 0) - (by norm_num : (2 : ℝ≥0∞) ≠ ⊤)] + (by norm_num : (2 : ℝ≥0∞) ≠ ⊤) haesm] simp only [ENNReal.toReal_ofNat, one_div, enorm_eq_nnnorm, F, g] simp only [heLpNorm_eq] have h_rpow_tendsto : Filter.Tendsto (fun R => (∫⁻ x, F R x ∂(stdGaussianE n)) ^ (2⁻¹ : ℝ)) @@ -552,7 +564,7 @@ lemma cutoff_gradient_extra_term (f : E n → ℝ) (hf : MemLp f 2 (stdGaussianE use 1 intro R hR have hf_ae : f =ᵐ[stdGaussianE n] (fun _ => (0 : ℝ)) := - (eLpNorm_eq_zero_iff hf.aestronglyMeasurable (by norm_num : (2 : ℝ≥0∞) ≠ 0)).mp hf_zero + (eLpNorm_eq_zero_iff (by norm_num : (2 : ℝ≥0∞) ≠ 0)).mp hf_zero have hgoal_ae : (fun x => f x • fderiv ℝ (smoothCutoffR R) x) =ᵐ[stdGaussianE n] (fun _ : E n => (0 : E n →L[ℝ] ℝ)) := by filter_upwards [hf_ae] with x hx @@ -560,7 +572,7 @@ lemma cutoff_gradient_extra_term (f : E n → ℝ) (hf : MemLp f 2 (stdGaussianE have h1 : eLpNorm (fun x => f x • fderiv ℝ (smoothCutoffR R) x) 2 (stdGaussianE n) = eLpNorm (fun _ : E n => (0 : E n →L[ℝ] ℝ)) 2 (stdGaussianE n) := eLpNorm_congr_ae hgoal_ae have h2 : eLpNorm (fun _ : E n => (0 : E n →L[ℝ] ℝ)) 2 (stdGaussianE n) = 0 := - eLpNorm_zero' (α := E n) (ε := E n →L[ℝ] ℝ) (p := 2) (μ := stdGaussianE n) + eLpNorm_fun_zero (α := E n) (ε := E n →L[ℝ] ℝ) (p := 2) (μ := stdGaussianE n) rw [h1, h2] exact le_of_lt hε · -- If ||f||_2 ≠ 0 @@ -605,11 +617,17 @@ lemma cutoff_gradient_extra_term (f : E n → ℝ) (hf : MemLp f 2 (stdGaussianE rwa [div_mul_cancel₀ _ hε_ne] at this linarith -- Use eLpNorm_mono and the pointwise bound + have hne : ((⊤ : ℕ∞) : WithTop ℕ∞) ≠ 0 := WithTop.coe_ne_zero.mpr ENat.top_ne_zero + have hcont_fderiv : Continuous (fun x : E n => fderiv ℝ (smoothCutoffR (n := n) R) x) := + (smoothCutoffR_contDiff (n := n) hR_pos).continuous_fderiv hne + have hprod_meas : AEStronglyMeasurable + (fun x => f x • fderiv ℝ (smoothCutoffR R) x) (stdGaussianE n) := + hf.aestronglyMeasurable.smul hcont_fderiv.aestronglyMeasurable have heLpNorm_le : eLpNorm (fun x => f x • fderiv ℝ (smoothCutoffR R) x) 2 (stdGaussianE n) ≤ ENNReal.ofReal (C / R) * eLpNorm f 2 (stdGaussianE n) := by calc eLpNorm (fun x => f x • fderiv ℝ (smoothCutoffR R) x) 2 (stdGaussianE n) ≤ eLpNorm (fun x => (C / R) * ‖f x‖) 2 (stdGaussianE n) := by - apply MeasureTheory.eLpNorm_mono_real + apply MeasureTheory.eLpNorm_mono_real hprod_meas intro x exact hfact x _ = ENNReal.ofReal (C / R) * eLpNorm (fun x => ‖f x‖) 2 (stdGaussianE n) := by @@ -622,7 +640,7 @@ lemma cutoff_gradient_extra_term (f : E n → ℝ) (hf : MemLp f 2 (stdGaussianE exact Real.enorm_eq_ofReal hCR_nneg _ = ENNReal.ofReal (C / R) * eLpNorm f 2 (stdGaussianE n) := by congr 1 - exact eLpNorm_norm (f := f) + exact eLpNorm_norm f hf.aestronglyMeasurable calc eLpNorm (fun x => f x • fderiv ℝ (smoothCutoffR R) x) 2 (stdGaussianE n) ≤ ENNReal.ofReal (C / R) * eLpNorm f 2 (stdGaussianE n) := heLpNorm_le _ = ENNReal.ofReal (C / R) * ENNReal.ofReal (eLpNorm f 2 (stdGaussianE n)).toReal := by @@ -812,14 +830,11 @@ lemma eLpNorm_norm_add_le {α : Type*} [MeasurableSpace α] {μ : Measure α} {E : Type*} [NormedAddCommGroup E] {f g : α → E} (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : eLpNorm (fun x => ‖f x‖ + ‖g x‖) 2 μ ≤ eLpNorm f 2 μ + eLpNorm g 2 μ := by - -- Pre-compute norm measurability to avoid repeated elaboration - have hfn : AEStronglyMeasurable (fun x => ‖f x‖) μ := hf.norm - have hgn : AEStronglyMeasurable (fun x => ‖g x‖) μ := hg.norm have h1 : (fun x => ‖f x‖ + ‖g x‖) = (fun x => ‖f x‖) + (fun x => ‖g x‖) := rfl rw [h1] - have hadd := eLpNorm_add_le hfn hgn (by norm_num : (1 : ℝ≥0∞) ≤ 2) - simp only [eLpNorm_norm] at hadd - exact hadd + have hadd := eLpNorm_add_le (μ := μ) (p := 2) (f := fun x => ‖f x‖) (g := fun x => ‖g x‖) + (by norm_num : (1 : ℝ≥0∞) ≤ 2) + rwa [eLpNorm_norm f hf, eLpNorm_norm g hg] at hadd /-- The cutoff f^(R) = f·χ_R converges to f in the W^{1,2}(γ) Sobolev norm as R → ∞. -/ theorem tendsto_cutoff_W12 (f : E n → ℝ) (hf : MemW12Gaussian n f (stdGaussianE n)) : @@ -884,7 +899,8 @@ theorem tendsto_cutoff_W12 (f : E n → ℝ) (hf : MemW12Gaussian n f (stdGaussi · -- Eventually LHS ≤ RHS (only need for R > 0) filter_upwards [Filter.eventually_gt_atTop (0 : ℝ)] with R (hR_pos : 0 < R) -- Need: ||∇(f * χ_R - f)|| ≤ ||(1-χ_R)∇f|| + ||f∇χ_R|| - rw [eLpNorm_norm (f := fun x => fderiv ℝ (f * smoothCutoffR R - f) x)] + rw [eLpNorm_norm (fun x => fderiv ℝ (f * smoothCutoffR R - f) x) + (measurable_fderiv ℝ (f * smoothCutoffR R - f)).aestronglyMeasurable] have hnorm_bound : ∀ x, ‖fderiv ℝ (f * smoothCutoffR R - f) x‖ ≤ ‖f x • fderiv ℝ (smoothCutoffR R) x‖ + ‖(1 - smoothCutoffR R x) • fderiv ℝ f x‖ := by intro x @@ -1024,7 +1040,10 @@ theorem tendsto_cutoff_W12 (f : E n → ℝ) (hf : MemW12Gaussian n f (stdGaussi -- Step 1: Use pointwise bound have hstep1 : eLpNorm (fun x => fderiv ℝ (f * smoothCutoffR R - f) x) 2 (stdGaussianE n) ≤ eLpNorm (fun x => ‖term2 x‖ + ‖term1 x‖) 2 (stdGaussianE n) := by - apply eLpNorm_mono_real; intro x; exact hnorm_bound x + apply eLpNorm_mono_real + (measurable_fderiv ℝ (f * smoothCutoffR R - f)).aestronglyMeasurable + intro x + exact hnorm_bound x -- Step 2: Triangle inequality for eLpNorm using helper have hmeas1 : AEStronglyMeasurable term2 (stdGaussianE n) := hf_L2.aestronglyMeasurable.smul hcont_fderiv.aestronglyMeasurable diff --git a/StatsMLlib/Probability/Gaussian/Sobolev/Defs.lean b/StatsMLlib/Probability/Gaussian/Sobolev/Defs.lean index 6ae40bc..5598ad8 100644 --- a/StatsMLlib/Probability/Gaussian/Sobolev/Defs.lean +++ b/StatsMLlib/Probability/Gaussian/Sobolev/Defs.lean @@ -83,19 +83,21 @@ lemma memW12Gaussian_iff_sobolevNormSq_lt_top {f : E n → ℝ} AEStronglyMeasurable f γ ∧ AEStronglyMeasurable (fun x ↦ fderiv ℝ f x) γ := by simp only [MemW12Gaussian, GaussianSobolevNormSq, MemLp] - -- Use: eLpNorm (‖g ·‖) p μ = eLpNorm g p μ - have heq : eLpNorm (fun x ↦ ‖fderiv ℝ f x‖) 2 γ = eLpNorm (fun x ↦ fderiv ℝ f x) 2 γ := - MeasureTheory.eLpNorm_norm (fun x ↦ fderiv ℝ f x) - rw [heq] constructor - · rintro ⟨⟨hf_meas, hf_norm⟩, hdf_meas, hdf_norm⟩ - refine ⟨?_, hf_meas, hdf_meas⟩ - exact ENNReal.add_lt_top.mpr ⟨ENNReal.pow_lt_top hf_norm, ENNReal.pow_lt_top hdf_norm⟩ + · rintro ⟨hf_norm, hdf_norm⟩ + have hf_meas : AEStronglyMeasurable f γ := + aestronglyMeasurable_of_eLpNorm_ne_top hf_norm.ne + have hdf_meas : AEStronglyMeasurable (fun x ↦ fderiv ℝ f x) γ := + aestronglyMeasurable_of_eLpNorm_ne_top hdf_norm.ne + -- Use: eLpNorm (‖g ·‖) p μ = eLpNorm g p μ + rw [MeasureTheory.eLpNorm_norm _ hdf_meas] + exact ⟨ENNReal.add_lt_top.mpr ⟨ENNReal.pow_lt_top hf_norm, ENNReal.pow_lt_top hdf_norm⟩, + hf_meas, hdf_meas⟩ · rintro ⟨hsum, hf_meas, hdf_meas⟩ - have ⟨h1, h2⟩ := ENNReal.add_lt_top.mp hsum - refine ⟨⟨hf_meas, ?_⟩, hdf_meas, ?_⟩ - · exact (ENNReal.pow_lt_top_iff.mp h1).resolve_right (by decide) - · exact (ENNReal.pow_lt_top_iff.mp h2).resolve_right (by decide) + rw [MeasureTheory.eLpNorm_norm _ hdf_meas] at hsum + obtain ⟨h1, h2⟩ := ENNReal.add_lt_top.mp hsum + exact ⟨(ENNReal.pow_lt_top_iff.mp h1).resolve_right (by decide), + (ENNReal.pow_lt_top_iff.mp h2).resolve_right (by decide)⟩ /-! ### Smooth Cutoff Functions -/ diff --git a/StatsMLlib/Probability/Gaussian/Sobolev/Density.lean b/StatsMLlib/Probability/Gaussian/Sobolev/Density.lean index 026b250..36a581b 100644 --- a/StatsMLlib/Probability/Gaussian/Sobolev/Density.lean +++ b/StatsMLlib/Probability/Gaussian/Sobolev/Density.lean @@ -75,11 +75,10 @@ lemma ennreal_sq_add_le (a b : ℝ≥0∞) : (a + b)^2 ≤ 2 * a^2 + 2 * b^2 := _ = 2 * a^2 + 2 * b^2 := by ring /-- Triangle inequality for eLpNorm squared when p ≥ 1 -/ -lemma eLpNorm_add_sq_le' (f g : E n → ℝ) (μ : Measure (E n)) - (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ) : +lemma eLpNorm_add_sq_le' (f g : E n → ℝ) (μ : Measure (E n)) : eLpNorm (f + g) 2 μ ^ 2 ≤ 2 * eLpNorm f 2 μ ^ 2 + 2 * eLpNorm g 2 μ ^ 2 := by have h2 : (1 : ℝ≥0∞) ≤ 2 := by norm_num - have htri := eLpNorm_add_le hf hg h2 + have htri := eLpNorm_add_le (μ := μ) (p := 2) (f := f) (g := g) h2 calc eLpNorm (f + g) 2 μ ^ 2 ≤ (eLpNorm f 2 μ + eLpNorm g 2 μ)^2 := ENNReal.pow_le_pow_left htri _ ≤ 2 * eLpNorm f 2 μ ^ 2 + 2 * eLpNorm g 2 μ ^ 2 := ennreal_sq_add_le _ _ @@ -88,7 +87,6 @@ lemma eLpNorm_add_sq_le' (f g : E n → ℝ) (μ : Measure (E n)) /-- Triangle inequality for GaussianSobolevNormSq for differentiable functions -/ lemma gaussianSobolevNormSq_add_le_of_diff (f g : E n → ℝ) (γ : Measure (E n)) - (hf : AEStronglyMeasurable f γ) (hg : AEStronglyMeasurable g γ) (hf_diff : Differentiable ℝ f) (hg_diff : Differentiable ℝ g) (hf_cont : Continuous (fun x => fderiv ℝ f x)) (hg_cont : Continuous (fun x => fderiv ℝ g x)) : @@ -96,7 +94,7 @@ lemma gaussianSobolevNormSq_add_le_of_diff (f g : E n → ℝ) (γ : Measure (E 2 * GaussianSobolevNormSq n f γ + 2 * GaussianSobolevNormSq n g γ := by simp only [GaussianSobolevNormSq] -- L² term uses the triangle inequality - have hL2 := eLpNorm_add_sq_le' f g γ hf hg + have hL2 := eLpNorm_add_sq_le' f g γ -- Gradient term: use that fderiv (f + g) = fderiv f + fderiv g for differentiable functions have hgrad_eq : ∀ x, fderiv ℝ (f + g) x = fderiv ℝ f x + fderiv ℝ g x := by intro x @@ -115,12 +113,14 @@ lemma gaussianSobolevNormSq_add_le_of_diff (f g : E n → ℝ) (γ : Measure (E have hmono : eLpNorm (fun x => ‖fderiv ℝ (f + g) x‖) 2 γ ≤ eLpNorm (fun x => ‖fderiv ℝ f x‖ + ‖fderiv ℝ g x‖) 2 γ := by apply eLpNorm_mono_real + (((measurable_fderiv ℝ (f + g)).norm).aestronglyMeasurable) intro x simp only [Real.norm_eq_abs, abs_norm] exact hgrad_bound x -- Triangle inequality for gradient L² norms have h2 : (1 : ℝ≥0∞) ≤ 2 := by norm_num - have hgrad_tri := eLpNorm_add_le hf_norm_aesm hg_norm_aesm h2 + have hgrad_tri := eLpNorm_add_le (μ := γ) (p := 2) + (f := fun x => ‖fderiv ℝ f x‖) (g := fun x => ‖fderiv ℝ g x‖) h2 -- Combine bounds for gradient term have hgrad : eLpNorm (fun x => ‖fderiv ℝ (f + g) x‖) 2 γ ^ 2 ≤ 2 * eLpNorm (fun x => ‖fderiv ℝ f x‖) 2 γ ^ 2 + @@ -147,9 +147,8 @@ lemma exists_lt_of_tendsto_nhdsWithin_right {f : ℝ → ℝ≥0∞} {b : ℝ≥ (hf : Tendsto f (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)) (hb : 0 < b) : ∃ ε : ℝ, 0 < ε ∧ f ε < b := by -- Use the Filter.Tendsto.eventually to get f x < b eventually - have hev : ∀ᶠ x in nhdsWithin (0 : ℝ) (Set.Ioi 0), f x < b := by - apply hf.eventually - exact Iio_mem_nhds hb + have hev : ∀ᶠ x in nhdsWithin (0 : ℝ) (Set.Ioi 0), f x < b := + hf.eventually (p := fun y => y < b) (Iio_mem_nhds hb) -- nhdsWithin 0 (Ioi 0) is the right filter rw [Filter.Eventually, mem_nhdsWithin] at hev obtain ⟨U, hU_open, h0U, hU_prop⟩ := hev @@ -258,7 +257,7 @@ theorem exists_smooth_compactSupport_approx (f : E n → ℝ) (hf : MemW12Gaussi exact hcont.congr (fun x => (heq x).symm) -- AE measurability - have hf_aesm : AEStronglyMeasurable f (stdGaussianE n) := hf.1.1 + have hf_aesm : AEStronglyMeasurable f (stdGaussianE n) := hf.1.aestronglyMeasurable have hfχ_aesm : AEStronglyMeasurable (f * smoothCutoffR R) (stdGaussianE n) := by apply AEStronglyMeasurable.mul hf_aesm exact (smoothCutoffR_contDiff hR).continuous.aestronglyMeasurable @@ -276,7 +275,7 @@ theorem exists_smooth_compactSupport_approx (f : E n → ℝ) (hf : MemW12Gaussi -- Apply triangle inequality have htriangle := gaussianSobolevNormSq_add_le_of_diff (f - f * smoothCutoffR R) (f * smoothCutoffR R - g) (stdGaussianE n) - h1_aesm h2_aesm h1_diff h2_diff h1_cont h2_cont + h1_diff h2_diff h1_cont h2_cont calc GaussianSobolevNormSq n (f - g) (stdGaussianE n) = GaussianSobolevNormSq n ((f - f * smoothCutoffR R) + (f * smoothCutoffR R - g)) diff --git a/StatsMLlib/Probability/Gaussian/Sobolev/Mollification.lean b/StatsMLlib/Probability/Gaussian/Sobolev/Mollification.lean index 09582e7..fcb3f6b 100644 --- a/StatsMLlib/Probability/Gaussian/Sobolev/Mollification.lean +++ b/StatsMLlib/Probability/Gaussian/Sobolev/Mollification.lean @@ -398,13 +398,14 @@ lemma mollify_tendsto_uniformly_on_compact {n : ℕ} {g : E n → ℝ} {K : Set finite-measure set. Bounds the L² norm by sup-norm times measure^(1/2). -/ lemma eLpNorm_tendsto_zero_of_tendstoUniformly_restrict {n : ℕ} {f : ℕ → E n → ℝ} {g : E n → ℝ} {s : Set (E n)} (hμ : volume s < ⊤) + (hfg_meas : ∀ i, AEStronglyMeasurable (f i - g) volume) (hf_zero : ∀ i x, x ∉ s → f i x = 0) (hg_zero : ∀ x, x ∉ s → g x = 0) (h_unif : TendstoUniformly f g Filter.atTop) : Filter.Tendsto (fun i => eLpNorm (f i - g) 2 volume) Filter.atTop (nhds 0) := by have h_restrict : ∀ i, eLpNorm (f i - g) 2 volume = eLpNorm (f i - g) 2 (volume.restrict s) := by intro i symm - apply eLpNorm_restrict_eq_of_support_subset + apply eLpNorm_restrict_eq_of_support_subset (hfg_meas i) intro x hx rw [Function.mem_support, Pi.sub_apply, sub_ne_zero] at hx by_contra hxs @@ -435,7 +436,7 @@ lemma eLpNorm_tendsto_zero_of_tendstoUniformly_restrict {n : ℕ} {f : ℕ → E have h_bound : eLpNorm (f i - g) 2 (volume.restrict s) ≤ ENNReal.ofReal δ * (volume s) ^ (1/2 : ℝ) := by calc eLpNorm (f i - g) 2 (volume.restrict s) ≤ eLpNorm (fun _ => δ) 2 (volume.restrict s) := by - apply eLpNorm_mono_ae + apply eLpNorm_mono_ae (hfg_meas i).restrict rw [Filter.eventually_iff_exists_mem] use Set.univ constructor @@ -484,13 +485,14 @@ lemma eLpNorm_tendsto_zero_of_tendstoUniformly_restrict {n : ℕ} {f : ℕ → E lemma eLpNorm_tendsto_zero_of_tendstoUniformly_general {n : ℕ} {μ : Measure (E n)} {f : ℕ → E n → ℝ} {g : E n → ℝ} {s : Set (E n)} (hμ : μ s < ⊤) + (hfg_meas : ∀ i, AEStronglyMeasurable (f i - g) μ) (hf_zero : ∀ i x, x ∉ s → f i x = 0) (hg_zero : ∀ x, x ∉ s → g x = 0) (h_unif : TendstoUniformly f g Filter.atTop) : Filter.Tendsto (fun i => eLpNorm (f i - g) 2 μ) Filter.atTop (nhds 0) := by have h_restrict : ∀ i, eLpNorm (f i - g) 2 μ = eLpNorm (f i - g) 2 (μ.restrict s) := by intro i symm - apply eLpNorm_restrict_eq_of_support_subset + apply eLpNorm_restrict_eq_of_support_subset (hfg_meas i) intro x hx rw [Function.mem_support, Pi.sub_apply, sub_ne_zero] at hx by_contra hxs @@ -521,7 +523,7 @@ lemma eLpNorm_tendsto_zero_of_tendstoUniformly_general {n : ℕ} {μ : Measure ( have h_bound : eLpNorm (f i - g) 2 (μ.restrict s) ≤ ENNReal.ofReal δ * (μ s) ^ (1/2 : ℝ) := by calc eLpNorm (f i - g) 2 (μ.restrict s) ≤ eLpNorm (fun _ => δ) 2 (μ.restrict s) := by - apply eLpNorm_mono_ae + apply eLpNorm_mono_ae (hfg_meas i).restrict rw [Filter.eventually_iff_exists_mem] use Set.univ constructor @@ -639,10 +641,16 @@ lemma mollify_L2_convergence_continuous {n : ℕ} {g : E n → ℝ} {R : ℝ} (h simp only [hg_xy, zero_mul, Pi.zero_apply] have h_pointwise_bound : ∀ x ∈ Metric.closedBall (0 : E n) (2 * R + 1), dist (mollify ε g x) (g x) < η := fun x hx => by rw [dist_comm]; exact hε_unif x hx + have hg_compact : HasCompactSupport g := + HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall 0 (2 * R)) + (fun x hx => hg_supp (subset_closure hx)) + have hdiff_meas : AEStronglyMeasurable (mollify ε g - g) volume := + (((mollify_smooth hg_compact hg_cont.locallyIntegrable hε_pos).continuous.sub + hg_cont)).aestronglyMeasurable have h_restrict : eLpNorm (mollify ε g - g) 2 volume = eLpNorm (mollify ε g - g) 2 (volume.restrict (Metric.closedBall 0 (2 * R + 1))) := by symm - apply eLpNorm_restrict_eq_of_support_subset + apply eLpNorm_restrict_eq_of_support_subset hdiff_meas intro x hx rw [Function.mem_support] at hx by_contra hx_not_in @@ -650,7 +658,7 @@ lemma mollify_L2_convergence_continuous {n : ℕ} {g : E n → ℝ} {R : ℝ} (h rw [h_restrict] calc eLpNorm (mollify ε g - g) 2 (volume.restrict (Metric.closedBall 0 (2 * R + 1))) ≤ eLpNorm (fun (_ : E n) => η) 2 (volume.restrict (Metric.closedBall 0 (2 * R + 1))) := by - apply eLpNorm_mono_ae + apply eLpNorm_mono_ae hdiff_meas.restrict rw [Filter.eventually_iff_exists_mem] use Set.univ constructor @@ -874,10 +882,16 @@ lemma mollify_L2_convergence_gaussian_continuous {n : ℕ} {g : E n → ℝ} {R simp [h_mol_zero] rw [h_integrand_zero, integral_zero] linarith + have hg_compact : HasCompactSupport g := + HasCompactSupport.of_support_subset_isCompact (isCompact_closedBall 0 (2 * R)) + (fun x hx => hg_supp (subset_closure hx)) + have hdiff_meas : AEStronglyMeasurable (mollify ε g - g) (stdGaussianE n) := + (((mollify_smooth hg_compact hg_cont.locallyIntegrable hε_pos).continuous.sub + hg_cont)).aestronglyMeasurable have h_norm_eq_restrict : eLpNorm (mollify ε g - g) 2 (stdGaussianE n) = eLpNorm (mollify ε g - g) 2 ((stdGaussianE n).restrict K) := by symm - apply eLpNorm_restrict_eq_of_support_subset + apply eLpNorm_restrict_eq_of_support_subset hdiff_meas intro x hx rw [Function.mem_support] at hx by_contra hx_not_in @@ -889,7 +903,7 @@ lemma mollify_L2_convergence_gaussian_continuous {n : ℕ} {g : E n → ℝ} {R exact this calc eLpNorm (mollify ε g - g) 2 ((stdGaussianE n).restrict K) ≤ eLpNorm (fun _ => η) 2 ((stdGaussianE n).restrict K) := by - apply eLpNorm_mono_ae + apply eLpNorm_mono_ae hdiff_meas.restrict filter_upwards with x rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_pos hη_pos] simp only [Pi.sub_apply] @@ -1283,6 +1297,8 @@ lemma gradient_L2_convergence_gaussian {g : E n → ℝ} {R : ℝ} (hR : 0 < R) calc eLpNorm (fun x => ‖fderiv ℝ (mollify ε g) x - fderiv ℝ g x‖) 2 (stdGaussianE n) ≤ eLpNorm (fun _ => δr) 2 (stdGaussianE n) := by apply eLpNorm_mono_ae + (((measurable_fderiv ℝ (mollify ε g)).sub + (measurable_fderiv ℝ g)).norm).aestronglyMeasurable filter_upwards with x rw [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg _)] rw [Real.norm_eq_abs, abs_of_pos hδr_pos] diff --git a/StatsMLlib/Probability/Independence/FinsetPi.lean b/StatsMLlib/Probability/Independence/FinsetPi.lean index 6f83320..119e0eb 100644 --- a/StatsMLlib/Probability/Independence/FinsetPi.lean +++ b/StatsMLlib/Probability/Independence/FinsetPi.lean @@ -60,13 +60,13 @@ theorem pi_eval_iIndepFun : · intro hx i _ dsimp [f''] if h : i ∈ s then - rw [dif_pos h] + rw [dite_eq_left h] have := Set.mem_iInter.mp hx i have := Set.mem_iInter.mp this h rw [←(hf' i h).2] at this exact this else - rw [dif_neg h] + rw [dite_eq_right h] trivial · intro hx apply Set.mem_iInter.mpr @@ -75,7 +75,7 @@ theorem pi_eval_iIndepFun : intro hi have := hx i trivial dsimp [f''] at this - rw [dif_pos hi] at this + rw [dite_eq_left hi] at this rw [←(hf' i hi).2] exact this rw [this, Measure.pi_pi] @@ -85,7 +85,7 @@ theorem pi_eval_iIndepFun : ext i dsimp only [f''] if h : i ∈ s then - rw [dif_pos h, if_pos h, ←(hf' i h).2] + rw [dite_eq_left h, ite_eq_left h, ←(hf' i h).2] dsimp [f'] rw [←Measure.map_apply] · congr @@ -94,7 +94,7 @@ theorem pi_eval_iIndepFun : · exact measurable_pi_apply i · exact (hf' i h).1 else - rw [dif_neg h, if_neg h] + rw [dite_eq_right h, ite_eq_right h] exact isProbabilityMeasure_iff.mp inferInstance _ = _ := Fintype.prod_ite_mem s fun i ↦ (Measure.pi fun x ↦ μ) (f i) diff --git a/StatsMLlib/Probability/Process/Dudley.lean b/StatsMLlib/Probability/Process/Dudley.lean index fea10b0..e746a0a 100644 --- a/StatsMLlib/Probability/Process/Dudley.lean +++ b/StatsMLlib/Probability/Process/Dudley.lean @@ -3,6 +3,7 @@ Copyright (c) 2026 Yuanhe Zhang. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Yuanhe Zhang, Jason D. Lee, Fanghui Liu -/ +import Mathlib.MeasureTheory.Order.Group.Lattice import StatsMLlib.Probability.Process.SubGaussian import StatsMLlib.Probability.Process.FiniteMaximum import StatsMLlib.Analysis.MetricEntropy.Chaining @@ -1394,7 +1395,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A : linarith use ⟨R_real, hR_real_nonneg⟩ intro K hK - rw [MeasureTheory.eLpNorm_one_eq_lintegral_enorm] + rw [MeasureTheory.eLpNorm_one_eq_lintegral_enorm (h_Y_meas K).aestronglyMeasurable] simp only [Real.enorm_eq_ofReal_abs] have h_int_abs := (h_Y_int K hK).abs rw [← MeasureTheory.ofReal_integral_eq_lintegral_ofReal h_int_abs (ae_of_all μ (fun ω => abs_nonneg _))] @@ -1406,12 +1407,11 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A : have h_ae_liminf_finite : ∀ᵐ ω ∂μ, Filter.liminf (fun K => ‖Y K ω‖ₑ) Filter.atTop < ⊤ := by let Y' : ℕ → Ω → ℝ := fun K => Y (K + 1) - have hY'_meas : ∀ K, Measurable (Y' K) := fun K => h_Y_meas (K + 1) have hY'_bound : ∀ K, MeasureTheory.eLpNorm (Y' K) 1 μ ≤ R := by intro K exact hR (K + 1) (Nat.le_add_left 1 K) have h := MeasureTheory.ae_bdd_liminf_atTop_of_eLpNorm_bdd (p := 1) - (by norm_num : (1 : ℝ≥0∞) ≠ 0) hY'_meas hY'_bound + (by norm_num : (1 : ℝ≥0∞) ≠ 0) hY'_bound filter_upwards [h] with ω hω -- liminf_nat_add: shifting doesn't change liminf have h_shift : Filter.liminf (fun K => ‖Y K ω‖ₑ) Filter.atTop = @@ -1559,7 +1559,8 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A : = ∑' K, ∫⁻ ω, ENNReal.ofReal |Δ K ω| ∂μ := by apply lintegral_tsum intro K - exact (hX_meas (proj (K + 1) 0)).sub (hX_meas (proj K 0)) |>.abs.ennreal_ofReal.aemeasurable + exact Measurable.aemeasurable (Measurable.ennreal_ofReal + (Measurable.abs ((hX_meas (proj (K + 1) 0)).sub (hX_meas (proj K 0))))) _ = ∑' K, ENNReal.ofReal (∫ ω, |Δ K ω| ∂μ) := by congr 1 ext K @@ -1590,8 +1591,8 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A : · exact h_geom.mul_left _ _ < ⊤ := ENNReal.ofReal_lt_top have h_ae_lt_top : ∀ᵐ ω ∂μ, ∑' K, ENNReal.ofReal |Δ K ω| < ⊤ := - ae_lt_top (Measurable.tsum (fun K => - (hX_meas (proj (K + 1) 0)).sub (hX_meas (proj K 0)) |>.abs.ennreal_ofReal)) + ae_lt_top (Measurable.tsum (fun K => Measurable.ennreal_ofReal + (Measurable.abs ((hX_meas (proj (K + 1) 0)).sub (hX_meas (proj K 0)))))) h_lintegral_sum.ne filter_upwards [h_ae_lt_top] with ω h_lt_top have h_conv : ∀ K, ENNReal.ofReal |Δ K ω| = (Real.toNNReal |Δ K ω| : ℝ≥0∞) := fun K => rfl @@ -1669,7 +1670,7 @@ theorem dudley_chaining_bound_countable {Ω : Type u} [MeasurableSpace Ω] {A : · exact (h_proj0_int.sub h_t0_int).abs · have h_Δ_abs_int : ∀ K, Integrable (fun ω => |Δ K ω|) μ := fun K => (h_Δ_int K).abs have h_Δ_abs_meas : ∀ K, Measurable (fun ω => |Δ K ω|) := - fun K => ((hX_meas (proj (K + 1) 0)).sub (hX_meas (proj K 0))).abs + fun K => Measurable.abs ((hX_meas (proj (K + 1) 0)).sub (hX_meas (proj K 0))) have h_integrable_tsum : Integrable (fun ω => ∑' K, |Δ K ω|) μ := by -- AEStronglyMeasurable via NNReal tsum measurability have h_ae_meas : AEStronglyMeasurable (fun ω => ∑' K, |Δ K ω|) μ := by diff --git a/StatsMLlib/Probability/Process/SubGaussian.lean b/StatsMLlib/Probability/Process/SubGaussian.lean index ec3e755..850c09f 100644 --- a/StatsMLlib/Probability/Process/SubGaussian.lean +++ b/StatsMLlib/Probability/Process/SubGaussian.lean @@ -175,7 +175,7 @@ lemma subGaussianPsi2Norm_le_maxSubGaussianPsi2Norm {Ω : Type*} subGaussianPsi2Norm (X i) μ ≤ maxSubGaussianPsi2Norm X μ := by classical unfold maxSubGaussianPsi2Norm - rw [dif_pos (show (Finset.univ : Finset (Fin n)).Nonempty from + rw [dite_eq_left (show (Finset.univ : Finset (Fin n)).Nonempty from ⟨i, Finset.mem_univ i⟩)] exact Finset.le_sup' (f := fun i => subGaussianPsi2Norm (X i) μ) (Finset.mem_univ i) diff --git a/StatsMLlib/Probability/Process/TruncatedDudley.lean b/StatsMLlib/Probability/Process/TruncatedDudley.lean index fd3749b..d05b041 100644 --- a/StatsMLlib/Probability/Process/TruncatedDudley.lean +++ b/StatsMLlib/Probability/Process/TruncatedDudley.lean @@ -406,7 +406,7 @@ lemma exists_dudley_chain choose! U_seq hU_seq using hU_seq; use fun n => if n = L then U else U_seq n; simp +zetaDelta at *; - exact ⟨ fun n hn => by rw [ if_neg ( ne_of_lt hn ) ] ; exact hU_seq n hn, by rw [ if_neg ( ne_of_lt hm ) ] ; exact hU_seq m hm |>.2.1.1 ⟩; + exact ⟨ fun n hn => by rw [ ite_eq_right ( ne_of_lt hn ) ] ; exact hU_seq n hn, by rw [ ite_eq_right ( ne_of_lt hm ) ] ; exact hU_seq m hm |>.2.1.1 ⟩; cases' L with L L; · exact ⟨ fun _ => U, fun _ => id, fun _ => hU_finite, fun _ => hU_subset, rfl, by norm_num, by norm_num, by norm_num ⟩; · obtain ⟨ U_seq, hU_seq₁, hU_seq₂, hU_seq ⟩ := h_chain_construction L ( Nat.lt_succ_self L ); @@ -1052,7 +1052,7 @@ lemma exists_dudley_chain_consistent · exact Set.singleton_subset_iff.mpr hcstar_T · exact hUs₀ m · - dsimp only; rw [if_neg (not_le.mpr hM_lt)]; exact hUL₀ + dsimp only; rw [ite_eq_right (not_le.mpr hM_lt)]; exact hUL₀ · intro m hm; dsimp only; split_ifs with h · rw [Set.ncard_singleton]; exact (h_all_sing m h hm).symm @@ -1067,23 +1067,23 @@ lemma exists_dudley_chain_consistent · intro m hm u hu; dsimp only at hu ⊢ by_cases hm_le : m ≤ M - · simp only [if_pos hm_le] + · simp only [ite_eq_left hm_le] constructor · exact Set.mem_singleton cstar · by_cases hm1_le : m + 1 ≤ M - · simp only [if_pos hm1_le] at hu + · simp only [ite_eq_left hm1_le] at hu rw [Set.mem_singleton_iff.mp hu, dist_self]; exact (h_eps_pos m).le - · simp only [if_neg hm1_le] at hu + · simp only [ite_eq_right hm1_le] at hu have hm_eq_M : m = M := by omega rw [hm_eq_M] at hu ⊢; exact hcstar_cov u (hUs₀ (M + 1) hu) - · simp only [if_neg hm_le] + · simp only [ite_eq_right hm_le] have hm1_gt : ¬(m + 1 ≤ M) := fun h => hm_le (by omega) - simp only [if_neg hm1_gt] at hu; exact hUp₀ m hm u hu + simp only [ite_eq_right hm1_gt] at hu; exact hUp₀ m hm u hu · intro m hm hN u hu; dsimp only at hu ⊢ have hm1_le_M : m + 1 ≤ M := by by_contra h; push Not at h; exact hM_max (m + 1) h hm hN - simp only [if_pos (show m ≤ M by omega), if_pos hm1_le_M] at hu ⊢ + simp only [ite_eq_left (show m ≤ M by omega), ite_eq_left hm1_le_M] at hu ⊢ exact (Set.mem_singleton_iff.mp hu).symm /- diff --git a/StatsMLlib/Probability/RandomMatrix/Basic.lean b/StatsMLlib/Probability/RandomMatrix/Basic.lean index 95f1182..12173ab 100644 --- a/StatsMLlib/Probability/RandomMatrix/Basic.lean +++ b/StatsMLlib/Probability/RandomMatrix/Basic.lean @@ -1456,7 +1456,7 @@ lemma subGaussianPsi2Norm_le_maxFamilySubGaussianPsi2Norm {ι : Type*} [Fintype subGaussianPsi2Norm (X i) μ ≤ maxFamilySubGaussianPsi2Norm X μ := by classical unfold maxFamilySubGaussianPsi2Norm - rw [dif_pos (show (Finset.univ : Finset ι).Nonempty from ⟨i, Finset.mem_univ i⟩)] + rw [dite_eq_left (show (Finset.univ : Finset ι).Nonempty from ⟨i, Finset.mem_univ i⟩)] exact Finset.le_sup' (f := fun i => subGaussianPsi2Norm (X i) μ) (Finset.mem_univ i) /-- Maximum entrywise MGF-ψ₂ scale for a random rectangular matrix. -/ @@ -1575,7 +1575,7 @@ lemma subGaussianVectorPsi2Norm_le_maxMatrixRowSubGaussianPsi2Norm {m n : ℕ} maxMatrixRowSubGaussianPsi2Norm A μ := by classical unfold maxMatrixRowSubGaussianPsi2Norm - rw [dif_pos (show (Finset.univ : Finset (Fin m)).Nonempty from ⟨i, Finset.mem_univ i⟩)] + rw [dite_eq_left (show (Finset.univ : Finset (Fin m)).Nonempty from ⟨i, Finset.mem_univ i⟩)] exact Finset.le_sup' (f := fun i => subGaussianVectorPsi2Norm (randomMatrixRowVector A i) μ) (Finset.mem_univ i) diff --git a/StatsMLlib/Probability/RandomMatrix/Bernstein.lean b/StatsMLlib/Probability/RandomMatrix/Bernstein.lean index 99d674b..6ec4ba2 100644 --- a/StatsMLlib/Probability/RandomMatrix/Bernstein.lean +++ b/StatsMLlib/Probability/RandomMatrix/Bernstein.lean @@ -934,9 +934,9 @@ theorem matrixBernstein_lieb_recursion_of_independent {n N : ℕ} have : ∀ i, IsProbabilityMeasure (μs i) := by intro i dsimp [μs] - exact Measure.isProbabilityMeasure_map (hX_ae i) + infer_instance have hφ : AEMeasurable φ μ := - aemeasurable_pi_lambda _ hX_ae + AEMeasurable.of_eval hX_ae have hmap_eq : μ.map φ = Measure.pi μs := by unfold MatrixBernsteinIndependent at h_independent simpa [φ, μs, Mat] using @@ -1481,7 +1481,7 @@ lemma matrixLargestEigenvalue_of_isHermitian {n : ℕ} (hn : 0 < n) matrixLargestEigenvalue hn A = hA.eigenvaluesToEuclideanLin ⟨0, by simpa using hn⟩ := by unfold matrixLargestEigenvalue - rw [dif_pos hA] + rw [dite_eq_left hA] omit [MeasurableSpace Ω] in /-- The trace exponential dominates the exponential of the largest eigenvalue. -/ diff --git a/StatsMLlib/Probability/SmallBall.lean b/StatsMLlib/Probability/SmallBall.lean index e99ff34..054655b 100644 --- a/StatsMLlib/Probability/SmallBall.lean +++ b/StatsMLlib/Probability/SmallBall.lean @@ -300,7 +300,7 @@ theorem small_ball_prob {ι : Type*} [Fintype ι] (X : ι → Ω → ℝ) -- Product bound have h_prod_bound : ∏ i, mgf (X i) μ (-ε⁻¹) ≤ ε ^ N := by calc ∏ i, mgf (X i) μ (-ε⁻¹) - ≤ ∏ _i : ι, ε := Finset.prod_le_prod (fun i _ => mgf_nonneg) (fun i _ => h_mgf_bound i) + ≤ ∏ _i : ι, ε := Finset.prod_le_prod₀ (fun i _ => mgf_nonneg) (fun i _ => h_mgf_bound i) _ = ε ^ N := by simp only [Finset.prod_const, Finset.card_univ, hN] -- Final calculation calc (μ {ω : Ω | (∑ i : ι, X i ω) ≤ ε * N}).toReal diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/L1/CoveringBound.lean b/StatsMLlib/Statistics/Regression/LeastSquares/L1/CoveringBound.lean index ba855cd..cf85ce8 100644 --- a/StatsMLlib/Statistics/Regression/LeastSquares/L1/CoveringBound.lean +++ b/StatsMLlib/Statistics/Regression/LeastSquares/L1/CoveringBound.lean @@ -600,7 +600,7 @@ lemma maurey_exists_good_sample (x : Fin n → EuclideanSpace ℝ (Fin d)) use fun _ => s have hPs : 0 < (maureyPMF θ R hθ) s := by simp only [maureyPMF, PMF.ofFintype_apply, s] - simp only [if_true] + simp only [ite_true] have hnorm_pos : 0 < ‖θ j‖ := norm_pos_iff.mpr hj have hdiv_pos : 0 < ‖θ j‖ / R := div_pos hnorm_pos hR exact ENNReal.ofReal_pos.mpr hdiv_pos diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/Linear/EuclideanReduction.lean b/StatsMLlib/Statistics/Regression/LeastSquares/Linear/EuclideanReduction.lean index 9a65714..4d0a7ed 100644 --- a/StatsMLlib/Statistics/Regression/LeastSquares/Linear/EuclideanReduction.lean +++ b/StatsMLlib/Statistics/Regression/LeastSquares/Linear/EuclideanReduction.lean @@ -427,7 +427,7 @@ lemma submodule_closedBall_eq_inter (V : Submodule ℝ (EuclideanSpace ℝ (Fin constructor · -- ‖V.subtypeL u‖ ≤ r have : ‖V.subtypeL u‖ = ‖u‖ := by - simp only [Submodule.subtypeL_apply, Submodule.coe_norm] + simp only [Submodule.subtypeL_apply, Submodule.norm_coe] rw [this] exact hu · exact u.2 @@ -435,7 +435,7 @@ lemma submodule_closedBall_eq_inter (V : Submodule ℝ (EuclideanSpace ℝ (Fin use ⟨v, hmem⟩ constructor · -- ‖⟨v, hmem⟩‖ ≤ r - simp only [Submodule.coe_norm] + simp only [← Submodule.norm_coe] exact hball · simp only [Submodule.subtypeL_apply] diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean b/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean index 3fa45dc..64fa81d 100644 --- a/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean +++ b/StatsMLlib/Statistics/Regression/LeastSquares/LocalGaussianComplexity.lean @@ -264,8 +264,9 @@ lemma innerProductProcess_isSubGaussianProcess (n : ℕ) (hn : 0 < n) : rw [h_fubini] have h_mgf : ∀ i : Fin n, ∫ x : ℝ, Real.exp (t * a i * x) ∂(gaussianReal 0 1) = Real.exp ((t * a i)^2 / 2) := fun i => by - have h_map : Measure.map id (gaussianReal 0 1) = gaussianReal 0 1 := Measure.map_id - have hmgf := mgf_gaussianReal h_map (t * a i) + have h_law : HasLaw (id : ℝ → ℝ) (gaussianReal 0 1) (gaussianReal 0 1) := + ⟨measurable_id.aemeasurable, Measure.map_id⟩ + have hmgf := mgf_gaussianReal h_law (t * a i) simp only [mgf, id_eq, zero_mul, NNReal.coe_one, zero_add, one_mul] at hmgf convert hmgf using 2 simp_rw [h_mgf] @@ -488,7 +489,7 @@ lemma localGaussianComplexity_integrand_integrable (n : ℕ) (H : Set (X → ℝ funext w simp only [Nat.cast_zero, inv_zero, zero_mul, abs_zero] conv_lhs => rw [show (fun g => ⨆ (_ : g ∈ localizedBall H δ x), (0 : ℝ)) = fun _ => 0 from by - ext g; by_cases hg : g ∈ localizedBall H δ x <;> simp [ciSup_neg, *]] + ext g; by_cases hg : g ∈ localizedBall H δ x <;> simp [*]] exact Real.iSup_const_zero rw [hfun] exact diff --git a/StatsMLlib/Statistics/Regression/LeastSquares/SubGaussianity.lean b/StatsMLlib/Statistics/Regression/LeastSquares/SubGaussianity.lean index e9d5e10..22d74eb 100644 --- a/StatsMLlib/Statistics/Regression/LeastSquares/SubGaussianity.lean +++ b/StatsMLlib/Statistics/Regression/LeastSquares/SubGaussianity.lean @@ -136,8 +136,9 @@ lemma empiricalProcess_increment_mgf (n : ℕ) [NeZero n] (x : Fin n → X) -- Each integral ∫ exp(t * aᵢ * x) d(gaussianReal 0 1) = exp((t * aᵢ)² / 2) have h_mgf : ∀ i : Fin n, ∫ x : ℝ, Real.exp (t * a i * x) ∂(gaussianReal 0 1) = Real.exp ((t * a i)^2 / 2) := fun i => by - have h_map : Measure.map id (gaussianReal 0 1) = gaussianReal 0 1 := Measure.map_id - have hmgf := mgf_gaussianReal h_map (t * a i) + have h_law : HasLaw (id : ℝ → ℝ) (gaussianReal 0 1) (gaussianReal 0 1) := + ⟨measurable_id.aemeasurable, Measure.map_id⟩ + have hmgf := mgf_gaussianReal h_law (t * a i) simp only [mgf, id_eq, zero_mul, NNReal.coe_one, zero_add, one_mul] at hmgf convert hmgf using 2 simp_rw [h_mgf] diff --git a/StatsMLlib/Topology/MetricSpace/CoveringNumber/Basic.lean b/StatsMLlib/Topology/MetricSpace/CoveringNumber/Basic.lean index b9ea7ee..7571c9e 100644 --- a/StatsMLlib/Topology/MetricSpace/CoveringNumber/Basic.lean +++ b/StatsMLlib/Topology/MetricSpace/CoveringNumber/Basic.lean @@ -298,7 +298,7 @@ lemma exists_enet_subset_from_half {eps : ℝ} {s : Set A} -- proj x is in s ∩ closedBall(x, eps/2) have hproj_spec : (s ∩ closedBall x (eps / 2)).Nonempty := ⟨y, hy, hy_ball⟩ have hproj_in : proj x ∈ s ∩ closedBall x (eps / 2) := by - simp only [proj, dif_pos hproj_spec] + simp only [proj, dite_eq_left hproj_spec] exact hproj_spec.some_mem have hdist_proj_x : dist (proj x) x ≤ eps / 2 := mem_closedBall.mp hproj_in.2 -- By triangle inequality: dist(y, proj x) ≤ dist(y, x) + dist(x, proj x) ≤ eps @@ -313,8 +313,8 @@ lemma exists_enet_subset_from_half {eps : ℝ} {s : Set A} rw [Finset.mem_coe, Finset.mem_image] at hz obtain ⟨x, _, rfl⟩ := hz by_cases h : (s ∩ closedBall x (eps / 2)).Nonempty - · simp only [proj, dif_pos h]; exact h.some_mem.1 - · simp only [proj, dif_neg h]; exact hs₀ + · simp only [proj, dite_eq_left h]; exact h.some_mem.1 + · simp only [proj, dite_eq_right h]; exact hs₀ -- 3. |t'| ≤ coveringNumber(eps/2, s) · have h_card_le : t'.card ≤ net.card := Finset.card_image_le calc (t'.card : WithTop ℕ) ≤ net.card := by exact_mod_cast h_card_le @@ -367,7 +367,7 @@ noncomputable def coveringNumberNat {s : Set A} (hs : TotallyBounded s) (eps : /-- At a positive radius, coercing `coveringNumberNat` recovers the canonical covering number. -/ lemma coe_coveringNumberNat {s : Set A} (hs : TotallyBounded s) {eps : ℝ} (heps : 0 < eps) : (coveringNumberNat hs eps : WithTop ℕ) = coveringNumber eps s := by - simp only [coveringNumberNat, dif_pos heps] + simp only [coveringNumberNat, dite_eq_left heps] exact WithTop.coe_untop _ _ /-- `ℕ`-valued form of `coveringNumber_le_card_of_cover`, for the total-boundedness @@ -442,7 +442,7 @@ lemma coveringFinset_cover {s : Set A} (hs : TotallyBounded s) {eps : ℝ} lemma coveringFinset_card {s : Set A} (hs : TotallyBounded s) {eps : ℝ} (heps : 0 < eps) : (coveringFinset hs heps).card = coveringNumberNat hs eps := by - simpa only [coveringFinset, coveringNumberNat, dif_pos heps] using + simpa only [coveringFinset, coveringNumberNat, dite_eq_left heps] using (Classical.choose_spec (exists_optimal_enet_nat heps hs)).2 end diff --git a/StatsMLlib/Topology/SeparableSpace/Supremum.lean b/StatsMLlib/Topology/SeparableSpace/Supremum.lean index b8b1ac1..c1d1e23 100644 --- a/StatsMLlib/Topology/SeparableSpace/Supremum.lean +++ b/StatsMLlib/Topology/SeparableSpace/Supremum.lean @@ -6,7 +6,7 @@ Authors: Kei Tsukamoto, Kazumi Kasaura, Naoto Onda, Yuma Mizuno, Sho Sonoda import Mathlib.Topology.Bases import Mathlib.Order.ConditionallyCompleteLattice.Indexed import Mathlib.Topology.Order.Lattice -import Mathlib.Data.Real.Basic +import Mathlib.Basic.Real.Basic import Mathlib.Topology.Algebra.Ring.Real import Mathlib.MeasureTheory.MeasurableSpace.Basic diff --git a/lake-manifest.json b/lake-manifest.json index 19bff15..2ccf9ee 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,17 +5,17 @@ "type": "git", "subDir": null, "scope": "", - "rev": "db584cd6d46c92f209a44c0f1c829460d327499d", + "rev": "5ed2965256430c3649e86755f9576b54eca72435", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/plausible", "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "b7eb3304aeae834b12dda98993a37f6a41f6f0bb", + "rev": "118aa17ee84656b8bd727fef7c458ee8c833385c", "name": "plausible", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5f4d51b81cbd3f6b32b156bfad9056621a040404", + "rev": "ddf04cf3949fa556442341e87d47f9f6e6074707", "name": "LeanSearchClient", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -35,7 +35,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "16f02aa7642864af59f1ff0e384a015994db9118", + "rev": "e928b72544873815af278d38681b31c0293588e3", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -45,7 +45,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4be2e3d5087eeb272cf5a8853b8f9dd025ef5957", + "rev": "106ff4fafc74ef4ac99d81dbf3ab399118f497a5", "name": "proofwidgets", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "3448c0bcc5ce01b2d1546e483ec3620e32df3d0e", + "rev": "355695d523e41d0554926416cba2a2b3544fbbc9", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "92c15be17b7caf78c2ad767ec40f89052d908d81", + "rev": "6a489d9af5d0c47e5b259e2e8bcdfc1811b5a259", "name": "Qq", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -75,7 +75,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "4488d40d070b9700d4d5a6aa342f0d40c31b2a2d", + "rev": "f2effa3d803fda822b1f97b806c47cf2adfbcbc2", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -85,10 +85,10 @@ "type": "git", "subDir": null, "scope": "leanprover", - "rev": "6130a47896ce867c6a4a55373441e59e565bad0f", + "rev": "e92c9f15fdfacc8536f31cfb3b7ad26c3c8cd204", "name": "Cli", "manifestFile": "lake-manifest.json", - "inputRev": "v4.33.0", + "inputRev": "v4.34.0", "inherited": true, "configFile": "lakefile.toml"}], "name": "StatsMLlib", diff --git a/lakefile.lean b/lakefile.lean index beba24c..99554c8 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -29,7 +29,7 @@ package «StatsMLlib» where moreServerOptions := linter require mathlib from git - "https://github.com/leanprover-community/mathlib4.git" @ "v4.33.0" + "https://github.com/leanprover-community/mathlib4.git" @ "v4.34.0" @[default_target] lean_lib «StatsMLlib» where @@ -37,4 +37,4 @@ lean_lib «StatsMLlib» where meta if get_config? env = some "dev" then require «doc-gen4» from git - "https://github.com/leanprover/doc-gen4" @ "v4.33.0" + "https://github.com/leanprover/doc-gen4" @ "v4.34.0" diff --git a/lean-toolchain b/lean-toolchain index 025e595..12359f9 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.33.0 +leanprover/lean4:v4.34.0