OAI/Geometry/RCD/Heat/HeatVarianceBounded.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reverse Poincaré for arbitrary bounded L² initial data

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

    Source documentation

    Small positive heat times approximate bounded L² data while preserving the amplitude bound, so the variance inequality holds without initial Sobolev regularity.

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

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD