RegularNeighborhoodBilinear.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The bilinear and cumulative heat estimates for the same regular-point data

theorem OAI.RegularPointCoordinates.regular_neighborhood_bilinear_heat_with_energy line 21
Source documentation
Published normalization, Bochner and kernel inputs produce both the actual bilinear comparison and the three cumulative estimates with one common family.
```
theorem regular_neighborhood_bilinear_heat_with_energy {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    {p : X} {a : ℝ} (ha : 0 ≤ a)
    (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)))
    (hinitial : LocalInitialSplittingInput hX) (htrans : LocalTransformationInput hX)
    (hsplit : LocalFlatSplittingInput hX) (hrigidity : UniformRegularFlatnessInput 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.LocalInitialSplittingInput, OAI.RegularPointCoordinates.LocalTransformationInput, OAI.RegularPointCoordinates.LocalFlatSplittingInput, OAI.RegularPointCoordinates.UniformRegularFlatnessInput
theorem OAI.RegularPointCoordinates.regular_neighborhood_bilinear_heat_uniform_degree line 291
Source documentation
Retain the original uniform-degree interface.
```
theorem regular_neighborhood_bilinear_heat_uniform_degree {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    {p : X} {a : ℝ} (ha : 0 ≤ a)
    (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)))
    (hinitial : LocalInitialSplittingInput hX) (htrans : LocalTransformationInput hX)
    (hsplit : LocalFlatSplittingInput hX) (hrigidity : UniformRegularFlatnessInput 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.LocalInitialSplittingInput, OAI.RegularPointCoordinates.LocalTransformationInput, OAI.RegularPointCoordinates.LocalFlatSplittingInput, OAI.RegularPointCoordinates.UniformRegularFlatnessInput
theorem OAI.RegularPointCoordinates.regular_neighborhood_bilinear_heat_with_cap line 364
Source documentation
The capped interface retains the original argument order.
```
theorem regular_neighborhood_bilinear_heat_with_cap {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    {p : X} {a : ℝ} (ha : 0 ≤ a)
    (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)))
    (hinitial : LocalInitialSplittingInput hX) (htrans : LocalTransformationInput hX)
    (hsplit : LocalFlatSplittingInput hX) (hrigidity : UniformRegularFlatnessInput 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.LocalInitialSplittingInput, OAI.RegularPointCoordinates.LocalTransformationInput, OAI.RegularPointCoordinates.LocalFlatSplittingInput, OAI.RegularPointCoordinates.UniformRegularFlatnessInput
theorem OAI.RegularPointCoordinates.regular_neighborhood_bilinear_heat line 433
Source documentation
The uncapped heat statement follows with unit radius cap.
```
theorem regular_neighborhood_bilinear_heat {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 2) X) [(hausdorff (m + 2) X).Regular]
    {p : X} {a : ℝ} (ha : 0 ≤ a)
    (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)))
    (hinitial : LocalInitialSplittingInput hX) (htrans : LocalTransformationInput hX)
    (hsplit : LocalFlatSplittingInput hX) (hrigidity : UniformRegularFlatnessInput 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.LocalInitialSplittingInput, OAI.RegularPointCoordinates.LocalTransformationInput, OAI.RegularPointCoordinates.LocalFlatSplittingInput, OAI.RegularPointCoordinates.UniformRegularFlatnessInput