OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/NormalizedBranchTrace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The eight actual local trajectories, translated to the fixed initial particle chart. Their derivatives are derivatives of the full processor, not merely of isolated polynomial fields.

  1. theorem OAI.ForcedComputation.Recorder.Planar.mem_translated_collar line 15
  2. def OAI.ForcedComputation.Recorder.Planar.branchCurve line 36
  3. theorem OAI.ForcedComputation.Recorder.Planar.branchCurve_start line 41
  4. theorem OAI.ForcedComputation.Recorder.Planar.branchCurve_endpoint line 47
  5. theorem OAI.ForcedComputation.Recorder.Planar.branchCurve_finish line 55
  6. def OAI.ForcedComputation.Recorder.Planar.normalizedAnchors line 65
  7. def OAI.ForcedComputation.Recorder.Planar.normalizedCurve line 71
  8. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_start line 77
  9. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_finish line 87
  10. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_smooth line 97
  11. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_mem line 102
  12. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_chart line 109
  13. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_ode line 129