OAI/Geometry/RCD/Coordinates/RegularCoreFrameDefect.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Quantitative frame energy on the actual regular core of an RCD space

The finite-dimensional inequality and common Bochner measure are constructed from RCD. The only source data supplied below are the actual weak Laplacians and their bounded local Sobolev representatives.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_core_frame_defect line 19