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

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Global transition maps for the actual planar differential equation. Existence and the inverse identities below use the bounded, globally Lipschitz finite expression, with no smooth-dependence assumption.

  1. structure OAI.ForcedComputation.IsPlanarTransition line 15
  2. theorem OAI.ForcedComputation.exists_planarTransition_of_bounds line 22
  3. theorem OAI.ForcedComputation.planarSlice_continuous line 43
  4. theorem OAI.ForcedComputation.planarSlice_bound line 65
  5. theorem OAI.ForcedComputation.exists_planarTransition line 75
  6. theorem OAI.ForcedComputation.IsPlanarTransition.compose line 89
  7. theorem OAI.ForcedComputation.IsPlanarTransition.inverse_left line 98
  8. theorem OAI.ForcedComputation.IsPlanarTransition.inverse_right line 103
  9. theorem OAI.ForcedComputation.IsPlanarTransition.bijective line 109
  10. theorem OAI.ForcedComputation.IsPlanarTransition.perturbation line 114