PL1/HilbertDyadicTrace.lean
All source files · Download exact source
SHA-256: efec64b32d010b847a3a5bf1712178153551f08d439d01a3e542ed270776523b
1import PL1.HilbertTraceBounds2import PL1.DyadicTrace34/-! # Dyadic trace decay from Hilbert smoothing on bounded inputs -/56noncomputable section7set_option autoImplicit false8set_option maxHeartbeats 8000009open MeasureTheory Filter10open scoped ENNReal BigOperators Topology1112namespace PL1.HilbertDyadicTrace1314attribute [local instance] DyadicTrace.intervalMeasure_probability1516variable {𝕜 H : Type*} [RCLike 𝕜] [NormedAddCommGroup H]17 [InnerProductSpace 𝕜 H] [CompleteSpace H]1819abbrev cellVector (n i : ℕ) : Lp 𝕜 ∞ intervalMeasure :=20 TraceBounds.cellVector intervalMeasure (DyadicTrace.cell n)21 (DyadicTrace.measurableSet_cell n) i2223theorem norm_trace_le (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)24 (T : H →L[𝕜] IntervalL1 𝕜) (V : Lp 𝕜 ∞ intervalMeasure →L[𝕜] H)25 (hfactor : DyadicTrace.restrictLinfty R = T.comp V) (n : ℕ) :26 ‖DyadicTrace.trace n R‖ ≤ ‖T‖ *27 Real.sqrt (∑ i ∈ Finset.range (2 ^ n), ‖V (cellVector (𝕜 := 𝕜) n i)‖ ^ 2) := by28 change ‖TraceBounds.finiteTrace (Finset.range (2 ^ n)) (cellVector (𝕜 := 𝕜) n)29 (TraceBounds.cellFunctional (𝕜 := 𝕜) intervalMeasure (DyadicTrace.cell n)30 (DyadicTrace.measurableSet_cell n)) (DyadicTrace.restrictLinfty R)‖ ≤ _31 rw [hfactor]32 exact HilbertTraceBounds.norm_sum_cell_apply_le intervalMeasure (DyadicTrace.cell n)33 (DyadicTrace.measurableSet_cell n) (Finset.range (2 ^ n))34 (DyadicTrace.pairwiseDisjoint_cell n) T (fun i => V (cellVector (𝕜 := 𝕜) n i))3536theorem trace_tendsto_zero_of_square_sum (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)37 (T : H →L[𝕜] IntervalL1 𝕜) (V : Lp 𝕜 ∞ intervalMeasure →L[𝕜] H)38 (hfactor : DyadicTrace.restrictLinfty R = T.comp V)39 (hV : Tendsto (fun n => ∑ i ∈ Finset.range (2 ^ n),40 ‖V (cellVector (𝕜 := 𝕜) n i)‖ ^ 2) atTop (𝓝 0)) :41 Tendsto (fun n => DyadicTrace.trace n R) atTop (𝓝 0) := by42 apply tendsto_zero_iff_norm_tendsto_zero.mpr43 apply squeeze_zero (fun n => norm_nonneg _) (norm_trace_le R T V hfactor)44 simpa using (hV.sqrt.const_mul ‖T‖)4546omit [CompleteSpace H] in47theorem square_sum_le_geometric48 (V : Lp 𝕜 ∞ intervalMeasure →L[𝕜] H) (C q : ℝ) (_hC : 0 ≤ C) (_hq : 0 ≤ q)49 (hV : ∀ n i, i < 2 ^ n → ‖V (cellVector (𝕜 := 𝕜) n i)‖ ≤ C * q ^ n) (n : ℕ) :50 (∑ i ∈ Finset.range (2 ^ n), ‖V (cellVector (𝕜 := 𝕜) n i)‖ ^ 2) ≤51 C ^ 2 * (2 * q ^ 2) ^ n := by52 calc53 _ ≤ ∑ i ∈ Finset.range (2 ^ n), (C * q ^ n) ^ 2 :=54 Finset.sum_le_sum (fun i hi =>55 pow_le_pow_left₀ (norm_nonneg _) (hV n i (Finset.mem_range.mp hi)) 2)56 _ = C ^ 2 * (2 * q ^ 2) ^ n := by57 simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat,58 mul_pow, ← pow_mul, mul_comm n 2]59 ring6061theorem trace_tendsto_zero_of_geometric_bound (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)62 (T : H →L[𝕜] IntervalL1 𝕜) (V : Lp 𝕜 ∞ intervalMeasure →L[𝕜] H)63 (hfactor : DyadicTrace.restrictLinfty R = T.comp V)64 (C q : ℝ) (hC : 0 ≤ C) (hq : 0 ≤ q) (hdecay : 2 * q ^ 2 < 1)65 (hV : ∀ n i, i < 2 ^ n → ‖V (cellVector (𝕜 := 𝕜) n i)‖ ≤ C * q ^ n) :66 Tendsto (fun n => DyadicTrace.trace n R) atTop (𝓝 0) := by67 apply trace_tendsto_zero_of_square_sum R T V hfactor68 apply squeeze_zero (fun n => Finset.sum_nonneg (fun i _ => sq_nonneg _))69 (square_sum_le_geometric V C q hC hq hV)70 simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one71 (show 0 ≤ 2 * q ^ 2 by positivity) hdecay).const_mul (C ^ 2)7273theorem one_le_norm_id_sub_of_geometric_bound (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)74 (T : H →L[𝕜] IntervalL1 𝕜) (V : Lp 𝕜 ∞ intervalMeasure →L[𝕜] H)75 (hfactor : DyadicTrace.restrictLinfty R = T.comp V)76 (C q : ℝ) (hC : 0 ≤ C) (hq : 0 ≤ q) (hdecay : 2 * q ^ 2 < 1)77 (hV : ∀ n i, i < 2 ^ n → ‖V (cellVector (𝕜 := 𝕜) n i)‖ ≤ C * q ^ n) :78 1 ≤ ‖DyadicTrace.restrictLinfty (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) - R)‖ :=79 DyadicTrace.one_le_norm_id_sub R80 (trace_tendsto_zero_of_geometric_bound R T V hfactor C q hC hq hdecay hV)8182theorem trace_tendsto_zero_of_power_bound (R : IntervalL1 𝕜 →L[𝕜] IntervalL1 𝕜)83 (T : H →L[𝕜] IntervalL1 𝕜) (V : Lp 𝕜 ∞ intervalMeasure →L[𝕜] H)84 (hfactor : DyadicTrace.restrictLinfty R = T.comp V)85 (C r : ℝ) (hC : 0 ≤ C) (hr : 1 / 2 < r)86 (hV : ∀ n i, i < 2 ^ n →87 ‖V (cellVector (𝕜 := 𝕜) n i)‖ ≤ C * (((2 : ℝ) ^ n)⁻¹) ^ r) :88 Tendsto (fun n => DyadicTrace.trace n R) atTop (𝓝 0) := by89 have hq : 0 ≤ (2 : ℝ) ^ (-r) := Real.rpow_nonneg (by norm_num) _90 have hdecay : 2 * ((2 : ℝ) ^ (-r)) ^ 2 < 1 := by91 have heq : 2 * ((2 : ℝ) ^ (-r)) ^ 2 = (2 : ℝ) ^ (1 - 2 * r) := by92 rw [← Real.rpow_mul_natCast (by norm_num : (0 : ℝ) ≤ 2)]93 norm_num only [Nat.cast_ofNat]94 rw [show -r * 2 = -(2 * r) by ring, Real.rpow_sub (by norm_num : (0 : ℝ) < 2)]95 rw [Real.rpow_one, Real.rpow_neg (by norm_num : (0 : ℝ) ≤ 2)]96 rfl97 rw [heq]98 exact Real.rpow_lt_one_of_one_lt_of_neg (by norm_num) (by linarith)99 apply trace_tendsto_zero_of_geometric_bound R T V hfactor C ((2 : ℝ) ^ (-r)) hC hq hdecay100 intro n i hi101 have heq : (((2 : ℝ) ^ n)⁻¹) ^ r = ((2 : ℝ) ^ (-r)) ^ n := by102 rw [← Real.rpow_neg_eq_inv_rpow, ← Real.rpow_natCast_mul (by norm_num : (0 : ℝ) ≤ 2),103 mul_comm (n : ℝ) (-r), Real.rpow_mul_natCast (by norm_num : (0 : ℝ) ≤ 2)]104 simpa only [heq] using hV n i hi105106end PL1.HilbertDyadicTrace107