OAI/Analysis/FactorGeneration/PredualContinuity.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Given-predual evaluations are uniformly small on operator order intervals bounded by positive contractions with small trace. This is derived from the constructed tail majorants, without assuming predual normality.

  1. theorem OAI.Generator.Tracial.predual_summable_trace_sandwich line 23
  2. theorem OAI.Generator.Tracial.predual_small_of_small_trace_sandwich line 32
  3. theorem OAI.Generator.Tracial.predual_trace_sandwich_tendsto_zero line 49
  4. theorem OAI.Generator.Tracial.predual_small_of_small_norm₂_selfAdjoint line 64
  5. theorem OAI.Generator.Tracial.predual_small_of_small_norm₂ line 75
  6. theorem OAI.Generator.Tracial.predual_norm₂_tendsto_zero_unitBall line 99
  7. theorem OAI.Generator.Tracial.predual_norm₂_tendsto_zero line 109
  8. theorem OAI.Generator.Tracial.predual_norm₂_tendsto line 135
  9. theorem OAI.Generator.Tracial.predualFunctional_unitBall_continuous line 157
  10. theorem OAI.Generator.Tracial.predualFunctional_mem_cyclicPredual line 174
  11. theorem OAI.Generator.Tracial.traceOrbit_isSeparable_of_separablePredual line 178