OAI/Geometry/EinsteinFour/FlowFiniteRegularity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Finite smooth dependence of actual local ODE solutions on initial data. The induction applies the existing first-variation construction to its own variational field, and uses uniqueness to identify the resulting derivatives.

  1. theorem OAI.PositiveEinsteinFour.FlowCalculus.local_flow_contDiffAt_finite line 19