OAI/Geometry/RCD/Sobolev/LocalGradientLipschitz.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A local Lipschitz estimate from weak-gradient and amplitude bounds

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

    Source documentation

    A radial cutoff reduces local gradient control to the proved global Sobolev-to-Lipschitz implication.

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

    Mentions: OAI.RegularPointCoordinates.NoncollapsedRCD