OAI/Analysis/KadisonKastler/ResolventCutMeasurable.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Measurability of resolvent cuts

Monotone projection norms make the diagonal coefficients measurable. Polarization and the countable Hilbert coefficient criterion then give the strong measurability needed for the regular-core field construction.

  1. theorem OAI.KadisonKastler.resolventLowerCut_diagonal line 22
  2. theorem OAI.KadisonKastler.resolventLowerCut_diagonal_measurable line 31
  3. theorem OAI.KadisonKastler.resolventLowerCut_coefficient_measurable line 38
  4. theorem OAI.KadisonKastler.resolventLowerCut_comp_aestronglyMeasurable line 56
  5. theorem OAI.KadisonKastler.modularUpperCut_measurable line 63