HaagerupCochains.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Matrix Hochschild identities for multiplication correction

The row-column estimates below retain all matrix levels. Associativity turns the differential of a multiplication defect into a quadratic expression.

theorem OAI.KadisonKastler.bilinearProduct_add line 17
theorem OAI.KadisonKastler.bilinearProduct_sub line 23
theorem OAI.KadisonKastler.bilinearProduct_add_left line 29
theorem OAI.KadisonKastler.bilinearProduct_add_right line 35
theorem OAI.KadisonKastler.bilinearProduct_smul line 41

theorem OAI.KadisonKastler.bilinearProduct_assoc line 49

Source documentation

Algebraic associativity survives every rectangular matrix amplification.

theorem bilinearProduct_assoc (m : A →ₗ[ℂ] A →ₗ[ℂ] A)
    (hm : ∀ x y z, m (m x y) z = m x (m y z)) {p r s q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin s) A)
    (Z : CStarMatrix (Fin s) (Fin q) A) :
    bilinearProduct m (bilinearProduct m X Y) Z =
      bilinearProduct m X (bilinearProduct m Y Z) := by
…

Mentions: OAI.KadisonKastler.bilinearProduct

theorem OAI.KadisonKastler.rectangular_mul_assoc line 60

def OAI.KadisonKastler.matrixBilinearDifferential line 70

Source documentation

The degree-two Hochschild differential, already amplified to matrices.

def matrixBilinearDifferential (f : A →ₗ[ℂ] A →ₗ[ℂ] A) {p r s q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin s) A)
    (Z : CStarMatrix (Fin s) (Fin q) A) : CStarMatrix (Fin p) (Fin q) A :=
…

theorem OAI.KadisonKastler.matrixBilinearDifferential_defect line 77

Source documentation

The Maurer--Cartan identity, with its signs fixed for the correction step.

theorem matrixBilinearDifferential_defect (m : A →ₗ[ℂ] A →ₗ[ℂ] A)
    (hm : ∀ x y z, m (m x y) z = m x (m y z)) {p r s q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin s) A)
    (Z : CStarMatrix (Fin s) (Fin q) A) :
    let f := m - LinearMap.mul ℂ A
…

theorem OAI.KadisonKastler.HaagerupBound.add line 103
theorem OAI.KadisonKastler.HaagerupBound.smul line 112

theorem OAI.KadisonKastler.matrixBilinearDifferential_defect_bound line 120

Source documentation

A defect bounded by q has differential bounded by 2q², uniformly in all four matrix dimensions.

theorem matrixBilinearDifferential_defect_bound
    (m : A →ₗ[ℂ] A →ₗ[ℂ] A)
    (hm : ∀ x y z, m (m x y) z = m x (m y z)) {c : ℝ} (hc : 0 ≤ c)
    (hf : HaagerupBound (m - LinearMap.mul ℂ A) c) {p r s q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin s) A)
    (Z : CStarMatrix (Fin s) (Fin q) A) :
    ‖matrixBilinearDifferential (m - LinearMap.mul ℂ A) X Y Z‖ ≤
      2 * c ^ 2 * ‖X‖ * ‖Y‖ * ‖Z‖ := by
…

Mentions: OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.matrixBilinearDifferential