OAI/Analysis/BoundedHochschild/MonotoneLimits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Monotone weak-star limits and bounded GNS limits.

  1. theorem OAI.HochschildSakai.nonneg_of_bounded_predual_limit line 33
  2. theorem OAI.HochschildSakai.le_of_bounded_predual_limit line 57
  3. theorem OAI.HochschildSakai.ge_of_bounded_predual_limit line 67
  4. theorem OAI.HochschildSakai.exists_monotone_predual_limit line 79
  5. theorem OAI.HochschildUltrafilter.diagonal_rank line 111
  6. lemma OAI.HochschildUltrapower.tendsto_quotient_preGNS_norm line 136
  7. lemma OAI.HochschildUltrapower.quotient_norm_le_of_eventually line 144
  8. theorem OAI.HochschildUltrapower.exists_bounded_GNS_limit line 169