OAI/MathematicalPhysics/ContinuumCoulomb/Reduction/UniformReciprocal.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A uniform four-derivative reciprocal estimate away from zero, used only for the positive density in the Moser field.

  1. theorem OAI.ContinuumCoulomb.reciprocal_derivatives_bounded line 12
  2. theorem OAI.ContinuumCoulomb.uniform_reciprocal_four_bound line 45

    Source documentation

    The constant depends on the density floor and on the four-derivative bound, not on the support or the number of wells.

    theorem uniform_reciprocal_four_bound {rho B : ℝ} (hrho : 0 < rho) :
    ∃ C : ℝ, 0 < C ∧ ∀ f : ℝ × Position → ℝ, ContDiff ℝ 4 f →
      ∀ x, f x ∈ Set.Icc (rho/2) (3*rho/2) →
      (∀ j ≤ 4, ‖iteratedFDeriv ℝ j f x‖ ≤ B) →
      ∀ k ≤ 4, ‖iteratedFDeriv ℝ k (fun y => (f y)⁻¹) x‖ ≤ C := by
…

    Mentions: OAI.ContinuumCoulomb.Position