OAI/Analysis/CharacterCriterion/AmplifiedComparison.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.KirchbergRordam.GenericRW.ClosedRightRange.map_mem line 28
2. lemma OAI.KirchbergRordam.GenericRW.CuntzBelow.of_right_range line 52
3. def OAI.KirchbergRordam.GenericRW.AmplifiedComparison.pair line 83
4. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.pair_mul line 86
5. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.pair_star line 106
6. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.pair_zero_left line 122
7. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.pair_zero_right line 135
8. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.pair_sum_left line 149
9. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.pair_sum_right line 166
10. def OAI.KirchbergRordam.GenericRW.AmplifiedComparison.gramVector line 187
11. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.sqrt_orthogonal line 191
12. lemma OAI.KirchbergRordam.GenericRW.AmplifiedComparison.gram_inner line 207
13. theorem OAI.KirchbergRordam.GenericRW.AmplifiedComparison.compare line 229
14. def OAI.KirchbergRordam.GenericRW.MaxTensor.pure line 263
15. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_mul line 264
16. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_star line 266
17. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_zero_left line 269
18. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_zero_right line 278
19. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_one line 287
20. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_sum_left line 296
21. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.pure_sum_right line 306
22. def OAI.KirchbergRordam.GenericRW.MaxTensor.word line 316
23. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_mul line 320
24. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_star line 325
25. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_one line 329
26. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_zero_coordinate line 333
27. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.sum_word line 346
28. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_full_comparison line 360
29. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_gram line 369
30. theorem OAI.KirchbergRordam.GenericRW.MaxTensor.auxiliary line 383
31. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.word_single line 406
32. lemma OAI.KirchbergRordam.GenericRW.MaxTensor.leg_word_mul line 422
33. lemma OAI.KirchbergRordam.GenericRW.ConeCube.left_fixed line 434
34. lemma OAI.KirchbergRordam.GenericRW.ConeCube.right_fixed line 441
35. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_word_succ line 445
36. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_word_zero line 454
37. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_word_fix line 470
38. def OAI.KirchbergRordam.GenericRW.ConeCut.unit line 491
39. lemma OAI.KirchbergRordam.GenericRW.ConeCut.unit_star line 492
40. lemma OAI.KirchbergRordam.GenericRW.ConeCut.unit_mul line 494
41. def OAI.KirchbergRordam.GenericRW.ConeCut.coeff line 501
42. lemma OAI.KirchbergRordam.GenericRW.ConeCut.coeff_continuous line 503
43. lemma OAI.KirchbergRordam.GenericRW.ConeCut.coeff_zero line 508
44. lemma OAI.KirchbergRordam.GenericRW.ConeCut.coeff_nonneg line 513
45. def OAI.KirchbergRordam.GenericRW.ConeCut.q line 518
46. def OAI.KirchbergRordam.GenericRW.ConeCut.z line 523
47. lemma OAI.KirchbergRordam.GenericRW.ConeCut.z_gram line 528
48. lemma OAI.KirchbergRordam.GenericRW.ConeCut.q_nonneg line 536
49. def OAI.KirchbergRordam.GenericRW.ConeCut.g line 542
50. lemma OAI.KirchbergRordam.GenericRW.ConeCut.g_nonneg line 543
51. lemma OAI.KirchbergRordam.GenericRW.ConeCut.qg_zero line 552
52. lemma OAI.KirchbergRordam.GenericRW.ConeCut.q_support line 560
53. lemma OAI.KirchbergRordam.GenericRW.ConeCut.g_support line 566
54. lemma OAI.KirchbergRordam.GenericRW.ConeCut.q_fix line 574
55. def OAI.KirchbergRordam.GenericRW.ConeCube.y line 584
56. lemma OAI.KirchbergRordam.GenericRW.ConeCube.x_fixes_y line 589
57. lemma OAI.KirchbergRordam.GenericRW.ConeCube.matrix_scalar_product line 614
58. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_one line 624
59. lemma OAI.KirchbergRordam.GenericRW.ConeCube.repr_scalar_word line 627
60. lemma OAI.KirchbergRordam.GenericRW.ConeCube.defect_word line 642