OAI/Analysis/CharacterCriterion/MatrixSimplex.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.KirchbergRordam.GenericRW.MatrixMix.Mat line 28
2. def OAI.KirchbergRordam.GenericRW.MatrixMix.e line 29
3. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.e_star line 32
4. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.e_mul line 41
5. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.e_sum line 52
6. def OAI.KirchbergRordam.GenericRW.MatrixMix.x line 64
7. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.x_star line 66
8. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.x_mul line 70
9. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.x_sum line 79
10. def OAI.KirchbergRordam.GenericRW.MatrixMix.linear line 82
11. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.linear_single line 87
12. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.linear_one line 102
13. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.linear_star line 104
14. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.linear_mul line 108
15. def OAI.KirchbergRordam.GenericRW.MatrixMix.tensor line 124
16. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.tensor_kronecker line 134
17. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.tensor_mem line 154
18. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.tensor_continuous line 166
19. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.tensor_left line 179
20. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.tensor_right line 182
21. def OAI.KirchbergRordam.GenericRW.MatrixMix.u line 186
22. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.u_star_mul line 187
23. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.u_mul_star line 189
24. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.u_zero line 191
25. def OAI.KirchbergRordam.GenericRW.MatrixMix.interpolate line 193
26. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.interpolate_zero line 207
27. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.interpolate_top line 210
28. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.interpolate_mem line 220
29. lemma OAI.KirchbergRordam.GenericRW.MatrixMix.interpolate_continuous line 225
30. def OAI.KirchbergRordam.GenericRW.CoordinateSimplex line 236
31. instance OAI.KirchbergRordam.GenericRW.CoordinateSimplex.(instance at line 243) line 243
32. lemma OAI.KirchbergRordam.GenericRW.CoordinateSimplex.ext line 248
33. lemma OAI.KirchbergRordam.GenericRW.CoordinateSimplex.zero_le line 258
34. lemma OAI.KirchbergRordam.GenericRW.CoordinateSimplex.sum_eq_one line 267
35. lemma OAI.KirchbergRordam.GenericRW.CoordinateSimplex.le_one line 275
36. abbrev OAI.KirchbergRordam.GenericRW.CoordinateSimplex.vertex line 279
37. lemma OAI.KirchbergRordam.GenericRW.CoordinateSimplex.vertex_coe line 288
38. abbrev OAI.KirchbergRordam.GenericRW.MatrixSimplex.Simplex line 302
39. def OAI.KirchbergRordam.GenericRW.MatrixSimplex.last line 304
40. def OAI.KirchbergRordam.GenericRW.MatrixSimplex.den line 306
41. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.den_pos line 308
42. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.prev_sum line 310
43. def OAI.KirchbergRordam.GenericRW.MatrixSimplex.prev line 317
44. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.prev_apply line 328
45. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.prev_pos line 334
46. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.last_continuous line 339
47. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.prev_continuous line 342
48. structure OAI.KirchbergRordam.GenericRW.MatrixSimplex.Family line 357
49. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.family_commute line 368
50. def OAI.KirchbergRordam.GenericRW.MatrixSimplex.extendHom line 381
51. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.extend_support line 384
52. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.prev_vertex line 397
53. lemma OAI.KirchbergRordam.GenericRW.MatrixSimplex.extend_vertex line 406
54. def OAI.KirchbergRordam.GenericRW.MatrixSimplex.extend line 416
55. theorem OAI.KirchbergRordam.GenericRW.MatrixSimplex.exists_family line 424
56. abbrev OAI.KirchbergRordam.GenericRW.CubeWeights.Cube line 446
57. abbrev OAI.KirchbergRordam.GenericRW.CubeWeights.Punctured line 447
58. def OAI.KirchbergRordam.GenericRW.CubeWeights.radius line 449
59. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.coord_le_radius line 451
60. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.radius_nonneg line 457
61. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.radius_pos line 458
62. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.radius_continuous line 467
63. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.radius_attained line 474
64. def OAI.KirchbergRordam.GenericRW.CubeWeights.weight line 482
65. def OAI.KirchbergRordam.GenericRW.CubeWeights.total line 483
66. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.weight_nonneg line 485
67. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.total_pos line 490
68. def OAI.KirchbergRordam.GenericRW.CubeWeights.normalized line 496
69. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.normalized_apply line 499
70. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.normalized_continuous line 500
71. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.normalized_zero line 507
72. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.normalized_support line 510
73. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.localized_normalized line 516
74. def OAI.KirchbergRordam.GenericRW.CubeWeights.g line 541
75. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.g_continuous line 543
76. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.g_nonneg line 548
77. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.g_le_one line 553
78. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.g_zero line 561
79. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.g_pos line 566
80. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.g_of_large line 575
81. def OAI.KirchbergRordam.GenericRW.CubeWeights.H line 583
82. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.H_continuous line 584
83. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.H_zero line 586
84. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.H_nonneg line 587
85. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.H_le_one line 590
86. lemma OAI.KirchbergRordam.GenericRW.CubeWeights.H_of_large line 593