Main.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bi-Lipschitz coordinates at regular noncollapsed RCD points

Harmonic coordinates, heat-kernel estimates, summable directional pinching, and nonlinear renormalization give an open chart at every regular point. Both chart domains and Euclidean images are open, and the metric estimates use the restricted ambient distance.

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.regular_point_chart_nonpositive line 18
theorem OAI.RegularPointCoordinates.every_regular_point_has_bilipschitz_coordinates line 48
Source documentation
Every regular point of a noncollapsed RCD(K,n) space, n ≥ 2, has an open neighborhood bi-Lipschitz homeomorphic to an open subset of Euclidean n.
```
theorem every_regular_point_has_bilipschitz_coordinates {K : ℝ} {n : ℕ}
    (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X) {p : X} (hp : IsRegular n p) :
    HasOpenBilipschitzChart n p := by
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.HasOpenBilipschitzChart