OAI/Geometry/RCD/Sobolev/PositiveSourceTest.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The bounded nonlinear test for positive sources

A primitive of (1+|s|)^(-1-alpha) is a global normal contraction and is bounded by 1/alpha on the positive half-line. Its actual Sobolev composition gives the reciprocal-weight energy bound.

  1. def OAI.RegularPointCoordinates.positiveSourceWeight line 21
  2. def OAI.RegularPointCoordinates.positiveSourceTest line 23
  3. theorem OAI.RegularPointCoordinates.positiveSourceWeight_continuous line 25
  4. theorem OAI.RegularPointCoordinates.positiveSourceWeight_bounds line 32
  5. theorem OAI.RegularPointCoordinates.positiveSourceTest_hasDerivAt line 38
  6. theorem OAI.RegularPointCoordinates.positiveSourceTest_zero line 45
  7. theorem OAI.RegularPointCoordinates.positiveSourceTest_lipschitz line 48
  8. theorem OAI.RegularPointCoordinates.positiveSourceTest_formula line 58
  9. theorem OAI.RegularPointCoordinates.positiveSourceTest_bounds line 83
  10. theorem OAI.RegularPointCoordinates.positive_source_weighted_energy line 98

    Source documentation

    The nonlinear test gives the weighted square-gradient bound, with linear dependence on the mass P of the source functional.

    theorem positive_source_weighted_energy (Ω : Set X)
    (H : SobolevSpace.dirichlet μ hQ Ω)
    (hH : ∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ H.val x)
    (P : ℝ)
    (hsource : ∀ φ : SobolevSpace.dirichlet μ hQ Ω, ∀ s : ℝ, 0 ≤ s →
      (∀ᵐ x ∂μ, 0 ≤ SobolevSpace.toLp μ hQ φ.val x ∧ SobolevSpace.toLp μ hQ φ.val x ≤ s) →
      energyForm μ hQ H.val φ.val ≤ P * s)
    {alpha : ℝ} (ha : 0 < alpha) :
    Integrable (fun x => (SobolevSpace.minimalSlope μ hQ H.val x) ^ 2 /
      (1 + SobolevSpace.toLp μ hQ H.val x) ^ (1 + alpha)) μ ∧
      (∫ x, (SobolevSpace.minimalSlope μ hQ H.val x) ^ 2 /
        (1 + SobolevSpace.toLp μ hQ H.val x) ^ (1 + alpha) ∂μ) ≤ P / alpha := by
…

    Mentions: OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm, OAI.RegularPointCoordinates.SobolevSpace.minimalSlope