ClippedSequenceDrift.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restoring the coordinate coefficient drift

The quotient norm estimate makes the discarded spectral tails strongly zero. This applies to both fixed vectors and vectors moved by a bounded unitary sequence. The latter restoration retains exactly the commutator of that unitary, independently of the number of coefficients.

theorem OAI.KadisonKastler.represented_discarded_column_contract line 33

Source documentation

The discarded column is contractive whenever the original one is.

theorem represented_discarded_column_contract
    (K : W → B) (β : W → ℝ) (hβ : ∀ w, 0 < β w)
    (hK : ∀ z : H, ‖WithLp.toLp 2 (fun w => ρ (K w) z)‖ ≤ ‖z‖) (z : H) :
    ‖WithLp.toLp 2 (fun w => ρ (K w - spectralClip (β w) (K w)) z)‖ ≤ ‖z‖ := by
…

Mentions: OAI.KadisonKastler.spectralClip

theorem OAI.KadisonKastler.IsTraceQuotient.eventually_coefficient_drift line 44

Source documentation

Restore all finitely many clipped coefficients on a fixed vector.

theorem IsTraceQuotient.eventually_coefficient_drift
    (hπ : IsTraceQuotient τ l π) (hρ : TraceStrongContinuous τ ρ)
    (K : W → BoundedSequence B) (β : W → ℝ) (hβ : ∀ w, 0 < β w)
    (hbound : ∀ w, ‖π (K w)‖ ≤ β w)
    (T : H →L[ℂ] H) (z : H) {C : ℝ}
    (hclip : ∀ j, ‖WithLp.toLp 2 (fun w =>
      (T * ρ (spectralClip (β w) (K w j)) -
        ρ (spectralClip (β w) (K w j)) * T) z)‖ ≤ C) :
    ∀ ε > 0, ∀ᶠ j in l,
      ‖WithLp.toLp 2 (fun w => (T * ρ (K w j) - ρ (K w j) * T) z)‖ ≤ C + ε := by
…

Mentions: OAI.KadisonKastler.IsTraceQuotient, OAI.KadisonKastler.TraceStrongContinuous, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.spectralClip

theorem OAI.KadisonKastler.IsTraceQuotient.eventually_moving_coefficient_drift line 74

Source documentation

The moving-vector version costs only the given coordinate commutator bound in addition to the clipped drift.

theorem IsTraceQuotient.eventually_moving_coefficient_drift
    (hπ : IsTraceQuotient τ l π) (hρ : TraceStrongContinuous τ ρ)
    (K : W → BoundedSequence B) (β : W → ℝ) (hβ : ∀ w, 0 < β w)
    (hbound : ∀ w, ‖π (K w)‖ ≤ β w)
    (hK : ∀ j z, ‖WithLp.toLp 2 (fun w => ρ (K w j) z)‖ ≤ ‖z‖)
    (s : BoundedSequence B) (T : H →L[ℂ] H) (y : H) {C D : ℝ}
    (hclip : ∀ j, ‖WithLp.toLp 2 (fun w =>
      (T * ρ (spectralClip (β w) (K w j)) -
        ρ (spectralClip (β w) (K w j)) * T) (ρ (s j) y))‖ ≤ C)
    (hcomm : ∀ j, ‖(T * ρ (s j) - ρ (s j) * T) y‖ ≤ D) :
    ∀ ε > 0, ∀ᶠ j in l,
      ‖WithLp.toLp 2 (fun w =>
…

Mentions: OAI.KadisonKastler.IsTraceQuotient, OAI.KadisonKastler.TraceStrongContinuous, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.spectralClip