OAI/Analysis/KadisonKastler/HilbertVariance.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal centering of Hilbert-valued square-integrable functions

The mean is the closest constant in L2. This is the variance estimate used after conditioning on the middle and right independent random-walk blocks.

  1. def OAI.KadisonKastler.hilbertConstantL2 line 22
  2. theorem OAI.KadisonKastler.hilbertConstantL2_ae line 26
  3. theorem OAI.KadisonKastler.integral_hilbertConstantL2 line 31
  4. theorem OAI.KadisonKastler.inner_hilbertConstantL2_left line 35
  5. theorem OAI.KadisonKastler.hilbertL2_centered_orthogonal line 45
  6. theorem OAI.KadisonKastler.hilbertL2_variance_identity line 50
  7. theorem OAI.KadisonKastler.hilbertL2_centering_minimizes line 66