OAI/MathematicalPhysics/ContinuumCoulomb/Nuclei/MoserUniformDensity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform joint density bounds for the actual Moser homotopy.

  1. theorem OAI.ContinuumCoulomb.contraction_four_bound line 11
  2. theorem OAI.ContinuumCoulomb.fst_four_bound line 24
  3. theorem OAI.ContinuumCoulomb.homotopyDensity_uniform_derivatives line 41

    Source documentation

    A uniform bound for the four joint derivatives of rho+t*charge.

    theorem homotopyDensity_uniform_derivatives {rho B : ℝ} (hB : 0 ≤ B)
    (V : Position → ℝ) (hV : ContDiff ℝ 6 V)
    (hb : ∀ k ≤ 6, ∀ x, ‖iteratedFDeriv ℝ k V x‖ ≤ B)
    {k : ℕ} (hk : k ≤ 4) {t : ℝ} (ht : t ∈ Set.Icc (0 : ℝ) 1) (x : Position) :
    ‖iteratedFDeriv ℝ k (fun p : ℝ × Position => homotopyDensity rho V p.1 p.2) (t,x)‖ ≤
      |rho|+16*(3*B/(4*Real.pi)) := by
…

    Mentions: OAI.ContinuumCoulomb.Position, OAI.ContinuumCoulomb.homotopyDensity