OAI/Geometry/RCD/Sobolev/PoissonHessianFromScalar.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The exact Poisson Hessian input reduced to scalar dimensional Bochner

All measures, representatives and Dirichlet Hessian pairings are constructed from the RCD space. The sole remaining analytic premise in this reduction is the scalar weak finite-dimensional Bochner inequality (Han, Theorem 3.3).

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_hessian_input_of_scalar line 23