OAI/Analysis/OperatorAlgebra/WeakOperatorUltralimit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Bounded operator families have weak operator ultralimits. The construction uses bounded scalar ultralimits and the Hilbert-space representation of each limiting linear functional. This is the compactness step for extending finite matrix cpc maps to Hilbert-space operator targets.

  1. def OAI.WeakPureInfiniteness.ultraOperatorForm line 19
  2. lemma OAI.WeakPureInfiniteness.ultraOperatorForm_tendsto line 23
  3. lemma OAI.WeakPureInfiniteness.ultraOperatorForm_bound line 34
  4. def OAI.WeakPureInfiniteness.ultraOperatorFunctional line 42
  5. lemma OAI.WeakPureInfiniteness.ultraOperatorForm_add_left line 58
  6. lemma OAI.WeakPureInfiniteness.ultraOperatorForm_smul_left line 66
  7. def OAI.WeakPureInfiniteness.operatorUltraLinear line 73
  8. def OAI.WeakPureInfiniteness.operatorUltraLimit line 87
  9. lemma OAI.WeakPureInfiniteness.operatorUltraLimit_inner line 94
  10. lemma OAI.WeakPureInfiniteness.operatorUltraLimit_norm_le line 99
  11. lemma OAI.WeakPureInfiniteness.operatorUltraLimit_inner_tendsto line 104