OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/MoserDerivatives.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform finite bounds for all joint field derivatives through order four. These bounds control the explicit velocity in the differentiated flow equations.

  1. theorem OAI.ContinuumCoulomb.moserVelocity_iterated_derivative_bound line 12
  2. theorem OAI.ContinuumCoulomb.moserVelocity_four_derivative_bounds line 39

    Source documentation

    A common finite bound works for all five derivative orders.

    theorem moserVelocity_four_derivative_bounds {rho : ℝ} (hrho : 0 < rho)
    (V : Position → ℝ) (hV : ContDiff ℝ 6 V) (hc : HasCompactSupport V)
    (hbound : ∀ x, |manufacturedCharge V x| ≤ rho / 2) :
    ∃ B : ℝ≥0, ∀ r ≤ 4, ∀ t ∈ Set.Icc (0 : ℝ) 1, ∀ x,
      ‖iteratedFDeriv ℝ r (fun p : ℝ × Position => moserVelocity rho V p.1 p.2) (t, x)‖ ≤ B := by
…

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