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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The actual elementary trajectories used by the finite processor. Each curve is polynomial in one smooth clock and satisfies the cutoff equation whenever it lies in its assigned filled rectangle.

  1. def OAI.ForcedComputation.PlanarHamiltonian.Primitive.path line 15
  2. def OAI.ForcedComputation.PlanarHamiltonian.Primitive.endpoint line 21
  3. theorem OAI.ForcedComputation.PlanarHamiltonian.Primitive.path_hasDerivAt line 23
  4. theorem OAI.ForcedComputation.PlanarHamiltonian.Primitive.path_smooth line 35
  5. theorem OAI.ForcedComputation.PlanarHamiltonian.Primitive.path_start line 43
  6. theorem OAI.ForcedComputation.PlanarHamiltonian.Primitive.path_end line 48
  7. def OAI.ForcedComputation.PlanarHamiltonian.Pulse.curve line 53
  8. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.curve_smooth line 56
  9. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.curve_ode line 59
  10. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.curve_before line 66
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.curve_after line 71