HeatVarianceLower.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

An integrated reverse Poincaré estimate from the actual RCD heat flow

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.heat_variance_lower line 18

Source documentation

The heat variance controls the gradient, with a uniform sufficient short-time curvature factor. The initial data are compact Lipschitz.

theorem NoncollapsedRCD.heat_variance_lower
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    {φ : X → ℝ} {L : ℝ≥0} (hφ : LipschitzWith L φ) (hφs : HasCompactSupport φ)
    (p : X) (f w : Lp ℝ 2 (hausdorff n X)) (hφf : φ =ᵐ[hausdorff n X] f)
    (C B : ℝ≥0) (hf : ∀ᵐ x ∂hausdorff n X, |f x| ≤ C)
    (hw : 0 ≤ w) (hwB : ∀ᵐ x ∂hausdorff n X, |w x| ≤ B)
    (T : ℝ) (hT : 0 < T) :
    letI : ProperSpace X := hX.proper K n hn
…

Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD, OAI.RegularPointCoordinates.hausdorff