PL1/ResolventAlmostInvariant.lean

All source files · Download exact source

SHA-256: e22d417e1f4607418db24bfd7836199dcb1ecfa6fbcd94772dc7d74b02469c0e

1import PL1.ResolventNorms23/-!4# Quantitative almost invariance of actual resolvent images56The estimate used in the paper's tail-spike construction holds for every7coordinate-rate sequence and over either scalar field.8-/910noncomputable section11open MeasureTheory12open scoped NNReal1314namespace PL1.Noise15open Walsh1617variable (𝕜 : Type*) [RCLike 𝕜] (rates : ℕ → ℝ≥0)1819theorem norm_noise_comp_resolvent_sub_le (t : PositiveTime) (u : ℝ≥0) :20    ‖(noiseL1 𝕜 rates u).comp (resolventL1 𝕜 rates t) - resolventL1 𝕜 rates t‖ ≤21      2 * (1 - Real.exp (-(u : ℝ) / (t : ℝ))) := by22  let α : ℝ := Real.exp (-(u : ℝ) / (t : ℝ))23  let S := (noiseL1 𝕜 rates u).comp (resolventL1 𝕜 rates t)24  have hα : 0 ≤ 1 - α := sub_nonneg.mpr (Real.exp_le_one_iff.mpr25    (div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr u.coe_nonneg) t.property.le))26  have hS : ‖S‖ ≤ 1 := by27    have h := ContinuousLinearMap.opNorm_comp_le (noiseL1 𝕜 rates u) (resolventL1 𝕜 rates t)28    simpa only [norm_noiseL1_eq_one, norm_resolventL1_eq_one, mul_one] using h29  have htail : ‖resolventL1 𝕜 rates t - (α : 𝕜) • S‖ = 1 - α := by30    rw [← truncatedResolventL1_eq_noise_comp_resolvent]31    exact norm_resolventL1_sub_truncated_eq 𝕜 rates t u32  have heq : S - resolventL1 𝕜 rates t =33      ((1 - α : ℝ) : 𝕜) • S - (resolventL1 𝕜 rates t - (α : 𝕜) • S) := by34    rw [RCLike.ofReal_sub, RCLike.ofReal_one, sub_smul (1 : 𝕜) (α : 𝕜) S, one_smul]35    abel36  change ‖S - resolventL1 𝕜 rates t‖ ≤ 2 * (1 - α)37  rw [heq]38  calc39    _ ≤ ‖((1 - α : ℝ) : 𝕜) • S‖ + ‖resolventL1 𝕜 rates t - (α : 𝕜) • S‖ := norm_sub_le _ _40    _ = (1 - α) * ‖S‖ + (1 - α) := by41      rw [norm_smul, RCLike.norm_ofReal, abs_of_nonneg hα, htail]42    _ ≤ 2 * (1 - α) := by nlinarith4344theorem one_sub_exp_neg_div_le (t : PositiveTime) (u : ℝ≥0) :45    1 - Real.exp (-(u : ℝ) / (t : ℝ)) ≤ (u : ℝ) / (t : ℝ) := by46  have h := Real.add_one_le_exp (-(u : ℝ) / (t : ℝ))47  simp only [neg_div] at h ⊢48  linarith4950theorem norm_noise_comp_resolvent_sub_le_time (t : PositiveTime) (u : ℝ≥0) :51    ‖(noiseL1 𝕜 rates u).comp (resolventL1 𝕜 rates t) - resolventL1 𝕜 rates t‖ ≤52      2 * (u : ℝ) / (t : ℝ) :=53  (norm_noise_comp_resolvent_sub_le 𝕜 rates t u).trans (by54    have h := one_sub_exp_neg_div_le t u55    convert mul_le_mul_of_nonneg_left h (by norm_num : (0 : ℝ) ≤ 2) using 156    ring)5758theorem norm_noise_resolvent_sub_le (t : PositiveTime) (u : ℝ≥0) (f : Lp 𝕜 1 haar) :59    ‖noiseL1 𝕜 rates u (resolventL1 𝕜 rates t f) - resolventL1 𝕜 rates t f‖ ≤60      2 * (1 - Real.exp (-(u : ℝ) / (t : ℝ))) * ‖f‖ := by61  exact ((noiseL1 𝕜 rates u |>.comp (resolventL1 𝕜 rates t)) -62    resolventL1 𝕜 rates t).le_opNorm f |>.trans63      (mul_le_mul_of_nonneg_right (norm_noise_comp_resolvent_sub_le 𝕜 rates t u) (norm_nonneg f))6465theorem norm_noise_resolvent_sub_le_time (t : PositiveTime) (u : ℝ≥0) (f : Lp 𝕜 1 haar) :66    ‖noiseL1 𝕜 rates u (resolventL1 𝕜 rates t f) - resolventL1 𝕜 rates t f‖ ≤67      (2 * (u : ℝ) / (t : ℝ)) * ‖f‖ := by68  exact ((noiseL1 𝕜 rates u |>.comp (resolventL1 𝕜 rates t)) -69    resolventL1 𝕜 rates t).le_opNorm f |>.trans70      (mul_le_mul_of_nonneg_right (norm_noise_comp_resolvent_sub_le_time 𝕜 rates t u) (norm_nonneg f))7172end PL1.Noise73