OAI/Geometry/RCD/Coordinates/BoundedRegularMixedHessianDensity.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

One fixed local Hessian density for two bounded regular directions

The finite positive measure is chosen using only the fixed potential. Directions need an L² Laplacian; no derivative of their source is used.

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