OAI/MathematicalPhysics/RapidForcing/Model.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.RapidForcing.Space line 9
  2. abbrev OAI.RapidForcing.Field line 10
  3. abbrev OAI.RapidForcing.MultiIndex line 11
  4. theorem OAI.RapidForcing.twoAtLeastTwo line 13
  5. theorem OAI.RapidForcing.neZeroThree line 15
  6. def OAI.RapidForcing.vec line 17
  7. def OAI.RapidForcing.basis line 21
  8. def OAI.RapidForcing.K line 23
  9. def OAI.RapidForcing.spatialD line 29
  10. def OAI.RapidForcing.timeD line 33
  11. def OAI.RapidForcing.spatialMulti line 37
  12. def OAI.RapidForcing.mixedD line 42
  13. def OAI.RapidForcing.order line 46
  14. def OAI.RapidForcing.Smooth line 48
  15. def OAI.RapidForcing.Supported line 51
  16. def OAI.RapidForcing.Rapid line 54
  17. def OAI.RapidForcing.RapidSpaceTime line 59
  18. def OAI.RapidForcing.advection line 65
  19. def OAI.RapidForcing.laplace line 68
  20. def OAI.RapidForcing.divergence line 71
  21. def OAI.RapidForcing.gradient line 74
  22. def OAI.RapidForcing.residual line 77
  23. def OAI.RapidForcing.NavierStokes line 80
  24. def OAI.RapidForcing.Classical line 87
  25. def OAI.RapidForcing.L2ContinuousOn line 100
  26. def OAI.RapidForcing.L2C1On line 107
  27. def OAI.RapidForcing.EnergyRegularity line 115
  28. def OAI.RapidForcing.EnergyClass line 121
  29. def OAI.RapidForcing.EnergyCompetitor line 126
  30. def OAI.RapidForcing.UniqueEnergySolution line 130
  31. def OAI.RapidForcing.TrajectoryOn line 136
  32. def OAI.RapidForcing.MaterialFlow line 140
  33. abbrev OAI.RapidForcing.Move line 147
  34. structure OAI.RapidForcing.Machine line 149
  35. abbrev OAI.RapidForcing.Machine.Input line 159
  36. def OAI.RapidForcing.Machine.blank line 161
  37. def OAI.RapidForcing.Machine.description line 163
  38. def OAI.RapidForcing.Machine.inputDescription line 169
  39. structure OAI.RapidForcing.Machine.Config line 172
  40. def OAI.RapidForcing.Machine.initialConfig line 177
  41. def OAI.RapidForcing.Machine.nextConfig line 181
  42. def OAI.RapidForcing.Machine.run line 190
  43. def OAI.RapidForcing.Machine.Halts line 193
  44. structure OAI.RapidForcing.ScaleData line 198
  45. def OAI.RapidForcing.ScaleData.A line 205
  46. def OAI.RapidForcing.ScaleData.S line 206
  47. def OAI.RapidForcing.ScaleData.P line 207
  48. def OAI.RapidForcing.ScaleData.L line 208
  49. def OAI.RapidForcing.ScaleData.capacity line 209
  50. def OAI.RapidForcing.ScaleData.C line 210
  51. def OAI.RapidForcing.ScaleData.s line 211
  52. def OAI.RapidForcing.ScaleData.D line 212
  53. def OAI.RapidForcing.ScaleData.δ line 213
  54. def OAI.RapidForcing.ScaleData.b line 216
  55. def OAI.RapidForcing.Machine.scaleData line 222
  56. def OAI.RapidForcing.Machine.instruction line 225
  57. def OAI.RapidForcing.Machine.terminalDigit line 235
  58. def OAI.RapidForcing.Machine.nextDigit line 238
  59. def OAI.RapidForcing.Machine.initialDigit line 249
  60. def OAI.RapidForcing.θ line 256
  61. def OAI.RapidForcing.ζ line 260
  62. def OAI.RapidForcing.cross line 264
  63. def OAI.RapidForcing.curl line 268
  64. def OAI.RapidForcing.movingCurl line 274
  65. def OAI.RapidForcing.addressCenter line 279
  66. def OAI.RapidForcing.addressDisplacement line 282
  67. def OAI.RapidForcing.addressPath line 287
  68. def OAI.RapidForcing.addressedVelocity line 290
  69. def OAI.RapidForcing.addressedForce line 300
  70. abbrev OAI.RapidForcing.Program line 303
  71. abbrev OAI.RapidForcing.RationalVector line 304
  72. abbrev OAI.RapidForcing.RationalPoint line 305
  73. def OAI.RapidForcing.rationalVector line 307
  74. def OAI.RapidForcing.accuracy line 310
  75. def OAI.RapidForcing.NamesReal line 314
  76. def OAI.RapidForcing.ComputableReal line 317
  77. def OAI.RapidForcing.NamesPoint line 319
  78. def OAI.RapidForcing.evalQuery line 323
  79. def OAI.RapidForcing.boundQuery line 327
  80. def OAI.RapidForcing.EvaluatesMixed line 331
  81. def OAI.RapidForcing.BoundsMixed line 337
  82. def OAI.RapidForcing.ForceProgram line 343