OAI/Geometry/RCD/Sobolev/VarianceLowerBound.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The scalar estimate turning variance differentiation into a gradient bound

  1. theorem OAI.RegularPointCoordinates.variance_lower_bound line 13

    Source documentation

    A weighted differential inequality yields a uniform endpoint estimate. The exponential constant is deliberately sufficient for short-time use.

    theorem variance_lower_bound {F : ℝ → ℝ} {K T E : ℝ} (hT : 0 < T) (hE : 0 ≤ E)
    (hc : ContinuousOn F (Icc 0 T))
    (hd : ∀ s ∈ Ioo 0 T, ∃ G : ℝ, HasDerivAt F (2*G) s ∧
      E ≤ Real.exp (-2*K*s)*G) :
    2*T*Real.exp (-2*|K| *T)*E ≤ F T-F 0 := by
…