OAI/Analysis/KadisonKastler/ProjectionStratumFields.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Transporting actual operator fields to the fixed-coordinate strata

  1. def OAI.KadisonKastler.compressedStratumField line 18
  2. theorem OAI.KadisonKastler.compressedStratumField_norm_le line 24
  3. theorem OAI.KadisonKastler.compressedStratumField_aestronglyMeasurable line 49
  4. theorem OAI.KadisonKastler.projectionStrataCoordinates_operator_action line 66