PL1/EnfloSmoothing.lean
All source files · Download exact source
SHA-256: 0e2ce418758e9135da325a3abd5e0960228bb848b2fb5a033b1821bede0c6542
1import PL1.EnfloTruncation2import PL1.EnfloHypercontractive3import PL1.EnfloDyadicDecay45/-! # Positive-time noise destroys the maximum mass of every L1 dyadic bush67The source operator is arbitrary. A common integrable majorant controls8the truncation tails, and the actual Lp-to-L2 noise contraction controls9the bounded part. No compactness or extraction theorem is assumed.10-/1112noncomputable section13open MeasureTheory Filter14open scoped BigOperators Topology NNReal ENNReal1516namespace PL1.EnfloBush17open Walsh Noise NoiseHypercontractivity DyadicTrace1819theorem noise_maxMass_le_truncated (u : ℝ≥0) (n : ℕ) (f : ℕ → Lp ℝ 1 haar)20 (M : ℝ) (hM : 0 ≤ M) (g : Walsh.Group → ℝ) (hg : Integrable g haar)21 (hg0 : ∀ x, 0 ≤ g x)22 (hfg : ∀ᵐ x ∂haar, (∑ j ∈ Finset.range n, |f j x|) ≤ g x) :23 maxMass n (fun j => noiseL1 ℝ constantRates u (f j)) ≤24 maxMass n (fun j => noiseL1 ℝ constantRates u (truncateLp M hM (f j))) +25 ∫ x, max (g x - M) 0 ∂haar := by26 apply (maxMass_le_add_sum_norm_sub n _ _).trans27 apply add_le_add le_rfl28 apply le_trans _ (sum_norm_truncation_error_le n f M hM g hg hg0 hfg)29 apply Finset.sum_le_sum30 intro j _31 rw [← map_sub]32 calc33 _ ≤ ‖noiseL1 ℝ constantRates u‖ * ‖f j - truncateLp M hM (f j)‖ :=34 (noiseL1 ℝ constantRates u).le_opNorm _35 _ ≤ 1 * ‖f j - truncateLp M hM (f j)‖ :=36 mul_le_mul_of_nonneg_right (norm_noiseL1_le_one ℝ constantRates u) (norm_nonneg _)37 _ = _ := one_mul _3839def truncatedDyadicNoiseMass (u : ℝ≥0) (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar)40 (M : ℝ) (hM : 0 ≤ M) (m : ℕ) : ℝ :=41 maxMass (2 ^ m) (fun j => noiseL1 ℝ constantRates u42 (truncateLp M hM (S (dyadicVector m j))))4344theorem truncatedDyadicNoiseMass_nonneg (u : ℝ≥0)45 (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar) (M : ℝ) (hM : 0 ≤ M) (m : ℕ) :46 0 ≤ truncatedDyadicNoiseMass u S M hM m := maxMass_nonneg _ _4748theorem truncatedDyadicNoiseMass_sq_le (u : ℝ≥0)49 (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar) (M : ℝ) (hM : 0 ≤ M) (m : ℕ) :50 truncatedDyadicNoiseMass u S M hM m ^ 2 ≤51 M ^ (2 * (1 - 1 / (exponent u).toReal)) *52 (‖S‖ * ((2 : ℝ) ^ m)⁻¹) ^ (2 / (exponent u).toReal - 1) * ‖S‖ := by53 apply bounded_family_noise_max_sq_le u (2 ^ m)54 (fun j => truncateLp M hM (S (dyadicVector m j))) M hM55 (fun j => truncateLp_bound M hM _) _ _ (by positivity) (norm_nonneg S)56 · intro j hj57 exact (norm_truncateLp_le M hM _).trans (norm_image_dyadicVector_le S m j hj)58 · exact (Finset.sum_le_sum (fun j _ => norm_truncateLp_le M hM _)).trans59 (dyadicSumMass_le S m)6061theorem truncatedDyadicNoiseMass_tendsto (u : ℝ≥0) (hu : 0 < u)62 (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar) (M : ℝ) (hM : 0 ≤ M) :63 Tendsto (truncatedDyadicNoiseMass u S M hM) atTop (𝓝 0) := by64 have hlim : Tendsto (fun m => M ^ (2 * (1 - 1 / (exponent u).toReal)) *65 (‖S‖ * ((2 : ℝ) ^ m)⁻¹) ^ (2 / (exponent u).toReal - 1) * ‖S‖) atTop (𝓝 0) := by66 simpa only [mul_zero, zero_mul] using ((hypercontractive_dyadic_decay S u hu).const_mul67 (M ^ (2 * (1 - 1 / (exponent u).toReal)))).mul_const ‖S‖68 have hs := squeeze_zero (fun m => sq_nonneg (truncatedDyadicNoiseMass u S M hM m))69 (truncatedDyadicNoiseMass_sq_le u S M hM) hlim70 have hr := hs.sqrt71 simpa only [Real.sqrt_zero, Real.sqrt_sq_eq_abs,72 abs_of_nonneg (truncatedDyadicNoiseMass_nonneg u S M hM _)] using hr7374/-- Every actual L1 operator followed by positive constant-rate noise has75vanishing maximum mass on the full interval dyadic partitions. -/76theorem noise_comp_dyadicVanishing (u : ℝ≥0) (hu : 0 < u)77 (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar) :78 DyadicVanishing ((noiseL1 ℝ constantRates u).comp S) := by79 obtain ⟨g, hg, hg0, hfg⟩ := exists_dyadic_majorant S80 have hbound (M m : ℕ) :81 dyadicMaxMass ((noiseL1 ℝ constantRates u).comp S) m ≤82 truncatedDyadicNoiseMass u S M (Nat.cast_nonneg M) m +83 ∫ x, max (g x - (M : ℝ)) 0 ∂haar := by84 apply noise_maxMass_le_truncated u (2 ^ m)85 (fun j => S (dyadicVector m j)) M (Nat.cast_nonneg M) g hg hg086 filter_upwards [hfg] with x hx87 exact hx m88 apply Metric.tendsto_atTop.mpr89 intro ε hε90 obtain ⟨M, hM⟩ := ((integral_tail_tendsto_zero g hg hg0).eventually_lt_const (half_pos hε)).exists91 obtain ⟨N, hN⟩ := eventually_atTop.mp92 ((truncatedDyadicNoiseMass_tendsto u hu S M (Nat.cast_nonneg M)).eventually_lt_const (half_pos hε))93 refine ⟨N, fun m hm => ?_⟩94 rw [Real.dist_eq, sub_zero, abs_of_nonneg (dyadicMaxMass_nonneg _ m)]95 have hb := hbound M m96 have hn := hN m hm97 linarith9899#print axioms noise_comp_dyadicVanishing100101end PL1.EnfloBush102