OAI/MathematicalPhysics/DefocusingNLS/Profile/RadialHardyInequality.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A Hardy inequality with the exact radial weight, uniform for small powers.

  1. theorem OAI.DefocusingNLS.radialHardyFlux_deriv_continuous line 13
  2. theorem OAI.DefocusingNLS.radialHardyInequality line 28

    Source documentation

    The twelve-dimensional radial Hardy estimate, with an explicit uniform constant. The boundary condition is exactly the one used for cutoff tests.

    theorem radialHardyInequality (a R : ℝ) (ha : 0 ≤ a) (ha1 : a ≤ 1/2)
    (hR : 0 ≤ R) (f : ℝ → ℝ) (hf : ContDiff ℝ 1 f) (hfR : f R=0) :
    16*(∫ r in (0 : ℝ)..R, r^9*radialHardyWeight a r*(f r)^2) ≤
      ∫ r in (0 : ℝ)..R, r^11*radialHardyWeight a r*(deriv f r)^2 := by
…

    Mentions: OAI.DefocusingNLS.radialHardyWeight