OAI/Analysis/Nuclearity/QuotientCommutingBound.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A uniform bound for arbitrary commuting representations of a separable quotient, obtained by the explicit two-GNS reduction to standard form.

  1. lemma OAI.WeakPureInfiniteness.nuclear_quotient_coefficient_bound line 20
  2. lemma OAI.WeakPureInfiniteness.nuclear_quotient_commuting_algebraic_bound line 51
  3. def OAI.WeakPureInfiniteness.nuclearQuotientCommutingRepresentation line 70
  4. lemma OAI.WeakPureInfiniteness.nuclearQuotientCommutingRepresentation_apply line 83
  5. lemma OAI.WeakPureInfiniteness.nuclearQuotientCommutingRepresentation_elementary line 93