OAI/MathematicalPhysics/SheetFlows/Circuits.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows circuits.

  1. def OAI.Solenoidal.flatMono line 14
  2. theorem OAI.Solenoidal.flatJet_sub line 16
  3. theorem OAI.Solenoidal.flatJet_C_mul line 20
  4. theorem OAI.Solenoidal.flatMono_deriv line 25
  5. theorem OAI.Solenoidal.flatMono_bound line 39
  6. abbrev OAI.Solenoidal.Atom line 43
  7. def OAI.Solenoidal.Atom.argument line 47
  8. def OAI.Solenoidal.Atom.profile line 49
  9. def OAI.Solenoidal.Atom.eval line 52
  10. def OAI.Solenoidal.Atom.approx line 55
  11. def OAI.Solenoidal.Atom.bound line 60
  12. theorem OAI.Solenoidal.Atom.profile_smooth line 64
  13. theorem OAI.Solenoidal.Atom.smooth line 72
  14. theorem OAI.Solenoidal.Atom.bound_nonneg line 76
  15. theorem OAI.Solenoidal.Atom.bound_correct line 82
  16. abbrev OAI.Solenoidal.Circuit line 97
  17. def OAI.Solenoidal.Circuit.data line 103
  18. def OAI.Solenoidal.Circuit.const line 106
  19. def OAI.Solenoidal.Circuit.atom line 107
  20. abbrev OAI.Solenoidal.Circuit.add line 108
  21. abbrev OAI.Solenoidal.Circuit.mul line 109
  22. def OAI.Solenoidal.Circuit.sub line 111
  23. def OAI.Solenoidal.Circuit.eval line 113
  24. def OAI.Solenoidal.Circuit.approx line 120
  25. def OAI.Solenoidal.Circuit.bound line 127
  26. theorem OAI.Solenoidal.Circuit.data_ofNat_encode line 134
  27. theorem OAI.Solenoidal.Circuit.eval_const line 138
  28. theorem OAI.Solenoidal.Circuit.eval_atom line 140
  29. theorem OAI.Solenoidal.Circuit.eval_sub line 142
  30. theorem OAI.Solenoidal.Circuit.smooth line 145
  31. theorem OAI.Solenoidal.Circuit.bound_nonneg line 153
  32. theorem OAI.Solenoidal.Circuit.bound_correct line 161
  33. def OAI.Solenoidal.Circuit.ofRational line 174
  34. theorem OAI.Solenoidal.Circuit.coordinate_ofRational line 177
  35. theorem OAI.Solenoidal.Circuit.flatten_ofRational line 180
  36. theorem OAI.Solenoidal.Circuit.atom_approximates line 183
  37. theorem OAI.Solenoidal.Circuit.approximates line 196
  38. def OAI.Solenoidal.Atom.profileDerivative line 214
  39. theorem OAI.Solenoidal.Atom.profile_deriv line 219
  40. def OAI.Solenoidal.Atom.withKind line 228
  41. def OAI.Solenoidal.Atom.reflect line 229
  42. def OAI.Solenoidal.Circuit.atomDiff line 235
  43. theorem OAI.Solenoidal.Circuit.eval_add line 244
  44. theorem OAI.Solenoidal.Circuit.eval_mul line 246
  45. theorem OAI.Solenoidal.Circuit.atomDiff_eval line 249
  46. def OAI.Solenoidal.Circuit.diff line 276
  47. theorem OAI.Solenoidal.Circuit.diff_correct line 283
  48. def OAI.Solenoidal.Circuit.mixed line 310
  49. def OAI.Solenoidal.Circuit.field line 314
  50. theorem OAI.Solenoidal.Circuit.field_smooth line 316
  51. theorem OAI.Solenoidal.Circuit.mixed_field line 319
  52. def OAI.Solenoidal.Circuit.suml line 330
  53. theorem OAI.Solenoidal.Circuit.eval_suml line 334
  54. def OAI.Solenoidal.Circuit.sum line 340
  55. theorem OAI.Solenoidal.Circuit.eval_sum line 343
  56. def OAI.Solenoidal.Circuit.polynomial line 346
  57. theorem OAI.Solenoidal.Circuit.eval_polynomial line 349
  58. def OAI.Solenoidal.JetExpr.compile line 364
  59. theorem OAI.Solenoidal.JetExpr.compile_correct line 373
  60. def OAI.Solenoidal.BoxExpr.compile line 390
  61. theorem OAI.Solenoidal.BoxExpr.compile_correct line 396