OAI/Analysis/CharacterCriterion/GeneralSystem.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GeneralBlockReindex.left_low line 46
2. lemma OAI.KirchbergRordam.GeneralBlockReindex.left_full line 72
3. lemma OAI.KirchbergRordam.GeneralBlockReindex.left_entry line 97
4. lemma OAI.KirchbergRordam.GeneralBlockReindex.left_matrix line 117
5. lemma OAI.KirchbergRordam.GeneralBlockReindex.right_low line 126
6. lemma OAI.KirchbergRordam.GeneralBlockReindex.right_full line 152
7. lemma OAI.KirchbergRordam.GeneralBlockReindex.right_entry line 177
8. lemma OAI.KirchbergRordam.GeneralBlockReindex.right_matrix line 197
9. lemma OAI.KirchbergRordam.GeneralDropSystem.eigen_cover line 212
10. lemma OAI.KirchbergRordam.GeneralDropSystem.eigen_lipschitz line 222
11. lemma OAI.KirchbergRordam.GeneralDropSystem.matrix_isTopologicalSemiring line 237
12. lemma OAI.KirchbergRordam.GeneralDropSystem.matrix_continuousStar line 240
13. lemma OAI.KirchbergRordam.GeneralDropSystem.fiberMap_continuous line 250
14. lemma OAI.KirchbergRordam.GeneralDropSystem.rawStep_apply line 255
15. lemma OAI.KirchbergRordam.GeneralDropSystem.zero_eval line 257
16. lemma OAI.KirchbergRordam.GeneralDropSystem.one_eval line 265
17. lemma OAI.KirchbergRordam.GeneralDropSystem.rawStep_zero line 276
18. lemma OAI.KirchbergRordam.GeneralDropSystem.rawStep_one line 284
19. lemma OAI.KirchbergRordam.GeneralDropSystem.rawStep_mem line 293
20. lemma OAI.KirchbergRordam.GeneralDropSystem.rawStep_injective line 301
21. lemma OAI.KirchbergRordam.GeneralDropSystem.step_injective line 307
22. lemma OAI.KirchbergRordam.GeneralDropSystem.step_norm line 311
23. def OAI.KirchbergRordam.GeneralEndpointMultiplicity.leftExpand line 319
24. def OAI.KirchbergRordam.GeneralEndpointMultiplicity.rightExpand line 328
25. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.leftExpand_matrix line 337
26. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.rightExpand_matrix line 351
27. def OAI.KirchbergRordam.GeneralEndpointMultiplicity.leftBase line 365
28. def OAI.KirchbergRordam.GeneralEndpointMultiplicity.rightBase line 369
29. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.leftBase_commute line 373
30. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.rightBase_commute line 389
31. def OAI.KirchbergRordam.GeneralEndpointMultiplicity.leftRep line 406
32. def OAI.KirchbergRordam.GeneralEndpointMultiplicity.rightRep line 409
33. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.leftRep_commute line 412
34. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.rightRep_commute line 423
35. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.leftRep_bound line 435
36. lemma OAI.KirchbergRordam.GeneralEndpointMultiplicity.rightRep_bound line 442