OAI/Analysis/BackwardIntertwiners/AlgebraCorollary.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BackwardIntertwiners.powerCost_quadratic line 8
  2. lemma OAI.BackwardIntertwiners.rootnorm_tendsto_zero_of_bound line 13
  3. lemma OAI.BackwardIntertwiners.forwardOperator_quasinilpotent line 30
  4. lemma OAI.BackwardIntertwiners.forward_transitiveCommutant line 33
  5. lemma OAI.BackwardIntertwiners.direct_mainClaim line 40
  6. instance OAI.BackwardIntertwiners.fiber_separable line 43
  7. instance OAI.BackwardIntertwiners.global_nontrivial line 63
  8. instance OAI.BackwardIntertwiners.global_separable line 68
  9. lemma OAI.BackwardIntertwiners.direct_fullClaim line 73
  10. theorem OAI.BackwardIntertwiners.direct_algebra_corollary line 78

    Distinct definitions of this name: ComparatorChallenges/BackwardIntertwiners.lean:36 (same statement text; different proof or body). Qualify references as OAI.BackwardIntertwiners.direct_algebra_corollary@path.