OAI/Analysis/JiangSu/DimensionDrop/Iterates.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OriginalJiangSu.stageMultiplicities line 14
2. def OAI.OriginalJiangSu.IteratedIndex line 15
3. instance OAI.OriginalJiangSu.iteratedFintype line 18
4. instance OAI.OriginalJiangSu.iteratedDecEq line 22
5. instance OAI.OriginalJiangSu.iteratedNonempty line 26
6. def OAI.OriginalJiangSu.iteratedFamily line 34
7. lemma OAI.OriginalJiangSu.iterated_contract line 38
8. lemma OAI.OriginalJiangSu.iterated_variation line 51
9. def OAI.OriginalJiangSu.stepUnitary line 64
10. lemma OAI.OriginalJiangSu.stageStep_eval line 71
11. theorem OAI.OriginalJiangSu.iterate_diagonalization line 76