RebasedHeatMeanComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform heat/mean comparison in the original working coordinates

theorem OAI.RegularPointCoordinates.uniform_rebased_heat_mean_comparison line 22

Source documentation

Normalizing the mean at the outer radius is an auxiliary calculation: the conclusion is the heat comparison for the original coordinates and their original scalar regularizer. The threshold is uniform in all frames with the stated fixed working-frame bound.

theorem uniform_rebased_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 R : ℝ) {η : ℝ} (hη : 0 < η) :
    ∃ N : ℕ, ∃ ε : ℝ, 0 < ε ∧ ∀ k, N + 1 ≤ k →
      ∀ (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
        (p : X) (r e : ℝ), 0 < r → r ≤ 1 → (2 : ℝ) ^ k * r ≤ R →
…

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