OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/CompactDetectorProgram.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

A finite force program relative to an arbitrary effectively supplied planar field. The rational time prefix is selected before any evaluation; all spatial and time derivatives are compiled by the local chain rule.

  1. def OAI.ForcedComputation.VelocityDetector.CompactProgram.components line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.components_smooth line 18
  3. def OAI.ForcedComputation.VelocityDetector.CompactProgram.sum line 26
  4. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.sum_valid line 29
  5. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.sum_value line 34
  6. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.sum_ofFn_valid line 43
  7. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.sum_ofFn_value line 47
  8. abbrev OAI.ForcedComputation.VelocityDetector.CompactProgram.Vector line 52
  9. def OAI.ForcedComputation.VelocityDetector.CompactProgram.Valid line 54
  10. def OAI.ForcedComputation.VelocityDetector.CompactProgram.value line 55
  11. def OAI.ForcedComputation.VelocityDetector.CompactProgram.diffWord line 56
  12. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.value_smooth line 58
  13. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.value_diffWord line 62
  14. def OAI.ForcedComputation.VelocityDetector.CompactProgram.residualCode line 78
  15. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.residualCode_valid line 84
  16. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.residualCode_value line 90
  17. def OAI.ForcedComputation.VelocityDetector.CompactProgram.driftTerm line 103
  18. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.driftTerm_valid line 108
  19. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.driftTerm_value line 112
  20. def OAI.ForcedComputation.VelocityDetector.CompactProgram.driftPrefix line 122
  21. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.driftPrefix_valid line 125
  22. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.driftPrefix_value line 128
  23. def OAI.ForcedComputation.VelocityDetector.CompactProgram.sourcePrefix line 141
  24. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.sourcePrefix_valid line 144
  25. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.sourcePrefix_value line 147
  26. def OAI.ForcedComputation.VelocityDetector.CompactProgram.forcePrefix line 151
  27. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.forcePrefix_valid line 154
  28. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.forcePrefix_value line 157
  29. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.forcePrefix_germ line 168
  30. def OAI.ForcedComputation.VelocityDetector.CompactProgram.evaluateUnitForce line 184
  31. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.evaluateUnitForce_spec line 192
  32. def OAI.ForcedComputation.VelocityDetector.CompactProgram.unitForceBound line 210
  33. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.unitForceBound_nonneg line 214
  34. theorem OAI.ForcedComputation.VelocityDetector.CompactProgram.unitForceBound_spec line 218