OAI/Analysis/CharacterCriterion/FiniteDrop.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GenericRW.ConeDrop.map_y line 34
2. lemma OAI.KirchbergRordam.GenericRW.ConeDrop.map_defect line 40
3. lemma OAI.KirchbergRordam.GenericRW.ConeDrop.map_fix line 44
4. lemma OAI.KirchbergRordam.GenericRW.ConeDrop.map_nonneg_generic line 50
5. theorem OAI.KirchbergRordam.GenericRW.ConeDrop.exists_drop_from_full_cone line 59
6. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.norm_pure_le line 127
7. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_nonneg line 141
8. def OAI.KirchbergRordam.GenericRW.FullRankWeighted.tensor line 160
9. def OAI.KirchbergRordam.GenericRW.FullRankWeighted.reindex line 173
10. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.pure_full line 184
11. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.abs_mul_self_zero line 222
12. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.self_mul_coabs_zero line 237
13. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.abs_coabs_zero line 251
14. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.self_abs line 256
15. def OAI.KirchbergRordam.GenericRW.FullRankWeighted.ofSquareZero line 268
16. abbrev OAI.KirchbergRordam.GenericRW.FullRankWeighted.Row line 311
17. def OAI.KirchbergRordam.GenericRW.FullRankWeighted.power line 313
18. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.power_full line 318
19. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.exists_flatten line 325
20. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.sqrt_star_mul_self_full line 343
21. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.sqrt_mul_star_self_full line 358
22. lemma OAI.KirchbergRordam.GenericRW.FullRankWeighted.ofSquareZero_full line 373
23. theorem OAI.KirchbergRordam.GenericRW.FullRankWeighted.exists_full_cone line 384
24. lemma OAI.KirchbergRordam.GenericRW.ConeCut.q_zero_eq_corner line 408
25. theorem OAI.KirchbergRordam.GenericRW.finite_prime_power_drop line 423