OAI/Analysis/OperatorAlgebra/HilbertOperatorExtension.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Cpc maps into Hilbert-space operators extend along faithful unital inclusions. Finite-dimensional compressions extend by the matrix theorem; a weak operator ultralimit preserves complete positivity and all matrix coefficients of the original map.

  1. lemma OAI.WeakPureInfiniteness.compression_contractive line 21
  2. lemma OAI.WeakPureInfiniteness.cpc_comp_norm line 29
  3. theorem OAI.WeakPureInfiniteness.finiteCorner_cpc_extension line 38
  4. theorem OAI.WeakPureInfiniteness.hilbertOperator_cpc_extension line 72

    Source documentation

    The Hilbert-operator cpc extension theorem, obtained from finite matrix extensions and weak operator compactness.

    theorem hilbertOperator_cpc_extension [Nontrivial H]
    (ι : A →⋆ₐ[ℂ] B) (hι : Function.Injective ι)
    (φ : A →L[ℂ] (H →L[ℂ] H)) (hφ : CompletelyPositive φ) (hφn : ‖φ‖ ≤ 1) :
    ∃ Φ : B →L[ℂ] (H →L[ℂ] H), CompletelyPositive Φ ∧ ‖Φ‖ ≤ 1 ∧
      ∀ a, Φ (ι a) = φ a := by
…

    Mentions: OAI.WeakPureInfiniteness.CompletelyPositive