OAI/Geometry/EinsteinFour/FlowVariationalExistence.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Jointly continuous local solutions of the actual augmented variational ODE. Only a C² vector field and ordinary Picard existence are used.

  1. abbrev OAI.PositiveEinsteinFour.FlowCalculus.VariationSpace line 17
  2. def OAI.PositiveEinsteinFour.FlowCalculus.variationalField line 20
  3. theorem OAI.PositiveEinsteinFour.FlowCalculus.variationalField_contDiffAt line 24
  4. theorem OAI.PositiveEinsteinFour.FlowCalculus.exists_continuous_local_variational_flow line 32

    Source documentation

    A common local interval and continuous parameter dependence for the base trajectory and its first variational linear map.

    theorem exists_continuous_local_variational_flow (f : E → E) (p : E)
    (hf : ContDiffAt ℝ 2 f p) (U : Set E) (hU : U ∈ 𝓝 p) :
    ∃ r > (0 : ℝ), ∃ ε > (0 : ℝ), ∃ β : E × ℝ → VariationSpace E,
      ContinuousOn β (closedBall p r ×ˢ Ioo (-ε) ε) ∧
      ∀ q ∈ closedBall p r,
        β (q, 0) = (q, ContinuousLinearMap.id ℝ E) ∧
        ∀ t ∈ Ioo (-ε) ε, (β (q, t)).1 ∈ U ∧
          HasDerivAt (fun s => β (q, s)) (variationalField f (β (q, t))) t := by
…

    Mentions: OAI.PositiveEinsteinFour.FlowCalculus.VariationSpace, OAI.PositiveEinsteinFour.FlowCalculus.variationalField