PL1/NoiseHypercontractivity.lean
All source files · Download exact source
SHA-256: f853afc290fe838948d72cf72afadca6ed05431d0e104ab9648c573df9f6c44c
1import PL1.NoiseSemigroup2import PL1.LpInclusions3import Mathlib.Analysis.Normed.Operator.Extend4import Mathlib.LinearAlgebra.Finsupp.LinearCombination5import PL1.BonamiHaarBridge6import PL1.ConvolutionHypercontractivity78/-! # Dense extension of finite Walsh noise estimates to actual Haar Lp910The norm hypothesis is explicit in the extension lemmas. The finite-cube11Bonami theorem supplies it in the final application.12-/1314noncomputable section15open MeasureTheory16open scoped ENNReal NNReal BigOperators1718namespace PL1.NoiseHypercontractivity19open Walsh Noise2021variable (K : Type*) [RCLike K]2223abbrev Coefficients := Finset ℕ →₀ K2425def polynomialLp (p : ℝ≥0∞) [Fact (1 ≤ p)] : Coefficients K →ₗ[K] Lp K p haar :=26 Finsupp.linearCombination K (scalarCharacterLp K p)2728def noisePolynomial (u : ℝ≥0) : Coefficients K →ₗ[K] Lp K 2 haar :=29 Finsupp.linearCombination K (fun F =>30 ((Real.exp (-(u : ℝ) * F.card) : ℝ) : K) • scalarCharacterLp K 2 F)3132@[simp] theorem polynomialLp_single (p : ℝ≥0∞) [Fact (1 ≤ p)] (F : Finset ℕ) (a : K) :33 polynomialLp K p (Finsupp.single F a) = a • scalarCharacterLp K p F := by34 simp [polynomialLp]3536@[simp] theorem noisePolynomial_single (u : ℝ≥0) (F : Finset ℕ) (a : K) :37 noisePolynomial K u (Finsupp.single F a) =38 a • (((Real.exp (-(u : ℝ) * F.card) : ℝ) : K) • scalarCharacterLp K 2 F) := by39 simp [noisePolynomial]4041theorem polynomialLp_denseRange (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞) :42 DenseRange (polynomialLp K p) := by43 change Dense (Set.range (polynomialLp K p))44 rw [← LinearMap.coe_range, polynomialLp, Finsupp.range_linearCombination]45 exact dense_span_scalarCharacterLp K p hp4647theorem inclusion_polynomialLp (p q : ℝ≥0∞) [Fact (1 ≤ p)] [Fact (1 ≤ q)] (hpq : p ≤ q)48 (c : Coefficients K) :49 ProbabilityLp.inclusion haar p q hpq (polynomialLp K q c) = polynomialLp K p c := by50 have h : (ProbabilityLp.inclusion (𝕜 := K) haar p q hpq).toLinearMap.comp51 (polynomialLp K q) = polynomialLp K p := by52 apply Finsupp.lhom_ext53 intro F a54 simp only [LinearMap.comp_apply, ContinuousLinearMap.coe_coe, polynomialLp_single,55 map_smul]56 congr 157 exact ProbabilityLp.inclusion_toLp haar p q hpq (memLp_scalarCharacter K q F)58 exact LinearMap.congr_fun h c5960theorem noisePolynomial_overlap (p : ℝ≥0∞) [Fact (1 ≤ p)] (u : ℝ≥0)61 (c : Coefficients K) :62 l2ToL1 (noisePolynomial K u c) = noiseL1 K constantRates u63 (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) (polynomialLp K p c)) := by64 rw [inclusion_polynomialLp]65 have h : l2ToL1.toLinearMap.comp (noisePolynomial K u) =66 (noiseL1 K constantRates u).toLinearMap.comp (polynomialLp K 1) := by67 apply Finsupp.lhom_ext68 intro F a69 simp only [LinearMap.comp_apply, ContinuousLinearMap.coe_coe, noisePolynomial_single,70 polynomialLp_single, map_smul, noiseL1_character, l2ToL1_scalarCharacter]71 simp [rateSum, constantRates]72 exact LinearMap.congr_fun h c7374def PolynomialBound (p : ℝ≥0∞) [Fact (1 ≤ p)] (u : ℝ≥0) : Prop :=75 ∀ c : Coefficients K, ‖noisePolynomial K u c‖ ≤ ‖polynomialLp K p c‖7677/-- Completion of the finite Walsh map. Its bound and noise identity are78proved below whenever the explicitly stated polynomial estimate holds. -/79def polynomialExtension (p : ℝ≥0∞) [Fact (1 ≤ p)] (u : ℝ≥0) :80 Lp K p haar →L[K] Lp K 2 haar :=81 (noisePolynomial K u).extendOfNorm (polynomialLp K p)8283theorem polynomialExtension_polynomial (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞)84 (u : ℝ≥0) (hbound : PolynomialBound K p u) (c : Coefficients K) :85 polynomialExtension K p u (polynomialLp K p c) = noisePolynomial K u c :=86 LinearMap.extendOfNorm_eq (polynomialLp_denseRange K p hp)87 ⟨1, fun c => by simpa only [one_mul] using hbound c⟩ c8889theorem norm_polynomialExtension_le_one (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞)90 (u : ℝ≥0) (hbound : PolynomialBound K p u) :91 ‖polynomialExtension K p u‖ ≤ 1 :=92 LinearMap.opNorm_extendOfNorm_le (polynomialLp_denseRange K p hp) zero_le_one93 (fun c => by simpa only [one_mul] using hbound c)9495theorem polynomialExtension_overlap (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞)96 (u : ℝ≥0) (hbound : PolynomialBound K p u) (f : Lp K p haar) :97 l2ToL1 (polynomialExtension K p u f) =98 noiseL1 K constantRates u (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f) := by99 have h : l2ToL1.comp (polynomialExtension K p u) =100 (noiseL1 K constantRates u).comp101 (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p)) := by102 apply ContinuousLinearMap.ext_on (dense_span_scalarCharacterLp K p hp)103 rintro x ⟨F, rfl⟩104 have he := polynomialExtension_polynomial K p hp u hbound (Finsupp.single F 1)105 have ho := noisePolynomial_overlap K p u (Finsupp.single F 1)106 simp only [polynomialLp_single, one_smul] at he ho107 simpa only [ContinuousLinearMap.comp_apply, he] using ho108 exact congrArg (fun T : Lp K p haar →L[K] Lp K 1 haar => T f) h109110theorem coeFn_weighted_polynomial (p : ℝ≥0∞) [Fact (1 ≤ p)]111 (a : Finset ℕ → K) (c : Coefficients K) :112 (Finsupp.linearCombination K (fun F => a F • scalarCharacterLp K p F) c) =ᵐ[haar]113 fun x => ∑ F ∈ c.support, c F * a F * scalarCharacter K F x := by114 have hh (F : Finset ℕ) : a F • scalarCharacterLp K p F =ᵐ[haar]115 fun x => a F * scalarCharacter K F x := by116 filter_upwards [Lp.coeFn_smul (a F) (scalarCharacterLp K p F),117 coeFn_scalarCharacterLp K p F] with x hs hc118 simp only [hs, Pi.smul_apply, hc, smul_eq_mul]119 filter_upwards [Lp.coeFn_linearCombination c (fun F => a F • scalarCharacterLp K p F),120 ae_all_iff.mpr hh] with x hx hall121 simpa only [Finsupp.linearCombination_apply, Finsupp.sum, Finset.sum_apply,122 Pi.smul_apply, smul_eq_mul, hall, mul_assoc] using hx123124theorem coeFn_polynomialLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (c : Coefficients K) :125 polynomialLp K p c =ᵐ[haar]126 fun x => ∑ F ∈ c.support, c F * scalarCharacter K F x := by127 simpa only [one_smul, mul_one, polynomialLp] using128 coeFn_weighted_polynomial K p (fun _ => 1) c129130theorem coeFn_noisePolynomial (u : ℝ≥0) (c : Coefficients K) :131 noisePolynomial K u c =ᵐ[haar]132 fun x => ∑ F ∈ c.support, c F * ((Real.exp (-(u : ℝ) * F.card) : ℝ) : K) *133 scalarCharacter K F x :=134 coeFn_weighted_polynomial K 2 (fun F => ((Real.exp (-(u : ℝ) * F.card) : ℝ) : K)) c135136theorem norm_sq_eq_integral_rpow (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞)137 (f : Lp K p haar) {g : Group → K} (hfg : f =ᵐ[haar] g) :138 ‖f‖ ^ 2 = (∫ x, ‖g x‖ ^ p.toReal ∂haar) ^ (2 / p.toReal) := by139 have hp0 : p ≠ 0 := ne_of_gt (lt_of_lt_of_le zero_lt_one (Fact.out : 1 ≤ p))140 have hi : 0 ≤ ∫ x, ‖f x‖ ^ p.toReal ∂haar := integral_nonneg (fun x => by positivity)141 rw [Lp.norm_def, MemLp.eLpNorm_eq_integral_rpow_norm hp0 hp (Lp.memLp f),142 ENNReal.toReal_ofReal (Real.rpow_nonneg hi _), ← Real.rpow_two,143 ← Real.rpow_mul hi]144 have he : p.toReal⁻¹ * 2 = 2 / p.toReal := by ring145 rw [he]146 congr 1147 apply integral_congr_ae148 filter_upwards [hfg] with x hx149 rw [hx]150151theorem real_polynomial_bound (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞)152 (hp2 : p.toReal ≤ 2) (u : ℝ≥0)153 (hu : (Real.exp (-(u : ℝ))) ^ 2 ≤ p.toReal - 1) :154 PolynomialBound ℝ p u := by155 intro c156 apply (sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)).mp157 rw [norm_sq_eq_integral_rpow ℝ 2 (by norm_num) _ (coeFn_noisePolynomial ℝ u c),158 norm_sq_eq_integral_rpow ℝ p hp _ (coeFn_polynomialLp ℝ p c)]159 simp only [ENNReal.toReal_ofNat, div_self (show (2 : ℝ) ≠ 0 by norm_num),160 Real.rpow_one, Real.rpow_two, Real.norm_eq_abs, sq_abs, scalarCharacter]161 have hp1 : 1 ≤ p.toReal := by162 simpa only [ENNReal.toReal_one] using ENNReal.toReal_mono hp (Fact.out : 1 ≤ p)163 have h := Bonami.finite_walsh_sum_bound p.toReal (Real.exp (-(u : ℝ))) hp1 hp2 hu c.support c164 have he (F : Finset ℕ) : Real.exp (-(u : ℝ)) ^ F.card =165 Real.exp (-(u : ℝ) * F.card) := by rw [← Real.exp_nat_mul]; congr 1; ring166 simpa [he] using h167168variable (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : p ≠ ∞) (hp2 : p.toReal ≤ 2)169 (u : ℝ≥0) (hu : (Real.exp (-(u : ℝ))) ^ 2 ≤ p.toReal - 1)170171/-- The actual constant-rate noise, extended from Haar Lp into Haar L2.172All finite-dimensional and real-to-complex estimates are discharged. -/173def noiseLpToL2 : Lp K p haar →L[K] Lp K 2 haar :=174 scalarLift K p (measure constantRates u) (polynomialExtension ℝ p u)175 (polynomialExtension_overlap ℝ p hp u (real_polynomial_bound p hp hp2 u hu))176177theorem norm_noiseLpToL2_le_one : ‖noiseLpToL2 K p hp hp2 u hu‖ ≤ 1 :=178 (norm_scalarLift_le K p (measure constantRates u) (polynomialExtension ℝ p u)179 (polynomialExtension_overlap ℝ p hp u (real_polynomial_bound p hp hp2 u hu))).trans180 (norm_polynomialExtension_le_one ℝ p hp u (real_polynomial_bound p hp hp2 u hu))181182theorem noiseLpToL2_overlap (f : Lp K p haar) :183 l2ToL1 (noiseLpToL2 K p hp hp2 u hu f) =184 noiseL1 K constantRates u (ProbabilityLp.inclusion haar 1 p (Fact.out : 1 ≤ p) f) :=185 scalarLift_overlap K p (measure constantRates u) (polynomialExtension ℝ p u)186 (polynomialExtension_overlap ℝ p hp u (real_polynomial_bound p hp hp2 u hu)) f187188/-- The sharp input exponent for a specified nonnegative time. -/189def exponent (u : ℝ≥0) : ℝ≥0∞ := ENNReal.ofReal (1 + Real.exp (-2 * (u : ℝ)))190191theorem exponent_ge_one (u : ℝ≥0) : 1 ≤ exponent u := by192 rw [exponent, ← ENNReal.ofReal_one]193 exact ENNReal.ofReal_le_ofReal (le_add_of_nonneg_right (Real.exp_nonneg _))194195instance exponent_fact (u : ℝ≥0) : Fact (1 ≤ exponent u) := ⟨exponent_ge_one u⟩196197@[simp] theorem exponent_ne_top (u : ℝ≥0) : exponent u ≠ ∞ := ENNReal.ofReal_ne_top198199@[simp] theorem exponent_toReal (u : ℝ≥0) :200 (exponent u).toReal = 1 + Real.exp (-2 * (u : ℝ)) := by201 exact ENNReal.toReal_ofReal (by positivity)202203theorem exponent_toReal_le_two (u : ℝ≥0) : (exponent u).toReal ≤ 2 := by204 rw [exponent_toReal]205 have he : Real.exp (-2 * (u : ℝ)) ≤ 1 :=206 Real.exp_le_one_iff.mpr (mul_nonpos_of_nonpos_of_nonneg (by norm_num) u.coe_nonneg)207 linarith208209theorem exponent_lt_two (u : ℝ≥0) (hu : 0 < u) : exponent u < 2 := by210 rw [exponent, ← ENNReal.ofReal_ofNat 2]211 have hur : 0 < (u : ℝ) := hu212 have he : Real.exp (-2 * (u : ℝ)) < 1 := Real.exp_lt_one_iff.mpr (by nlinarith)213 exact ENNReal.ofReal_lt_ofReal_iff_of_nonneg (by positivity) |>.mpr (by linarith)214215theorem exponent_noise_condition (u : ℝ≥0) :216 (Real.exp (-(u : ℝ))) ^ 2 ≤ (exponent u).toReal - 1 := by217 rw [exponent_toReal, add_sub_cancel_left, ← Real.exp_nat_mul]218 apply le_of_eq219 congr 1220 norm_num221222/-- A concrete dimension-independent Lp-L2 contraction at every positive time,223with the displayed sharp exponent strictly below two. -/224def positiveTimeNoiseL2 (u : ℝ≥0) : Lp K (exponent u) haar →L[K] Lp K 2 haar :=225 noiseLpToL2 K (exponent u) (exponent_ne_top u) (exponent_toReal_le_two u) u226 (exponent_noise_condition u)227228theorem norm_positiveTimeNoiseL2_le_one (u : ℝ≥0) : ‖positiveTimeNoiseL2 K u‖ ≤ 1 :=229 norm_noiseLpToL2_le_one K (exponent u) (exponent_ne_top u) (exponent_toReal_le_two u) u230 (exponent_noise_condition u)231232theorem positiveTimeNoiseL2_overlap (u : ℝ≥0) (f : Lp K (exponent u) haar) :233 l2ToL1 (positiveTimeNoiseL2 K u f) = noiseL1 K constantRates u234 (ProbabilityLp.inclusion haar 1 (exponent u) (exponent_ge_one u) f) :=235 noiseLpToL2_overlap K (exponent u) (exponent_ne_top u) (exponent_toReal_le_two u) u236 (exponent_noise_condition u) f237238#print axioms noiseLpToL2_overlap239#print axioms norm_positiveTimeNoiseL2_le_one240#print axioms positiveTimeNoiseL2_overlap241242end PL1.NoiseHypercontractivity243