LipschitzRepresentative

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

A bounded weak gradient produces a Lipschitz representative

A function with a weak gradient bounded by K on a bounded open convex set agrees, away from a null set, with a Lipschitz function. The Lipschitz constant is d · K: the ambient norm on Vec d = Fin d → ℝ is the supremum norm, the gradient bound ‖∇u x‖ ≤ K therefore bounds each partial derivative by K, and the operator norm of the differential on (Fin d → ℝ, ‖·‖_∞) is the sum of the d partial derivatives. The factor d is sharp, attained by a linear function whose d partial derivatives all equal K.

Route

Mollification. The convex smoothing operator produces smooth approximants whose classical partial derivatives agree, away from a null set, with the smoothed weak partial derivatives; both sides are continuous, so on an open set the identity holds at every point. The mollifier is nonnegative with unit mass, so the smoothed partials inherit the bound K pointwise, and the mean value theorem makes every approximant d·K-Lipschitz on the convex set. The approximants converge in L², hence in measure, hence pointwise away from a null set along a subsequence; a pointwise limit of d·K-Lipschitz functions is d·K-Lipschitz on the set where the limit exists, and a real-valued Lipschitz function on a subset extends to a Lipschitz function on the whole space.

Main results

• exists_lipschitzWith_representative_of_hasWeakGradientOn.

References

• CoarseGraining, Homogenization/Sobolev/W1p/ConvexApproxSmoothing/.

1. The mollified field inherits a pointwise bound

theorem Algsuperdiff.Section5.Support.abs_convexApproxSmoothRepresentative_le {d : ℕ} {V : Set (HCPolySupport.Vec d)} {rho g : HCPolySupport.Vec d → ℝ} (hrho : HCPolySupport.IsConvexApproxKernel rho) {K : ℝ} (hK : 0 ≤ K) (hg : ∀ x ∈ V, |g x| ≤ K) {x0 : HCPolySupport.Vec d} {r ep : ℝ} (hepr : 0 < ep * r) (x : HCPolySupport.Vec d) : |HCPolySupport.convexApproxSmoothRepresentative V rho g x0 r ep x| ≤ K

A nonnegative unit-mass mollifier does not increase a pointwise bound.

2. Every approximant is d · K-Lipschitz on the domain

3. The representative

theorem Algsuperdiff.Section5.Support.exists_lipschitzWith_representative_of_hasWeakGradientOn {d : ℕ} {V : Set (HCPolySupport.Vec d)} (hV : HCPolySupport.IsOpenBoundedConvexDomain V) (hVne : V.Nonempty) {u : HCPolySupport.Vec d → ℝ} {G : HCPolySupport.Vec d → HCPolySupport.Vec d} {K : ℝ} (hK : 0 ≤ K) (hu : HCPolySupport.MemLpOn V 2 u) (hG : ∀ (i : Fin d), HCPolySupport.MemLpOn V 2 fun (x : HCPolySupport.Vec d) => G x i) (hweak : HCPolySupport.HasWeakGradientOn V u G) (hGbd : ∀ (x : HCPolySupport.Vec d), ‖G x‖ ≤ K) : ∃ (uRep : HCPolySupport.Vec d → ℝ), LipschitzWith (↑d * K).toNNReal uRep ∧ u =ᵐ[MeasureTheory.volume.restrict V] uRep

A bounded weak gradient produces a Lipschitz representative.

If u has weak gradient G on a nonempty bounded open convex set V and ‖G x‖ ≤ K everywhere, then u agrees away from a null set with a function that is d · K-Lipschitz on the whole space. The factor d is the price of the supremum norm on Vec d and is sharp.