PoissonBallEnergy.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Caccioppoli control of Poisson energy on an interior ball

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_ball_energy line 16

Source documentation

The actual square gradient has its expected amplitude/source bound.

theorem NoncollapsedRCD.poisson_ball_energy {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) (p : X) (r : ℝ) (hr : 0 < r)
    (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ) (A : ℝ≥0)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (4*r)) f c)
    (hA : ∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp (hausdorff n X) hX.quadratic f x| ≤ A) :
    (∫ x in ball p r, localGamma (hausdorff n X) hX.quadratic f f x ∂hausdorff n X) ≤
      (2*|c| *A+4*(A:ℝ)^2*(r⁻¹)^2)*(hausdorff n X).real (ball p (4*r)) := by
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.localGamma