OAI/Geometry/EinsteinFour/ActualJacobiODEDependence.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PositiveEinsteinFour.Jacobi.global_linear_solution_unique line 17
2. theorem OAI.PositiveEinsteinFour.Jacobi.linear_solution_difference_bound line 28

   Source documentation

   A perturbation estimate uses a bound only on the reference solution.

   theorem linear_solution_difference_bound (A B : ℝ → E →L[ℝ] E)
       (γ η : ℝ → E) (K : ℝ≥0) (δ C T : ℝ) (hδ : 0 ≤ δ)
       (hK : ∀ t, ‖A t‖ ≤ K)
       (hγ : ∀ t, HasDerivAt γ (A t (γ t)) t)
       (hη : ∀ t, HasDerivAt η (B t (η t)) t) (h0 : γ 0 = η 0)
       (hAB : ∀ s ∈ Icc 0 T, ‖A s - B s‖ ≤ δ)
       (hC : ∀ s ∈ Icc 0 T, ‖η s‖ ≤ C) :
       ∀ t ∈ Icc 0 T, ‖γ t - η t‖ ≤ gronwallBound 0 K (δ * C) t := by
   …

3. theorem OAI.PositiveEinsteinFour.Jacobi.linear_solution_difference_bound_abs line 57
4. theorem OAI.PositiveEinsteinFour.Jacobi.coefficient_eventually_close line 95
5. theorem OAI.PositiveEinsteinFour.Jacobi.continuous_linear_solution_family line 107

   Source documentation

   Continuity holds for any choice of the global solutions, since their initial values are fixed and the bounded linear equation is unique.

   theorem continuous_linear_solution_family (A : ℝ × P → E →L[ℝ] E)
       (γ : P → ℝ → E) (x : E) (hA : Continuous A) (K : ℝ≥0)
       (hK : ∀ s p, ‖A (s, p)‖ ≤ K) (h0 : ∀ p, γ p 0 = x)
       (hd : ∀ p s, HasDerivAt (γ p) (A (s, p) (γ p s)) s) :
       Continuous (fun p : ℝ × P => γ p.2 p.1) := by
   …