Haagerup.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Row-column bounds for bilinear multiplication

The Haagerup bound is expressed directly by all finite rectangular matrix products, as in the UCP criterion of §2 of Universal strong Kadison–Kastler stability (2026). For multiplication transported through a linear equivalence, this is exactly the matrix defect already bounded in CompletelyBounded.

def OAI.KadisonKastler.bilinearProduct line 26

Source documentation

The row-column extension of a bilinear product to rectangular matrices.

def bilinearProduct (m : A →ₗ[ℂ] A →ₗ[ℂ] A) {p r q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin q) A) :
    CStarMatrix (Fin p) (Fin q) A :=
…

theorem OAI.KadisonKastler.bilinearProduct_apply line 32
def OAI.KadisonKastler.HaagerupBound line 39
Source documentation
The norm bound on the bilinear map viewed on the Haagerup product, in its concrete finite row-column formulation.
```
def HaagerupBound (m : A →ₗ[ℂ] A →ₗ[ℂ] A) (c : ℝ) : Prop :=
…
```
def OAI.KadisonKastler.transportedBilinear line 46
Source documentation
Transported multiplication as a bundled complex-bilinear product.
```
def transportedBilinear (F : A ≃ₗ[ℂ] B) : A →ₗ[ℂ] A →ₗ[ℂ] A where
…
```
theorem OAI.KadisonKastler.transportedBilinear_apply line 59

theorem OAI.KadisonKastler.transportedBilinear_assoc line 64

Source documentation

Associativity of the bundled transported product.

theorem transportedBilinear_assoc (F : A ≃ₗ[ℂ] B) (x y z : A) :
    transportedBilinear F (transportedBilinear F x y) z =
      transportedBilinear F x (transportedBilinear F y z) :=
…

Mentions: OAI.KadisonKastler.transportedBilinear

theorem OAI.KadisonKastler.transportedBilinear_star line 71

Source documentation

Star compatibility of the bundled transported product.

theorem transportedBilinear_star (F : A ≃ₗ[ℂ] B)
    (hstar : ∀ x, F (star x) = star (F x)) (x y : A) :
    star (transportedBilinear F x y) = transportedBilinear F (star y) (star x) :=
…

Mentions: OAI.KadisonKastler.transportedBilinear

theorem OAI.KadisonKastler.bilinearProduct_mul line 79
Source documentation
The ordinary bilinear multiplication extends to the usual rectangular matrix product.
```
@[simp] theorem bilinearProduct_mul {p r q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin q) A) :
    bilinearProduct (LinearMap.mul ℂ A) X Y = X * Y := by
…
```
Mentions: OAI.KadisonKastler.bilinearProduct

theorem OAI.KadisonKastler.bilinearProduct_transported_defect line 88

Source documentation

Exact equality between the row-column bilinear defect and the matrix defect of multiplication transported through F.

theorem bilinearProduct_transported_defect (F : A ≃ₗ[ℂ] B) {p r q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin q) A) :
    bilinearProduct (transportedBilinear F - LinearMap.mul ℂ A) X Y =
      CStarMatrix.mapₗ F.symm.toLinearMap
        (CStarMatrix.mapₗ F.toLinearMap X * CStarMatrix.mapₗ F.toLinearMap Y) - X * Y := by
…

Mentions: OAI.KadisonKastler.bilinearProduct, OAI.KadisonKastler.transportedBilinear

theorem OAI.KadisonKastler.haagerupBound_transported_defect_iff line 101
Source documentation
The transported-product matrix estimate is precisely the Haagerup bound on the difference between transported and original multiplication.
```
theorem haagerupBound_transported_defect_iff (F : A ≃ₗ[ℂ] B) (c : ℝ) :
    HaagerupBound (transportedBilinear F - LinearMap.mul ℂ A) c ↔
      TransportedProductBound F c := by
…
```
Mentions: OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.transportedBilinear, OAI.KadisonKastler.TransportedProductBound