EuclideanVariations.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The Euclidean specialization of the smooth-dependence equations (Teschl, Theorem 2.10, equations (2.49)--(2.51)). These equations concern the actual Euclidean-coordinate transition; the estimates are proved here.

structure OAI.ForcedComputation.EuclideanVariations line 17
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 EuclideanVariations (V : ℝ → EuclideanPlane → EuclideanPlane)
    (Ψ : ℝ → ℝ → EuclideanPlane → EuclideanPlane) : Prop where
…
```
Mentions: OAI.ForcedComputation.EuclideanPlane
theorem OAI.ForcedComputation.euclidean_first_variation_vector line 30
theorem OAI.ForcedComputation.euclidean_first_variation_operator line 44
theorem OAI.ForcedComputation.euclidean_second_variation_vector line 53
theorem OAI.ForcedComputation.euclidean_second_variation_operator line 101
theorem OAI.ForcedComputation.euclidean_second_variation_sharp_vector line 122
theorem OAI.ForcedComputation.euclidean_second_variation_sharp_operator line 171
def OAI.ForcedComputation.euclideanFlowBound line 188
theorem OAI.ForcedComputation.euclidean_quantitative_variations line 190