OAI/Analysis/JiangSu/Absorption/OneSidedIntertwiningChain.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CStarIntertwining.error line 17
  2. lemma OAI.CStarIntertwining.error_pos line 18
  3. lemma OAI.CStarIntertwining.error_tendsto line 19
  4. lemma OAI.CStarIntertwining.error_add line 21
  5. lemma OAI.CStarIntertwining.controlled_cauchy line 23
  6. lemma OAI.CStarIntertwining.controlled_limit_distance line 32
  7. theorem OAI.CStarIntertwining.equiv_of_chain line 46
  8. def OAI.CStarIntertwining.LocalApproximation line 89
  9. structure OAI.CStarIntertwining.ProtectedEmbedding line 95
  10. def OAI.CStarIntertwining.ProtectedEmbedding.hom line 99
  11. def OAI.CStarIntertwining.Transition line 102
  12. lemma OAI.CStarIntertwining.transition_exists line 108
  13. theorem OAI.CStarIntertwining.equiv_of_local_approximation line 134
  14. def OAI.CStarIntertwining.diagonal line 168
  15. lemma OAI.CStarIntertwining.eventually_norm_lt line 172
  16. def OAI.CStarIntertwining.QuotientConjugacy line 177
  17. theorem OAI.CStarIntertwining.local_approximation_of_quotient line 185
  18. theorem OAI.CStarIntertwining.equiv_of_quotient_conjugacy line 220