InfiniteCornerInflation.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Inflation through countably many matrix corners

The hypotheses are the algebraic matrix-unit relations and the strong sum of their diagonal projections. They give an actual Hilbert direct-sum decomposition. A corner operator is then applied on each summand; in particular a corner unitary inflates with no loss in displacement.

abbrev OAI.KadisonKastler.CountableHilbertSum line 25
def OAI.KadisonKastler.l2DiagonalLinear line 27
theorem OAI.KadisonKastler.norm_l2DiagonalLinear_le line 34
def OAI.KadisonKastler.l2Diagonal line 43
theorem OAI.KadisonKastler.l2Diagonal_apply line 46
theorem OAI.KadisonKastler.norm_l2Diagonal_le line 49
theorem OAI.KadisonKastler.l2Diagonal_single line 52
theorem OAI.KadisonKastler.l2Diagonal_star line 59
def OAI.KadisonKastler.l2DiagonalHom line 68
structure OAI.KadisonKastler.FullMatrixCorner line 84
Source documentation
Actual countable matrix units with initial corner E and strong sum one.
```
structure FullMatrixCorner where
…
```
def OAI.KadisonKastler.FullMatrixCorner.columnLinear line 95
theorem OAI.KadisonKastler.FullMatrixCorner.inner_columns line 97
def OAI.KadisonKastler.FullMatrixCorner.column line 112
theorem OAI.KadisonKastler.FullMatrixCorner.column_apply line 118
theorem OAI.KadisonKastler.FullMatrixCorner.columns_orthogonal line 120
theorem OAI.KadisonKastler.FullMatrixCorner.diagonal_apply line 124
theorem OAI.KadisonKastler.FullMatrixCorner.columns_total line 129
theorem OAI.KadisonKastler.FullMatrixCorner.hilbertSum line 140
def OAI.KadisonKastler.FullMatrixCorner.coordinates line 144
Source documentation
The coordinate equivalence obtained from the actual matrix units.
```
def coordinates : H ≃ₗᵢ[ℂ] CountableHilbertSum E := F.hilbertSum.linearIsometryEquiv
```
Mentions: OAI.KadisonKastler.CountableHilbertSum
theorem OAI.KadisonKastler.FullMatrixCorner.coordinates_symm_single line 146
theorem OAI.KadisonKastler.FullMatrixCorner.coordinates_column line 150
theorem OAI.KadisonKastler.FullMatrixCorner.column_adjoint_apply line 154
theorem OAI.KadisonKastler.FullMatrixCorner.coordinates_apply line 166
def OAI.KadisonKastler.FullMatrixCorner.inflateHom line 184
Source documentation
Inflate a corner operator by the same operator on every matrix summand.
```
def inflateHom : (E →L[ℂ] E) →⋆ₐ[ℂ] (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.inflateHom_apply line 187
theorem OAI.KadisonKastler.FullMatrixCorner.norm_inflateHom_le line 190
theorem OAI.KadisonKastler.FullMatrixCorner.inflateHom_column line 198
theorem OAI.KadisonKastler.FullMatrixCorner.hasSum_inflateHom line 205
Source documentation
The constructed operator is the strong sum of its actual matrix-corner copies, rather than an abstract operator with prescribed coefficients.
```
theorem hasSum_inflateHom (T : E →L[ℂ] E) (x : H) :
    HasSum (fun i => (F.entry i 0 * cornerExtension E T * F.entry 0 i) x)
      (F.inflateHom T x) := by
…
```
Mentions: OAI.KadisonKastler.cornerExtension
def OAI.KadisonKastler.FullMatrixCorner.inflateUnitary line 215
Source documentation
The actual unitary on the whole Hilbert space obtained from a corner unitary.
```
def inflateUnitary (v : unitary (E →L[ℂ] E)) : unitary (H →L[ℂ] H) :=
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.coe_inflateUnitary line 222
theorem OAI.KadisonKastler.FullMatrixCorner.norm_inflateUnitary_sub_one_le line 225
def OAI.KadisonKastler.FullMatrixCorner.matrixEntry line 234
theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_apply line 238
theorem OAI.KadisonKastler.FullMatrixCorner.matrixEntry_unitaryConj line 245
Source documentation
Matrix coefficients of the inflated unitary conjugation are the original corner conjugation, with no change of representation or norm.
```
theorem matrixEntry_unitaryConj (v : unitary (E →L[ℂ] E))
    (T : H →L[ℂ] H) (i j : ℕ) :
    F.matrixEntry (unitaryConj (F.inflateUnitary v) T) i j =
      unitaryConj v (F.matrixEntry T i j) := by
…
```
Mentions: OAI.KadisonKastler.unitaryConj