OAI/Analysis/KadisonKastler/ScalarSectionSelection.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Selecting a scalar section by a countable measurable coordinate

The rooted random walk evaluates a bounded boundary family at its root. Countability makes the simultaneous almost-everywhere representative bounds and linear identities legitimate.

  1. theorem OAI.KadisonKastler.measurable_scalarSectionSelect line 26
  2. theorem OAI.KadisonKastler.scalarSectionSelect_ae_bound line 33
  3. def OAI.KadisonKastler.scalarSectionSelect line 38
  4. theorem OAI.KadisonKastler.scalarSectionSelect_ae line 43
  5. theorem OAI.KadisonKastler.scalarSectionSelect_add line 47
  6. theorem OAI.KadisonKastler.scalarSectionSelect_smul line 60
  7. theorem OAI.KadisonKastler.scalarSectionSelect_const line 71
  8. theorem OAI.KadisonKastler.scalarSectionSelect_module line 75
  9. theorem OAI.KadisonKastler.scalarSectionSelect_positive line 87
  10. theorem OAI.KadisonKastler.norm_scalarSectionSelect_le line 98
  11. def OAI.KadisonKastler.scalarSectionSelectL line 106