OAI/Geometry/EinsteinFour/ActualJacobiODEExistence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Global solutions of a bounded continuous linear equation, constructed from Picard–Lindelöf on overlapping intervals. The uniform local time depends on the operator bound, while the Picard ball may depend on the initial value.

  1. def OAI.PositiveEinsteinFour.Jacobi.LinearCurveOn line 18
  2. theorem OAI.PositiveEinsteinFour.Jacobi.linear_uniform_local_solution line 21
  3. theorem OAI.PositiveEinsteinFour.Jacobi.LinearCurveOn.mono line 56
  4. theorem OAI.PositiveEinsteinFour.Jacobi.linear_curve_eqOn_interval line 61
  5. theorem OAI.PositiveEinsteinFour.Jacobi.linear_curve_piecewise line 74
  6. theorem OAI.PositiveEinsteinFour.Jacobi.extend_linear_curve_interval line 107
  7. theorem OAI.PositiveEinsteinFour.Jacobi.exists_global_linear_solution line 149

    Source documentation

    A continuous globally bounded operator coefficient admits a genuine global linear solution through every initial value.

    theorem exists_global_linear_solution (A : ℝ → E →L[ℝ] E) (hA : Continuous A)
    (K : ℝ≥0) (hK : ∀ t, ‖A t‖ ≤ K) (x : E) :
    ∃ Γ : ℝ → E, Γ 0 = x ∧ ∀ t, HasDerivAt Γ (A t (Γ t)) t := by
…