OAI/MathematicalPhysics/Transonic/Certificates/HighMinusCertificate.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.HighMinusBarrierTransfer.S line 12
  2. def OAI.SepticProfile.HighMinusBarrierTransfer.deltaBox line 13
  3. theorem OAI.SepticProfile.HighMinusBarrierTransfer.scale_eq line 14
  4. theorem OAI.SepticProfile.HighMinusBarrierTransfer.S_pos line 15
  5. theorem OAI.SepticProfile.HighMinusBarrierTransfer.u_zero line 16
  6. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_1 line 17
  7. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_21 line 19
  8. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_41 line 21
  9. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_61 line 23
  10. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_81 line 25
  11. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_101 line 27
  12. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_121 line 29
  13. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_141 line 31
  14. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_161 line 33
  15. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_181 line 35
  16. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u_201 line 37
  17. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_u line 39
  18. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_0 line 61
  19. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_24 line 63
  20. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_48 line 65
  21. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_72 line 67
  22. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_96 line 69
  23. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_120 line 71
  24. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_144 line 73
  25. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_168 line 75
  26. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_192 line 77
  27. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_216 line 79
  28. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_240 line 81
  29. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_264 line 83
  30. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_288 line 85
  31. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_312 line 87
  32. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_336 line 89
  33. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_360 line 91
  34. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_384 line 93
  35. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_408 line 95
  36. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_432 line 97
  37. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_456 line 99
  38. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_480 line 101
  39. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_504 line 103
  40. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_528 line 105
  41. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_552 line 107
  42. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_576 line 109
  43. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_600 line 111
  44. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_624 line 113
  45. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_648 line 115
  46. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_672 line 117
  47. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_696 line 119
  48. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r_720 line 121
  49. theorem OAI.SepticProfile.HighMinusBarrierTransfer.data_r line 123
  50. lemma OAI.SepticProfile.HighMinusBarrierTransfer.holds_delta line 185
  51. theorem OAI.SepticProfile.HighMinusBarrierTransfer.barrier_coefficients_enclosed line 189
  52. def OAI.SepticProfile.HighMinusRange.b line 221
  53. theorem OAI.SepticProfile.HighMinusRange.Q_pos line 222
  54. theorem OAI.SepticProfile.HighMinusRange.middle line 223
  55. theorem OAI.SepticProfile.HighMinusRange.all_bound line 225
  56. theorem OAI.SepticProfile.HighMinusRange.tail_bound line 226
  57. theorem OAI.SepticProfile.HighMinusRange.head_bound line 227
  58. theorem OAI.SepticProfile.HighMinusRange.velocity_range line 229