OAI/Geometry/RCD/Heat/HeatSmoothingScale.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A scale-explicit form of bounded-data heat smoothing

  1. theorem OAI.RegularPointCoordinates.heat_smoothing_constant_le line 13
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_bounded_gradient_scale line 41

    Source documentation

    The coefficient depends on the outer time; the singularity at zero is only inverse square root and can therefore be integrated.

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

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD