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

Semiconvexity for compact sup-convolutions

This file records the semiconvexity inequality used in the finite-dimensional maximum-principle proof.

def ViscositySolns.CoordinateSemiconvexOn {n : ℕ} (lambda : ℝ) (C : Set (Point n)) (f : Point n → ℝ) : Prop

The coordinate semiconvexity inequality with constant lambda.

In quantified mathematical form, a function f : R^n -> R satisfies CoordinateSemiconvexOn lambda C f if for every x, y ∈ C and every real numbers a, b with 0 ≤ a, 0 ≤ b, and a + b = 1, whenever a x + b y ∈ C, one has

f (a x + b y) ≤ a f x + b f y + (lambda / 2) a b ∑ i, (x i - y i)^2.

Equations

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

noncomputable def ViscositySolns.semiconvexConvexification {n : ℕ} (lambda : ℝ) (f : Point n → ℝ) : Point n → ℝ

The quadratic function added to a semiconvex function in order to obtain a convex function.

In quantified mathematical form, this is

x ↦ f x + (lambda / 2) * ∑ i, x_i^2.

Equations

• ViscositySolns.semiconvexConvexification lambda f x = f x + ViscositySolns.quadraticModel 0 0 0 (lambda • 1) x

theorem ViscositySolns.quadraticModel_scalar_identity_convex_combination {n : ℕ} (lambda : ℝ) (x y : Point n) {a b : ℝ} (hab : a + b = 1) : quadraticModel 0 0 0 (lambda • 1) (a • x + b • y) + lambda / 2 * a * b * (x - y) ⬝ᵥ (x - y) = a * quadraticModel 0 0 0 (lambda • 1) x + b * quadraticModel 0 0 0 (lambda • 1) y

The quadratic identity used to convert semiconvexity into convexity.

In quantified mathematical form, if a + b = 1, then

Q(a x + b y) + (lambda / 2) a b ∑ i, (x_i - y_i)^2 = a Q(x) + b Q(y),

where Q(x) = (lambda / 2) * ∑ i, x_i^2.

theorem ViscositySolns.quadraticModel_zero_convex_combination {n : ℕ} (B : Hessian n) (x y : Point n) {a b : ℝ} (hab : a + b = 1) : quadraticModel 0 0 0 B (a • x + b • y) = a * quadraticModel 0 0 0 B x + b * quadraticModel 0 0 0 B y - 1 / 2 * a * b * Matrix.mulVec B (x - y) ⬝ᵥ (x - y)

The quadratic identity for an arbitrary Hessian.

In quantified mathematical form, if a + b = 1, then

Q(a x + b y) = a Q(x) + b Q(y) - (1 / 2) a b ⟪B(x - y), x - y⟫,

where Q(x) = (1 / 2) * ⟪B x, x⟫.

theorem ViscositySolns.dotProduct_mulVec_le_entrywise_abs_mul_dotProduct_self {n : ℕ} (B : Hessian n) {eta : ℝ} (heta : 0 ≤ eta) (hB : ∀ (i j : Fin n), |B i j| ≤ eta) (v : Point n) : Matrix.mulVec B v ⬝ᵥ v ≤ eta * ↑n * ↑n * v ⬝ᵥ v

A finite entrywise bound on a Hessian gives a quadratic-form upper bound.

In quantified mathematical form, if η ≥ 0 and |Bᵢⱼ| ≤ η for every matrix entry, then for every vector v,

⟪Bv, v⟫ ≤ η n^2 ⟪v, v⟫.

theorem ViscositySolns.coordinateSemiconvexOn_neg_quadraticModel_of_entrywise_abs_le {n : ℕ} {C : Set (Point n)} (B : Hessian n) {eta : ℝ} (heta : 0 ≤ eta) (hB : ∀ (i j : Fin n), |B i j| ≤ eta) : CoordinateSemiconvexOn (eta * ↑n * ↑n) C fun (x : Point n) => -quadraticModel 0 0 0 B x

The negative of a bounded quadratic form is coordinate semiconvex.

In quantified mathematical form, if η ≥ 0 and |Bᵢⱼ| ≤ η for every matrix entry, then the function

x ↦ - (1 / 2) * ⟪Bx, x⟫

satisfies the coordinate semiconvexity inequality with constant η n^2 on every set.

theorem ViscositySolns.CoordinateSemiconvexOn.convexOn_semiconvexConvexification {n : ℕ} {lambda : ℝ} {C : Set (Point n)} {f : Point n → ℝ} (hsemi : CoordinateSemiconvexOn lambda C f) (hC : Convex ℝ C) : ConvexOn ℝ C (semiconvexConvexification lambda f)

Coordinate semiconvexity implies convexity after adding the quadratic function x ↦ (lambda / 2) * ∑ i, x_i^2.

In quantified mathematical form, if f satisfies the coordinate semiconvexity inequality on C with constant lambda, then x ↦ f x + (lambda / 2) * ∑ i, x_i^2 is convex on C.

theorem ViscositySolns.ConvexOn.coordinateSemiconvexOn_of_semiconvexConvexification {n : ℕ} {lambda : ℝ} {C : Set (Point n)} {f : Point n → ℝ} (hconv : ConvexOn ℝ C (semiconvexConvexification lambda f)) : CoordinateSemiconvexOn lambda C f

Convexity after adding the quadratic function implies coordinate semiconvexity.

In quantified mathematical form, if C is convex and x ↦ f x + (lambda / 2) * ∑ i, x_i^2 is convex on C, then f satisfies the coordinate semiconvexity inequality on C with constant lambda.

theorem ViscositySolns.coordinateSemiconvexOn_iff_convexOn_semiconvexConvexification {n : ℕ} {lambda : ℝ} {C : Set (Point n)} {f : Point n → ℝ} (hC : Convex ℝ C) : CoordinateSemiconvexOn lambda C f ↔ ConvexOn ℝ C (semiconvexConvexification lambda f)

On a convex set, coordinate semiconvexity is equivalent to convexity after adding the quadratic function x ↦ (lambda / 2) * ∑ i, x_i^2.

theorem ViscositySolns.ConvexOn.coordinateSemiconvexOn_zero {n : ℕ} {C : Set (Point n)} {f : Point n → ℝ} (hconv : ConvexOn ℝ C f) : CoordinateSemiconvexOn 0 C f

A convex function is coordinate semiconvex with constant 0.

In quantified mathematical form, if f is convex on C, then for every x, y ∈ C and every a, b ≥ 0 with a + b = 1, whenever a x + b y ∈ C, one has

f (a x + b y) ≤ a f x + b f y.

This is exactly the coordinate semiconvexity inequality with the penalty term equal to 0.

theorem ViscositySolns.CoordinateSemiconvexOn.mono {n : ℕ} {lambda mu : ℝ} {C : Set (Point n)} {f : Point n → ℝ} (hsemi : CoordinateSemiconvexOn lambda C f) (hlambda_mu : lambda ≤ mu) : CoordinateSemiconvexOn mu C f

The coordinate semiconvexity inequality is monotone in the semiconvexity constant.

In quantified mathematical form, if lambda ≤ mu and f satisfies the coordinate semiconvexity inequality with constant lambda, then f satisfies the same inequality with constant mu.

theorem ViscositySolns.CoordinateSemiconvexOn.add {n : ℕ} {lambda mu : ℝ} {C : Set (Point n)} {f g : Point n → ℝ} (hf : CoordinateSemiconvexOn lambda C f) (hg : CoordinateSemiconvexOn mu C g) : CoordinateSemiconvexOn (lambda + mu) C fun (x : Point n) => f x + g x

The sum of two coordinate semiconvex functions is coordinate semiconvex, with constant equal to the sum of the two constants.

In quantified mathematical form, if f satisfies the coordinate semiconvexity inequality with constant lambda on C, and g satisfies it with constant mu on C, then x ↦ f x + g x satisfies it with constant lambda + mu on C.

theorem ViscositySolns.CoordinateSemiconvexOn.mono_set {n : ℕ} {lambda : ℝ} {C D : Set (Point n)} {f : Point n → ℝ} (hsemi : CoordinateSemiconvexOn lambda C f) (hDC : D ⊆ C) : CoordinateSemiconvexOn lambda D f

The coordinate semiconvexity inequality restricts to subsets.

In quantified mathematical form, if D ⊆ C and f satisfies the coordinate semiconvexity inequality on C, then f satisfies the same inequality on D.

theorem ViscositySolns.CoordinateSemiconvexOn.congr {n : ℕ} {lambda : ℝ} {C : Set (Point n)} {f g : Point n → ℝ} (hsemi : CoordinateSemiconvexOn lambda C f) (hfg : ∀ x ∈ C, f x = g x) : CoordinateSemiconvexOn lambda C g

The coordinate semiconvexity inequality is unchanged by replacing a function with an equal function on the set.

In quantified mathematical form, suppose f x = g x for every x ∈ C. If f satisfies the coordinate semiconvexity inequality on C, then g satisfies the same inequality on C.

theorem ViscositySolns.CoordinateSemiconvexOn.continuous_univ {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} (hsemi : CoordinateSemiconvexOn lambda Set.univ f) : Continuous f

Coordinate semiconvexity on all of R^n implies continuity.

In quantified mathematical form, if f : R^n -> R satisfies CoordinateSemiconvexOn lambda Set.univ f, then f is continuous.

theorem ViscositySolns.CoordinateSemiconvexOn.continuousOn_ball_of_closedBall {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} {x0 : Point n} {R : ℝ} (hsemi : CoordinateSemiconvexOn lambda (Metric.closedBall x0 R) f) : ContinuousOn f (Metric.ball x0 R)

Coordinate semiconvexity on a closed ball implies continuity on the corresponding open ball.

In quantified mathematical form, if f : R^n -> R satisfies the coordinate semiconvexity inequality on closedBall x0 R, then f is continuous at each point of ball x0 R, relative to ball x0 R. The proof applies the usual continuity theorem for finite convex functions on open convex sets to x ↦ f x + (lambda / 2) |x|^2, and then subtracts the continuous quadratic function.

theorem ViscositySolns.CoordinateSemiconvexOn.continuousOn_sphere_of_closedBall {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} {x0 : Point n} {r R : ℝ} (hsemi : CoordinateSemiconvexOn lambda (Metric.closedBall x0 R) f) (hrR : r < R) : ContinuousOn f (Metric.sphere x0 r)

Coordinate semiconvexity on a larger closed ball implies continuity on a smaller sphere.

In quantified mathematical form, if f : R^n -> R satisfies the coordinate semiconvexity inequality on closedBall x0 R and r < R, then f is continuous on sphere x0 r.

theorem ViscositySolns.supConvolutionKernel_convex_combination {n : ℕ} (lambda : ℝ) (v : Point n → ℝ) (z ξ ζ : Point n) {a b : ℝ} (hab : a + b = 1) : supConvolutionKernel lambda v (a • ξ + b • ζ) z = a * supConvolutionKernel lambda v ξ z + b * supConvolutionKernel lambda v ζ z + lambda / 2 * a * b * (ξ - ζ) ⬝ᵥ (ξ - ζ)

The quadratic identity behind the semiconvexity of the sup-convolution kernel.

In quantified mathematical form, if a + b = 1, then for every z, ξ, and ζ,

`K(a ξ + b ζ, z) = a K(ξ, z) + b K(ζ, z)

• (lambda / 2) a b ∑ i, (ξ i - ζ i)^2`,

where K(ξ, z) = v z - (lambda / 2) ∑ i, (z i - ξ i)^2.

theorem ViscositySolns.coordinateSemiconvexOn_compactSupConvolution_of_exists_isMaxOn {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} (hmax_exists : ∀ (ξ : Point n), ∃ z ∈ K, IsMaxOn (fun (x : Point n) => supConvolutionKernel lambda v ξ x) K z) : CoordinateSemiconvexOn lambda Set.univ fun (ξ : Point n) => compactSupConvolution lambda K v ξ

Compact sup-convolutions satisfy the coordinate semiconvexity inequality.

In quantified mathematical form, suppose that for every ξ : R^n there exists z ∈ K at which

x ↦ v x - (lambda / 2) * ∑ i, (x i - ξ i)^2

has a maximum on K. Then ξ ↦ compactSupConvolution lambda K v ξ is semiconvex on all of R^n with constant lambda.

theorem ViscositySolns.coordinateSemiconvexOn_compactSupConvolution_of_isCompact {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) : CoordinateSemiconvexOn lambda Set.univ fun (ξ : Point n) => compactSupConvolution lambda K v ξ

Compactness and upper semicontinuity supply the maximum points needed for the semiconvexity of compact sup-convolutions.

In quantified mathematical form, if K is nonempty and compact and v is upper semicontinuous on K, then ξ ↦ compactSupConvolution lambda K v ξ is semiconvex on all of R^n with constant lambda.

theorem ViscositySolns.continuous_compactSupConvolution_of_isCompact {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) : Continuous fun (ξ : Point n) => compactSupConvolution lambda K v ξ

Compact sup-convolutions are continuous.

In quantified mathematical form, if K is a nonempty compact subset of R^n and v is upper semicontinuous on K, then

ξ ↦ sup { v(x) - (lambda / 2) * ∑ i, (x i - ξ i)^2 | x ∈ K }

is continuous on R^n.

theorem ViscositySolns.continuous_compactInfConvolution_of_isCompact {n : ℕ} {K : Set (Point n)} {v : Point n → ℝ} {lambda : ℝ} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : LowerSemicontinuousOn v K) : Continuous fun (ξ : Point n) => compactInfConvolution lambda K v ξ

Compact inf-convolutions are continuous.

In quantified mathematical form, if K is a nonempty compact subset of R^n and v is lower semicontinuous on K, then

ξ ↦ inf { v(x) + (lambda / 2) * ∑ i, (x i - ξ i)^2 | x ∈ K }

is continuous on R^n.

noncomputable def ViscositySolns.semiconvexQuadraticObjective {n : ℕ} (f : Point n → ℝ) (B : Hessian n) : Point n → ℝ

The function whose maximum at the origin is used in the semiconvex matrix lemma.

In quantified mathematical form, for a function f : R^n -> R and a matrix B, this is the function

ξ ↦ f ξ - (1 / 2) * ∑ i, (B ξ i) * ξ i.

Equations

• ViscositySolns.semiconvexQuadraticObjective f B ξ = f ξ - ViscositySolns.quadraticModel 0 0 0 B ξ

theorem ViscositySolns.semiconvexQuadraticObjective_convexification_add_scalar_identity {n : ℕ} (lambda : ℝ) (f : Point n → ℝ) (B : Hessian n) (x : Point n) : semiconvexQuadraticObjective (semiconvexConvexification lambda f) (B + lambda • 1) x = semiconvexQuadraticObjective f B x

Adding the quadratic function used to convexify a semiconvex function changes the quadratic matrix in the same amount.

In quantified mathematical form, for every x : R^n,

`(f x + (lambda / 2) * ∑ i, x_i^2)

• (1 / 2) * ⟪(B + lambda I) x, x⟫ = f x - (1 / 2) * ⟪B x, x⟫`.

theorem ViscositySolns.isMaxOn_semiconvexQuadraticObjective_convexification_add_scalar_identity_iff {n : ℕ} (lambda : ℝ) (f : Point n → ℝ) (B : Hessian n) (C : Set (Point n)) (x : Point n) : IsMaxOn (semiconvexQuadraticObjective (semiconvexConvexification lambda f) (B + lambda • 1)) C x ↔ IsMaxOn (semiconvexQuadraticObjective f B) C x

The maximum hypothesis for the semiconvex function is equivalent to the corresponding maximum hypothesis for its convexification, provided the quadratic matrix is changed from B to B + lambda I.

def ViscositySolns.SemiconvexMatrixConclusion {n : ℕ} (lambda : ℝ) (f : Point n → ℝ) (B : Hessian n) : Prop

The matrix conclusion in the semiconvex part of the finite-dimensional maximum principle.

In quantified mathematical form, SemiconvexMatrixConclusion lambda f B means that there exists a matrix X such that

• (0, X) ∈ \overline J^{2,+}_{R^n} f(0);
• -lambda I ≤ X;
• X ≤ B.

Equations

• ViscositySolns.SemiconvexMatrixConclusion lambda f B = ∃ (X : ViscositySolns.Hessian n), { gradient := 0, hessian := X } ∈ ViscositySolns.ClosedSuperjet Set.univ f 0 ∧ -lambda • 1 ≤ X ∧ X ≤ B

theorem ViscositySolns.closedSuperjet_of_closedSuperjet_semiconvexConvexification_at_zero {n : ℕ} (lambda : ℝ) (f : Point n → ℝ) (Z : Hessian n) (hZ : { gradient := 0, hessian := Z } ∈ ClosedSuperjet Set.univ (semiconvexConvexification lambda f) 0) : { gradient := 0, hessian := Z - lambda • 1 } ∈ ClosedSuperjet Set.univ f 0

Closed superjets at the origin transform under subtraction of the quadratic function used to convexify a semiconvex function.

In quantified mathematical form, if (0, Z) ∈ \overline J^{2,+}_{R^n} (f + lambda |x|^2 / 2)(0), then (0, Z - lambda I) ∈ \overline J^{2,+}_{R^n} f(0).

theorem ViscositySolns.SemiconvexMatrixConclusion.of_convexification_zero {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} {B : Hessian n} (h : SemiconvexMatrixConclusion 0 (semiconvexConvexification lambda f) (B + lambda • 1)) : SemiconvexMatrixConclusion lambda f B

The matrix conclusion for the convexified function with semiconvexity constant 0 implies the matrix conclusion for the original function with semiconvexity constant lambda.

def ViscositySolns.SemiconvexMatrixLemmaOn {n : ℕ} (lambda : ℝ) : Prop

The semiconvex matrix lemma used in the proof of the finite-dimensional maximum principle.

In quantified mathematical form, SemiconvexMatrixLemmaOn lambda says that for every continuous function f : R^n -> R and every Hermitian matrix B, if

• 0 ≤ lambda;
• f satisfies the coordinate semiconvexity inequality on all of R^n with constant lambda;
• ξ ↦ f ξ - (1 / 2) * ∑ i, (B ξ i) * ξ i has a maximum at 0 on all of R^n;

then there exists a matrix X such that (0, X) ∈ \overline J^{2,+}_{R^n} f(0) and -lambda I ≤ X ≤ B.

The proof of this proposition is the Aleksandrov/Jensen part of the Crandall--Ishii--Lions maximum principle.

Equations

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

def ViscositySolns.ConvexifiedSemiconvexMatrixLemmaOn {n : ℕ} (lambda : ℝ) : Prop

The semiconvex matrix lemma in the formulation used in the appendix of the Crandall--Ishii--Lions paper.

In quantified mathematical form, ConvexifiedSemiconvexMatrixLemmaOn lambda says that for every continuous function f : R^n -> R and every Hermitian matrix B, if

• 0 ≤ lambda;
• x ↦ f x + (lambda / 2) * ∑ i, x_i^2 is convex on all of R^n;
• ξ ↦ f ξ - (1 / 2) * ∑ i, (B ξ i) * ξ i has a maximum at 0 on all of R^n;

then there exists a matrix X such that (0, X) ∈ \overline J^{2,+}_{R^n} f(0) and -lambda I ≤ X ≤ B.

Equations

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

theorem ViscositySolns.SemiconvexMatrixLemmaOn.of_convexified {n : ℕ} {lambda : ℝ} (hlemma : ConvexifiedSemiconvexMatrixLemmaOn lambda) : SemiconvexMatrixLemmaOn lambda

The paper's convexity formulation of the semiconvex matrix lemma implies the coordinate-semiconvexity formulation.

theorem ViscositySolns.ConvexifiedSemiconvexMatrixLemmaOn.of_coordinate {n : ℕ} {lambda : ℝ} (hlemma : SemiconvexMatrixLemmaOn lambda) : ConvexifiedSemiconvexMatrixLemmaOn lambda

The coordinate-semiconvexity formulation of the semiconvex matrix lemma implies the paper's convexity formulation.

theorem ViscositySolns.semiconvexMatrixLemmaOn_iff_convexifiedSemiconvexMatrixLemmaOn {n : ℕ} {lambda : ℝ} : SemiconvexMatrixLemmaOn lambda ↔ ConvexifiedSemiconvexMatrixLemmaOn lambda

The coordinate-semiconvexity and convexified formulations of the semiconvex matrix lemma are equivalent.

theorem ViscositySolns.SemiconvexMatrixConclusion.exists_matrix {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} {B : Hessian n} (h : SemiconvexMatrixConclusion lambda f B) : ∃ (X : Hessian n), { gradient := 0, hessian := X } ∈ ClosedSuperjet Set.univ f 0 ∧ -lambda • 1 ≤ X ∧ X ≤ B

Unpack SemiconvexMatrixConclusion into the matrix X and the two matrix inequalities.

theorem ViscositySolns.SemiconvexMatrixLemmaOn.apply {n : ℕ} {lambda : ℝ} (hlemma : SemiconvexMatrixLemmaOn lambda) (hlambda : 0 ≤ lambda) {f : Point n → ℝ} (hf : Continuous f) {B : Hessian n} (hB : Matrix.IsHermitian B) (hsemi : CoordinateSemiconvexOn lambda Set.univ f) (hmax : IsMaxOn (semiconvexQuadraticObjective f B) Set.univ 0) : SemiconvexMatrixConclusion lambda f B

Apply SemiconvexMatrixLemmaOn to a continuous semiconvex function whose quadratic modification has a maximum at the origin.

theorem ViscositySolns.SemiconvexMatrixLemmaOn.apply_of_coordinateSemiconvexOn {n : ℕ} {lambda : ℝ} (hlemma : SemiconvexMatrixLemmaOn lambda) (hlambda : 0 ≤ lambda) {f : Point n → ℝ} {B : Hessian n} (hB : Matrix.IsHermitian B) (hsemi : CoordinateSemiconvexOn lambda Set.univ f) (hmax : IsMaxOn (semiconvexQuadraticObjective f B) Set.univ 0) : SemiconvexMatrixConclusion lambda f B

Apply SemiconvexMatrixLemmaOn using only coordinate semiconvexity on all of R^n.

The continuity hypothesis in SemiconvexMatrixLemmaOn is supplied by CoordinateSemiconvexOn.continuous_univ.

theorem ViscositySolns.SemiconvexMatrixLemmaOn.compactSupConvolution_of_isCompact {n : ℕ} {lambda : ℝ} (hlemma : SemiconvexMatrixLemmaOn lambda) (hlambda : 0 ≤ lambda) {K : Set (Point n)} {v : Point n → ℝ} (hKne : K.Nonempty) (hKcompact : IsCompact K) (hv : UpperSemicontinuousOn v K) {B : Hessian n} (hB : Matrix.IsHermitian B) (hmax : IsMaxOn (semiconvexQuadraticObjective (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) B) Set.univ 0) : SemiconvexMatrixConclusion lambda (fun (ξ : Point n) => compactSupConvolution lambda K v ξ) B

Apply the semiconvex matrix lemma to a compact sup-convolution.

In quantified mathematical form, suppose K is nonempty and compact, v : R^n -> R is upper semicontinuous on K, 0 ≤ lambda, B is Hermitian, and semiconvexQuadraticObjective (ξ ↦ compactSupConvolution lambda K v ξ) B has a maximum at 0 on all of R^n. If SemiconvexMatrixLemmaOn lambda holds, then there exists a matrix X such that

(0, X) ∈ \overline J^{2,+}_{R^n} (ξ ↦ compactSupConvolution lambda K v ξ)(0)

and -lambda I ≤ X ≤ B.