RowCochainResidual.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The finite-row residual has a quadratic bound after removing its module defect.

def OAI.KadisonKastler.finiteCochainModuleDefect line 15
Source documentation
Failure of the finite average to be a right module map in its last argument.
```
def finiteCochainModuleDefect {κ : Type*} [Fintype κ] (r : κ → A)
    (f : A →ₗ[ℂ] A →ₗ[ℂ] A) : A →ₗ[ℂ] A →ₗ[ℂ] A :=
…
```

def OAI.KadisonKastler.finiteAveragedDifferential line 20

Source documentation

The averaged differential, written as an actual bilinear map.

def finiteAveragedDifferential {κ : Type*} [Fintype κ] (r : κ → A)
    (f : A →ₗ[ℂ] A →ₗ[ℂ] A) : A →ₗ[ℂ] A →ₗ[ℂ] A :=
…

theorem OAI.KadisonKastler.finiteAveragedDifferential_apply line 24
theorem OAI.KadisonKastler.cochainDifferential_zero line 34
theorem OAI.KadisonKastler.finiteMatrixDifferential_apply line 37

theorem OAI.KadisonKastler.finiteAveragedDifferential_matrix line 51

Source documentation

Exact matrix identity for the averaged Hochschild differential.

theorem finiteAveragedDifferential_matrix {κ : Type*} [Fintype κ]
    (r : κ → A) (hr : ∑ k, r k * star (r k) = 1)
    (f : A →ₗ[ℂ] A →ₗ[ℂ] A) {p t q : ℕ}
    (X : CStarMatrix (Fin p) (Fin t) A) (Y : CStarMatrix (Fin t) (Fin q) A) :
    bilinearProduct (finiteAveragedDifferential r f) X Y =
      finiteMatrixDifferential f X Y (rowReplication r) * (rowReplication r).conjTranspose := by
…

Mentions: OAI.KadisonKastler.bilinearProduct, OAI.KadisonKastler.finiteAveragedDifferential, OAI.KadisonKastler.finiteMatrixDifferential, OAI.KadisonKastler.rowReplication

theorem OAI.KadisonKastler.finiteAveragedDifferential_defect_bound line 73

Source documentation

Averaging the differential of an associative multiplication defect costs at most twice the square of its complete norm.

theorem finiteAveragedDifferential_defect_bound {κ : Type*} [Fintype κ]
    (r : κ → A) (hr : ∑ k, r k * star (r k) = 1)
    (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) :
    HaagerupBound (finiteAveragedDifferential r (m - LinearMap.mul ℂ A)) (2 * c ^ 2) := by
…

Mentions: OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.finiteAveragedDifferential