OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/FlowCompactExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Compact extensions of the autonomous field along a compact trajectory. The extension has a complete C⁴ flow by bounded Picard existence.

  1. theorem OAI.ContinuumCoulomb.flow_c4_compact_extension line 14
  2. theorem OAI.ContinuumCoulomb.flow_compact_global_exists line 48