OAI/Geometry/RCD/Heat/UniformHeatMeanComparison.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.uniform_finite_scale_heat_mean_comparison line 22

   Source documentation

   The actual heat Gram is close to the identity in every exact small-scale frame. The thresholds are chosen before the center, radius, harmonic column and cutoff. Only the finite range up to the working radius is normalized.

   theorem uniform_finite_scale_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 V Vlo : ℝ} (hL : 0 ≤ L) (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