CompleteMapTensorGap.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Complete linear approximation controls the actual regular tensor gap

theorem OAI.KadisonKastler.rescale_contraction line 14

theorem OAI.KadisonKastler.matrix_approx_of_completely_close_map line 44

Source documentation

Normalizing the output of a completely close linear map costs at most one further copy of its error. No positivity assumption is required.

theorem matrix_approx_of_completely_close_map
    (M N : VonNeumannAlgebra H) (F : Algebra M →ₗ[ℂ] (H →L[ℂ] H))
    (hFN : ∀ x, F x ∈ N) {γ : ℝ} (hγ : 0 ≤ γ)
    (hclose : CompletelyBoundedBy (M.toStarSubalgebra.subtype.toAlgHom.toLinearMap - F) γ)
    (n : ℕ) (X : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H))
    (hX : ∀ i j, X i j ∈ M) (hXn : ‖X‖ ≤ 1) :
    ∃ Y : CStarMatrix (Fin n) (Fin n) (H →L[ℂ] H),
      (∀ i j, Y i j ∈ N) ∧ ‖Y‖ ≤ 1 ∧ ‖X - Y‖ ≤ 2 * γ := by
…

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

theorem OAI.KadisonKastler.kkDistance_regularTensorAlgebra_le_of_completely_close_maps line 76