RegularCoreMatrixData.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Countable equivalent projection families give full matrix corners

The input here is actual projection and partial-isometry data in a represented von Neumann algebra. No existence of a semifinite decomposition is assumed as a published input. Once such a decomposition has been constructed, the matrix-corner machinery applies to the explicit operators v i * star (v j).

def OAI.KadisonKastler.projectionFamilyEntry line 26
Source documentation
The matrix entries associated to partial isometries with a common initial projection.
```
def projectionFamilyEntry (v : ℕ → Algebra M) (i j : ℕ) : Algebra M :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.projectionFamilyEntry_star line 29
theorem OAI.KadisonKastler.projectionFamilyEntry_diagonal line 33

theorem OAI.KadisonKastler.projectionFamily_cross_eq_zero line 40

Source documentation

Orthogonality of the final projections forces the cross-products of the partial isometries to vanish.

theorem projectionFamily_cross_eq_zero
    (p : ℕ → AlgebraProjection M) (v : ℕ → Algebra M)
    (hvi : ∀ i, star (v i) * v i = (p 0).val)
    (hvf : ∀ i, v i * star (v i) = (p i).val)
    (horth : Pairwise (fun i j => (p i).val * (p j).val = 0))
    {i j : ℕ} (hij : i ≠ j) : star (v i) * v j = 0 := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.projectionFamilyEntry_mul line 53

def OAI.KadisonKastler.FullMatrixCorner.ofEquivalentProjectionFamily line 84

Source documentation

A countable strong partition into equivalent projections supplies actual full matrix units with the prescribed initial Hilbert corner.

def ofEquivalentProjectionFamily
    (E : Submodule ℂ H) [CompleteSpace E]
    (p : ℕ → AlgebraProjection M) (v : ℕ → Algebra M)
    (hvi : ∀ i, star (v i) * v i = (p 0).val)
    (hvf : ∀ i, v i * star (v i) = (p i).val)
    (horth : Pairwise (fun i j => (p i).val * (p j).val = 0))
    (hp0 : ((p 0).val : H →L[ℂ] H) = E.starProjection)
    (htotal : ∀ x : H, HasSum (fun i => ((p i).val : H →L[ℂ] H) x) x) :
    FullMatrixCorner E where
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FullMatrixCorner

theorem OAI.KadisonKastler.FullMatrixCorner.ofEquivalentProjectionFamily_entry line 105
theorem OAI.KadisonKastler.FullMatrixCorner.ofEquivalentProjectionFamily_entry_mem line 117