PL1/EnfloVanishing.lean
All source files · Download exact source
SHA-256: 74443a0701d7336123abefe2e3071731a263c6510ecd307cd041c4af802d8c61
1import PL1.EnfloMaxMass2import PL1.ResolventAlmostInvariant34/-! Stability of actual dyadic maximum decay and the resolvent consequence. -/56noncomputable section7set_option backward.isDefEq.respectTransparency false8open MeasureTheory Filter9open scoped BigOperators Topology ENNReal NNReal1011namespace PL1.EnfloBush1213section General14variable {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω}1516theorem maxMass_smul_le (n : ℕ) (f : ℕ → Lp ℝ 1 μ) (c : ℝ) :17 maxMass n (fun j => c • f j) ≤ |c| * maxMass n f := by18 rw [maxMass, maxMass, ← integral_const_mul]19 apply integral_mono_ae (integrable_maxAbs n _) ((integrable_maxAbs n f).const_mul |c|)20 filter_upwards [ae_all_iff.mpr (fun j => Lp.coeFn_smul c (f j))] with x hx21 apply maxAbs_le (mul_nonneg (abs_nonneg c) (maxAbs_nonneg n _))22 intro j hj23 rw [hx j, Pi.smul_apply, smul_eq_mul, abs_mul]24 exact mul_le_mul_of_nonneg_left (abs_le_maxAbs (fun j => f j x) hj) (abs_nonneg c)2526theorem DyadicVanishing.add {T S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ}27 (hT : DyadicVanishing T) (hS : DyadicVanishing S) : DyadicVanishing (T + S) := by28 apply squeeze_zero (dyadicMaxMass_nonneg (T + S))29 (fun n => maxMass_add_le (2 ^ n)30 (fun j => T (DyadicTrace.dyadicVector n j))31 (fun j => S (DyadicTrace.dyadicVector n j)))32 simpa only [dyadicMaxMass, add_zero] using Filter.Tendsto.add hT hS3334theorem DyadicVanishing.smul {T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ}35 (hT : DyadicVanishing T) (c : ℝ) : DyadicVanishing (c • T) := by36 apply squeeze_zero (dyadicMaxMass_nonneg (c • T))37 (fun n => maxMass_smul_le (2 ^ n) (fun j => T (DyadicTrace.dyadicVector n j)) c)38 simpa only [dyadicMaxMass, mul_zero] using hT.const_mul |c|3940theorem DyadicVanishing.sub {T S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ}41 (hT : DyadicVanishing T) (hS : DyadicVanishing S) : DyadicVanishing (T - S) := by42 have he : T - S = T + (-1 : ℝ) • S := by43 exact (sub_eq_add_neg T S).trans44 (congrArg (fun A => T + A) (neg_one_smul ℝ S).symm)45 rw [he]46 exact hT.add (hS.smul (-1))4748theorem dyadicVanishing_of_approximation (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ)49 (h : ∀ ε : ℝ, 0 < ε → ∃ S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ,50 DyadicVanishing S ∧ ‖T - S‖ < ε) : DyadicVanishing T := by51 rw [DyadicVanishing, Metric.tendsto_nhds]52 intro ε hε53 obtain ⟨S, hS, hnorm⟩ := h (ε / 2) (half_pos hε)54 have hs := Metric.tendsto_nhds.mp hS (ε / 2) (half_pos hε)55 filter_upwards [hs] with n hn56 rw [Real.dist_eq, sub_zero, abs_of_nonneg (dyadicMaxMass_nonneg T n)]57 rw [Real.dist_eq, sub_zero, abs_of_nonneg (dyadicMaxMass_nonneg S n)] at hn58 exact (dyadicMaxMass_le_add_norm_sub T S n).trans_lt (by linarith)5960theorem dyadicVanishing_of_opNorm_tendsto61 (T : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ)62 (S : ℕ → IntervalL1 ℝ →L[ℝ] Lp ℝ 1 μ)63 (hS : ∀ n, DyadicVanishing (S n))64 (ht : Tendsto (fun n => ‖S n - T‖) atTop (𝓝 0)) : DyadicVanishing T := by65 apply dyadicVanishing_of_approximation T66 intro ε hε67 obtain ⟨n, hn⟩ := ((tendsto_order.mp ht).2 ε hε).exists68 exact ⟨S n, hS n, by simpa only [norm_sub_rev] using hn⟩6970end General7172open Walsh Noise7374theorem dyadicVanishing_resolvent_of_noise (rates : ℕ → ℝ≥0)75 (hnoise : ∀ (u : ℝ≥0), 0 < u →76 ∀ S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar,77 DyadicVanishing ((noiseL1 ℝ rates u).comp S))78 (t : PositiveTime) (S : IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar) :79 DyadicVanishing ((resolventL1 ℝ rates t).comp S) := by80 let u : ℕ → ℝ≥0 := fun n => ⟨(1 / 2 : ℝ) ^ n, by positivity⟩81 let A := (resolventL1 ℝ rates t).comp S82 let B : ℕ → IntervalL1 ℝ →L[ℝ] Lp ℝ 1 haar :=83 fun n => (noiseL1 ℝ rates (u n)).comp A84 apply dyadicVanishing_of_opNorm_tendsto A B85 · intro n86 exact hnoise (u n) (by change 0 < (1 / 2 : ℝ) ^ n; positivity) A87 · have hb (n : ℕ) : ‖B n - A‖ ≤ (2 * (u n : ℝ) / (t : ℝ)) * ‖S‖ := by88 have he : B n - A =89 ((noiseL1 ℝ rates (u n)).comp (resolventL1 ℝ rates t) -90 resolventL1 ℝ rates t).comp S := by91 apply ContinuousLinearMap.ext92 intro f93 rfl94 rw [he]95 exact (ContinuousLinearMap.opNorm_comp_le _ _).trans96 (mul_le_mul_of_nonneg_right97 (norm_noise_comp_resolvent_sub_le_time ℝ rates t (u n)) (norm_nonneg S))98 apply squeeze_zero (fun n => norm_nonneg _) hb99 have hu : Tendsto (fun n => (u n : ℝ)) atTop (𝓝 0) :=100 tendsto_pow_atTop_nhds_zero_of_lt_one (by norm_num) (by norm_num)101 simpa using ((hu.const_mul 2).div_const (t : ℝ)).mul_const ‖S‖102103end PL1.EnfloBush104