OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/FlowLocalDomain.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Local C⁴ flows on the open domain of the autonomous lift. A compactly supported extension is used only in a neighborhood of the initial point.

  1. theorem OAI.ContinuumCoulomb.flow_c4_extension_near line 13
  2. theorem OAI.ContinuumCoulomb.flow_c4_local_on line 40