OAI/Geometry/RCD/Sobolev/PoissonSecondOrderData.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Poisson measure and Hessian data on a finite span

The common full measure and local integrated Hessian pairings follow from the RCD structure. Shifted-square and dimension trace estimates control their mass.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.poisson_second_order_data line 20