OAI/Geometry/RCD/Coordinates/BoundedRegularPrescribedHessian.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Mixed Hessian domination by a prescribed full Bochner measure

Localizing the potential and directions preserves the original measure, so quantitative mass estimates survive the compact-core reduction.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.bounded_regular_prescribed_hessian line 21