Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Jensen Contact-Set Theorem (ConvexMollification)

Part of the localized Jensen contact-set theorem and the smooth convex approximation machinery used to prove it. Split from Jensen.lean; see the umbrella module docstring.

def ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem (n : ℕ) : Prop

Localized Jensen contact-set theorem on a closed ball.

In quantified mathematical form, this says: if f : R^n -> R is coordinate semiconvex on closedBall x0 r, 0 < r, and f has a strict local maximum at x0, then for every delta > 0, the set of points x ∈ closedBall x0 r for which there exists p ∈ ball 0 delta such that y ↦ f y + p · y has a local maximum at x has positive Lebesgue measure.

Equations

• One or more equations did not get rendered due to their size.

def ViscositySolns.JensenContactSetLimsupApproximationPrincipleOnClosedBall (n : ℕ) : Prop

The approximation principle needed to pass from the smooth Jensen theorem to the localized Jensen contact-set theorem.

In quantified mathematical form, suppose f : R^n -> R is coordinate semiconvex on closedBall x0 r, 0 < r, and f x < f x0 for every x ∈ closedBall x0 r with x ≠ x0. For every delta > 0, there exists a sequence of functions f_m : R^n -> R and a number c > 0 such that:

• every set JensenContactSet f_m x0 r (delta / 2) is measurable;
• the set-theoretic limsup ⋂ k, ⋃ m, ⋃ (_ : k ≤ m), JensenContactSet f_m x0 r (delta / 2) is contained in JensenContactSet f x0 r delta;
• for every m, the measure of JensenContactSet f_m x0 r (delta / 2) is at least c.

This is the exact nonsmooth approximation statement needed by the measure-theoretic limsup lemma below. The smaller perturbation radius delta / 2 leaves room to pass perturbing vectors to a limit while remaining inside Metric.ball 0 delta.

Equations

• One or more equations did not get rendered due to their size.

def ViscositySolns.JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall (n : ℕ) : Prop

The approximation principle in the form closest to the proof in the paper.

In quantified mathematical form, suppose f : R^n -> R is coordinate semiconvex on closedBall x0 r, 0 < r, and f x < f x0 for every x ∈ closedBall x0 r with x ≠ x0. For every delta > 0, there exists a sequence of functions f_m : R^n -> R and a number c > 0 such that:

• every set JensenGlobalContactSet f_m x0 r (delta / 2) is measurable;
• the set-theoretic limsup ⋂ k, ⋃ m, ⋃ (_ : k ≤ m), JensenGlobalContactSet f_m x0 r (delta / 2) is contained in JensenContactSet f x0 r delta;
• for every m, the measure of JensenGlobalContactSet f_m x0 r (delta / 2) is at least c.

Here JensenGlobalContactSet f_m x0 r (delta / 2) consists of the points in ball x0 r which maximize y ↦ f_m y + p · y on closedBall x0 r for some p ∈ ball 0 (delta / 2). The use of delta / 2 leaves a positive margin when passing perturbing vectors to a limit.

Equations

• One or more equations did not get rendered due to their size.

def ViscositySolns.JensenGlobalContactSetInteriorLimsupApproximationPrincipleOnClosedBall (n : ℕ) : Prop

The source-aligned global-contact approximation principle with semiconvexity available on a larger closed ball.

In quantified mathematical form, suppose 0 < r, r < R, f : R^n -> R is coordinate semiconvex on closedBall x0 R, and f x < f x0 for every x ∈ closedBall x0 r with x ≠ x0. For every delta > 0, there exists a sequence of functions f_m : R^n -> R and a number c > 0 such that:

• every set JensenGlobalContactSet f_m x0 r (delta / 2) is measurable;
• the set-theoretic limsup ⋂ k, ⋃ m, ⋃ (_ : k ≤ m), JensenGlobalContactSet f_m x0 r (delta / 2) is contained in JensenContactSet f x0 r delta;
• for every m, the measure of JensenGlobalContactSet f_m x0 r (delta / 2) is at least c.

The strict inequality r < R is the formal version of the source proof's choice of a smaller closed ball inside a region where the semiconvex function is defined. It gives continuity on the boundary sphere of radius r.

Equations

• One or more equations did not get rendered due to their size.

def ViscositySolns.SmoothConvexApproximationOnInteriorClosedBallTheorem (n : ℕ) : Prop

The remaining smooth convex approximation theorem needed for the mollification step.

In quantified mathematical form, suppose 0 < r, r < R, and g : R^n -> R is convex on closedBall x0 R. Then there should be smooth functions g_m : R^n -> R such that:

• for every ε > 0, there is a natural number N such that for every m ≥ N and every z ∈ closedBall x0 r, |g_m z - g z| ≤ ε;
• every g_m is twice continuously differentiable;
• every g_m is convex on closedBall x0 r.

This is the analytic mollification theorem for convex functions, stated separately from the viscosity-solution notation. It is stronger than ordinary smooth approximation because convexity must be preserved on the closed ball where the Jensen contact-set estimate is applied.

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.exists_continuous_extension_eqOn_intermediate_closedBall_of_convexOn_closedBall {n : ℕ} {g : Point n → ℝ} {x0 : Point n} {R r : ℝ} (_hr : 0 < r) (hrR : r < R) (hconv : ConvexOn ℝ (Metric.closedBall x0 R) g) : ∃ (Rmid : ℝ), r < Rmid ∧ Rmid < R ∧ ∃ (G : Point n → ℝ), Continuous G ∧ ∀ x ∈ Metric.closedBall x0 Rmid, G x = g x

Convexity on a closed ball supplies a continuous extension from an intermediate closed ball to the whole ambient coordinate space.

In quantified mathematical form, suppose 0 < r, r < R, and g : R^n -> R is convex on closedBall x0 R. Then there exists a radius Rmid satisfying r < Rmid < R and a continuous function G : R^n -> R such that G x = g x for every x ∈ closedBall x0 Rmid.

This is the extension step used before mollification. The intermediate radius ensures that convolution kernels with sufficiently small support do not sample outside the region on which the original convex function is known.

def ViscositySolns.ContinuousExtensionConvexMollificationOnInteriorClosedBallTheorem (n : ℕ) : Prop

The remaining convolution-only smooth approximation theorem after extending the convex function to a continuous function on the whole space.

In quantified mathematical form, suppose 0 < r, r < R, g : R^n -> R is convex on closedBall x0 R, and G : R^n -> R is continuous on all of R^n and agrees with g on closedBall x0 R. Then there are functions g_m : R^n -> R such that:

• for every ε > 0, there exists N such that for every m ≥ N and every z ∈ closedBall x0 r, |g_m z - g z| ≤ ε;
• every g_m is twice continuously differentiable;
• every g_m is convex on closedBall x0 r.

The intended proof is by convolution of G with nonnegative smooth kernels whose supports are eventually contained in a ball of radius smaller than R - r. The equality G = g on closedBall x0 R then ensures that, on closedBall x0 r, the convolution only uses values where the original function is convex.

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.SmoothConvexApproximationOnInteriorClosedBallTheorem.of_extensionMollification {n : ℕ} (hmoll : ContinuousExtensionConvexMollificationOnInteriorClosedBallTheorem n) : SmoothConvexApproximationOnInteriorClosedBallTheorem n

The continuous-extension convolution theorem implies smooth convex approximation on interior closed balls.

In quantified mathematical form, start with a convex function on closedBall x0 R and choose an intermediate radius Rmid with r < Rmid < R. The extension theorem gives a continuous function on the ambient space agreeing with the original convex function on closedBall x0 Rmid; the convolution theorem applied on the pair of radii r < Rmid gives the desired smooth convex approximants on closedBall x0 r.

theorem ViscositySolns.contDiff_two_normedBumpConvolution_left {n : ℕ} (φ : ContDiffBump 0) {G : Point n → ℝ} (hG : Continuous G) : ContDiff ℝ 2 (MeasureTheory.convolution (φ.normed MeasureTheory.volume) G (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

Convolution with a normalized smooth bump is twice continuously differentiable in the spatial variable.

In quantified mathematical form, if G : R^n -> R is continuous and φ is a compactly supported smooth bump function centered at the origin, then x ↦ ∫ φ(z) G(x - z) dz, normalized by the Haar measure integral of φ, is C^2.

theorem ViscositySolns.ball_subset_closedBall_of_mem_closedBall_add_le {n : ℕ} {x0 z : Point n} {r R ρ : ℝ} (hz : z ∈ Metric.closedBall x0 r) (hρR : r + ρ ≤ R) : Metric.ball z ρ ⊆ Metric.closedBall x0 R

A ball centered at a point of a smaller closed ball is contained in a larger closed ball if the two radii satisfy the corresponding triangle inequality.

In quantified mathematical form, if z ∈ closedBall x0 r and r + ρ ≤ R, then every point in ball z ρ belongs to closedBall x0 R.

theorem ViscositySolns.sub_mem_closedBall_of_mem_closedBall_mem_ball_add_le {n : ℕ} {x0 x z : Point n} {r R ρ : ℝ} (hx : x ∈ Metric.closedBall x0 r) (hz : z ∈ Metric.ball 0 ρ) (hρR : r + ρ ≤ R) : x - z ∈ Metric.closedBall x0 R

Subtracting a vector in a small ball from a point of the smaller closed ball keeps the result in the larger closed ball.

In quantified mathematical form, if x ∈ closedBall x0 r, z ∈ ball 0 ρ, and r + ρ ≤ R, then x - z ∈ closedBall x0 R.

theorem ViscositySolns.convexCombination_sub_mem_closedBall_of_mem_closedBall_mem_ball_add_le {n : ℕ} {x0 x y z : Point n} {r R ρ a b : ℝ} (hx : x ∈ Metric.closedBall x0 r) (hy : y ∈ Metric.closedBall x0 r) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (hz : z ∈ Metric.ball 0 ρ) (hρR : r + ρ ≤ R) : x - z ∈ Metric.closedBall x0 R ∧ y - z ∈ Metric.closedBall x0 R ∧ a • x + b • y - z ∈ Metric.closedBall x0 R

The convolution sample points used in the convexity argument lie in the larger closed ball.

In quantified mathematical form, assume x,y ∈ closedBall x0 r, a,b ≥ 0, a+b=1, z ∈ ball 0 ρ, and r + ρ ≤ R. Then x - z, y - z, and a • x + b • y - z all belong to closedBall x0 R.

theorem ViscositySolns.convolution_sample_convexity_inequality {n : ℕ} {g G : Point n → ℝ} {x0 x y z : Point n} {R a b : ℝ} (hconv : ConvexOn ℝ (Metric.closedBall x0 R) g) (hGeq : ∀ w ∈ Metric.closedBall x0 R, G w = g w) (hxz : x - z ∈ Metric.closedBall x0 R) (hyz : y - z ∈ Metric.closedBall x0 R) (hxyz : a • x + b • y - z ∈ Metric.closedBall x0 R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : G (a • x + b • y - z) ≤ a * G (x - z) + b * G (y - z)

The pointwise convexity inequality for the convolution integrand.

In quantified mathematical form, suppose G = g on closedBall x0 R, g is convex on closedBall x0 R, and the translated sample points x - z, y - z, and a x + b y - z lie in this closed ball. Then the corresponding values of G satisfy the convexity inequality.

theorem ViscositySolns.convexOn_normedBumpConvolution_of_convexOn_extension {n : ℕ} (φ : ContDiffBump 0) {g G : Point n → ℝ} (hG : Continuous G) {x0 : Point n} {R r : ℝ} (hconv : ConvexOn ℝ (Metric.closedBall x0 R) g) (hGeq : ∀ w ∈ Metric.closedBall x0 R, G w = g w) (hcontain : r + φ.rOut ≤ R) : ConvexOn ℝ (Metric.closedBall x0 r) (MeasureTheory.convolution (φ.normed MeasureTheory.volume) G (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume)

Fixed-kernel convexity preservation for normalized bump convolution.

In quantified mathematical form, suppose g is convex on closedBall x0 R, G = g on this closed ball, and the outer support radius of the bump is at most R - r. Then the normalized convolution of G with this bump is convex on closedBall x0 r.

theorem ViscositySolns.abs_normedBumpConvolution_sub_le_of_local_oscillation {n : ℕ} (φ : ContDiffBump 0) {G : Point n → ℝ} (hG : Continuous G) {x0 : Point n} {r eps : ℝ} (hosc : ∀ z ∈ Metric.closedBall x0 r, ∀ y ∈ Metric.ball z φ.rOut, dist (G y) (G z) ≤ eps) (z : Point n) : z ∈ Metric.closedBall x0 r → |MeasureTheory.convolution (φ.normed MeasureTheory.volume) G (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume z - G z| ≤ eps

The fixed-kernel uniform approximation estimate for normalized bump convolution.

In quantified mathematical form, let G : R^n -> R be continuous and let φ be a normalized smooth bump. If, for every z ∈ closedBall x0 r, the oscillation of G on ball z φ.rOut is at most ε, then the convolution of G with φ.normed volume differs from G by at most ε at every z ∈ closedBall x0 r.

theorem ViscositySolns.abs_normedBumpConvolution_sub_extension_le_of_local_oscillation {n : ℕ} (φ : ContDiffBump 0) {g G : Point n → ℝ} (hG : Continuous G) {x0 : Point n} {R r eps : ℝ} (hGeq : ∀ x ∈ Metric.closedBall x0 R, G x = g x) (hcontain : r + φ.rOut ≤ R) (hosc : ∀ z ∈ Metric.closedBall x0 r, ∀ y ∈ Metric.ball z φ.rOut, dist (G y) (G z) ≤ eps) (z : Point n) : z ∈ Metric.closedBall x0 r → |MeasureTheory.convolution (φ.normed MeasureTheory.volume) G (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume z - g z| ≤ eps

The fixed-kernel approximation estimate, rewritten for a function g which agrees with the continuous extension G on a closed ball containing all points sampled by the kernel.

In quantified mathematical form, suppose G = g on closedBall x0 R, every point in closedBall x0 r is at distance at least φ.rOut from the outside of closedBall x0 R, and G varies by at most ε on the balls ball z φ.rOut centered at points z ∈ closedBall x0 r. Then the normalized bump convolution of G is within ε of g on closedBall x0 r.

theorem ViscositySolns.exists_pos_le_sub_forall_dist_le_of_continuous_on_closedBall {n : ℕ} {G : Point n → ℝ} (hG : Continuous G) {x0 : Point n} {R r eps : ℝ} (hrR : r < R) (heps : 0 < eps) : ∃ (η : ℝ), 0 < η ∧ η ≤ R - r ∧ ∀ z ∈ Metric.closedBall x0 r, ∀ y ∈ Metric.ball z η, dist (G y) (G z) ≤ eps

Compact uniform continuity supplies a support radius for the local oscillation estimate used by mollification.

In quantified mathematical form, suppose G : R^n -> R is continuous, 0 < r < R, and ε > 0. Then there exists η > 0 such that η ≤ R - r and, for every z ∈ closedBall x0 r, every point y ∈ ball z η satisfies dist (G y) (G z) ≤ ε.

theorem ViscositySolns.exists_pos_forall_rOut_le_abs_normedBumpConvolution_sub_extension_le {n : ℕ} {g G : Point n → ℝ} (hG : Continuous G) {x0 : Point n} {R r eps : ℝ} (hrR : r < R) (heps : 0 < eps) (hGeq : ∀ x ∈ Metric.closedBall x0 R, G x = g x) : ∃ (η : ℝ), 0 < η ∧ ∀ (φ : ContDiffBump 0), φ.rOut ≤ η → ∀ z ∈ Metric.closedBall x0 r, |MeasureTheory.convolution (φ.normed MeasureTheory.volume) G (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume z - g z| ≤ eps

Uniform approximation by any sufficiently small normalized bump convolution.

In quantified mathematical form, suppose G = g on closedBall x0 R, G is continuous, and 0 < r < R. For every ε > 0, there exists η > 0 such that, for every smooth bump φ centered at the origin with outer support radius at most η, the normalized convolution of G with φ is within ε of g at every point of closedBall x0 r.

noncomputable def ViscositySolns.jensenMollifierBump (n : ℕ) (rho : ℝ) (hrho : 0 < rho) (m : ℕ) : ContDiffBump 0

A concrete family of smooth bump functions whose outer support radii are rho / (m + 1).

In quantified mathematical form, if rho > 0, then for each natural number m this is a smooth bump centered at the origin, with inner radius rho / (2 * (m + 1)) and outer radius rho / (m + 1).

Equations

• ViscositySolns.jensenMollifierBump n rho hrho m = { rIn := rho / (↑m + 1) / 2, rOut := rho / (↑m + 1), rIn_pos := ⋯, rIn_lt_rOut := ⋯ }

@[simp]

theorem ViscositySolns.jensenMollifierBump_rOut {n : ℕ} (rho : ℝ) (hrho : 0 < rho) (m : ℕ) : (jensenMollifierBump n rho hrho m).rOut = rho / (↑m + 1)

theorem ViscositySolns.tendsto_jensenMollifierBump_rOut {n : ℕ} (rho : ℝ) (hrho : 0 < rho) : Filter.Tendsto (fun (m : ℕ) => (jensenMollifierBump n rho hrho m).rOut) Filter.atTop (nhds 0)

The outer support radii of jensenMollifierBump n rho hrho m converge to zero as m -> ∞.

theorem ViscositySolns.jensenMollifierBump_rOut_le_rho {n : ℕ} (rho : ℝ) (hrho : 0 < rho) (m : ℕ) : (jensenMollifierBump n rho hrho m).rOut ≤ rho

For fixed positive rho, every outer support radius rho / (m + 1) is bounded above by rho.