OAI/Analysis/PureInfiniteness/ExactCompressionRelations.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The multiplicative-domain calculation in KR02 Lemma 7.9. Preserving an element and its square by a contractive compression forces the relative commutation and initial-support identities.

  1. theorem OAI.WeakPureInfiniteness.relative_relations_of_fixed_compression line 15
  2. theorem OAI.WeakPureInfiniteness.fixed_compression_of_relative_relations line 30
  3. theorem OAI.WeakPureInfiniteness.selfAdjoint_fixed_compression_iff line 38