OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/FlowSpatialRegularity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial C⁴ regularity on the entire closed transport interval, derived from local C⁴ dependence and uniqueness along each compact trajectory.

  1. theorem OAI.ContinuumCoulomb.flow_lifted_local_model line 14
  2. theorem OAI.ContinuumCoulomb.flow_lifted_interval_C4 line 54
  3. theorem OAI.ContinuumCoulomb.flow_spatial_C4 line 68