OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/MoserChargeBounds.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform derivative control of the actual Poisson charge, from exactly the six derivatives of the manufactured scalar potential.

  1. theorem OAI.ContinuumCoulomb.dirPartial_iterated_norm_bound line 14
  2. theorem OAI.ContinuumCoulomb.axis_second_partial_bound line 24
  3. theorem OAI.ContinuumCoulomb.manufacturedCharge_derivative_bound line 42

    Source documentation

    All derivatives of the manufactured charge through order four have a bound depending only on the scalar field's order-six bound.

    theorem manufacturedCharge_derivative_bound (V : Position → ℝ) (hV : ContDiff ℝ 6 V)
    {B : ℝ} (_hB : 0 ≤ B)
    (hbound : ∀ k ≤ 6, ∀ x, ‖iteratedFDeriv ℝ k V x‖ ≤ B)
    {k : ℕ} (hk : k ≤ 4) (x : Position) :
    ‖iteratedFDeriv ℝ k (manufacturedCharge V) x‖ ≤ 3*B/(4*Real.pi) := by
…

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