PoissonEnergySubsolution.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The actual Poisson energy as a weak subsolution

theorem OAI.RegularPointCoordinates.LocalPoissonHessianInput.energy_subsolution line 18

Source documentation

The one-dimensional span of a constant-source solution is enough for the finite-span Bochner input.

theorem LocalPoissonHessianInput.energy_subsolution {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} (hess : LocalPoissonHessianInput hX)
    (κ : ℝ) (hκ : 0 ≤ κ) (hK : -κ ≤ K) (p : X) (r : ℝ) (hr : 0 < r)
    (f : SobolevSpace (hausdorff n X) hX.quadratic) (c : ℝ) (L : ℝ≥0)
    (hf : IsConstantLaplacianOn (hausdorff n X) hX.quadratic (ball p (8*r)) f c)
    (hgrad : ∀ᵐ x ∂(hausdorff n X).restrict (ball p (8*r)),
      localGamma (hausdorff n X) hX.quadratic f f x ≤ (L:ℝ)^2) :
    ∃ (e : SobolevSpace (hausdorff n X) hX.quadratic) (B : ℝ), 0 ≤ B ∧
      SobolevSpace.toLp (hausdorff n X) hX.quadratic e =ᵐ[(hausdorff n X).restrict (ball p (2*r))]
        localGamma (hausdorff n X) hX.quadratic f f ∧
      (∀ᵐ x ∂hausdorff n X, |SobolevSpace.toLp (hausdorff n X) hX.quadratic e x| ≤ B) ∧
      IsWeakSubsolutionOn (hausdorff n X) hX.quadratic (ball p (2*r)) e (2*κ) := by
…

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