OAI/Geometry/RCD/Heat/DyadicHeatAtStability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RegularPointCoordinates.dyadic_heat_at_step_of_conjugated_comparison line 19

   Source documentation

   Exact normalizers and the proved heat-to-mean comparison give the adjacent 9/8 bound without changing the original coordinate frame.

   theorem dyadic_heat_at_step_of_conjugated_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)
       (u : Fin (m + 1) → SobolevSpace (hausdorff (m + 1) X) hX.quadratic)
       (S : ℕ → Euclidean (m + 1) ≃L[ℝ] Euclidean (m + 1))
       {p c : X} {ρ Ccut R lambda e : ℝ}
       (χ : GoodLaplacianCutoff (hausdorff (m + 1) X) hX.quadratic c ρ Ccut)
       (hR : 0 < R) (hlambda : 0 < lambda) (he : 0 ≤ e)
       (hscale : a * (3 * R) ≤ 1)
   …

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