OAI/MathematicalPhysics/Transonic/Certificates/FixedLowMinusBarrier.lean

GitHub source file

190 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.FixedLowMinusBarrier.Q line 9
  2. def OAI.SepticProfile.FixedLowMinusBarrier.u line 10
  3. def OAI.SepticProfile.FixedLowMinusBarrier.b line 11
  4. def OAI.SepticProfile.FixedLowMinusBarrier.c line 12
  5. def OAI.SepticProfile.FixedLowMinusBarrier.d line 13
  6. def OAI.SepticProfile.FixedLowMinusBarrier.r line 14
  7. def OAI.SepticProfile.FixedLowMinusBarrier.sigma line 15
  8. def OAI.SepticProfile.FixedLowMinusBarrier.kappa line 16
  9. def OAI.SepticProfile.FixedLowMinusBarrier.params line 17
  10. def OAI.SepticProfile.FixedLowMinusBarrier.trace line 18
  11. theorem OAI.SepticProfile.FixedLowMinusBarrier.Q_pos line 19
  12. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_0 line 20
  13. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_16 line 22
  14. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_32 line 24
  15. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_48 line 26
  16. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_64 line 28
  17. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_80 line 30
  18. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_96 line 32
  19. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_112 line 34
  20. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_128 line 36
  21. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_144 line 38
  22. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_160 line 40
  23. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_176 line 42
  24. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_192 line 44
  25. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_208 line 46
  26. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_224 line 48
  27. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_240 line 50
  28. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_256 line 52
  29. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_272 line 54
  30. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_288 line 56
  31. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_304 line 58
  32. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_320 line 60
  33. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_336 line 62
  34. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_352 line 64
  35. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_368 line 66
  36. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_384 line 68
  37. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_400 line 70
  38. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_416 line 72
  39. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_432 line 74
  40. theorem OAI.SepticProfile.FixedLowMinusBarrier.square_data line 76
  41. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_0 line 132
  42. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_16 line 134
  43. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_32 line 136
  44. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_48 line 138
  45. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_64 line 140
  46. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_80 line 142
  47. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_96 line 144
  48. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_112 line 146
  49. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_128 line 148
  50. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_144 line 150
  51. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_160 line 152
  52. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_176 line 154
  53. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_192 line 156
  54. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_208 line 158
  55. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_224 line 160
  56. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_240 line 162
  57. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_256 line 164
  58. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_272 line 166
  59. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_288 line 168
  60. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_304 line 170
  61. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_320 line 172
  62. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_336 line 174
  63. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_352 line 176
  64. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_368 line 178
  65. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_384 line 180
  66. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_400 line 182
  67. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_416 line 184
  68. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_432 line 186
  69. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_448 line 188
  70. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_464 line 190
  71. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_480 line 192
  72. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_496 line 194
  73. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_512 line 196
  74. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_528 line 198
  75. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_544 line 200
  76. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_560 line 202
  77. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_576 line 204
  78. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_592 line 206
  79. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_608 line 208
  80. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_624 line 210
  81. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_640 line 212
  82. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_656 line 214
  83. theorem OAI.SepticProfile.FixedLowMinusBarrier.cube_data line 216
  84. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_0 line 300
  85. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_16 line 302
  86. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_32 line 304
  87. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_48 line 306
  88. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_64 line 308
  89. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_80 line 310
  90. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_96 line 312
  91. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_112 line 314
  92. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_128 line 316
  93. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_144 line 318
  94. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_160 line 320
  95. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_176 line 322
  96. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_192 line 324
  97. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_208 line 326
  98. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_224 line 328
  99. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_240 line 330
  100. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_256 line 332
  101. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_272 line 334
  102. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_288 line 336
  103. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_304 line 338
  104. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_320 line 340
  105. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_336 line 342
  106. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_352 line 344
  107. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_368 line 346
  108. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_384 line 348
  109. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_400 line 350
  110. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_416 line 352
  111. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_432 line 354
  112. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_448 line 356
  113. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_464 line 358
  114. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_480 line 360
  115. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_496 line 362
  116. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_512 line 364
  117. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_528 line 366
  118. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_544 line 368
  119. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_560 line 370
  120. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_576 line 372
  121. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_592 line 374
  122. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_608 line 376
  123. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_624 line 378
  124. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_640 line 380
  125. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_656 line 382
  126. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_672 line 384
  127. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_688 line 386
  128. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_704 line 388
  129. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_720 line 390
  130. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_736 line 392
  131. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_752 line 394
  132. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_768 line 396
  133. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_784 line 398
  134. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_800 line 400
  135. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_816 line 402
  136. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_832 line 404
  137. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_848 line 406
  138. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_864 line 408
  139. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_880 line 410
  140. theorem OAI.SepticProfile.FixedLowMinusBarrier.fourth_data line 412
  141. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_140 line 524
  142. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_156 line 526
  143. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_172 line 528
  144. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_188 line 530
  145. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_204 line 532
  146. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_220 line 534
  147. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_236 line 536
  148. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_252 line 538
  149. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_268 line 540
  150. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_284 line 542
  151. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_300 line 544
  152. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_316 line 546
  153. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_332 line 548
  154. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_348 line 550
  155. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_364 line 552
  156. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_380 line 554
  157. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_396 line 556
  158. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_412 line 558
  159. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_428 line 560
  160. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_444 line 562
  161. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_460 line 564
  162. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_476 line 566
  163. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_492 line 568
  164. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_508 line 570
  165. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_524 line 572
  166. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_540 line 574
  167. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_556 line 576
  168. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_572 line 578
  169. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_588 line 580
  170. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_604 line 582
  171. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_620 line 584
  172. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_636 line 586
  173. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_652 line 588
  174. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_668 line 590
  175. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_684 line 592
  176. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_700 line 594
  177. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_716 line 596
  178. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_732 line 598
  179. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_748 line 600
  180. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_764 line 602
  181. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_780 line 604
  182. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_796 line 606
  183. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_812 line 608
  184. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_828 line 610
  185. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_844 line 612
  186. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_860 line 614
  187. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_876 line 616
  188. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_data line 618
  189. theorem OAI.SepticProfile.FixedLowMinusBarrier.validPowers line 712
  190. theorem OAI.SepticProfile.FixedLowMinusBarrier.residual_coefficients_enclosed line 722