BoundedGradientLipschitz.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded relaxed gradients give Lipschitz representatives on RCD spaces

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.average_bound_of_gradient line 18

Source documentation

Transport between small balls controls their averages by the weak upper gradient, with no volume-comparison factor.

theorem NoncollapsedRCD.average_bound_of_gradient
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    {u G : Lp ℝ 2 (hausdorff n X)} (hG : IsRelaxedSlope (hausdorff n X) u G)
    (L : ℝ≥0) (hGb : ∀ᵐ x ∂hausdorff n X, G x ≤ L) (x y : X) (r : ℝ) (hr : 0 < r) :
    |(⨍ z in closedBall x r, u z ∂hausdorff n X)-
      (⨍ z in closedBall y r, u z ∂hausdorff n X)| ≤ L*(dist x y+2*r) := by
…

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

theorem OAI.RegularPointCoordinates.NoncollapsedRCD.lipschitz_of_bounded_gradient line 91

Source documentation

The RCD Sobolev-to-Lipschitz implication needed for the heat kernel.

theorem NoncollapsedRCD.lipschitz_of_bounded_gradient
    (K : ℝ) (n : ℕ) (hn : 2 ≤ n) (hX : NoncollapsedRCD K n X)
    {u G : Lp ℝ 2 (hausdorff n X)} (hG : IsRelaxedSlope (hausdorff n X) u G)
    (L : ℝ≥0) (hGb : ∀ᵐ x ∂hausdorff n X, G x ≤ L) :
    ∃ v : X → ℝ, LipschitzWith L v ∧ u =ᵐ[hausdorff n X] v := by
…

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