OAI/Analysis/KadisonSimilarity/FreeProduct/StrongCompressionTransfer.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite-compression estimates pass to the full representation. Only strong convergence of the selfadjoint compressions is needed: the two projection factors are moved to the two test vectors in the weak operator matrix coefficients.

  1. theorem OAI.KadisonSimilarity.weakOperator_tendsto_selfadjoint_compressions line 20
  2. theorem OAI.KadisonSimilarity.matrix_commutator_bound_of_selfadjoint_compressions line 34

    Source documentation

    A fixed matrix commutator estimate for all finite compressions survives the limit, with exactly the same constant.

    theorem matrix_commutator_bound_of_selfadjoint_compressions
    (Q : I → H →L[ℂ] H) (hQ : ∀ i, (Q i).adjoint = Q i)
    (hlim : ∀ x, Tendsto (fun i => Q i x) l (𝓝 x))
    [l.NeBot] (T : H →L[ℂ] H) (n : ℕ)
    (X : HilbertCopies H n →L[ℂ] HilbertCopies H n) {c : ℝ} (hc : 0 ≤ c)
    (hbound : ∀ᶠ i in l,
      ‖commutator (amplify ((Q i).comp (T.comp (Q i))) n) X‖ ≤ c) :
    ‖commutator (amplify T n) X‖ ≤ c := by
…

    Mentions: OAI.KadisonSimilarity.HilbertCopies, OAI.KadisonSimilarity.commutator, OAI.KadisonSimilarity.amplify