PlanarVariations.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The variational equations used for the planar quantitative estimates. The regularity input is the finite-dimensional smooth-dependence theorem: Teschl, Ordinary Differential Equations and Dynamical Systems (2012), Theorem 2.10, equations (2.49)--(2.51). The quantitative estimates follow from these equations by Gronwall inequalities.

structure OAI.ForcedComputation.PlanarVariations line 19
Source documentation
The first two variational equations for a transition map. The second time argument is elapsed time; the first is its initial phase.
```
structure PlanarVariations (V : ℝ → Plane → Plane)
    (Ψ : ℝ → ℝ → Plane → Plane) : Prop where
…
```
theorem OAI.ForcedComputation.planar_first_variation_vector line 32
theorem OAI.ForcedComputation.planar_first_variation_operator line 46
theorem OAI.ForcedComputation.planar_second_variation_vector line 55
theorem OAI.ForcedComputation.planar_second_variation_operator line 103
def OAI.ForcedComputation.planarFlowBound line 124
theorem OAI.ForcedComputation.planar_quantitative_variations line 126