InflatedConjugacy.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Recovering the full algebra from its common matrix corners

theorem OAI.KadisonKastler.FullMatrixCorner.extension_matrixEntry line 22
def OAI.KadisonKastler.FullMatrixCorner.partialDiagonal line 36
theorem OAI.KadisonKastler.FullMatrixCorner.partialDiagonal_star line 38
theorem OAI.KadisonKastler.FullMatrixCorner.partialDiagonal_tendsto line 42
theorem OAI.KadisonKastler.FullMatrixCorner.mem_of_matrixEntries line 49
Source documentation
Membership of every transported matrix entry determines membership of the whole operator. The proof uses actual finite compressions and WOT closure.
```
theorem mem_of_matrixEntries (N : VonNeumannAlgebra H)
    (hF : ∀ i j, F.entry i j ∈ N) (T : H →L[ℂ] H)
    (hT : ∀ i j, cornerExtension E (F.matrixEntry T i j) ∈ N) : T ∈ N := by
…
```
Mentions: OAI.KadisonKastler.cornerExtension

theorem OAI.KadisonKastler.FullMatrixCorner.conjugates_inflateUnitary line 82

Source documentation

A conjugacy of the common initial corners inflates to a conjugacy of the original algebras, retaining the corner displacement bound.

theorem conjugates_inflateUnitary (M N : VonNeumannAlgebra H)
    (hM : ∀ i j, F.entry i j ∈ M) (hN : ∀ i j, F.entry i j ∈ N)
    (v : unitary (E →L[ℂ] E))
    (hv : Conjugates v
      (representedCorner E M (F.zero_zero ▸ hM 0 0))
      (representedCorner E N (F.zero_zero ▸ hN 0 0))) :
    Conjugates (F.inflateUnitary v) M N := by
…

Mentions: OAI.KadisonKastler.Conjugates, OAI.KadisonKastler.representedCorner