OAI/Geometry/EinsteinFour/FlowGermUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform local uniqueness for parameterized actual ODE solutions. This identifies the existing flow with its variational lifts on a whole neighborhood, as required for higher derivatives in the initial data.

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