AdjacentMeanComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Adjacent-scale relative mean comparison from the published splitting input

theorem OAI.RegularPointCoordinates.normalized_adjacent_mean_comparison line 19

Source documentation

A fixed dimensional Bishop--Gromov ratio controls the restriction to half radius. No interscale transformation bound is assumed.

theorem normalized_adjacent_mean_comparison {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 1) X) {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
    (A : Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
    {p : X} {r ε : ℝ} {w : X → Euclidean (m + 1)}
    (hr : 0 < r) (hscale : a * (3 * (r / 2)) ≤ 1) (hε : 0 ≤ ε)
    (hfirst : FirstOrderSplittingOn (hausdorff (m + 1) X) hX.quadratic p r ε
      (transformedColumn (hausdorff (m + 1) X) hX.quadratic u A) w)
    (hexact : IsExactMeanNormalization (hausdorff (m + 1) X) hX.quadratic
      (sobolevColumnMap (hausdorff (m + 1) X) hX.quadratic u) (ball p r) measurableSet_ball A)
    (v : Euclidean (m + 1)) :
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.SobolevSpace, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.FirstOrderSplittingOn, OAI.RegularPointCoordinates.transformedColumn, OAI.RegularPointCoordinates.IsExactMeanNormalization, OAI.RegularPointCoordinates.sobolevColumnMap