OAI/Analysis/KadisonSimilarity/Representation/ConullFieldExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Extend fields from a conull measurable base by zero while retaining their actual L² action on the original measure space.

  1. def OAI.KadisonSimilarity.zeroExtendOperatorField line 16
  2. theorem OAI.KadisonSimilarity.zeroExtendOperatorField_action line 20
  3. theorem OAI.KadisonSimilarity.zeroExtendOperatorField_mem line 39