OAI/MathematicalPhysics/Transonic/Certificates/FixedHighJet.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.FixedHighJet.Q line 9
  2. def OAI.SepticProfile.FixedHighJet.w line 10
  3. def OAI.SepticProfile.FixedHighJet.b line 11
  4. def OAI.SepticProfile.FixedHighJet.c line 12
  5. def OAI.SepticProfile.FixedHighJet.d line 13
  6. def OAI.SepticProfile.FixedHighJet.br line 14
  7. def OAI.SepticProfile.FixedHighJet.r line 15
  8. def OAI.SepticProfile.FixedHighJet.sigma line 16
  9. def OAI.SepticProfile.FixedHighJet.kappa line 17
  10. def OAI.SepticProfile.FixedHighJet.a line 18
  11. def OAI.SepticProfile.FixedHighJet.params line 19
  12. def OAI.SepticProfile.FixedHighJet.trace line 20
  13. theorem OAI.SepticProfile.FixedHighJet.Q_pos line 21
  14. theorem OAI.SepticProfile.FixedHighJet.square_0 line 22
  15. theorem OAI.SepticProfile.FixedHighJet.square_16 line 24
  16. theorem OAI.SepticProfile.FixedHighJet.square_32 line 26
  17. theorem OAI.SepticProfile.FixedHighJet.square_48 line 28
  18. theorem OAI.SepticProfile.FixedHighJet.square_64 line 30
  19. theorem OAI.SepticProfile.FixedHighJet.square_80 line 32
  20. theorem OAI.SepticProfile.FixedHighJet.square_96 line 34
  21. theorem OAI.SepticProfile.FixedHighJet.square_112 line 36
  22. theorem OAI.SepticProfile.FixedHighJet.square_128 line 38
  23. theorem OAI.SepticProfile.FixedHighJet.square_144 line 40
  24. theorem OAI.SepticProfile.FixedHighJet.square_160 line 42
  25. theorem OAI.SepticProfile.FixedHighJet.square_176 line 44
  26. theorem OAI.SepticProfile.FixedHighJet.square_192 line 46
  27. theorem OAI.SepticProfile.FixedHighJet.square_208 line 48
  28. theorem OAI.SepticProfile.FixedHighJet.square_data line 50
  29. theorem OAI.SepticProfile.FixedHighJet.cube_0 line 78
  30. theorem OAI.SepticProfile.FixedHighJet.cube_16 line 80
  31. theorem OAI.SepticProfile.FixedHighJet.cube_32 line 82
  32. theorem OAI.SepticProfile.FixedHighJet.cube_48 line 84
  33. theorem OAI.SepticProfile.FixedHighJet.cube_64 line 86
  34. theorem OAI.SepticProfile.FixedHighJet.cube_80 line 88
  35. theorem OAI.SepticProfile.FixedHighJet.cube_96 line 90
  36. theorem OAI.SepticProfile.FixedHighJet.cube_112 line 92
  37. theorem OAI.SepticProfile.FixedHighJet.cube_128 line 94
  38. theorem OAI.SepticProfile.FixedHighJet.cube_144 line 96
  39. theorem OAI.SepticProfile.FixedHighJet.cube_160 line 98
  40. theorem OAI.SepticProfile.FixedHighJet.cube_176 line 100
  41. theorem OAI.SepticProfile.FixedHighJet.cube_192 line 102
  42. theorem OAI.SepticProfile.FixedHighJet.cube_208 line 104
  43. theorem OAI.SepticProfile.FixedHighJet.cube_data line 106
  44. theorem OAI.SepticProfile.FixedHighJet.fourth_0 line 134
  45. theorem OAI.SepticProfile.FixedHighJet.fourth_16 line 136
  46. theorem OAI.SepticProfile.FixedHighJet.fourth_32 line 138
  47. theorem OAI.SepticProfile.FixedHighJet.fourth_48 line 140
  48. theorem OAI.SepticProfile.FixedHighJet.fourth_64 line 142
  49. theorem OAI.SepticProfile.FixedHighJet.fourth_80 line 144
  50. theorem OAI.SepticProfile.FixedHighJet.fourth_96 line 146
  51. theorem OAI.SepticProfile.FixedHighJet.fourth_112 line 148
  52. theorem OAI.SepticProfile.FixedHighJet.fourth_128 line 150
  53. theorem OAI.SepticProfile.FixedHighJet.fourth_144 line 152
  54. theorem OAI.SepticProfile.FixedHighJet.fourth_160 line 154
  55. theorem OAI.SepticProfile.FixedHighJet.fourth_176 line 156
  56. theorem OAI.SepticProfile.FixedHighJet.fourth_192 line 158
  57. theorem OAI.SepticProfile.FixedHighJet.fourth_208 line 160
  58. theorem OAI.SepticProfile.FixedHighJet.fourth_data line 162
  59. theorem OAI.SepticProfile.FixedHighJet.squareR_2 line 190
  60. theorem OAI.SepticProfile.FixedHighJet.squareR_18 line 192
  61. theorem OAI.SepticProfile.FixedHighJet.squareR_34 line 194
  62. theorem OAI.SepticProfile.FixedHighJet.squareR_50 line 196
  63. theorem OAI.SepticProfile.FixedHighJet.squareR_66 line 198
  64. theorem OAI.SepticProfile.FixedHighJet.squareR_82 line 200
  65. theorem OAI.SepticProfile.FixedHighJet.squareR_98 line 202
  66. theorem OAI.SepticProfile.FixedHighJet.squareR_114 line 204
  67. theorem OAI.SepticProfile.FixedHighJet.squareR_130 line 206
  68. theorem OAI.SepticProfile.FixedHighJet.squareR_146 line 208
  69. theorem OAI.SepticProfile.FixedHighJet.squareR_162 line 210
  70. theorem OAI.SepticProfile.FixedHighJet.squareR_178 line 212
  71. theorem OAI.SepticProfile.FixedHighJet.squareR_194 line 214
  72. theorem OAI.SepticProfile.FixedHighJet.squareR_210 line 216
  73. theorem OAI.SepticProfile.FixedHighJet.squareR_data line 218
  74. theorem OAI.SepticProfile.FixedHighJet.residual_2 line 246
  75. theorem OAI.SepticProfile.FixedHighJet.residual_18 line 248
  76. theorem OAI.SepticProfile.FixedHighJet.residual_34 line 250
  77. theorem OAI.SepticProfile.FixedHighJet.residual_50 line 252
  78. theorem OAI.SepticProfile.FixedHighJet.residual_66 line 254
  79. theorem OAI.SepticProfile.FixedHighJet.residual_82 line 256
  80. theorem OAI.SepticProfile.FixedHighJet.residual_98 line 258
  81. theorem OAI.SepticProfile.FixedHighJet.residual_114 line 260
  82. theorem OAI.SepticProfile.FixedHighJet.residual_130 line 262
  83. theorem OAI.SepticProfile.FixedHighJet.residual_146 line 264
  84. theorem OAI.SepticProfile.FixedHighJet.residual_162 line 266
  85. theorem OAI.SepticProfile.FixedHighJet.residual_178 line 268
  86. theorem OAI.SepticProfile.FixedHighJet.residual_194 line 270
  87. theorem OAI.SepticProfile.FixedHighJet.residual_210 line 272
  88. theorem OAI.SepticProfile.FixedHighJet.residual_data line 274
  89. theorem OAI.SepticProfile.FixedHighJet.update_2 line 302
  90. theorem OAI.SepticProfile.FixedHighJet.update_18 line 304
  91. theorem OAI.SepticProfile.FixedHighJet.update_34 line 306
  92. theorem OAI.SepticProfile.FixedHighJet.update_50 line 308
  93. theorem OAI.SepticProfile.FixedHighJet.update_66 line 310
  94. theorem OAI.SepticProfile.FixedHighJet.update_82 line 312
  95. theorem OAI.SepticProfile.FixedHighJet.update_98 line 314
  96. theorem OAI.SepticProfile.FixedHighJet.update_114 line 316
  97. theorem OAI.SepticProfile.FixedHighJet.update_130 line 318
  98. theorem OAI.SepticProfile.FixedHighJet.update_146 line 320
  99. theorem OAI.SepticProfile.FixedHighJet.update_162 line 322
  100. theorem OAI.SepticProfile.FixedHighJet.update_178 line 324
  101. theorem OAI.SepticProfile.FixedHighJet.update_194 line 326
  102. theorem OAI.SepticProfile.FixedHighJet.update_210 line 328
  103. theorem OAI.SepticProfile.FixedHighJet.update_data line 330
  104. theorem OAI.SepticProfile.FixedHighJet.nonzero_2 line 358
  105. theorem OAI.SepticProfile.FixedHighJet.nonzero_18 line 360
  106. theorem OAI.SepticProfile.FixedHighJet.nonzero_34 line 362
  107. theorem OAI.SepticProfile.FixedHighJet.nonzero_50 line 364
  108. theorem OAI.SepticProfile.FixedHighJet.nonzero_66 line 366
  109. theorem OAI.SepticProfile.FixedHighJet.nonzero_82 line 368
  110. theorem OAI.SepticProfile.FixedHighJet.nonzero_98 line 370
  111. theorem OAI.SepticProfile.FixedHighJet.nonzero_114 line 372
  112. theorem OAI.SepticProfile.FixedHighJet.nonzero_130 line 374
  113. theorem OAI.SepticProfile.FixedHighJet.nonzero_146 line 376
  114. theorem OAI.SepticProfile.FixedHighJet.nonzero_162 line 378
  115. theorem OAI.SepticProfile.FixedHighJet.nonzero_178 line 380
  116. theorem OAI.SepticProfile.FixedHighJet.nonzero_194 line 382
  117. theorem OAI.SepticProfile.FixedHighJet.nonzero_210 line 384
  118. theorem OAI.SepticProfile.FixedHighJet.nonzero_data line 386
  119. theorem OAI.SepticProfile.FixedHighJet.valid line 414
  120. theorem OAI.SepticProfile.FixedHighJet.coefficients_enclosed line 427