OAI/Analysis/KadisonKastler/ProductInvariantL2.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The product range of a one-coordinate invariant projection

An L2 function fixed by the shift in its first coordinate is measurable, modulo null sets, for the product of the invariant and second sigma algebras. The proof tests its orthogonal-projection remainder against rectangles.

  1. def OAI.KadisonKastler.firstCoordinateShift line 25
  2. def OAI.KadisonKastler.firstInvariantSigma line 28
  3. theorem OAI.KadisonKastler.firstInvariantSigma_le line 32
  4. theorem OAI.KadisonKastler.firstCoordinateShift_quasi line 38
  5. theorem OAI.KadisonKastler.firstInvariantSigma_le_shiftInvariantSigma line 43
  6. theorem OAI.KadisonKastler.firstInvariantSigma_fixed line 59
  7. theorem OAI.KadisonKastler.L2_mem_firstInvariantSigma_of_fixed line 68
  8. theorem OAI.KadisonKastler.scalarInfinity_mem_firstInvariantSigma_of_fixed line 107