OAI/Analysis/KadisonKastler/FiniteCoordinateL2.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Density of finite-coordinate Hilbert functions

The random-walk proof needs approximants depending on a finite block. The orthogonal complement is zero because its integrals over all cylinder sets vanish, and cylinders generate the product sigma algebra.

  1. def OAI.KadisonKastler.finiteCoordinateL2 line 26
  2. theorem OAI.KadisonKastler.finiteCoordinateL2_indicator line 42
  3. theorem OAI.KadisonKastler.finiteCoordinateL2_orthogonal_eq_bot line 56
  4. theorem OAI.KadisonKastler.finiteCoordinateL2_dense line 82
  5. theorem OAI.KadisonKastler.exists_finiteCoordinate_L2_approximation line 92