OAI/Analysis/BoundedHochschild/SpectralProjections.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Support projections, power limits and density of projection spans.

  1. theorem OAI.HochschildUltrapower.exists_power_projection line 34
  2. lemma OAI.HochschildUltrapower.exists_support_contraction line 72
  3. theorem OAI.HochschildUltrapower.exists_support_projection line 94
  4. lemma OAI.HochschildSakai.norm_add_smul_sq_of_star_mul_zero line 125
  5. theorem OAI.HochschildSakai.projection_range_limit line 140
  6. theorem OAI.HochschildSakai.predual_tendsto_projection_mul_bounded line 184
  7. theorem OAI.HochschildSakai.projection_mul_hasPreadjoint line 212
  8. lemma OAI.HochschildSakai.isGLB_of_antitone_predual_limit line 254
  9. lemma OAI.HochschildSakai.exists_antitone_predual_limit line 265
  10. lemma OAI.HochschildSakai.isGLB_star_conjugate line 276
  11. lemma OAI.HochschildSakai.le_of_positive_fixed line 292
  12. theorem OAI.HochschildSakai.power_limit_fixed line 305
  13. theorem OAI.HochschildSakai.exists_power_projection line 390
  14. lemma OAI.HochschildSakai.exists_support_contraction line 454
  15. theorem OAI.HochschildSakai.exists_support_projection line 477
  16. theorem OAI.HochschildSakai.exists_dyadic_projection line 500
  17. theorem OAI.HochschildSakai.dual_zero_of_projection_zero line 557
  18. theorem OAI.HochschildSakai.projection_span_dense line 603