OAI/Geometry/RCD/Coordinates/ScalarBochnerCoordinates.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The chart theorem under a scalar second-order estimate

The scalar finite-dimensional Bochner inequality implies the local second-order estimates required for the coordinate construction.

  1. theorem OAI.RegularPointCoordinates.regular_coordinates_of_scalar_bochner line 21