FlowDifferentiability.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

First variation of a real autonomous ODE. These elementary Taylor, Grönwall and endpoint lemmas are shared by horizontal-frame and cotangent Hamiltonian flows.

theorem OAI.PositiveEinsteinFour.FlowCalculus.taylor_remainder_le line 20
theorem OAI.PositiveEinsteinFour.FlowCalculus.variation_remainder_derivative line 49
theorem OAI.PositiveEinsteinFour.FlowCalculus.variation_quadratic_error line 66
theorem OAI.PositiveEinsteinFour.FlowCalculus.gronwall_quadratic line 112
Source documentation
The Grönwall remainder is uniformly quadratic in the initial increment.
```
theorem gronwall_quadratic (K A T : ℝ) (h : E) :
    gronwallBound 0 K (A * ‖h‖ ^ 2) T = gronwallBound 0 K A T * ‖h‖ ^ 2 := by
…
```
theorem OAI.PositiveEinsteinFour.FlowCalculus.hasFDerivAt_of_quadratic_error line 123
Source documentation
A quadratic remainder for a local endpoint map proves the claimed Fréchet derivative; no differentiability premise on that map is needed.
```
theorem hasFDerivAt_of_quadratic_error
    (F : E → E) (p : E)
    (V : E →L[ℝ] E) (C : ℝ)
    (hb : ∀ᶠ q in 𝓝 p, ‖F q - F p - V (q - p)‖ ≤ C * ‖q - p‖ ^ 2) :
    HasFDerivAt F V p := by
…
```

theorem OAI.PositiveEinsteinFour.FlowCalculus.hasFDerivAt_flow_endpoint line 139

Source documentation

The endpoint map of a local family of genuine solutions has the variational derivative. All quantitative hypotheses concern the local vector field and its containing convex neighborhood.

theorem hasFDerivAt_flow_endpoint (f : E → E) (α : E × ℝ → E)
    (p : E) (S B : Set E) (hS : S ∈ 𝓝 p)
    (hB : Convex ℝ B) (hf : ∀ z ∈ B, DifferentiableAt ℝ f z)
    (K L : ℝ≥0) (T : ℝ) (hT : 0 ≤ T)
    (hK : LipschitzOnWith K (f) B)
    (hL : LipschitzOnWith L (fderiv ℝ (f)) B)
    (hD : ∀ z ∈ B, ‖fderiv ℝ (f) z‖ ≤ K)
    (hα0 : ∀ q ∈ S, α (q, 0) = q)
    (hα : ∀ q ∈ S, ∀ t ∈ Icc 0 T,
      HasDerivAt (fun s => α (q, s)) (f (α (q, t))) t)
    (hαB : ∀ q ∈ S, ∀ t ∈ Icc 0 T, α (q, t) ∈ B)
    (V : ℝ → E →L[ℝ] E)
…