FlowJointDifferentiability.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual time derivative and the constructed initial-data derivative give the joint derivative of a local autonomous flow.

theorem OAI.PositiveEinsteinFour.FlowCalculus.hasStrictFDerivAt_joint_flow line 18

theorem OAI.PositiveEinsteinFour.FlowCalculus.exists_jointly_differentiable_local_flow line 44

Source documentation

A C² autonomous field has an actual jointly differentiable local flow. The linear part in the initial state is supplied by the variational ODE.

theorem exists_jointly_differentiable_local_flow [CompleteSpace E]
    (f : E → E) (p : E) (hf : ContDiffAt ℝ 2 f p) :
    ∃ r > (0 : ℝ), ∃ ε > (0 : ℝ),
      ∃ α : E × ℝ → E, ∃ V : E × ℝ → E →L[ℝ] E,
        ContinuousOn α (Metric.ball p r ×ˢ Ioo (-ε) ε) ∧
        ContinuousOn V (Metric.ball p r ×ˢ Ioo (-ε) ε) ∧
        ∀ q ∈ Metric.ball p r,
          α (q, 0) = q ∧ V (q, 0) = ContinuousLinearMap.id ℝ E ∧
          ∀ t ∈ Ioo (-ε) ε,
            HasDerivAt (fun s => α (q, s)) (f (α (q, t))) t ∧
            HasDerivAt (fun s => V (q, s))
              ((fderiv ℝ f (α (q, t))).comp (V (q, t))) t ∧
…