Mollification

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

L^∞ control and weak-derivative bookkeeping for the convex-domain smoothing

This module supplies the two elementary facts that the W^{1,∞}-to-Lipschitz bridge needs about the CoarseGraining convex-domain mollifier Homogenization.convexApproxSmoothRepresentative:

• abs_convexApproxSmoothRepresentative_le: the mollifier is an averaging operator, hence it never increases a uniform bound. This is exactly Mathlib's dist_convolution_le applied at z₀ = 0, using that the scaled convex-approximation kernel is nonnegative, compactly supported, and has unit integral.
• HasWeakPartialDerivOn.congr_deriv_ae: the weak-derivative relation only sees the derivative field through an integral against test functions, so it is invariant under a.e. modification of that field. This lets one replace a derivative field bounded almost everywhere by its truncation, which is bounded everywhere — the form needed by the convolution estimate above.

The truncation itself is packaged as boundedTruncation.

Support of the scaled kernel

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.support_scaledConvexApproxKernel_subset_ball {d : ℕ} {ρ : HCPolySupport.Vec d → ℝ} (hρ : HCPolySupport.IsConvexApproxKernel ρ) {a : ℝ} (ha : 0 < a) : Function.support (HCPolySupport.scaledConvexApproxKernel ρ a) ⊆ Metric.ball 0 (a + 1)

The scaled convex-approximation kernel at scale a is supported in the ball of radius a + 1 about the origin.

L^∞ preservation

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.abs_convexApproxSmoothRepresentative_le {d : ℕ} {U : Set (HCPolySupport.Vec d)} {ρ w : HCPolySupport.Vec d → ℝ} (hU : MeasurableSet U) (hρ : HCPolySupport.IsConvexApproxKernel ρ) (hw : HCPolySupport.MemLpOn U ⊤ w) {B : ℝ} (hB : 0 ≤ B) (hbound : ∀ y ∈ U, |w y| ≤ B) {x0 : HCPolySupport.Vec d} {r ε : ℝ} (hr : 0 < r) (hε0 : 0 < ε) (x : HCPolySupport.Vec d) : |HCPolySupport.convexApproxSmoothRepresentative U ρ w x0 r ε x| ≤ B

The mollifier does not increase a uniform bound. If w is bounded by B on U, then the globally smooth representative convexApproxSmoothRepresentative U ρ w x0 r ε is bounded by B everywhere.

Congruence of the weak-derivative relation

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.HasWeakPartialDerivOn.congr_deriv_ae {d : ℕ} {U : Set (HCPolySupport.Vec d)} {i : Fin d} {u g g' : HCPolySupport.Vec d → ℝ} (h : HCPolySupport.HasWeakPartialDerivOn U i u g) (hgg : g =ᵐ[MeasureTheory.volume.restrict U] g') : HCPolySupport.HasWeakPartialDerivOn U i u g'

The weak partial derivative relation is invariant under a.e. modification of the derivative field.

Truncation of a field to a uniform bound

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.boundedTruncation {d : ℕ} (B : ℝ) (f : HCPolySupport.Vec d → ℝ) : HCPolySupport.Vec d → ℝ

The truncation of f to the interval [-B, B].

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.boundedTruncation B f x = max (-B) (min B (f x))

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.continuous_truncationMap (B : ℝ) : Continuous fun (t : ℝ) => max (-B) (min B t)

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.abs_boundedTruncation_le {d : ℕ} {B : ℝ} (hB : 0 ≤ B) (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : |boundedTruncation B f x| ≤ B

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.boundedTruncation_eq_self {d : ℕ} {B : ℝ} {f : HCPolySupport.Vec d → ℝ} {x : HCPolySupport.Vec d} (hx : |f x| ≤ B) : boundedTruncation B f x = f x

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.boundedTruncation_ae_eq {d : ℕ} {U : Set (HCPolySupport.Vec d)} {B : ℝ} {f : HCPolySupport.Vec d → ℝ} (hf : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict U, |f x| ≤ B) : f =ᵐ[MeasureTheory.volume.restrict U] boundedTruncation B f

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Lipschitz.memLpOn_top_boundedTruncation {d : ℕ} {U : Set (HCPolySupport.Vec d)} {B : ℝ} (hB : 0 ≤ B) {f : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict U)) : HCPolySupport.MemLpOn U ⊤ (boundedTruncation B f)