OAI/Geometry/RCD/Heat/ScaledRebasedHeatComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.uniform_scaled_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_scaled_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 : ℝ) {η : ℝ} (hη : 0 < η) :
       ∃ N : ℕ, ∃ ε : ℝ, 0 < ε ∧ ∀ (lambda : ℝ) 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 ≤ 1 → |lambda| * ((2 : ℝ) ^ k * r) ^ 2 ≤ Lambda →
   …

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