OAI/Geometry/RCD/Coordinates/RegularLimitChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The chart limit of the regular-neighborhood iteration

Scalar smallness and geometric patch estimates yield an open chart with two-sided ambient-distance bounds.

  1. theorem OAI.RegularPointCoordinates.regular_iteration_limit_chart line 22

    Source documentation

    Once the scalar tolerances are met, the actual heat-coordinate iteration has an open ambient-distance bi-Lipschitz limit chart.

    theorem regular_iteration_limit_chart {K : ℝ} {n : ℕ}
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    (psi : EuclideanGevreyCutoff n) {Cpin Theta : ℝ} (hCpin : 0 ≤ Cpin) (hTheta : 1 ≤ Theta) :
    let N := patchOverlapBound n (1 / 2) 2 3
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.EuclideanGevreyCutoff, OAI.RegularPointCoordinates.patchOverlapBound