OAI/Geometry/EinsteinFour/WeylEstimates00.lean

GitHub source file

600 declarations, 0 contain sorry, 0 declared as axioms

The finite matrix certificates for the quadratic coupling estimate.

  1. def OAI.PositiveEinsteinFour.Quadratic.weight line 21
  2. def OAI.PositiveEinsteinFour.Quadratic.Pk line 22
  3. def OAI.PositiveEinsteinFour.Quadratic.Pl line 23
  4. def OAI.PositiveEinsteinFour.Quadratic.P0 line 24
  5. def OAI.PositiveEinsteinFour.Quadratic.K2 line 25
  6. def OAI.PositiveEinsteinFour.Quadratic.K1 line 28
  7. def OAI.PositiveEinsteinFour.Quadratic.K12 line 31
  8. def OAI.PositiveEinsteinFour.Quadratic.A11 line 33
  9. def OAI.PositiveEinsteinFour.Quadratic.A22 line 35
  10. def OAI.PositiveEinsteinFour.Quadratic.A12 line 37
  11. theorem OAI.PositiveEinsteinFour.Quadratic.combine_quadratic_sums line 40
  12. theorem OAI.PositiveEinsteinFour.Quadratic.combine_quadratic_nonneg line 53
  13. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc0 line 64
  14. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc1 line 69
  15. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc2 line 74
  16. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc3 line 79
  17. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc4 line 84
  18. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc5 line 89
  19. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc6 line 94
  20. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc7 line 99
  21. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc8 line 104
  22. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc9 line 109
  23. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc10 line 114
  24. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc11 line 119
  25. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc12 line 124
  26. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc13 line 129
  27. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc14 line 134
  28. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc15 line 139
  29. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc16 line 144
  30. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc17 line 149
  31. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc18 line 154
  32. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc19 line 159
  33. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc20 line 164
  34. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc21 line 169
  35. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc22 line 174
  36. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc23 line 179
  37. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc24 line 184
  38. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc25 line 189
  39. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc26 line 194
  40. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc27 line 199
  41. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc28 line 204
  42. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc29 line 209
  43. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc30 line 214
  44. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc31 line 219
  45. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc32 line 224
  46. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc33 line 229
  47. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc34 line 234
  48. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc35 line 239
  49. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc36 line 244
  50. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc37 line 249
  51. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc38 line 254
  52. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc39 line 259
  53. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc40 line 264
  54. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc41 line 269
  55. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc42 line 274
  56. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc43 line 279
  57. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_hc44 line 284
  58. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_entry11 line 288
  59. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_entry22 line 337
  60. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_entry12 line 386
  61. def OAI.PositiveEinsteinFour.Quadratic.A_OSC_data line 431
  62. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_entry11_list line 478
  63. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_entry22_list line 483
  64. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC_entry12_list line 488
  65. theorem OAI.PositiveEinsteinFour.Quadratic.A_OSC line 493
  66. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc0 line 547
  67. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc1 line 552
  68. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc2 line 557
  69. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc3 line 562
  70. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc4 line 567
  71. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc5 line 572
  72. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc6 line 577
  73. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc7 line 582
  74. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc8 line 587
  75. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc9 line 592
  76. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc10 line 597
  77. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc11 line 602
  78. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc12 line 607
  79. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc13 line 612
  80. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc14 line 617
  81. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc15 line 622
  82. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc16 line 627
  83. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc17 line 632
  84. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc18 line 637
  85. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc19 line 642
  86. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc20 line 647
  87. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc21 line 652
  88. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc22 line 657
  89. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc23 line 662
  90. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc24 line 667
  91. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc25 line 672
  92. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc26 line 677
  93. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc27 line 682
  94. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc28 line 687
  95. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc29 line 692
  96. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc30 line 697
  97. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc31 line 702
  98. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc32 line 707
  99. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc33 line 712
  100. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc34 line 717
  101. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc35 line 722
  102. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc36 line 727
  103. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc37 line 732
  104. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc38 line 737
  105. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc39 line 742
  106. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc40 line 747
  107. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc41 line 752
  108. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc42 line 757
  109. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc43 line 762
  110. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_hc44 line 767
  111. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_entry11 line 771
  112. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_entry22 line 820
  113. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_entry12 line 869
  114. def OAI.PositiveEinsteinFour.Quadratic.A_OCW_data line 900
  115. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_entry11_list line 947
  116. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_entry22_list line 952
  117. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW_entry12_list line 957
  118. theorem OAI.PositiveEinsteinFour.Quadratic.A_OCW line 962
  119. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc0 line 1016
  120. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc1 line 1021
  121. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc2 line 1026
  122. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc3 line 1031
  123. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc4 line 1036
  124. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc5 line 1041
  125. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc6 line 1046
  126. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc7 line 1051
  127. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc8 line 1056
  128. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc9 line 1061
  129. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc10 line 1066
  130. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc11 line 1071
  131. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc12 line 1076
  132. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc13 line 1081
  133. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc14 line 1086
  134. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc15 line 1091
  135. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc16 line 1096
  136. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc17 line 1101
  137. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc18 line 1106
  138. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc19 line 1111
  139. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc20 line 1116
  140. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc21 line 1121
  141. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc22 line 1126
  142. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc23 line 1131
  143. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc24 line 1136
  144. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc25 line 1141
  145. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc26 line 1146
  146. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc27 line 1151
  147. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc28 line 1156
  148. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc29 line 1161
  149. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc30 line 1166
  150. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc31 line 1171
  151. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc32 line 1176
  152. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc33 line 1181
  153. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc34 line 1186
  154. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc35 line 1191
  155. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc36 line 1196
  156. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc37 line 1201
  157. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc38 line 1206
  158. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc39 line 1211
  159. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc40 line 1216
  160. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc41 line 1221
  161. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc42 line 1226
  162. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc43 line 1231
  163. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_hc44 line 1236
  164. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_entry11 line 1240
  165. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_entry22 line 1289
  166. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_entry12 line 1338
  167. def OAI.PositiveEinsteinFour.Quadratic.A_SCU_data line 1386
  168. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_entry11_list line 1433
  169. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_entry22_list line 1438
  170. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU_entry12_list line 1443
  171. theorem OAI.PositiveEinsteinFour.Quadratic.A_SCU line 1448
  172. theorem OAI.PositiveEinsteinFour.Quadratic.axial_matrix_nonneg line 1504

    Source documentation

    Equation (21) at the axial spectral value, on the whole closed triangle. The proof checks the three finite triangle expansions above.

    theorem axial_matrix_nonneg {v b : ℝ}
    (hv : 0 ≤ v) (hb : 0 ≤ b) (hsum : v + b ≤ 2) (x y : ℝ) :
    0 ≤ A11 v b 1 * x ^ 2 + 2 * A12 v b 1 * x * y + A22 v b 1 * y ^ 2 := by
…

    Mentions: OAI.PositiveEinsteinFour.Quadratic.A11, OAI.PositiveEinsteinFour.Quadratic.A12, OAI.PositiveEinsteinFour.Quadratic.A22

  173. theorem OAI.PositiveEinsteinFour.Quadratic.spectral_matrix_identity line 1518

    Source documentation

    The exact matrix monotonicity identity used to move away from the axial spectral value. Its remainder is a square and a nonnegative diagonal term.

    theorem spectral_matrix_identity (v b σ x y : ℝ) :
    A11 v b σ * x ^ 2 + 2 * A12 v b σ * x * y + A22 v b σ * y ^ 2 =
      (A11 v b 1 * x ^ 2 + 2 * A12 v b 1 * x * y + A22 v b 1 * y ^ 2) +
      (1 - σ) * v ^ 2 * ((51 * v * x - Pl v b * y) ^ 2 +
        (51 / 5) * v * P0 v b * y ^ 2) := by
…

    Mentions: OAI.PositiveEinsteinFour.Quadratic.A11, OAI.PositiveEinsteinFour.Quadratic.A12, OAI.PositiveEinsteinFour.Quadratic.A22, OAI.PositiveEinsteinFour.Quadratic.Pl, OAI.PositiveEinsteinFour.Quadratic.P0

  174. theorem OAI.PositiveEinsteinFour.Quadratic.spectral_matrix_nonneg line 1529

    Source documentation

    The full matrix inequality (21) for every spectral value σ ≤ 1. The lower bound -1 ≤ σ is needed later for the Schur complement, but is not needed for this monotonicity implication.

    theorem spectral_matrix_nonneg {v b σ : ℝ}
    (hv : 0 ≤ v) (hb : 0 ≤ b) (hsum : v + b ≤ 2) (hσ : σ ≤ 1) (x y : ℝ) :
    0 ≤ A11 v b σ * x ^ 2 + 2 * A12 v b σ * x * y + A22 v b σ * y ^ 2 := by
…

    Mentions: OAI.PositiveEinsteinFour.Quadratic.A11, OAI.PositiveEinsteinFour.Quadratic.A12, OAI.PositiveEinsteinFour.Quadratic.A22

  175. def OAI.PositiveEinsteinFour.Quadratic.kappaV line 1539
  176. def OAI.PositiveEinsteinFour.Quadratic.kappaB line 1551
  177. theorem OAI.PositiveEinsteinFour.Quadratic.hasDerivAt_kappa_first line 1563
  178. theorem OAI.PositiveEinsteinFour.Quadratic.hasDerivAt_kappa_second line 1576
  179. def OAI.PositiveEinsteinFour.Quadratic.denominator line 1589
  180. def OAI.PositiveEinsteinFour.Quadratic.radialDenominator line 1590
  181. def OAI.PositiveEinsteinFour.Quadratic.axialCoefficient line 1591
  182. def OAI.PositiveEinsteinFour.Quadratic.Hdiag line 1594
  183. def OAI.PositiveEinsteinFour.Quadratic.Sbound line 1598
  184. def OAI.PositiveEinsteinFour.Quadratic.mixedNumerator line 1600
  185. def OAI.PositiveEinsteinFour.Quadratic.Hmixed line 1602
  186. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc0 line 1604
  187. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc1 line 1609
  188. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc2 line 1614
  189. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc3 line 1619
  190. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc4 line 1624
  191. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc5 line 1629
  192. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc6 line 1634
  193. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc7 line 1639
  194. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc8 line 1644
  195. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc9 line 1649
  196. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc10 line 1654
  197. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc11 line 1659
  198. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc12 line 1664
  199. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc13 line 1669
  200. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc14 line 1674
  201. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc15 line 1679
  202. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc16 line 1684
  203. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc17 line 1689
  204. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc18 line 1694
  205. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc19 line 1699
  206. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc20 line 1704
  207. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc21 line 1709
  208. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc22 line 1714
  209. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc23 line 1719
  210. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc24 line 1724
  211. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc25 line 1729
  212. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc26 line 1734
  213. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc27 line 1739
  214. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc28 line 1744
  215. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc29 line 1749
  216. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc30 line 1754
  217. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc31 line 1759
  218. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc32 line 1764
  219. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc33 line 1769
  220. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc34 line 1774
  221. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc35 line 1779
  222. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc36 line 1784
  223. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc37 line 1789
  224. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc38 line 1794
  225. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc39 line 1799
  226. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc40 line 1804
  227. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc41 line 1809
  228. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc42 line 1814
  229. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc43 line 1819
  230. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc44 line 1824
  231. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc45 line 1829
  232. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc46 line 1834
  233. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc47 line 1839
  234. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc48 line 1844
  235. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc49 line 1849
  236. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc50 line 1854
  237. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc51 line 1859
  238. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc52 line 1864
  239. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc53 line 1869
  240. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_hc54 line 1874
  241. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_entry11 line 1878
  242. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_entry22 line 1937
  243. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_entry12 line 1996
  244. def OAI.PositiveEinsteinFour.Quadratic.B_OAS_data line 2053
  245. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_entry11_list line 2110
  246. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_entry22_list line 2115
  247. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS_entry12_list line 2120
  248. theorem OAI.PositiveEinsteinFour.Quadratic.B_OAS line 2125
  249. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc0 line 2189
  250. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc1 line 2194
  251. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc2 line 2199
  252. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc3 line 2204
  253. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc4 line 2209
  254. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc5 line 2214
  255. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc6 line 2219
  256. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc7 line 2224
  257. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc8 line 2229
  258. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc9 line 2234
  259. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc10 line 2239
  260. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc11 line 2244
  261. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc12 line 2249
  262. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc13 line 2254
  263. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc14 line 2259
  264. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc15 line 2264
  265. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc16 line 2269
  266. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc17 line 2274
  267. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc18 line 2279
  268. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc19 line 2284
  269. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc20 line 2289
  270. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc21 line 2294
  271. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc22 line 2299
  272. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc23 line 2304
  273. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc24 line 2309
  274. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc25 line 2314
  275. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc26 line 2319
  276. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc27 line 2324
  277. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc28 line 2329
  278. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc29 line 2334
  279. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc30 line 2339
  280. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc31 line 2344
  281. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc32 line 2349
  282. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc33 line 2354
  283. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc34 line 2359
  284. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc35 line 2364
  285. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc36 line 2369
  286. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc37 line 2374
  287. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc38 line 2379
  288. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc39 line 2384
  289. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc40 line 2389
  290. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc41 line 2394
  291. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc42 line 2399
  292. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc43 line 2404
  293. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc44 line 2409
  294. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc45 line 2414
  295. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc46 line 2419
  296. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc47 line 2424
  297. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc48 line 2429
  298. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc49 line 2434
  299. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc50 line 2439
  300. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc51 line 2444
  301. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc52 line 2449
  302. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc53 line 2454
  303. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_hc54 line 2459
  304. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_entry11 line 2463
  305. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_entry22 line 2522
  306. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_entry12 line 2581
  307. def OAI.PositiveEinsteinFour.Quadratic.B_ASE_data line 2639
  308. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_entry11_list line 2696
  309. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_entry22_list line 2701
  310. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE_entry12_list line 2706
  311. theorem OAI.PositiveEinsteinFour.Quadratic.B_ASE line 2711
  312. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc0 line 2775
  313. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc1 line 2780
  314. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc2 line 2785
  315. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc3 line 2790
  316. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc4 line 2795
  317. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc5 line 2800
  318. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc6 line 2805
  319. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc7 line 2810
  320. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc8 line 2815
  321. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc9 line 2820
  322. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc11 line 2825
  323. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc12 line 2830
  324. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc13 line 2835
  325. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc14 line 2840
  326. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc15 line 2845
  327. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc16 line 2850
  328. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc17 line 2855
  329. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc18 line 2860
  330. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc19 line 2865
  331. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc20 line 2870
  332. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc21 line 2875
  333. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc22 line 2880
  334. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc23 line 2885
  335. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc24 line 2890
  336. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc25 line 2895
  337. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc26 line 2900
  338. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc27 line 2905
  339. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc28 line 2910
  340. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc29 line 2915
  341. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc30 line 2920
  342. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc31 line 2925
  343. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc32 line 2930
  344. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc33 line 2935
  345. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc34 line 2940
  346. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc35 line 2945
  347. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc36 line 2950
  348. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc37 line 2955
  349. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc38 line 2960
  350. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc39 line 2965
  351. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc40 line 2970
  352. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc41 line 2975
  353. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc42 line 2980
  354. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc43 line 2985
  355. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc44 line 2990
  356. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc45 line 2995
  357. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc46 line 3000
  358. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc47 line 3005
  359. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc48 line 3010
  360. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc49 line 3015
  361. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc50 line 3020
  362. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc51 line 3025
  363. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc52 line 3030
  364. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc53 line 3035
  365. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc54 line 3040
  366. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc55 line 3045
  367. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc56 line 3050
  368. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc57 line 3055
  369. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc58 line 3060
  370. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc59 line 3065
  371. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc60 line 3070
  372. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc61 line 3075
  373. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc62 line 3080
  374. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc63 line 3085
  375. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc64 line 3090
  376. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_hc65 line 3095
  377. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_entry11 line 3099
  378. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_entry22 line 3168
  379. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_entry12 line 3237
  380. def OAI.PositiveEinsteinFour.Quadratic.B_ACE_data line 3305
  381. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_entry11_list line 3372
  382. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_entry22_list line 3377
  383. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE_entry12_list line 3382
  384. theorem OAI.PositiveEinsteinFour.Quadratic.B_ACE line 3387
  385. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc0 line 3461
  386. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc1 line 3466
  387. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc2 line 3471
  388. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc3 line 3476
  389. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc4 line 3481
  390. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc5 line 3486
  391. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc6 line 3491
  392. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc7 line 3496
  393. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc8 line 3501
  394. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc9 line 3506
  395. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc10 line 3511
  396. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc11 line 3516
  397. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc12 line 3521
  398. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc13 line 3526
  399. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc14 line 3531
  400. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc15 line 3536
  401. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc16 line 3541
  402. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc17 line 3546
  403. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc18 line 3551
  404. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc19 line 3556
  405. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc20 line 3561
  406. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc21 line 3566
  407. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc22 line 3571
  408. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc23 line 3576
  409. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc24 line 3581
  410. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc25 line 3586
  411. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc26 line 3591
  412. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc27 line 3596
  413. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc28 line 3601
  414. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc29 line 3606
  415. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc30 line 3611
  416. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc31 line 3616
  417. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc32 line 3621
  418. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc33 line 3626
  419. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc34 line 3631
  420. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc35 line 3636
  421. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc36 line 3641
  422. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc37 line 3646
  423. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc38 line 3651
  424. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc39 line 3656
  425. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc40 line 3661
  426. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc41 line 3666
  427. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc42 line 3671
  428. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc43 line 3676
  429. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc44 line 3681
  430. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc45 line 3686
  431. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc46 line 3691
  432. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc47 line 3696
  433. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc48 line 3701
  434. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc49 line 3706
  435. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc50 line 3711
  436. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc51 line 3716
  437. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc52 line 3721
  438. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc53 line 3726
  439. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_hc54 line 3731
  440. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_entry11 line 3735
  441. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_entry22 line 3794
  442. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_entry12 line 3853
  443. def OAI.PositiveEinsteinFour.Quadratic.B_SBE_data line 3911
  444. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_entry11_list line 3968
  445. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_entry22_list line 3973
  446. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE_entry12_list line 3978
  447. theorem OAI.PositiveEinsteinFour.Quadratic.B_SBE line 3983
  448. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc0 line 4047
  449. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc1 line 4052
  450. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc2 line 4057
  451. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc3 line 4062
  452. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc4 line 4067
  453. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc5 line 4072
  454. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc6 line 4077
  455. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc7 line 4082
  456. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc8 line 4087
  457. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc9 line 4092
  458. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc10 line 4097
  459. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc11 line 4102
  460. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc12 line 4107
  461. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc13 line 4112
  462. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc14 line 4117
  463. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc15 line 4122
  464. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc16 line 4127
  465. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc17 line 4132
  466. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc18 line 4137
  467. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc19 line 4142
  468. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc20 line 4147
  469. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc21 line 4152
  470. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc22 line 4157
  471. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc23 line 4162
  472. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc24 line 4167
  473. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc25 line 4172
  474. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc26 line 4177
  475. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc27 line 4182
  476. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc28 line 4187
  477. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc29 line 4192
  478. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc30 line 4197
  479. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc31 line 4202
  480. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc32 line 4207
  481. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc33 line 4212
  482. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc34 line 4217
  483. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc35 line 4222
  484. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc36 line 4227
  485. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc37 line 4232
  486. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc38 line 4237
  487. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc39 line 4242
  488. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc40 line 4247
  489. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc41 line 4252
  490. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc42 line 4257
  491. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc43 line 4262
  492. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc44 line 4267
  493. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc45 line 4272
  494. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc46 line 4277
  495. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc47 line 4282
  496. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc48 line 4287
  497. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc49 line 4292
  498. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc50 line 4297
  499. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc51 line 4302
  500. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc52 line 4307
  501. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc53 line 4312
  502. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc54 line 4317
  503. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc55 line 4322
  504. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc56 line 4327
  505. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc57 line 4332
  506. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc58 line 4337
  507. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc59 line 4342
  508. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc60 line 4347
  509. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc61 line 4352
  510. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc62 line 4357
  511. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_hc63 line 4362
  512. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_entry11 line 4366
  513. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_entry22 line 4434
  514. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_entry12 line 4502
  515. def OAI.PositiveEinsteinFour.Quadratic.B_CBE_data line 4569
  516. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_entry11_list line 4635
  517. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_entry22_list line 4640
  518. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE_entry12_list line 4645
  519. theorem OAI.PositiveEinsteinFour.Quadratic.B_CBE line 4650
  520. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc0 line 4723
  521. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc1 line 4728
  522. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc2 line 4733
  523. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc3 line 4738
  524. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc4 line 4743
  525. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc5 line 4748
  526. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc6 line 4753
  527. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc7 line 4758
  528. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc8 line 4763
  529. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc9 line 4768
  530. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc10 line 4773
  531. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc11 line 4778
  532. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc12 line 4783
  533. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc13 line 4788
  534. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc14 line 4793
  535. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc15 line 4798
  536. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc16 line 4803
  537. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc17 line 4808
  538. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc18 line 4813
  539. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc19 line 4818
  540. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc20 line 4823
  541. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc21 line 4828
  542. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc22 line 4833
  543. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc23 line 4838
  544. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc24 line 4843
  545. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc25 line 4848
  546. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc26 line 4853
  547. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc27 line 4858
  548. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc28 line 4863
  549. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc29 line 4868
  550. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc30 line 4873
  551. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc31 line 4878
  552. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc32 line 4883
  553. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc33 line 4888
  554. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc34 line 4893
  555. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc35 line 4898
  556. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc36 line 4903
  557. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc37 line 4908
  558. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc38 line 4913
  559. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc39 line 4918
  560. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc40 line 4923
  561. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc41 line 4928
  562. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc42 line 4933
  563. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc43 line 4938
  564. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc44 line 4943
  565. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc45 line 4948
  566. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc46 line 4953
  567. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc47 line 4958
  568. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc48 line 4963
  569. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc49 line 4968
  570. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc50 line 4973
  571. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc51 line 4978
  572. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc52 line 4983
  573. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc53 line 4988
  574. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_hc54 line 4993
  575. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_entry11 line 4997
  576. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_entry22 line 5056
  577. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_entry12 line 5115
  578. def OAI.PositiveEinsteinFour.Quadratic.B_SUB_data line 5173
  579. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_entry11_list line 5230
  580. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_entry22_list line 5235
  581. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB_entry12_list line 5240
  582. theorem OAI.PositiveEinsteinFour.Quadratic.B_SUB line 5245
  583. theorem OAI.PositiveEinsteinFour.Quadratic.coupling_matrix_nonneg line 5311

    Source documentation

    The second matrix certificate, on the ordered half of the closed spectral triangle. The six Bernstein triangles retain their boundary zero matrices.

    theorem coupling_matrix_nonneg {v b : ℝ}
    (hb : 0 ≤ b) (horder : b ≤ v) (hsum : v + b ≤ 2) (x y : ℝ) :
    0 ≤ Hdiag v b * x ^ 2 + 2 * Hmixed v b * x * y + Hdiag b v * y ^ 2 := by
…

    Mentions: OAI.PositiveEinsteinFour.Quadratic.Hdiag, OAI.PositiveEinsteinFour.Quadratic.Hmixed

  584. def OAI.PositiveEinsteinFour.Quadratic.quadraticCoefficient line 5366
  585. def OAI.PositiveEinsteinFour.Quadratic.mixedCoefficient line 5369
  586. def OAI.PositiveEinsteinFour.Quadratic.diagonalDifference line 5372
  587. theorem OAI.PositiveEinsteinFour.Quadratic.denominator_pos line 5375
  588. theorem OAI.PositiveEinsteinFour.Quadratic.radialDenominator_pos line 5379
  589. theorem OAI.PositiveEinsteinFour.Quadratic.denominator_swap line 5384
  590. theorem OAI.PositiveEinsteinFour.Quadratic.diagonalDifference_eq line 5388
  591. theorem OAI.PositiveEinsteinFour.Quadratic.mixedCoefficient_eq line 5397
  592. theorem OAI.PositiveEinsteinFour.Quadratic.Sbound_sq line 5403
  593. theorem OAI.PositiveEinsteinFour.Quadratic.quotient_matrix_nonneg line 5414
  594. theorem OAI.PositiveEinsteinFour.Quadratic.ordered_quadratic_bound line 5453
  595. theorem OAI.PositiveEinsteinFour.Quadratic.quadratic_bound line 5469

    Source documentation

    The scalar quadratic-form inequality (22) on the positive part of the spectral triangle. The result is symmetric, although its finite certificate was verified on the half with the first block larger.

    theorem quadratic_bound {v b : ℝ}
    (hv : 0 < v) (hb : 0 < b) (hsum : v + b ≤ 2) (x y : ℝ) :
    quadraticCoefficient v b * x ^ 2 + 2 * mixedCoefficient v b * x * y +
      quadraticCoefficient b v * y ^ 2 ≤
      2 * theta v b * (normWeight v * x ^ 2 + normWeight b * y ^ 2) := by
…

    Mentions: OAI.PositiveEinsteinFour.Quadratic.quadraticCoefficient, OAI.PositiveEinsteinFour.Quadratic.mixedCoefficient, OAI.PositiveEinsteinFour.normWeight

  596. theorem OAI.PositiveEinsteinFour.Quadratic.zero_second_diagonal_bound line 5485
  597. theorem OAI.PositiveEinsteinFour.Quadratic.quadratic_bound_closed line 5501

    Source documentation

    Equation (22) on the closed spectral triangle, using the zero-set convention that derivative entries vanish with their Weyl norm. No continuity of a coefficient containing 1/v or 1/b is asserted.

    theorem quadratic_bound_closed {v b : ℝ}
    (hv : 0 ≤ v) (hb : 0 ≤ b) (hsum : v + b ≤ 2) (x y : ℝ)
    (hx : v = 0 → x = 0) (hy : b = 0 → y = 0) :
    quadraticCoefficient v b * x ^ 2 + 2 * mixedCoefficient v b * x * y +
      quadraticCoefficient b v * y ^ 2 ≤
      2 * theta v b * (normWeight v * x ^ 2 + normWeight b * y ^ 2) := by
…

    Mentions: OAI.PositiveEinsteinFour.Quadratic.quadraticCoefficient, OAI.PositiveEinsteinFour.Quadratic.mixedCoefficient, OAI.PositiveEinsteinFour.normWeight

  598. theorem OAI.PositiveEinsteinFour.hilbert_quadratic_bound_closed line 5554

    Source documentation

    The scalar quadratic estimate also holds for tangent vectors, with their actual pairing. The proof chooses the sign of a scalar test vector according to the sign of the mixed coefficient.

    theorem hilbert_quadratic_bound_closed
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    {v b : ℝ} (hv : 0 ≤ v) (hb : 0 ≤ b) (hsum : v + b ≤ 2)
    (p q : E) (hp : v = 0 → p = 0) (hq : b = 0 → q = 0) :
    quadraticCoefficient v b * ‖p‖ ^ 2 + 2 * mixedCoefficient v b * inner ℝ p q +
      quadraticCoefficient b v * ‖q‖ ^ 2 ≤
      2 * theta v b * (normWeight v * ‖p‖ ^ 2 + normWeight b * ‖q‖ ^ 2) := by
…

    Mentions: OAI.PositiveEinsteinFour.normWeight

  599. def OAI.PositiveEinsteinFour.reducedIntegrand line 5579

    Source documentation

    The explicit upper expression obtained after the quartic projection and quadratic axial reductions. It retains the two actual total derivative energies and the inner product of the two norm gradients.

    def reducedIntegrand
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    (v b r s σ τ ρ χ e f : ℝ) (p q : E) : ℝ :=
…
  600. theorem OAI.PositiveEinsteinFour.reduced_integrand_bound line 5591

    Source documentation

    Every scalar estimate needed for the final coupled bound, including all zero sets, follows from the concrete polynomial certificates.

    theorem reduced_integrand_bound
    {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E]
    {v b r s σ τ ρ χ e f : ℝ} (p q : E)
    (hv : 0 ≤ v) (hb : 0 ≤ b)
    (hr : 1 ≤ r) (hr2 : r ≤ 2) (hs : 1 ≤ s) (hs2 : s ≤ 2)
    (hspectral : v * r + b * s ≤ 2)
    (hσ : σ = (3 * r - r ^ 3) / 2) (hρ : ρ ^ 2 = 1 - σ ^ 2)
    (hτ : τ = (3 * s - s ^ 3) / 2) (hχ : χ ^ 2 = 1 - τ ^ 2)
    (he : (5 / 3) * ‖p‖ ^ 2 ≤ e) (hf : (5 / 3) * ‖q‖ ^ 2 ≤ f)
    (hve : v = 0 → e = 0) (hbf : b = 0 → f = 0) :
    reducedIntegrand v b r s σ τ ρ χ e f p q ≤
      -couplingCoefficient v b * (‖p‖ ^ 2 + ‖q‖ ^ 2) *
…

    Mentions: OAI.PositiveEinsteinFour.reducedIntegrand, OAI.PositiveEinsteinFour.couplingCoefficient