MatrixCorrection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Rectangular matrix estimates for multiplication correction

The inverse and corrected-map bounds used in the UCP criterion hold at every rectangular C⋆-matrix size. The source and target may be represented in a third ambient C⋆-algebra.

theorem OAI.KadisonKastler.matrix_map_comp line 24

Source documentation

Entrywise application respects composition on rectangular matrices.

theorem matrix_map_comp (F : A →ₗ[ℂ] B) (G : B →ₗ[ℂ] C) {p q : ℕ}
    (X : CStarMatrix (Fin p) (Fin q) A) :
    CStarMatrix.mapₗ (G.comp F) X = CStarMatrix.mapₗ G (CStarMatrix.mapₗ F X) := by
…

theorem OAI.KadisonKastler.matrix_map_id line 32

Source documentation

The identity linear map acts identically at every rectangular level.

theorem matrix_map_id {p q : ℕ} (X : CStarMatrix (Fin p) (Fin q) A) :
    CStarMatrix.mapₗ (LinearMap.id : A →ₗ[ℂ] A) X = X := by
…

theorem OAI.KadisonKastler.inverse_completelyBoundedBy_of_close_isometries line 39

Source documentation

A linear equivalence which is completely close to a complete isometry has completely bounded inverse, with the same bound at every matrix size.

theorem inverse_completelyBoundedBy_of_close_isometries
    (F : A ≃ₗ[ℂ] B) (ρ : A →ₗ[ℂ] C) (ι : B →ₗ[ℂ] C) {e : ℝ}
    (he : e < 1) (hρ : CompletelyIsometric ρ) (hι : CompletelyIsometric ι)
    (hclose : CompletelyBoundedBy (ι.comp F.toLinearMap - ρ) e) :
    CompletelyBoundedBy F.symm.toLinearMap ((1 - e)⁻¹) := by
…

Mentions: OAI.KadisonKastler.CompletelyIsometric, OAI.KadisonKastler.CompletelyBoundedBy

theorem OAI.KadisonKastler.correctedMap_completelyBoundedBy_thirty_two_mul line 59

Source documentation

Correcting multiplication changes the represented map by at most 32e at every rectangular matrix size, under the explicit UCP tolerance.

theorem correctedMap_completelyBoundedBy_thirty_two_mul
    (F : A ≃ₗ[ℂ] B) (L : A ≃ₗ[ℂ] A) (ρ : A →ₗ[ℂ] C) (ι : B →ₗ[ℂ] C)
    {e : ℝ} (he : 0 ≤ e) (he₁ : e < 1 / 1000)
    (hι : CompletelyIsometric ι) (hF : CompletelyBoundedBy F.toLinearMap 1)
    (hclose : CompletelyBoundedBy (ι.comp F.toLinearMap - ρ) e)
    (hL : CompletelyBoundedBy (L.toLinearMap - LinearMap.id) (30 * e / (1 - e))) :
    CompletelyBoundedBy (ι.comp (F.toLinearMap.comp L.symm.toLinearMap) - ρ) (32 * e) := by
…

Mentions: OAI.KadisonKastler.CompletelyIsometric, OAI.KadisonKastler.CompletelyBoundedBy