OAI/MathematicalPhysics/SheetFlows/EffectiveForcing.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows effective forcing.

  1. def OAI.Solenoidal.Computing.readCode line 15
  2. theorem OAI.Solenoidal.Computing.readCode_pr line 18
  3. theorem OAI.Solenoidal.Computing.readCode_mem line 23
  4. def OAI.Solenoidal.Computing.precision line 29
  5. theorem OAI.Solenoidal.Computing.precision_pr line 32
  6. abbrev OAI.Solenoidal.Computing.BallVector line 38
  7. abbrev OAI.Solenoidal.Computing.RationalPoint line 39
  8. abbrev OAI.Solenoidal.Computing.JetRequest line 40
  9. abbrev OAI.Solenoidal.Computing.BallOracle line 41
  10. def OAI.Solenoidal.Computing.radiusSum line 43
  11. def OAI.Solenoidal.Computing.centers line 45
  12. theorem OAI.Solenoidal.Computing.radiusSum_pr line 47
  13. theorem OAI.Solenoidal.Computing.centers_pr line 50
  14. def OAI.Solenoidal.Computing.ballTest line 54
  15. theorem OAI.Solenoidal.Computing.ballTest_pr line 56
  16. def OAI.Solenoidal.Computing.improve line 59
  17. theorem OAI.Solenoidal.Computing.improve_pr line 63
  18. def OAI.Solenoidal.Computing.evalJets line 75
  19. theorem OAI.Solenoidal.Computing.evalJets_pr line 80
  20. theorem OAI.Solenoidal.Computing.precision_correct line 102
  21. def OAI.Solenoidal.Computing.OracleCorrect line 120
  22. theorem OAI.Solenoidal.Computing.radiusSum_nonneg line 124
  23. theorem OAI.Solenoidal.Computing.centers_error line 127
  24. theorem OAI.Solenoidal.Computing.improve_correct line 134
  25. theorem OAI.Solenoidal.Computing.ofRational_distance line 156
  26. theorem OAI.Solenoidal.Computing.evalJets_correct line 163
  27. theorem OAI.Solenoidal.effective_of_oracle line 194
  28. theorem OAI.Solenoidal.HasCircuit.effective line 204
  29. theorem OAI.Solenoidal.mixedDerivative_add line 220
  30. theorem OAI.Solenoidal.mixedDerivative_smul line 232
  31. theorem OAI.Solenoidal.smooth_linear line 243
  32. theorem OAI.Solenoidal.mixedDerivative_linear line 246
  33. def OAI.Solenoidal.Computing.realBall line 253
  34. theorem OAI.Solenoidal.Computing.realBall_pr line 256
  35. theorem OAI.Solenoidal.Computing.realBall_correct line 260
  36. def OAI.Solenoidal.Computing.linearBalls line 270
  37. theorem OAI.Solenoidal.Computing.linearBalls_pr line 272
  38. def OAI.Solenoidal.Computing.linearOracle line 280
  39. theorem OAI.Solenoidal.Computing.linearOracle_pr line 284
  40. theorem OAI.Solenoidal.Computing.linearOracle_correct line 295
  41. theorem OAI.Solenoidal.NamesReal.rationalBound line 311
  42. def OAI.Solenoidal.linearBound line 323
  43. theorem OAI.Solenoidal.linearBound_pr line 325
  44. theorem OAI.Solenoidal.linearBound_nonneg line 328
  45. theorem OAI.Solenoidal.linearBound_correct line 332
  46. theorem OAI.Solenoidal.effectiveBounds_of_bound line 343
  47. theorem OAI.Solenoidal.HasCircuit.computable_linear line 349
  48. theorem OAI.Solenoidal.HasRationalFormula.directForce_effective line 373