MultiplicationNewtonStep.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

One quadratic step in correction of multiplication

These are the concrete matrix identities used in the perturbation iteration. The choice of a correcting cochain is a separate construction.

def OAI.KadisonKastler.linearCoboundary line 19
Source documentation
The Hochschild coboundary of a linear cochain.
```
def linearCoboundary (D : A →ₗ[ℂ] A) : A →ₗ[ℂ] A →ₗ[ℂ] A where
…
```
theorem OAI.KadisonKastler.linearCoboundary_apply line 31

theorem OAI.KadisonKastler.bilinearProduct_linearCoboundary line 35

Source documentation

The coboundary formula is unchanged at every rectangular matrix level.

theorem bilinearProduct_linearCoboundary (D : A →ₗ[ℂ] A) {p r q : ℕ}
    (X : CStarMatrix (Fin p) (Fin r) A) (Y : CStarMatrix (Fin r) (Fin q) A) :
    bilinearProduct (linearCoboundary D) X Y =
      X * CStarMatrix.mapₗ D Y - CStarMatrix.mapₗ D (X * Y) +
        CStarMatrix.mapₗ D X * Y := by
…

Mentions: OAI.KadisonKastler.bilinearProduct, OAI.KadisonKastler.linearCoboundary

def OAI.KadisonKastler.conjugatedBilinear line 45
Source documentation
Transport an arbitrary bilinear multiplication by a linear equivalence.
```
def conjugatedBilinear (L : A ≃ₗ[ℂ] A) (m : A →ₗ[ℂ] A →ₗ[ℂ] A) :
    A →ₗ[ℂ] A →ₗ[ℂ] A where
…
```
theorem OAI.KadisonKastler.conjugatedBilinear_apply line 51
theorem OAI.KadisonKastler.bilinearProduct_conjugated line 55
theorem OAI.KadisonKastler.conjugatedBilinear_assoc line 65
theorem OAI.KadisonKastler.conjugatedBilinear_star line 72

theorem OAI.KadisonKastler.matrix_newton_residual line 85

Source documentation

Exact error before conjugating by the near-identity correction.

theorem matrix_newton_residual (m : A →ₗ[ℂ] A →ₗ[ℂ] A) (D : A →ₗ[ℂ] A)
    {p r q : ℕ} (X : CStarMatrix (Fin p) (Fin r) A)
    (Y : CStarMatrix (Fin r) (Fin q) A) :
    CStarMatrix.mapₗ (LinearMap.id + D) (bilinearProduct m X Y) -
      CStarMatrix.mapₗ (LinearMap.id + D) X * CStarMatrix.mapₗ (LinearMap.id + D) Y =
    bilinearProduct (m - LinearMap.mul ℂ A - linearCoboundary D) X Y +
      CStarMatrix.mapₗ D (bilinearProduct (m - LinearMap.mul ℂ A) X Y) -
      CStarMatrix.mapₗ D X * CStarMatrix.mapₗ D Y := by
…

Mentions: OAI.KadisonKastler.bilinearProduct, OAI.KadisonKastler.linearCoboundary

theorem OAI.KadisonKastler.matrix_newton_residual_bound line 104

Source documentation

The new error is the uncorrected cohomology error plus two quadratic terms.

theorem matrix_newton_residual_bound (m : A →ₗ[ℂ] A →ₗ[ℂ] A) (D : A →ₗ[ℂ] A)
    {c q r : ℝ} (hc : 0 ≤ c)
    (hD : CompletelyBoundedBy D c)
    (hm : HaagerupBound (m - LinearMap.mul ℂ A) q)
    (hres : HaagerupBound (m - LinearMap.mul ℂ A - linearCoboundary D) r)
    {p s t : ℕ} (X : CStarMatrix (Fin p) (Fin s) A)
    (Y : CStarMatrix (Fin s) (Fin t) A) :
    ‖CStarMatrix.mapₗ (LinearMap.id + D) (bilinearProduct m X Y) -
      CStarMatrix.mapₗ (LinearMap.id + D) X * CStarMatrix.mapₗ (LinearMap.id + D) Y‖ ≤
      (r + c * q + c ^ 2) * ‖X‖ * ‖Y‖ := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.linearCoboundary, OAI.KadisonKastler.bilinearProduct

theorem OAI.KadisonKastler.conjugatedBilinear_defect_bound line 131

Source documentation

After changing coordinates, the new multiplication has the same quadratic bound divided by the two inverse-coordinate bounds.

theorem conjugatedBilinear_defect_bound
    (m : A →ₗ[ℂ] A →ₗ[ℂ] A) (D : A →ₗ[ℂ] A) (L : A ≃ₗ[ℂ] A)
    (hL : L.toLinearMap = LinearMap.id + D) {c q r : ℝ}
    (hc : 0 ≤ c) (hc1 : c < 1) (hq : 0 ≤ q) (hr : 0 ≤ r)
    (hD : CompletelyBoundedBy D c)
    (hm : HaagerupBound (m - LinearMap.mul ℂ A) q)
    (hres : HaagerupBound (m - LinearMap.mul ℂ A - linearCoboundary D) r) :
    HaagerupBound (conjugatedBilinear L m - LinearMap.mul ℂ A)
      ((r + c * q + c ^ 2) / (1 - c) ^ 2) := by
…

Mentions: OAI.KadisonKastler.CompletelyBoundedBy, OAI.KadisonKastler.HaagerupBound, OAI.KadisonKastler.linearCoboundary, OAI.KadisonKastler.conjugatedBilinear