OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarNeighborhoodMotion.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Exact pulse equations on positive neighborhoods of the source boxes.

  1. theorem OAI.ForcedComputation.PlanarHamiltonian.mem_translatedPlateau line 14
  2. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated_velocity_plateau line 30
  3. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.translated_hasDerivAt_plateau line 42
  4. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.plateau_in_unit line 50
  5. theorem OAI.ForcedComputation.Recorder.Planar.branchCurve_dist_lt_collar line 65
  6. theorem OAI.ForcedComputation.Recorder.Planar.branchCurve_near_plateau line 78
  7. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_ode_near line 90
  8. theorem OAI.ForcedComputation.Recorder.Planar.translatedPoint_dist line 121
  9. theorem OAI.ForcedComputation.Recorder.Planar.normalizedAnchors_dist_lt_collar line 129
  10. theorem OAI.ForcedComputation.Recorder.Planar.routingCollar_half_lt line 141
  11. theorem OAI.ForcedComputation.Recorder.Planar.near_clock_in_unit line 148
  12. theorem OAI.ForcedComputation.Recorder.Planar.normalizedAnchors_near_unit line 157
  13. theorem OAI.ForcedComputation.Recorder.Planar.normalized_sparseAnchor_zero_near line 167