RegularProjectionEnvironment.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

One regular-neighborhood environment for heat and sharp projection

structure OAI.RegularPointCoordinates.RegularProjectionEnvironment line 20
Source documentation
Actual heat data and actual small-source replacements with identical root radii. Every later coordinate estimate uses heat.coordinates.
```
structure RegularProjectionEnvironment {K : ℝ} {n : ℕ} (hX : NoncollapsedRCD K n X)
    [(hausdorff n X).Regular] [IsFiniteMeasureOnCompacts (hausdorff n X)]
    (p : X) {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff n X) hX.quadratic ker)
    (a κ B J C A Cχ enlargement zeta eta : ℝ) where
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.IsContinuousHeatKernel
theorem OAI.RegularPointCoordinates.exists_regular_projection_environment_uniform_degree line 50
Source documentation
The radius cap synchronizes the already proved heat construction with the source neighborhood. All five construction constants are chosen before the source and coordinate tolerances.
```
theorem exists_regular_projection_environment_uniform_degree {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    {p : X} {a κ : ℝ} (ha : 0 ≤ a) (hκ : 0 ≤ κ) (hK : -κ ≤ K)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 2) p)
    (hvolume : EuclideanRescalingVolumeConvergence (hausdorff (m + 2) X) (m + 2) p
      (euclideanUnitVolume (m + 2)))
    (hmeasured : EuclideanMeasuredRescalingConvergence (hausdorff (m + 2) X) (m + 2) p)
    (hBG : BallVolumeComparison (hausdorff (m + 2) X) (comparisonModelVolume (m + 1) a))
    (hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff (m + 2) X)
      (comparisonModelVolume (m + 1) a) y (euclideanUnitVolume (m + 2)))
    (hdistance : LocalSquaredDistanceInput hX) (hsobolev : LocalDirichletSobolevInput hX)
    (hpoisson : LocalPoissonGradientInput 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, OAI.RegularPointCoordinates.LocalPoissonGradientInput

theorem OAI.RegularPointCoordinates.exists_regular_projection_environment line 161

Source documentation

The original interface follows by forgetting the uniform degree.

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