PL1/TraceVanishing.lean

All source files · Download exact source

SHA-256: 890c7b3c367774d840b52a5338772b4c890cff506b2fa2d7916b17579ad7fab0

1import PL1.MatrixSmoothing23/-! # An operator property preserved by bounded composition45The quantified pre- and post-compositions are actual bounded linear maps6to and from the reviewed interval L1 space. The definition does not assert7that any particular operator has this property.8-/910noncomputable section11open MeasureTheory Filter12open scoped Topology ENNReal1314namespace PL11516variable {𝕜 X Y Z : Type*} [RCLike 𝕜]17  [NormedAddCommGroup X] [NormedSpace 𝕜 X]18  [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]19  [NormedAddCommGroup Z] [NormedSpace 𝕜 Z]2021def HasVanishingDyadicTrace (S : X →L[𝕜] Y) : Prop :=22  ∀ (A : Y →L[𝕜] IntervalL1 𝕜) (B : IntervalL1 𝕜 →L[𝕜] X),23    Tendsto (fun n => DyadicTrace.trace n (A.comp (S.comp B))) atTop (𝓝 0)2425namespace HasVanishingDyadicTrace2627theorem comp_left {S : X →L[𝕜] Y} (hS : HasVanishingDyadicTrace S)28    (T : Y →L[𝕜] Z) : HasVanishingDyadicTrace (T.comp S) := by29  intro A B30  simpa only [ContinuousLinearMap.comp_assoc] using hS (A.comp T) B3132theorem comp_right {S : Y →L[𝕜] Z} (hS : HasVanishingDyadicTrace S)33    (T : X →L[𝕜] Y) : HasVanishingDyadicTrace (S.comp T) := by34  intro A B35  simpa only [ContinuousLinearMap.comp_assoc] using hS A (T.comp B)3637theorem smul {S : X →L[𝕜] Y} (hS : HasVanishingDyadicTrace S) (c : 𝕜) :38    HasVanishingDyadicTrace (c • S) := by39  intro A B40  have he : A.comp ((c • S).comp B) = (c • A).comp (S.comp B) := by41    apply ContinuousLinearMap.ext42    intro x43    simp only [ContinuousLinearMap.comp_apply, smul_apply, map_smul]44  rw [he]45  exact hS (c • A) B4647theorem one_le_norm_id_sub {S : X →L[𝕜] Y} (hS : HasVanishingDyadicTrace S)48    (A : Y →L[𝕜] IntervalL1 𝕜) (B : IntervalL1 𝕜 →L[𝕜] X) :49    1 ≤ ‖DyadicTrace.restrictLinfty50      (ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) - A.comp (S.comp B))‖ :=51  DyadicTrace.one_le_norm_id_sub _ (hS A B)5253theorem not_factors_identity {S : X →L[𝕜] Y} (hS : HasVanishingDyadicTrace S)54    (A : Y →L[𝕜] IntervalL1 𝕜) (B : IntervalL1 𝕜 →L[𝕜] X) :55    A.comp (S.comp B) ≠ ContinuousLinearMap.id 𝕜 (IntervalL1 𝕜) := by56  intro he57  have hn := hS.one_le_norm_id_sub A B58  rw [he, sub_self] at hn59  simp only [DyadicTrace.restrictLinfty, ContinuousLinearMap.zero_comp, norm_zero] at hn60  norm_num at hn6162end HasVanishingDyadicTrace6364end PL165