OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/FlowGlobalExistence.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Complete flows of bounded Lipschitz fields, obtained from the existing Picard theorem on finite intervals and uniqueness on overlaps.

  1. theorem OAI.ContinuumCoulomb.flow_interval_coherence line 13
  2. theorem OAI.ContinuumCoulomb.flow_bounded_global_exists line 39