CompletelyBounded.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Matrix bounds for perturbation maps

All norms here are the C*-matrix norms, including for rectangular matrices. The rectangular formulation records exactly the estimates needed for the Haagerup product norm in the multiplication-correction argument.

theorem OAI.KadisonKastler.rectangular_toCLM_mul line 23

theorem OAI.KadisonKastler.rectangular_norm_mul_le line 31

Source documentation

Submultiplicativity also holds for rectangular C*-matrices.

theorem rectangular_norm_mul_le {p r q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin q) A) :
    ‖X * Y‖ ≤ ‖X‖ * ‖Y‖ := by
…

def OAI.KadisonKastler.CompletelyBoundedBy line 38
Source documentation
A complete bound, expressed on all finite rectangular matrix levels.
```
def CompletelyBoundedBy (F : A →ₗ[ℂ] B) (c : ℝ) : Prop :=
…
```
def OAI.KadisonKastler.CompletelyIsometric line 43
Source documentation
Complete isometry in the same rectangular convention.
```
def CompletelyIsometric (F : A →ₗ[ℂ] B) : Prop :=
…
```
def OAI.KadisonKastler.matrixLinearEquiv line 50
Source documentation
Entrywise application of a linear equivalence is an equivalence at every rectangular matrix size.
```
def matrixLinearEquiv (F : A ≃ₗ[ℂ] B) (p q : ℕ) :
    CStarMatrix (Fin p) (Fin q) A ≃ₗ[ℂ] CStarMatrix (Fin p) (Fin q) B where
…
```
theorem OAI.KadisonKastler.matrixLinearEquiv_symm_apply line 60
theorem OAI.KadisonKastler.matrix_map_sub line 65
theorem OAI.KadisonKastler.matrix_map_mul line 72

theorem OAI.KadisonKastler.matrix_multiplicative_defect_le line 81

Source documentation

The multiplicative defect estimate at all rectangular matrix sizes. This is the estimate used before transporting multiplication through F.

theorem matrix_multiplicative_defect_le
    (ρ : A →ₐ[ℂ] B) (F : A →ₗ[ℂ] B) {e : ℝ} (he : 0 ≤ e)
    (hρ : CompletelyIsometric ρ.toLinearMap)
    (hF : CompletelyBoundedBy F 1)
    (hclose : CompletelyBoundedBy (F - ρ.toLinearMap) e)
    {p r q : ℕ} (X : CStarMatrix (Fin p) (Fin r) A)
    (Y : CStarMatrix (Fin r) (Fin q) A) :
    ‖CStarMatrix.mapₗ F (X * Y) - CStarMatrix.mapₗ F X * CStarMatrix.mapₗ F Y‖ ≤
      3 * e * ‖X‖ * ‖Y‖ := by
…

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

def OAI.KadisonKastler.TransportedProductBound line 129
Source documentation
The row-column defect of the transported multiplication. This is the concrete inequality used to invoke the published multiplication theorem.
```
def TransportedProductBound (F : A ≃ₗ[ℂ] B) (c : ℝ) : Prop :=
…
```
theorem OAI.KadisonKastler.transportedProductBound_of_defect line 136
theorem OAI.KadisonKastler.inverse_completelyBoundedBy_of_close_to_id line 159
theorem OAI.KadisonKastler.inverse_sub_completelyBoundedBy_of_close_to_id line 173