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

Jensen Contact-Set Theorem (MainTheorems)

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.

theorem ViscositySolns.ContinuousExtensionConvexMollificationOnInteriorClosedBallTheorem.proof {n : ℕ} : ContinuousExtensionConvexMollificationOnInteriorClosedBallTheorem n

The continuous-extension convolution theorem.

In quantified mathematical form, suppose 0 < r < R, g is convex on closedBall x0 R, G is continuous on all of R^n, and G = g on closedBall x0 R. Choose rho = (R - r) / 2. The functions

g_m = (jensenMollifierBump n rho _ m).normed volume ⋆ G

converge uniformly to g on closedBall x0 r, are twice continuously differentiable, and are convex on closedBall x0 r.

theorem ViscositySolns.SmoothConvexApproximationOnInteriorClosedBallTheorem.proof {n : ℕ} : SmoothConvexApproximationOnInteriorClosedBallTheorem n

Smooth convex approximation on interior closed balls, obtained by continuous extension and mollification.

def ViscositySolns.JensenSmoothConvexApproximationOnInteriorClosedBallTheorem (n : ℕ) : Prop

The smooth approximation theorem needed for the mollification step in Jensen's lemma.

In quantified mathematical form, this says: if 0 < r, r < R, f : R^n -> R is coordinate semiconvex on closedBall x0 R with nonnegative constant lambda, and f x < f x0 for every x ∈ closedBall x0 r with x ≠ x0, then there are a number gamma > 0 and smooth functions f_m : R^n -> R such that:

• every boundary point of closedBall x0 r satisfies f x ≤ f x0 - gamma;
• f_m -> f uniformly on closedBall x0 r;
• every f_m is twice continuously differentiable;
• every x ↦ f_m x + (lambda / 2) |x|^2 is convex on closedBall x0 r.

This is the exact mollification input from the source proof, separated from the measure-theoretic and semijet arguments.

Equations

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

theorem ViscositySolns.JensenSmoothConvexApproximationOnInteriorClosedBallTheorem.of_smoothConvexApproximation {n : ℕ} (happrox : SmoothConvexApproximationOnInteriorClosedBallTheorem n) : JensenSmoothConvexApproximationOnInteriorClosedBallTheorem n

Smooth convex approximation of the convexified function implies the smooth semiconvex approximation theorem used in Jensen's lemma.

In quantified mathematical form, let g(x) = f(x) + (lambda / 2) |x|^2. If g can be approximated uniformly on closedBall x0 r by twice continuously differentiable functions g_m that are convex on closedBall x0 r, then f_m(x) = g_m(x) - (lambda / 2) |x|^2 approximates f uniformly on closedBall x0 r, each f_m is twice continuously differentiable, and each x ↦ f_m(x) + (lambda / 2) |x|^2 is convex on closedBall x0 r.

theorem ViscositySolns.JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall.of_uniform_approximation {n : ℕ} (hdata : ∀ (f : Point n → ℝ) (x0 : Point n) (r : ℝ), 0 < r → (∃ (lambda : ℝ), CoordinateSemiconvexOn lambda (Metric.closedBall x0 r) f) → (∀ x ∈ Metric.closedBall x0 r, x ≠ x0 → f x < f x0) → ∀ (delta : ℝ), 0 < delta → ∃ (fseq : ℕ → Point n → ℝ) (c : ENNReal), 0 < c ∧ (∀ (eps : ℝ), 0 < eps → ∃ (N : ℕ), ∀ (m : ℕ), N ≤ m → ∀ z ∈ Metric.closedBall x0 r, |fseq m z - f z| ≤ eps) ∧ (∀ (m : ℕ), MeasurableSet (JensenGlobalContactSet (fseq m) x0 r (delta / 2))) ∧ ∀ (m : ℕ), c ≤ MeasureTheory.volume (JensenGlobalContactSet (fseq m) x0 r (delta / 2))) : JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall n

It is enough to construct approximants which converge uniformly on the closed ball and whose closed-ball global contact sets have a common positive lower measure bound.

In quantified mathematical form, suppose that in the situation of JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall, for every delta > 0 there are functions f_m : R^n -> R and a number c > 0 such that:

• for every ε > 0, there exists N such that, for every m ≥ N and every y ∈ closedBall x0 r, |f_m(y) - f(y)| ≤ ε;
• for every m, JensenGlobalContactSet f_m x0 r (delta / 2) is measurable;
• for every m, the measure of JensenGlobalContactSet f_m x0 r (delta / 2) is at least c.

Then the global-contact limsup approximation principle follows.

theorem ViscositySolns.JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall.of_uniform_approximation_tail {n : ℕ} (hdata : ∀ (f : Point n → ℝ) (x0 : Point n) (r : ℝ), 0 < r → (∃ (lambda : ℝ), CoordinateSemiconvexOn lambda (Metric.closedBall x0 r) f) → (∀ x ∈ Metric.closedBall x0 r, x ≠ x0 → f x < f x0) → ∀ (delta : ℝ), 0 < delta → ∃ (N : ℕ) (fseq : ℕ → Point n → ℝ) (c : ENNReal), 0 < c ∧ (∀ (eps : ℝ), 0 < eps → ∃ (M : ℕ), ∀ (m : ℕ), M ≤ m → ∀ z ∈ Metric.closedBall x0 r, |fseq m z - f z| ≤ eps) ∧ (∀ (m : ℕ), N ≤ m → MeasurableSet (JensenGlobalContactSet (fseq m) x0 r (delta / 2))) ∧ ∀ (m : ℕ), N ≤ m → c ≤ MeasureTheory.volume (JensenGlobalContactSet (fseq m) x0 r (delta / 2))) : JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall n

It is enough to prove the uniform-approximation form of the global-contact principle after discarding finitely many approximating functions.

In quantified mathematical form, suppose that in the situation of JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall, for every delta > 0 there are a natural number N, functions f_m : R^n -> R, and a number c > 0 such that:

• for every ε > 0, there exists M such that, for every m ≥ M and every y ∈ closedBall x0 r, |f_m(y) - f(y)| ≤ ε;
• for every m ≥ N, JensenGlobalContactSet f_m x0 r (delta / 2) is measurable;
• for every m ≥ N, the measure of JensenGlobalContactSet f_m x0 r (delta / 2) is at least c.

Then the global-contact limsup approximation principle follows by replacing f_m with the sequence f_{N+m}. This matches the source proof, where the smooth estimates are required only for sufficiently small mollification parameters, equivalently for sufficiently large integer indices.

theorem ViscositySolns.JensenGlobalContactSetInteriorLimsupApproximationPrincipleOnClosedBall.of_smooth_approximation {n : ℕ} (hsmooth : JensenSmoothConvexApproximationOnInteriorClosedBallTheorem n) : JensenGlobalContactSetInteriorLimsupApproximationPrincipleOnClosedBall n

The smooth approximation theorem implies the global-contact approximation principle used to prove Jensen's lemma.

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. If mollification provides smooth functions f_m converging uniformly to f on closedBall x0 r such that, for some nonnegative semiconvexity constant lambda, every x ↦ f_m x + (lambda / 2) |x|^2 is convex on closedBall x0 r, then the smooth closed-ball contact-set estimate applies to all sufficiently large m. Consequently the closed-ball global contact sets for the functions f_m have a common positive lower measure bound, and their limsup is contained in the Jensen contact set of f.

theorem ViscositySolns.JensenContactSetLimsupApproximationPrincipleOnClosedBall.of_eventually {n : ℕ} (hdata : ∀ (f : Point n → ℝ) (x0 : Point n) (r : ℝ), 0 < r → (∃ (lambda : ℝ), CoordinateSemiconvexOn lambda (Metric.closedBall x0 r) f) → (∀ x ∈ Metric.closedBall x0 r, x ≠ x0 → f x < f x0) → ∀ (delta : ℝ), 0 < delta → ∃ (N : ℕ) (fseq : ℕ → Point n → ℝ) (c : ENNReal), 0 < c ∧ (∀ (m : ℕ), N ≤ m → MeasurableSet (JensenContactSet (fseq m) x0 r (delta / 2))) ∧ ⋂ (k : ℕ), ⋃ (m : ℕ), ⋃ (_ : k ≤ m), JensenContactSet (fseq m) x0 r (delta / 2) ⊆ JensenContactSet f x0 r delta ∧ ∀ (m : ℕ), N ≤ m → c ≤ MeasureTheory.volume (JensenContactSet (fseq m) x0 r (delta / 2))) : JensenContactSetLimsupApproximationPrincipleOnClosedBall n

It is enough to prove the approximation principle for all sufficiently large indices.

In quantified mathematical form, suppose that in the situation of JensenContactSetLimsupApproximationPrincipleOnClosedBall, for every delta > 0 there exist a sequence f_m, a natural number N, and a number c > 0 such that the measurability and common lower-measure bound for the contact sets with perturbation radius delta / 2 hold for every m ≥ N, and the limsup of the full sequence is contained in the original contact set with perturbation radius delta. Then the approximation principle follows by replacing f_m with the shifted sequence f_{N+m}.

theorem ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem.of_limsup_approximation {n : ℕ} (happrox : JensenContactSetLimsupApproximationPrincipleOnClosedBall n) : JensenContactSetPositiveMeasureOnClosedBallTheorem n

The nonsmooth approximation principle implies the localized Jensen contact-set theorem.

In quantified mathematical form, if every strict closed-ball maximum satisfying the coordinate semiconvexity hypothesis admits the approximating sequence and uniform positive lower measure bound described in JensenContactSetLimsupApproximationPrincipleOnClosedBall, then the Jensen contact set has positive measure at every strict local maximum.

theorem ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem.of_global_limsup_approximation {n : ℕ} (happrox : JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall n) : JensenContactSetPositiveMeasureOnClosedBallTheorem n

The global-contact approximation principle implies the localized Jensen contact-set theorem.

In quantified mathematical form, if every strict closed-ball maximum satisfying the coordinate semiconvexity hypothesis admits the approximating sequence of closed-ball global contact sets and uniform positive lower measure bound described in JensenGlobalContactSetLimsupApproximationPrincipleOnClosedBall, then the Jensen contact set has positive measure at every strict local maximum.

theorem ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem.of_interior_global_limsup_approximation {n : ℕ} (happrox : JensenGlobalContactSetInteriorLimsupApproximationPrincipleOnClosedBall n) : JensenContactSetPositiveMeasureOnClosedBallTheorem n

The source-aligned interior global-contact approximation principle implies the localized Jensen contact-set theorem.

In quantified mathematical form, assume that the approximation principle is available whenever the contact-set radius r is strictly smaller than a radius R on which the function is semiconvex. If f is semiconvex on closedBall x0 R and has a strict local maximum at x0, choose a positive radius r ≤ R / 2 on which the maximum is strict. Then r < R, so the interior approximation principle gives approximating closed-ball global contact sets on closedBall x0 r with a common positive lower measure bound. The limsup measure lemma gives positive measure for JensenContactSet f x0 r delta, and monotonicity in the radius gives positive measure for JensenContactSet f x0 R delta.

theorem ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem.of_smoothConvexApproximation {n : ℕ} (happrox : SmoothConvexApproximationOnInteriorClosedBallTheorem n) : JensenContactSetPositiveMeasureOnClosedBallTheorem n

Smooth convex approximation on interior closed balls implies the localized Jensen contact-set theorem.

In quantified mathematical form, assume that every convex function on a closed ball closedBall x0 R can be uniformly approximated on each smaller closed ball closedBall x0 r, with 0 < r < R, by twice continuously differentiable functions which are convex on closedBall x0 r. Then Jensen's contact set has positive Lebesgue measure for every semiconvex function with a strict local maximum.

theorem ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem.proof {n : ℕ} : JensenContactSetPositiveMeasureOnClosedBallTheorem n

The localized Jensen contact-set theorem for semiconvex functions.

In quantified mathematical form, if f : R^n -> R is semiconvex in a neighborhood of a strict local maximum point x0, then for every delta > 0 the set of points where some linear perturbation with slope of norm less than delta has a local maximum has positive Lebesgue measure.

theorem ViscositySolns.JensenContactSetPositiveMeasureOnClosedBallTheorem.of_forall_closedBall_strict {n : ℕ} (hsmall : ∀ (f : Point n → ℝ) (x0 : Point n) (r : ℝ), 0 < r → (∃ (lambda : ℝ), CoordinateSemiconvexOn lambda (Metric.closedBall x0 r) f) → (∀ x ∈ Metric.closedBall x0 r, x ≠ x0 → f x < f x0) → ∀ (delta : ℝ), 0 < delta → 0 < MeasureTheory.volume (JensenContactSet f x0 r delta)) : JensenContactSetPositiveMeasureOnClosedBallTheorem n

It suffices to prove the localized Jensen contact-set theorem for closed balls on which the center is strictly larger than every other point.

In quantified mathematical form, suppose that the following statement has been proved: for every f, x0, and r > 0, if f is coordinate semiconvex on closedBall x0 r and f x < f x0 for every x ∈ closedBall x0 r with x ≠ x0, then JensenContactSet f x0 r δ has positive measure for every δ > 0. Then the full localized Jensen contact-set theorem follows for every strict local maximum point.