HarmonicBochnerFromHessian.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Harmonic Bochner calculus from the Poisson Hessian input

The n-dimensional harmonic span embeds isometrically into the existing (n+2)-dimensional Poisson span. Restricting the full positive measure to that subspace proves the harmonic Bochner input, including its original extension bound, without a separate assumption.

def OAI.RegularPointCoordinates.harmonicCoordinateInclusion line 20
def OAI.RegularPointCoordinates.harmonicMeasureRestriction line 32
theorem OAI.RegularPointCoordinates.LocalPoissonHessianInput.harmonicBochnerInput line 45
Source documentation
The separate harmonic Bochner premise is a consequence of the already required Poisson Hessian specialization of Gigli--Han.
```
theorem LocalPoissonHessianInput.harmonicBochnerInput {K : ℝ} {n : ℕ}
    {hX : NoncollapsedRCD K n X} (h : LocalPoissonHessianInput hX) :
    LocalHarmonicBochnerInput hX := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.LocalPoissonHessianInput, OAI.RegularPointCoordinates.LocalHarmonicBochnerInput