OAI/Geometry/RCD/Coordinates/ConditionalMain.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Bi-Lipschitz coordinates from local geometric and analytic estimates

The neighborhood and chart are constructed from harmonic approximation, heat-kernel bounds, and summable directional pinching.

  1. theorem OAI.RegularPointCoordinates.regular_point_has_open_bilipschitz_chart_of_flat_coordinate_heat_bounds_actual line 25
  2. theorem OAI.RegularPointCoordinates.regular_point_has_open_bilipschitz_chart_of_flat_coordinate_heat_bounds line 153
  3. theorem OAI.RegularPointCoordinates.regular_point_has_open_bilipschitz_chart_conditional line 188
  4. theorem OAI.RegularPointCoordinates.regular_point_has_open_bilipschitz_chart_of_coordinate_heat_bounds line 223
  5. theorem OAI.RegularPointCoordinates.every_regular_point_has_bilipschitz_coordinates_of_flat_coordinate_heat_bounds line 260

    Source documentation

    Regular points in dimension at least two admit charts with two-sided ambient-distance bounds under the stated local estimates.

    theorem every_regular_point_has_bilipschitz_coordinates_of_flat_coordinate_heat_bounds {K : ℝ} {n : ℕ}
    (hn : 2 ≤ n)
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {p : X} {a : ℝ} (ha : 0 ≤ a)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular n p)
    (hvolume : EuclideanRescalingVolumeConvergence (hausdorff n X) n p
      (euclideanUnitVolume n))
    (hmeasured : EuclideanMeasuredRescalingConvergence (hausdorff n X) n p)
    (hBG : BallVolumeComparison (hausdorff n X) (comparisonModelVolume (n - 1) a))
    (hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff n X)
      (comparisonModelVolume (n - 1) a) y (euclideanUnitVolume n))
    (hdistance : LocalSquaredDistanceInput hX) (hsobolev : LocalDirichletSobolevInput hX)
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.euclideanUnitVolume, OAI.RegularPointCoordinates.EuclideanMeasuredRescalingConvergence, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SmallScaleVolumeUpper, OAI.RegularPointCoordinates.LocalSquaredDistanceInput, OAI.RegularPointCoordinates.LocalDirichletSobolevInput

  6. theorem OAI.RegularPointCoordinates.every_regular_point_has_bilipschitz_coordinates_of_flat_coordinate_heat_bounds_actual line 297
  7. theorem OAI.RegularPointCoordinates.every_regular_point_has_bilipschitz_coordinates_of_coordinate_heat_bounds line 334
  8. theorem OAI.RegularPointCoordinates.every_regular_point_has_bilipschitz_coordinates_conditional line 373

    Source documentation

    Regular points in dimension at least two admit charts with two-sided ambient-distance bounds under the stated local estimates.

    theorem every_regular_point_has_bilipschitz_coordinates_conditional {K : ℝ} {n : ℕ}
    (hn : 2 ≤ n)
    (hX : NoncollapsedRCD K n X) [(hausdorff n X).Regular]
    {p : X} {a : ℝ} (ha : 0 ≤ a)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular n p)
    (hvolume : EuclideanRescalingVolumeConvergence (hausdorff n X) n p
      (euclideanUnitVolume n))
    (hmeasured : EuclideanMeasuredRescalingConvergence (hausdorff n X) n p)
    (hBG : BallVolumeComparison (hausdorff n X) (comparisonModelVolume (n - 1) a))
    (hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff n X)
      (comparisonModelVolume (n - 1) a) y (euclideanUnitVolume n))
    (hdistance : LocalSquaredDistanceInput hX) (hsobolev : LocalDirichletSobolevInput hX)
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.euclideanUnitVolume, OAI.RegularPointCoordinates.EuclideanMeasuredRescalingConvergence, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SmallScaleVolumeUpper, OAI.RegularPointCoordinates.LocalSquaredDistanceInput, OAI.RegularPointCoordinates.LocalDirichletSobolevInput