PL1/EnfloDyadicDecay.lean

All source files · Download exact source

SHA-256: 1c9b01d9dd14d4932b9fb39524127227a85473e5bded2e5b73b2aba1d081da64

1import PL1.EnfloMaxMass2import PL1.NoiseHypercontractivity3import Mathlib.Analysis.SpecialFunctions.Pow.Continuity45/-! Actual dyadic image decay and the positive hypercontractive exponent. -/6noncomputable section7open MeasureTheory Filter8open scoped Topology NNReal ENNReal9namespace PL1.EnfloBush10open DyadicTrace NoiseHypercontractivity1112section AnyTarget13variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}1415theorem norm_image_dyadicVector_le (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ)16    (m j : ℕ) (hj : j < 2 ^ m) :17    ‖S (dyadicVector (𝕜 := ℝ) m j)‖ ≤ ‖S‖ * ((2 : ℝ)^m)⁻¹ := by18  have he : ‖dyadicVector (𝕜 := ℝ) m j‖ = ((2 : ℝ)^m)⁻¹ := by19    rw [PartitionAverages.norm_vector]20    exact intervalMeasure_cell_toReal m j hj21  simpa only [he] using S.le_opNorm (dyadicVector (𝕜 := ℝ) m j)2223theorem dyadic_norm_bound_tendsto (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ) :24    Tendsto (fun m : ℕ => ‖S‖ * ((2 : ℝ)^m)⁻¹) atTop (𝓝 0) := by25  have h := (tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num : (0 : ℝ) ≤ 1 / 2)26    (by norm_num : (1 / 2 : ℝ) < 1)).const_mul ‖S‖27  simpa only [one_div, inv_pow, mul_zero] using h2829theorem dyadic_norm_bound_rpow_tendsto (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ)30    {r : ℝ} (hr : 0 < r) :31    Tendsto (fun m : ℕ => (‖S‖ * ((2 : ℝ)^m)⁻¹)^r) atTop (𝓝 0) :=32  (dyadic_norm_bound_tendsto S).rpow_const_nhds_zero hr3334end AnyTarget3536theorem exponent_toReal_lt_two (u : ℝ≥0) (hu : 0 < u) : (exponent u).toReal < 2 := by37  rw [exponent_toReal]38  have hur : 0 < (u : ℝ) := hu39  have h := Real.exp_lt_one_iff.mpr (by nlinarith : -2 * (u : ℝ) < 0)40  linarith4142theorem decay_exponent_pos (u : ℝ≥0) (hu : 0 < u) :43    0 < 2 / (exponent u).toReal - 1 := by44  have hp : 0 < (exponent u).toReal := by rw [exponent_toReal]; positivity45  apply sub_pos.mpr46  apply (lt_div_iff₀ hp).mpr47  simpa only [one_mul] using exponent_toReal_lt_two u hu4849theorem hypercontractive_dyadic_decay50    (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 Walsh.haar) (u : ℝ≥0) (hu : 0 < u) :51    Tendsto (fun m : ℕ => (‖S‖ * ((2 : ℝ)^m)⁻¹)^(2 / (exponent u).toReal - 1)) atTop (𝓝 0) :=52  dyadic_norm_bound_rpow_tendsto S (decay_exponent_pos u hu)5354#print axioms hypercontractive_dyadic_decay55end PL1.EnfloBush5657