GraphRowApproximation.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Actual row approximants from a completely close linear map

The map need only be linear with range in the second algebra. Its complete norm distance from inclusion supplies the same row approximants used by the graph argument, with no further approximation assumption.

theorem OAI.KadisonKastler.injective_starAlgHom_finite_rectangular_norm line 25

Source documentation

A faithful star homomorphism preserves arbitrary finite rectangular matrix norms, not only matrices indexed by finite ordinals.

theorem injective_starAlgHom_finite_rectangular_norm
    (φ : A →⋆ₐ[ℂ] B) (hφ : Function.Injective φ)
    {I J : Type*} [Fintype I] [Fintype J] (X : CStarMatrix I J A) :
    ‖CStarMatrix.mapₗ φ.toAlgHom.toLinearMap X‖ = ‖X‖ := by
…

theorem OAI.KadisonKastler.completelyBoundedBy_operator_row line 33

Source documentation

A complete bound controls a row indexed on the left by Unit.

theorem completelyBoundedBy_operator_row (F : A →ₗ[ℂ] B) {γ : ℝ}
    (hF : CompletelyBoundedBy F γ) {k : ℕ} (hk : 0 < k)
    (X : CStarMatrix Unit (Fin k) A) :
    ‖CStarMatrix.mapₗ F X‖ ≤ γ * ‖X‖ := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.exists_graphRow_approx_of_completelyBoundedBy line 59

Source documentation

A completely close map with range in N provides each concrete row approximant required by the graph comparison theorem.

theorem exists_graphRow_approx_of_completelyBoundedBy
    (M N : VonNeumannAlgebra H) (F : Algebra M →ₗ[ℂ] (H →L[ℂ] H))
    (hFN : ∀ x, F x ∈ N) {γ : ℝ}
    (hclose : CompletelyBoundedBy (M.toStarSubalgebra.subtype.toAlgHom.toLinearMap - F) γ)
    (k : ℕ) (X : Fin k → H →L[ℂ] H) (hX : ∀ i, X i ∈ M) :
    ∃ Z : Fin k → H →L[ℂ] H, (∀ i, Z i ∈ N) ∧
      ‖operatorRow X - operatorRow Z‖ ≤ γ * ‖operatorRow X‖ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.operatorRow