OAI/Geometry/CubicTorus/Profiles/GainEnclosure150.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_150 line 19
2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_154 line 23
3. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_154 line 26
4. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_158 line 30
5. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_158 line 33
6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_162 line 37
7. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.gain_enclosure_162 line 40
8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_170 line 44
9. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_190 line 47
10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_enclosure_225 line 50
11. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_64 line 53
12. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_74 line 56
13. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_84 line 59
14. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_92 line 62
15. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_98 line 65
16. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_102 line 68
17. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_102 line 71
18. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_106 line 76
19. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_106 line 79
20. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_110 line 84
21. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_110 line 87
22. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_114 line 92
23. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_114 line 95
24. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_118 line 100
25. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_118 line 103
26. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_122 line 108
27. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_122 line 111
28. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_126 line 116
29. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_126 line 119
30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_130 line 124
31. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_130 line 127
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_134 line 132
33. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_134 line 135
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_138 line 140
35. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_138 line 143
36. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_142 line 148
37. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_142 line 151
38. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_146 line 156
39. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_146 line 159
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_150 line 164
41. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_150 line 167
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_154 line 172
43. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_154 line 175
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_158 line 180
45. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_158 line 183
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_162 line 188
47. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_lower_162 line 191
48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_170 line 196
49. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_190 line 199
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_lower_225 line 202
51. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_64_74 line 205
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_74_84 line 210
53. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_84_92 line 215
54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_92_98 line 220
55. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_98_102 line 225
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_102_106 line 230
57. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_106_110 line 235
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_110_114 line 240
59. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_114_118 line 245
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_118_122 line 250
61. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_122_126 line 255
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_126_130 line 260
63. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_130_134 line 265
64. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_134_138 line 270
65. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_138_142 line 275
66. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_142_146 line 280
67. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_146_150 line 285
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_150_154 line 290
69. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_154_158 line 295
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_158_162 line 300
71. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_162_170 line 305
72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_170_190 line 310
73. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.positive_190_225 line 315
74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_positive_left line 320
75. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.baseline_positive_right line 342
76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.combined_positive line 356
77. theorem OAI.ReusedScalar205.CubicTorus.Scalar.Cert.scalar_positive line 418
78. lemma OAI.CubicTorus.unitPlanarProfile_eq_reused line 443
79. lemma OAI.CubicTorus.nestingBaseline_eq_reused line 450
80. lemma OAI.CubicTorus.nestingGainInfimum_eq_reused line 470
81. theorem OAI.CubicTorus.nesting_scalar_positive line 483
82. lemma OAI.CubicTorus.nesting_scalar_contradiction line 511
83. theorem OAI.CubicTorus.isMinimizerAt_nonstandard_not_three_vertices line 528
84. theorem OAI.CubicTorus.isMinimizerAt_fixed_downset_not_three_vertices line 556
85. lemma OAI.CubicTorus.isMinimizerAt_missing_neighbor_volume_le_half_null line 615
86. lemma OAI.CubicTorus.orientedUpperVertex_reverse line 638
87. theorem OAI.CubicTorus.isMinimizerAt_small_side_no_face_vertex line 644
88. lemma OAI.CubicTorus.tangentPart_inner_pair line 686
89. lemma OAI.CubicTorus.normal_coordinate_trace line 692
90. lemma OAI.CubicTorus.periodic_coordinates_trace line 707
91. lemma OAI.CubicTorus.periodic_coordinates_divergence line 731
92. theorem OAI.CubicTorus.Periodic.isMinimizerAt_stationary_translation_system line 752
93. theorem OAI.CubicTorus.periodic_minkowski_identities line 812