Assembly

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

The W^{1,∞}-to-Lipschitz bridge on a convex domain

A function on a bounded open convex domain whose weak partial derivatives are bounded by B in every coordinate direction has a Lipschitz representative with constant d * B.

The proof is the classical mollification argument, carried out with the CoarseGraining convex-domain smoothing operator Homogenization.convexApproxSmoothRepresentative:

1. Replace the weak derivative fields by their truncations, which are bounded by B everywhere (Mollification).
2. Mollify. The mollified function is smooth, its directional derivatives are the mollifications of the truncated derivative fields up to the harmless factor 1 - ε, and mollification does not increase the uniform bound. Hence ‖D u_ε‖ ≤ d * B pointwise on the domain, and the mean value inequality on a convex set gives LipschitzOnWith (d * B) u_ε U.
3. The mollifications converge to u in L²(U), hence in measure, hence a.e. along a subsequence. A pointwise a.e. limit of uniformly Lipschitz functions is Lipschitz on the full-measure set where the limit exists, and LipschitzOnWith.extend_real turns this into a globally Lipschitz function a.e. equal to u.

The public results are

• lipschitzOnWith_convexApproxSmoothRepresentative (step 2),
• exists_lipschitzWith_ae_eq_of_hasWeakPartialDeriv_bound (the bridge), and
• exists_lipschitz_ae_eq_of_hasWeakPartialDeriv_bound, its unbundled pointwise-oscillation form.

Pointwise limits preserve a Lipschitz bound

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.lipschitzOnWith_of_tendsto {α : Type u_1} [PseudoMetricSpace α] {s : Set α} {K : NNReal} {f : ℕ → α → ℝ} {F : α → ℝ} (hf : ∀ (n : ℕ), LipschitzOnWith K (f n) s) (hF : ∀ x ∈ s, Filter.Tendsto (fun (n : ℕ) => f n x) Filter.atTop (nhds (F x))) : LipschitzOnWith K F s

A pointwise limit of K-Lipschitz functions on s is K-Lipschitz on s.

Step 2: the mollified function is Lipschitz on the domain

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.lipschitzOnWith_convexApproxSmoothRepresentative {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {ρ : HCPolySupport.Vec d → ℝ} (hρ : HCPolySupport.IsConvexApproxKernel ρ) {u : HCPolySupport.Vec d → ℝ} {g : Fin d → HCPolySupport.Vec d → ℝ} {B : ℝ} (hB : 0 ≤ B) (hu2 : HCPolySupport.MemLpOn U 2 u) (hgtop : ∀ (i : Fin d), HCPolySupport.MemLpOn U ⊤ (g i)) (hg2 : ∀ (i : Fin d), HCPolySupport.MemLpOn U 2 (g i)) (hgbd : ∀ (i : Fin d) (y : HCPolySupport.Vec d), |g i y| ≤ B) (hweak : ∀ (i : Fin d), HCPolySupport.HasWeakPartialDerivOn U i u (g i)) {x0 : HCPolySupport.Vec d} {r ε : ℝ} (hball : Metric.closedBall x0 r ⊆ U) (hr : 0 < r) (hε0 : 0 < ε) (hε1 : ε < 1) : LipschitzOnWith (↑d * B).toNNReal (HCPolySupport.convexApproxSmoothRepresentative U ρ u x0 r ε) U

If the weak partial derivatives of u are bounded by B everywhere, then every convex-domain mollification of u is d * B-Lipschitz on the domain.

Step 3: from a uniformly Lipschitz L²-approximating sequence

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.exists_lipschitzWith_ae_eq_of_tendsto_eLpNorm {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUmeas : MeasurableSet U) {u : HCPolySupport.Vec d → ℝ} {K : NNReal} {W : ℕ → HCPolySupport.Vec d → ℝ} (hlip : ∀ (n : ℕ), LipschitzOnWith K (W n) U) (htend : Filter.Tendsto (fun (n : ℕ) => MeasureTheory.eLpNorm (W n - u) 2 (MeasureTheory.volume.restrict U)) Filter.atTop (nhds 0)) : ∃ (v : HCPolySupport.Vec d → ℝ), LipschitzWith K v ∧ v =ᵐ[MeasureTheory.volume.restrict U] u

If u is the L²(U) limit of a sequence of uniformly K-Lipschitz functions on U, then u agrees a.e. on U with a globally K-Lipschitz function.

The bridge

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.exists_lipschitzWith_ae_eq_of_hasWeakPartialDeriv_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {u : HCPolySupport.Vec d → ℝ} {g : Fin d → HCPolySupport.Vec d → ℝ} {B : ℝ} (hB : 0 ≤ B) (hu : HCPolySupport.MemLpOn U ⊤ u) (hg : ∀ (i : Fin d), HCPolySupport.MemLpOn U ⊤ (g i)) (hgB : ∀ (i : Fin d), ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, |g i x| ≤ B) (hweak : ∀ (i : Fin d), HCPolySupport.HasWeakPartialDerivOn U i u (g i)) : ∃ (v : HCPolySupport.Vec d → ℝ), LipschitzWith (↑d * B).toNNReal v ∧ v =ᵐ[MeasureTheory.volume.restrict U] u

W^{1,∞} implies Lipschitz on a convex domain. If u has weak partial derivatives g i on the bounded open convex domain U and each g i is bounded by B almost everywhere, then u agrees a.e. on U with a globally d * B-Lipschitz function.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.exists_lipschitz_ae_eq_of_hasWeakPartialDeriv_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {u : HCPolySupport.Vec d → ℝ} {g : Fin d → HCPolySupport.Vec d → ℝ} {B : ℝ} (hB : 0 ≤ B) (hu : HCPolySupport.MemLpOn U ⊤ u) (hg : ∀ (i : Fin d), HCPolySupport.MemLpOn U ⊤ (g i)) (hgB : ∀ (i : Fin d), ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, |g i x| ≤ B) (hweak : ∀ (i : Fin d), HCPolySupport.HasWeakPartialDerivOn U i u (g i)) : ∃ (v : HCPolySupport.Vec d → ℝ), (∀ (x y : HCPolySupport.Vec d), ‖v x - v y‖ ≤ ↑d * B * ‖x - y‖) ∧ v =ᵐ[MeasureTheory.volume.restrict U] u

Unbundled form of the bridge: the representative is stated through its pointwise oscillation bound, which is the form consumed by the Besov estimates.