UltrapowerCommutators.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Coordinatewise commutator estimates pass to the Hilbert ultrapower, and then to any reducing closed subspace.

theorem OAI.KadisonSimilarity.hilbertUltraproduct_commutator line 18

Source documentation

The actual operator map on the Hilbert ultrapower respects commutators.

theorem hilbertUltraproduct_commutator (ω : Ultrafilter ι)
    (T X : lp (fun _ : ι => H →L[ℂ] H) ∞) :
    commutator (HilbertUltraproduct.map ω T) (HilbertUltraproduct.map ω X) =
      HilbertUltraproduct.map ω (T * X - X * T) := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_hilbertUltraproduct_commutator_le line 29

Source documentation

Only an eventual coordinate bound is required, exactly as in the small-corner lifting argument.

theorem norm_hilbertUltraproduct_commutator_le (ω : Ultrafilter ι)
    (T X : lp (fun _ : ι => H →L[ℂ] H) ∞) {c : ℝ} (hc : 0 ≤ c)
    (hbound : ∀ᶠ i in (ω : Filter ι), ‖commutator (T i) (X i)‖ ≤ c) :
    ‖commutator (HilbertUltraproduct.map ω T) (HilbertUltraproduct.map ω X)‖ ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator

theorem OAI.KadisonSimilarity.norm_reducing_compression_commutator_le line 41

Source documentation

Compression to a reducing subspace preserves a commutator estimate. The operator being tested need not preserve that subspace.

theorem norm_reducing_compression_commutator_le (V : K →ₗᵢ[ℂ] H)
    (T X : H →L[ℂ] H) (X₀ : K →L[ℂ] K)
    (hXV : X.comp V.toContinuousLinearMap = V.toContinuousLinearMap.comp X₀)
    (hXVstar : X.adjoint.comp V.toContinuousLinearMap =
      V.toContinuousLinearMap.comp X₀.adjoint)
    {c : ℝ} (hbound : ‖commutator T X‖ ≤ c) :
    ‖commutator (V.toContinuousLinearMap.adjoint.comp (T.comp V.toContinuousLinearMap)) X₀‖
      ≤ c := by
…

Mentions: OAI.KadisonSimilarity.commutator