RegularCorePeriodic.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Increasing periodic matrix algebras

Divisibility of the period gives inclusion of the represented matrix algebras. A factorial sequence therefore gives increasing finite matrix stages, while agreement on each fixed finite set of columns gives strong approximation to the original countable matrix units.

theorem OAI.KadisonKastler.FullMatrixCorner.periodicMatrixUnits_column_block line 30

theorem OAI.KadisonKastler.FullMatrixCorner.periodicMatrixUnits_refinement line 40

Source documentation

A period-n matrix unit is the sum of its copies in any period k*n.

theorem periodicMatrixUnits_refinement (n k : ℕ) [NeZero n] [NeZero k]
    (i j : Fin n) :
    (F.periodicMatrixUnits n).entry i j =
      ∑ r : Fin k, (F.periodicMatrixUnits (k * n)).entry
        (finProdFinEquiv (r, i)) (finProdFinEquiv (r, j)) := by
…

theorem OAI.KadisonKastler.FullMatrixCorner.periodicMatrixUnits_algebra_le_of_dvd line 73
theorem OAI.KadisonKastler.FullMatrixCorner.matrixUnit_norm_le_one line 92
theorem OAI.KadisonKastler.FullMatrixCorner.entry_norm_le_one line 101

theorem OAI.KadisonKastler.FullMatrixCorner.tendsto_apply_of_eventually_eq_columns line 111

Source documentation

Uniformly bounded operators that eventually agree on each column converge strongly. Only finite sums of columns are used.

theorem tendsto_apply_of_eventually_eq_columns
    (a : ℕ → H →L[ℂ] H) (T : H →L[ℂ] H)
    (ha : ∀ n, ‖a n‖ ≤ 1) (hT : ‖T‖ ≤ 1)
    (hc : ∀ k (x : E), ∀ᶠ n in atTop, a n (F.column k x) = T (F.column k x))
    (x : H) : Tendsto (fun n => a n x) atTop (𝓝 (T x)) := by
…

def OAI.KadisonKastler.FullMatrixCorner.periodicEntryApprox line 145
Source documentation
The actual factorial-period approximation to one countable matrix unit.
```
def periodicEntryApprox (i j n : ℕ) : H →L[ℂ] H :=
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.norm_periodicEntryApprox_le_one line 150
theorem OAI.KadisonKastler.FullMatrixCorner.periodicEntryApprox_strong line 157