OAI/Geometry/RCD/Heat/KernelGradientFromReverse.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A kernel-row gradient estimate from reverse Poincaré

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.kernel_row_gradient_bound line 18

    Source documentation

    A bound on the earlier kernel row controls the weak gradient of its heat evolution. The remaining row retains its spatial Gaussian decay.

    theorem NoncollapsedRCD.kernel_row_gradient_bound
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X) (p : X) :
    letI : ProperSpace X := hX.proper K n hn
…

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD