OAI/Geometry/RCD/Coordinates/RegularPairingChoiceBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The shifted estimate on every Dirichlet test

The finite regular-family estimate applies to the actual dense core of a local Hessian pairing, and continuity then gives the full Dirichlet bound.

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