PL1/IntrinsicSpikes.lean
All source files · Download exact source
SHA-256: 331dfd2fdd5ea3f3d056c7ae7085be90381f16951a029c215848494ab7c047dc
1import PL1.IntrinsicSpikeEstimates2import PL1.ConcreteResolvents34/-!5# The dyadic intrinsic spike norm and separation bounds67This file sums the actual resolvent commutator estimates with the intrinsic8coordinate weights. The remaining inputs explicitly concern multiplication9and head/tail independence in the genuine Haar L¹ space, over real or complex10scalars. No alternative intrinsic norm is introduced.11-/1213noncomputable section14open MeasureTheory15open scoped BigOperators ENNReal NNReal1617namespace PL1.IntrinsicSpikes18open Noise Walsh IntrinsicGraph ResolventEstimates IntrinsicSpikeEstimates1920/-- The exact error coefficient in the manuscript's spike norm estimate. -/21def eta (T : PositiveTime) : ℝ := (2 / (T : ℝ)) * (dyadicRatio / (1 - dyadicRatio))2223theorem eta_pos (T : PositiveTime) : 0 < eta T :=24 mul_pos (div_pos (by norm_num) T.property)25 (div_pos dyadicRatio_pos one_sub_dyadicRatio_pos)2627theorem eta_eq (T : PositiveTime) : eta T = 2 / ((T : ℝ) * (Real.sqrt 2 - 1)) := by28 have hs : Real.sqrt 2 ≠ 0 := (Real.sqrt_pos.mpr (by norm_num)).ne'29 have hs1 : Real.sqrt 2 - 1 ≠ 0 := by30 have hsq := Real.sq_sqrt (by norm_num : (0 : ℝ) ≤ 2)31 have hnonneg := Real.sqrt_nonneg (2 : ℝ)32 nlinarith33 unfold eta dyadicRatio34 field_simp3536theorem exists_eta_lt {ε : ℝ} (hε : 0 < ε) : ∃ T : PositiveTime, eta T < ε := by37 let C : ℝ := 2 * (dyadicRatio / (1 - dyadicRatio))38 have hC : 0 < C := mul_pos (by norm_num)39 (div_pos dyadicRatio_pos one_sub_dyadicRatio_pos)40 let T : PositiveTime := ⟨C / ε + 1, by positivity⟩41 refine ⟨T, ?_⟩42 have heq : eta T = C / (T : ℝ) := by dsimp [eta, C]; ring43 rw [heq, div_lt_iff₀ T.property]44 have hc := div_mul_cancel₀ C hε.ne'45 change C < ε * (C / ε + 1)46 nlinarith4748def error (T : PositiveTime) (b : ℝ) : ℕ → ℝ49 | 0 => 050 | n + 1 => (2 / (T : ℝ)) * dyadicRatio ^ (n + 1) * b5152theorem error_summable (T : PositiveTime) (b : ℝ) : Summable (error T b) :=53 (summable_nat_add_iff 1).mp54 ((geometric_tail_summable.mul_left (2 / (T : ℝ))).mul_right b)5556theorem error_tsum (T : PositiveTime) (b : ℝ) : (∑' n, error T b n) = eta T * b := by57 rw [(error_summable T b).tsum_eq_zero_add]58 simp only [error, zero_add, tsum_mul_right, tsum_mul_left, geometric_tail_tsum, eta]5960variable {𝕜 : Type*} [RCLike 𝕜]6162theorem coordinate_commutator_le (rates : ℕ → ℝ≥0)63 (M : Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar)64 (f : (dyadicSystem 𝕜 rates).IntrinsicSpace) (T : PositiveTime)65 (hdefect : ∀ t : PositiveTime,66 ‖(M (evalZero (dyadicSystem 𝕜 rates).analysis f) -67 resolventL1 𝕜 rates t (M (evalZero (dyadicSystem 𝕜 rates).analysis f))) -68 M (evalZero (dyadicSystem 𝕜 rates).analysis f -69 resolventL1 𝕜 rates t (evalZero (dyadicSystem 𝕜 rates).analysis f))‖ ≤70 2 * (t : ℝ) / (T : ℝ) * ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖) :71 ∀ n, ‖(dyadicSystem 𝕜 rates).analysis n72 (M (evalZero (dyadicSystem 𝕜 rates).analysis f)) -73 M (coord (dyadicSystem 𝕜 rates).analysis n f)‖ ≤74 error T ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖ n := by75 intro n76 rw [coord_eq]77 cases n with78 | zero => simp [DyadicSystem.analysis, analysisCoordinate, error]79 | succ n =>80 simp only [DyadicSystem.analysis, analysisCoordinate,81 smul_apply, sub_apply,82 ContinuousLinearMap.id_apply, map_smul, ← smul_sub, norm_smul,83 RCLike.norm_ofReal,84 abs_of_nonneg (inv_nonneg.mpr (pow_nonneg dyadicRatio_nonneg _))]85 have h := mul_le_mul_of_nonneg_left (hdefect (dyadicTime (n + 1)))86 (inv_nonneg.mpr (pow_nonneg dyadicRatio_nonneg (n + 1)))87 apply h.trans_eq88 have ht : (dyadicTime (n + 1) : ℝ) = (dyadicRatio ^ (n + 1)) ^ 2 := by89 dsimp [dyadicTime]90 rw [← pow_mul, ← pow_mul, Nat.mul_comm]91 rw [ht]92 dsimp [error]93 field_simp9495theorem exists_product (rates : ℕ → ℝ≥0)96 (M : Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar)97 (f : (dyadicSystem 𝕜 rates).IntrinsicSpace) (T : PositiveTime)98 (hpres : ∀ n, ‖M (coord (dyadicSystem 𝕜 rates).analysis n f)‖ =99 ‖coord (dyadicSystem 𝕜 rates).analysis n f‖)100 (hcomm : ∀ n, ‖(dyadicSystem 𝕜 rates).analysis n101 (M (evalZero (dyadicSystem 𝕜 rates).analysis f)) -102 M (coord (dyadicSystem 𝕜 rates).analysis n f)‖ ≤103 error T ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖ n) :104 ∃ g : (dyadicSystem 𝕜 rates).IntrinsicSpace,105 evalZero (dyadicSystem 𝕜 rates).analysis g =106 M (evalZero (dyadicSystem 𝕜 rates).analysis f) ∧107 |‖g‖ - ‖f‖| ≤ eta T * ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖ := by108 simpa only [error_tsum] using IntrinsicSpikeEstimates.exists_product rfl M f109 (error T ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖)110 (error_summable T _) hpres hcomm111112theorem separation (rates : ℕ → ℝ≥0)113 (M : Lp 𝕜 1 haar →L[𝕜] Lp 𝕜 1 haar)114 (h f g : (dyadicSystem 𝕜 rates).IntrinsicSpace)115 (hg : evalZero (dyadicSystem 𝕜 rates).analysis g =116 M (evalZero (dyadicSystem 𝕜 rates).analysis f)) (T : PositiveTime) (δ : ℝ)117 (hsep : ∀ n, (1 - 2 * δ) *118 (‖coord (dyadicSystem 𝕜 rates).analysis n h‖ +119 ‖coord (dyadicSystem 𝕜 rates).analysis n f‖) ≤120 ‖coord (dyadicSystem 𝕜 rates).analysis n h +121 M (coord (dyadicSystem 𝕜 rates).analysis n f)‖)122 (hcomm : ∀ n, ‖(dyadicSystem 𝕜 rates).analysis n123 (M (evalZero (dyadicSystem 𝕜 rates).analysis f)) -124 M (coord (dyadicSystem 𝕜 rates).analysis n f)‖ ≤125 error T ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖ n) :126 (1 - 2 * δ) * (‖h‖ + ‖f‖) -127 eta T * ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖ ≤ ‖h + g‖ := by128 simpa only [error_tsum] using IntrinsicSpikeEstimates.separation M h f g hg129 (error T ‖evalZero (dyadicSystem 𝕜 rates).analysis f‖)130 (error_summable T _) (1 - 2 * δ) hsep hcomm131132end PL1.IntrinsicSpikes133