RegularDyadicData.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

One regular-point map with bounded dyadic frames and one Bochner measure

theorem OAI.RegularPointCoordinates.regular_uniform_dyadic_data_with_cap line 23
Source documentation
The published geometric normalization and local Bochner inputs provide the actual common data required by the heat argument. The root frames are bounded before any small-scale heat comparison is invoked.
```
theorem regular_uniform_dyadic_data_with_cap {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 1) X) (hn : 2 ≤ m + 1) {p : X} {a : ℝ} (ha : 0 ≤ a)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 1) p)
    (hvolume : EuclideanRescalingVolumeConvergence (hausdorff (m + 1) X) (m + 1) p
      (euclideanUnitVolume (m + 1)))
    (hmeasured : EuclideanMeasuredRescalingConvergence (hausdorff (m + 1) X) (m + 1) p)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff (m + 1) X)
      (comparisonModelVolume m a) y (euclideanUnitVolume (m + 1)))
    (hinitial : LocalInitialSplittingInput hX) (htrans : LocalTransformationInput hX)
    (hsplit : LocalFlatSplittingInput hX) (hrigidity : UniformRegularFlatnessInput hX)
    (hbochner : LocalHarmonicBochnerInput hX)
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.hausdorff, 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, OAI.RegularPointCoordinates.LocalHarmonicBochnerInput
theorem OAI.RegularPointCoordinates.regular_uniform_dyadic_data line 160
Source documentation
The original uncapped interface is the unit-cap specialization.
```
theorem regular_uniform_dyadic_data {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 1) X) (hn : 2 ≤ m + 1) {p : X} {a : ℝ} (ha : 0 ≤ a)
    (hcompact : PointedRescalingPrecompactness p) (hregular : IsRegular (m + 1) p)
    (hvolume : EuclideanRescalingVolumeConvergence (hausdorff (m + 1) X) (m + 1) p
      (euclideanUnitVolume (m + 1)))
    (hmeasured : EuclideanMeasuredRescalingConvergence (hausdorff (m + 1) X) (m + 1) p)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (hdensity : ∀ y, SmallScaleVolumeUpper (hausdorff (m + 1) X)
      (comparisonModelVolume m a) y (euclideanUnitVolume (m + 1)))
    (hinitial : LocalInitialSplittingInput hX) (htrans : LocalTransformationInput hX)
    (hsplit : LocalFlatSplittingInput hX) (hrigidity : UniformRegularFlatnessInput hX)
    (hbochner : LocalHarmonicBochnerInput hX)
…
```
Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.PointedRescalingPrecompactness, OAI.RegularPointCoordinates.IsRegular, OAI.RegularPointCoordinates.EuclideanRescalingVolumeConvergence, OAI.RegularPointCoordinates.hausdorff, 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, OAI.RegularPointCoordinates.LocalHarmonicBochnerInput