OAI/Geometry/RCD/Sobolev/LipschitzL2PointControl.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Pointwise control of uniformly Lipschitz L² representatives

Small L² mass prevents a fixed nonzero value from persisting on a ball of positive measure. Applied to bounded heat data, this turns L² convergence into pointwise convergence without presupposing a kernel bound.

  1. theorem OAI.RegularPointCoordinates.lipschitz_value_sq_mass line 22

    Source documentation

    A value separated from zero forces explicit L² mass on a metric ball.

    theorem lipschitz_value_sq_mass (u : Lp ℝ 2 μ) (v : X → ℝ)
    (hu : u =ᵐ[μ] v) (L : ℝ≥0) (hv : LipschitzWith L v)
    (x : X) {r a : ℝ} (hfinite : μ (ball x r) ≠ ∞) (ha : 0 ≤ a) (hvalue : a + L * r ≤ |v x|) :
    a ^ 2 * μ.real (ball x r) ≤ ‖u‖ ^ 2 := by
…