PL1/TailSpikeMultiplication.lean

All source files · Download exact source

SHA-256: a962945af651b61a976557e5b13ca79b9b60650e946189e0acd86d4f8de4e247

1import PL1.TailSpikes2import PL1.HeadTailNoise3import PL1.HeadTailNorms4import PL1.ResolventMultiplication5import PL1.IntrinsicSpikes67/-! # Actual semigroup and resolvent commutators of tail-spike multiplication -/89noncomputable section10open MeasureTheory11open scoped ENNReal NNReal12namespace PL1.TailSpikes13open Walsh Noise HeadTail FiniteCoordinateKernels1415variable {K : Type*} [RCLike K]1617/-- The commutator norm factors exactly into its tail and head norms. -/18theorem norm_noise_multiplier_commutator_eq (rates : ℕ → ℝ≥0) (u : ℝ≥0)19    {S T : Finset ℕ} (hST : Disjoint S T)20    (f : C(Walsh.Group, K)) (q : C(Walsh.Group, ℝ))21    (hf : HeadTail.DependsOn S f) (hq : HeadTail.DependsOn T q) :22    ‖noiseL1 K rates u (L1Multiplication.multiplier K q (ContinuousMap.toLp 1 haar K f)) -23      L1Multiplication.multiplier K q (noiseL1 K rates u (ContinuousMap.toLp 1 haar K f))‖ =24      ‖noiseL1 ℝ rates u (ContinuousMap.toLp 1 haar ℝ q) - ContinuousMap.toLp 1 haar ℝ q‖ *25        ‖noiseL1 K rates u (ContinuousMap.toLp 1 haar K f)‖ := by26  let f' := noiseContinuous K rates u S f hf27  let q' := noiseContinuous ℝ rates u T q hq - q28  have hf' : HeadTail.DependsOn S f' := noiseContinuous_dependsOn rates u S f hf29  have hq' : HeadTail.DependsOn T q' := by30    intro x y hxy31    exact congrArg₂ (fun a b : ℝ => a - b)32      (noiseContinuous_dependsOn rates u T q hq x y hxy) (hq x y hxy)33  rw [noiseL1_multiplier_toLp rates u hST f q hf hq,34    ← L1Multiplication.multiplier_sub, ← noiseContinuous_toLp rates u S f hf]35  change ‖L1Multiplication.multiplier K q' (ContinuousMap.toLp 1 haar K f')‖ = _36  rw [norm_multiplier_toLp hST f' q' hf' hq']37  simp only [q', f', map_sub, noiseContinuous_toLp]3839/-- The genuine semigroup commutator estimate for every member of an actual spike family. -/40theorem RateFamily.norm_noise_commutator_le {rates : ℕ → ℝ≥0} {d : ℕ}41    {T : PositiveTime} {δ : ℝ} (Q : RateFamily rates d T δ)42    (a : Assignments Q.coordinates) (f : C(Walsh.Group, K))43    (hf : HeadTail.DependsOn (Finset.range d) f) (u : ℝ≥0) :44    ‖noiseL1 K rates u (L1Multiplication.multiplier K (Q.q a) (ContinuousMap.toLp 1 haar K f)) -45      L1Multiplication.multiplier K (Q.q a) (noiseL1 K rates u (ContinuousMap.toLp 1 haar K f))‖ ≤46      2 * (1 - Real.exp (-(u : ℝ) / (T : ℝ))) * ‖ContinuousMap.toLp 1 haar K f‖ := by47  rw [norm_noise_multiplier_commutator_eq rates u Q.beyond_prefix.symm f (Q.q a) hf (Q.q_depends a)]48  apply mul_le_mul (Q.almost_invariant a u) ?_ (norm_nonneg _) ?_49  · exact ((noiseL1 K rates u).le_opNorm _).trans50      (by simpa only [one_mul] using (mul_le_mul_of_nonneg_right51        (norm_noiseL1_le_one K rates u) (norm_nonneg (ContinuousMap.toLp 1 haar K f))))52  · exact (norm_nonneg _).trans (Q.almost_invariant a u)5354/-- Exponential averaging yields the quantitative resolvent commutator used by the intrinsic norm. -/55theorem RateFamily.norm_resolvent_commutator_le {rates : ℕ → ℝ≥0} {d : ℕ}56    {T : PositiveTime} {δ : ℝ} (Q : RateFamily rates d T δ)57    (a : Assignments Q.coordinates) (f : C(Walsh.Group, K))58    (hf : HeadTail.DependsOn (Finset.range d) f) (t : PositiveTime) :59    ‖resolventL1 K rates t (L1Multiplication.multiplier K (Q.q a) (ContinuousMap.toLp 1 haar K f)) -60      L1Multiplication.multiplier K (Q.q a) (resolventL1 K rates t (ContinuousMap.toLp 1 haar K f))‖ ≤61      (2 * (t : ℝ) / (T : ℝ)) * ‖ContinuousMap.toLp 1 haar K f‖ :=62  Noise.norm_resolvent_commutator_le_time K rates t T _ _ (Q.norm_noise_commutator_le a f hf)6364/-- The same bound for the identity-minus-resolvent coordinates. -/65theorem RateFamily.norm_id_sub_resolvent_commutator_le {rates : ℕ → ℝ≥0} {d : ℕ}66    {T : PositiveTime} {δ : ℝ} (Q : RateFamily rates d T δ)67    (a : Assignments Q.coordinates) (f : C(Walsh.Group, K))68    (hf : HeadTail.DependsOn (Finset.range d) f) (t : PositiveTime) :69    ‖(L1Multiplication.multiplier K (Q.q a) (ContinuousMap.toLp 1 haar K f) -70        resolventL1 K rates t (L1Multiplication.multiplier K (Q.q a) (ContinuousMap.toLp 1 haar K f))) -71      L1Multiplication.multiplier K (Q.q a) (ContinuousMap.toLp 1 haar K f -72        resolventL1 K rates t (ContinuousMap.toLp 1 haar K f))‖ ≤73      (2 * (t : ℝ) / (T : ℝ)) * ‖ContinuousMap.toLp 1 haar K f‖ :=74  Noise.norm_id_sub_resolvent_commutator_le_time K rates t T _ _ (Q.norm_noise_commutator_le a f hf)7576#print axioms RateFamily.norm_id_sub_resolvent_commutator_le77end PL1.TailSpikes78