PoissonHessianInput.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The Hessian input for the finite Poisson span

Gigli (2018), equation (3.1.10) and Theorem 3.3.8, give the local Hessian pairing and its Bochner bound. Han (2018), Proposition 3.2 and Theorem 3.3, give the top-dimensional trace identity and the lower-dimensional trace defect. Completing the trace-defect square and applying integral Cauchy--Schwarz gives the displayed bound on the integrated pairing on every concentric inner ball, using the same canonical measure. This localization is needed to apply cutoff mass bounds before constructing the harmonic correction. The tensor pairing is restricted to the finite harmonic and Poisson span.

def OAI.RegularPointCoordinates.LocalPoissonHessianInput line 32
Source documentation
Local second-order calculus for n harmonic coordinates and two constant-Laplacian replacements. The same full Bochner measure occurs in the energy equation, the positivity assertion and the Hessian bound.
```
def LocalPoissonHessianInput {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X) : Prop :=
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD
theorem OAI.RegularPointCoordinates.LocalPoissonHessianInput.constantLaplacianBochnerInput line 58
Source documentation
The second-order specialization includes the earlier scalar constant-Laplacian Bochner input.
```
theorem LocalPoissonHessianInput.constantLaplacianBochnerInput
    {K : ℝ} {n : ℕ} {hX : NoncollapsedRCD K n X} (h : LocalPoissonHessianInput hX) :
    LocalConstantLaplacianBochnerInput hX := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalConstantLaplacianBochnerInput

theorem OAI.RegularPointCoordinates.LocalHessianPairing.harmonic_correction_of_shifted_mass line 70

Source documentation

The exact shift correction is the full positive mass on the interior set. This removes the raw Hessian bound from the harmonic-correction step.

theorem LocalHessianPairing.harmonic_correction_of_shifted_mass
    {Ω : Set X} (hΩ : MeasurableSet Ω) [IsFiniteMeasure (μ.restrict Ω)]
    (U : E →L[ℝ] SobolevSpace μ hQ) (M : PositiveBilinearMeasure X E)
    (ell : E →ₗ[ℝ] ℝ) (n : ℝ) (hshift : ShiftedBochnerLowerBound M (μ.restrict Ω) ell n)
    (v w : E) (G : LocalHessianPairing μ hQ Ω (U v) (U w))
    (hf : IsConstantLaplacianOn μ hQ Ω (U v) (ell v))
    (ha : IsSobolevHarmonicOn μ hQ Ω (U w))
    (b L P : ℝ) (hP : 0 ≤ P)
    (hpoincare : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      ‖SobolevSpace.toLp μ hQ φ.val‖ ^ 2 ≤ P * energyForm μ hQ φ.val φ.val)
    (hbound : ∀ φ : SobolevSpace.dirichlet μ hQ Ω,
      (G.hessian φ - b * energyForm μ hQ (U w) φ.val) ^ 2 ≤
…

Mentions: OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.ShiftedBochnerLowerBound, OAI.RegularPointCoordinates.LocalHessianPairing, OAI.RegularPointCoordinates.IsConstantLaplacianOn, OAI.RegularPointCoordinates.IsSobolevHarmonicOn, OAI.RegularPointCoordinates.SobolevSpace.dirichlet, OAI.RegularPointCoordinates.SobolevSpace.toLp, OAI.RegularPointCoordinates.energyForm