OAI/Geometry/CubicTorus/Profiles/GainBounds.lean

GitHub source file

189 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_gain line 20
2. lemma OAI.ReusedScalar205.CubicTorus.Scalar.active_upper_argument_jets line 32
3. lemma OAI.ReusedScalar205.CubicTorus.Scalar.gain_upper_support line 91
4. theorem OAI.ReusedScalar205.CubicTorus.Scalar.concaveOn_gain_corrected line 167
5. lemma OAI.ReusedScalar205.CubicTorus.Scalar.planar_switches line 178
6. lemma OAI.ReusedScalar205.CubicTorus.Scalar.le_rho_of_le_switch line 184
7. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rho_le_of_switch_le line 195
8. lemma OAI.ReusedScalar205.CubicTorus.Scalar.minSection_quadratic line 209
9. lemma OAI.ReusedScalar205.CubicTorus.Scalar.minSection_linear line 215
10. lemma OAI.ReusedScalar205.CubicTorus.Scalar.minSection_rho line 222
11. def OAI.ReusedScalar205.CubicTorus.Scalar.beta line 231
12. def OAI.ReusedScalar205.CubicTorus.Scalar.J₀ line 232
13. def OAI.ReusedScalar205.CubicTorus.Scalar.J₁ line 233
14. def OAI.ReusedScalar205.CubicTorus.Scalar.J₂ line 234
15. lemma OAI.ReusedScalar205.CubicTorus.Scalar.beta_pos line 237
16. lemma OAI.ReusedScalar205.CubicTorus.Scalar.beta_sq line 241
17. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_beta line 245
18. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_J₀ line 251
19. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_J₁ line 256
20. lemma OAI.ReusedScalar205.CubicTorus.Scalar.hasDerivAt_J₂ line 273
21. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuous_beta line 295
22. lemma OAI.ReusedScalar205.CubicTorus.Scalar.beta_ne_zero_on line 297
23. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_J₀ line 300
24. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_J₁ line 303
25. lemma OAI.ReusedScalar205.CubicTorus.Scalar.continuousOn_J₂ line 311
26. lemma OAI.ReusedScalar205.CubicTorus.Scalar.moment_integral line 322
27. lemma OAI.ReusedScalar205.CubicTorus.Scalar.moments_zero line 340
28. def OAI.ReusedScalar205.CubicTorus.Scalar.rhoChord line 343
29. def OAI.ReusedScalar205.CubicTorus.Scalar.chordMoment line 346
30. lemma OAI.ReusedScalar205.CubicTorus.Scalar.rhoChord_le line 350
31. lemma OAI.ReusedScalar205.CubicTorus.Scalar.integral_rhoChord line 367
32. lemma OAI.ReusedScalar205.CubicTorus.Scalar.section_density_integrable line 385
33. lemma OAI.ReusedScalar205.CubicTorus.Scalar.integral_section_quadratic line 391
34. lemma OAI.ReusedScalar205.CubicTorus.Scalar.integral_section_linear line 411
35. lemma OAI.ReusedScalar205.CubicTorus.Scalar.integral_section_chord line 437
36. def OAI.ReusedScalar205.CubicTorus.Scalar.twoChordBaseline line 453
37. def OAI.ReusedScalar205.CubicTorus.Scalar.linearBaseline line 460
38. lemma OAI.ReusedScalar205.CubicTorus.Scalar.twoChordBaseline_le line 464
39. lemma OAI.ReusedScalar205.CubicTorus.Scalar.linearBaseline_eq line 502
40. lemma OAI.ReusedScalar205.CubicTorus.Scalar.semiconcave_chord_bound line 520
41. lemma OAI.ReusedScalar205.CubicTorus.Scalar.baseline_chord_lower line 546
42. lemma OAI.ReusedScalar205.CubicTorus.Scalar.combined_chord_lower line 559
43. lemma OAI.ReusedScalar205.CubicTorus.Scalar.coarse_switch_bounds line 580
44. lemma OAI.ReusedScalar205.CubicTorus.Scalar.coarse_cutoff_bounds line 590
45. lemma OAI.ReusedScalar205.CubicTorus.Scalar.twoChordBaseline_le_of_range line 593
46. lemma OAI.ReusedScalar205.CubicTorus.Scalar.linearBaseline_eq_of_range line 599
47. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e0 line 615
48. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b0 line 616
49. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e1 line 622
50. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b1 line 623
51. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e2 line 626
52. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b2 line 627
53. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e3 line 630
54. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b3 line 631
55. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e4 line 634
56. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b4 line 635
57. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e5 line 638
58. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b5 line 639
59. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e6 line 642
60. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b6 line 643
61. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e7 line 646
62. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b7 line 647
63. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e8 line 650
64. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b8 line 651
65. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e9 line 654
66. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b9 line 655
67. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e10 line 658
68. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b10 line 659
69. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e11 line 662
70. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b11 line 663
71. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e12 line 666
72. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b12 line 667
73. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e13 line 670
74. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b13 line 671
75. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e14 line 674
76. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b14 line 675
77. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e15 line 678
78. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b15 line 679
79. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e16 line 682
80. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b16 line 683
81. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e17 line 686
82. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b17 line 687
83. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e18 line 690
84. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b18 line 691
85. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e19 line 694
86. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b19 line 695
87. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e20 line 698
88. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b20 line 699
89. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e21 line 702
90. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b21 line 703
91. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e22 line 706
92. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b22 line 707
93. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e23 line 710
94. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b23 line 711
95. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e24 line 714
96. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b24 line 715
97. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e25 line 718
98. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b25 line 719
99. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e26 line 722
100. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b26 line 723
101. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e27 line 726
102. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b27 line 727
103. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e28 line 730
104. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b28 line 731
105. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e29 line 734
106. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b29 line 735
107. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e30 line 738
108. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b30 line 739
109. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e31 line 742
110. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b31 line 743
111. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e32 line 746
112. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b32 line 747
113. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e33 line 750
114. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b33 line 751
115. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e34 line 754
116. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b34 line 755
117. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e35 line 758
118. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b35 line 759
119. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e36 line 762
120. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b36 line 763
121. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e37 line 766
122. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b37 line 767
123. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e38 line 770
124. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b38 line 771
125. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e39 line 774
126. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b39 line 775
127. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e40 line 778
128. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b40 line 779
129. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e41 line 782
130. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b41 line 783
131. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e42 line 786
132. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b42 line 787
133. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e43 line 790
134. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b43 line 791
135. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e44 line 794
136. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b44 line 795
137. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e45 line 798
138. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b45 line 799
139. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e46 line 802
140. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b46 line 803
141. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e47 line 806
142. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b47 line 807
143. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e48 line 810
144. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b48 line 811
145. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e49 line 814
146. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b49 line 815
147. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e50 line 818
148. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b50 line 819
149. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e51 line 822
150. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b51 line 823
151. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e52 line 826
152. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b52 line 827
153. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e53 line 830
154. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b53 line 831
155. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e54 line 834
156. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b54 line 835
157. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e55 line 838
158. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b55 line 839
159. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e56 line 842
160. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b56 line 843
161. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e57 line 846
162. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b57 line 847
163. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e58 line 850
164. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b58 line 851
165. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e59 line 860
166. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b59 line 861
167. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e60 line 864
168. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b60 line 865
169. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e61 line 868
170. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b61 line 869
171. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e62 line 872
172. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b62 line 873
173. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e63 line 876
174. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b63 line 877
175. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e64 line 880
176. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b64 line 881
177. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e65 line 884
178. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b65 line 885
179. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e66 line 888
180. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b66 line 889
181. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e67 line 892
182. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b67 line 893
183. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e68 line 896
184. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b68 line 897
185. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e69 line 900
186. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b69 line 901
187. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e70 line 904
188. lemma OAI.ReusedScalar205.CubicTorus.Scalar.Cert.b70 line 905
189. def OAI.ReusedScalar205.CubicTorus.Scalar.Cert.e71 line 908