OAI/Geometry/RCD/Heat/HeatVarianceSobolev.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reverse Poincaré for bounded Sobolev initial data

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

    Source documentation

    L² continuity after positive heat time passes the compact Lipschitz inequality to any bounded Sobolev function.

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

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD