ScaledDyadicHeatComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Scale-invariant comparison along a fixed-root dyadic family

theorem OAI.RegularPointCoordinates.scaled_dyadic_heat_mean_comparison line 20

Source documentation

A single fixed coordinate map and its exact dyadic normalizers give uniform heat comparisons at all sufficiently fine scales. The outer normalizer is used only for the working-frame calculation.

theorem scaled_dyadic_heat_mean_comparison {K : ℝ} (m : ℕ)
    (hX : NoncollapsedRCD K (m + 1) X) [(hausdorff (m + 1) X).Regular]
    {a : ℝ} (ha : 0 ≤ a)
    (hBG : BallVolumeComparison (hausdorff (m + 1) X) (comparisonModelVolume m a))
    {ker : ℝ → X → X → ℝ}
    (hk : IsContinuousHeatKernel (hausdorff (m + 1) X) hX.quadratic ker)
    (hg : HasCoordinateHeatBounds (hausdorff (m + 1) X) ker)
    {L B V Vlo η : ℝ} (hL : 0 ≤ L) (hB : 0 ≤ B) (hV : 0 ≤ V) (hVlo : 0 < Vlo)
    (Lambda : ℝ) (hη : 0 < η) :
    ∃ N : ℕ, ∃ ε : ℝ, 0 < ε ∧
      ∀ (R : ℝ), 0 < R → R ≤ 1 → ∀ lambda : ℝ, |lambda| * R ^ 2 ≤ Lambda →
        a * (3 * R) ≤ 1 →
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff, OAI.RegularPointCoordinates.BallVolumeComparison, OAI.RegularPointCoordinates.comparisonModelVolume, OAI.RegularPointCoordinates.IsContinuousHeatKernel, OAI.RegularPointCoordinates.HasCoordinateHeatBounds