OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/MoserRegularity.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite C⁶ regularity of the manufactured well gives the C⁴ transport field required by the unit-charge cubature. No C∞ assumption is added.

  1. theorem OAI.ContinuumCoulomb.manufacturedCharge_C4 line 14
  2. def OAI.ContinuumCoulomb.moserDomain line 28
  3. theorem OAI.ContinuumCoulomb.homotopyDensity_joint_C4 line 31
  4. theorem OAI.ContinuumCoulomb.moserDomain_isOpen line 35
  5. theorem OAI.ContinuumCoulomb.moserVelocity_joint_C4 line 39
  6. theorem OAI.ContinuumCoulomb.moserDomain_contains_time_slab line 53
  7. theorem OAI.ContinuumCoulomb.moserVelocity_C4 line 61

    Source documentation

    Actual spatial C⁴ regularity at each transport time, sufficient for four differentiated flow equations and fourth-order cubature composition.

    theorem moserVelocity_C4 {rho : ℝ} (hrho : 0 < rho)
    (V : Position → ℝ) (hV : ContDiff ℝ 6 V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho / 2)
    {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : ContDiff ℝ 4 (moserVelocity rho V t) := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.manufacturedCharge, OAI.ContinuumCoulomb.moserVelocity