OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/MoserBounds.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform boundedness and spatial Lipschitz regularity of the actual Moser field on the complete transport interval. Compact support is used only to obtain finite constants; quantitative cubature constants are a separate step.

  1. theorem OAI.ContinuumCoulomb.moserVelocity_joint_tsupport_subset line 14
  2. theorem OAI.ContinuumCoulomb.moserVelocity_uniform_bounds line 24

    Source documentation

    Bounds are uniform over every position and all times from zero to one.

    theorem moserVelocity_uniform_bounds {rho : ℝ} (hrho : 0 < rho)
    (V : Position → ℝ) (hV : ContDiff ℝ 6 V) (hc : HasCompactSupport V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho / 2) :
    ∃ L K : ℝ≥0, (∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ x, ‖moserVelocity rho V t x‖ ≤ L) ∧
      (∀ t ∈ Set.Icc (0 : ℝ) 1, LipschitzWith K (moserVelocity rho V t)) ∧
      (∀ x, ContinuousOn (fun t => moserVelocity rho V t x) (Set.Icc (0 : ℝ) 1)) := by
…

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