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

Declarations for the finite-dimensional maximum principle

This file contains declarations used to state the maximum principle for semicontinuous functions. It does not assert the maximum principle as a theorem.

The intended mathematical statement is: if (x, y) is a local maximum point of (x', y') ↦ u x' - v y' - φ (x', y') on C × D, then there exist matrices X and Y such that the jet with gradient p and Hessian X belongs to the closed superjet of u at x, the jet with gradient q and Hessian Y belongs to the closed subjet of v at y, and the matrices X and Y satisfy the matrix inequality supplied by the maximum principle.

def ViscositySolns.HasDoubledLocalMaximumOn {n : ℕ} (C D : Set (Point n)) (u v : Point n → ℝ) (φ : DoubledPoint n → ℝ) (x y : Point n) : Prop

The statement that (x, y) ∈ C × D is a local maximum point of (x', y') ↦ u x' - v y' - φ (x', y') relative to C × D.

Equations

• ViscositySolns.HasDoubledLocalMaximumOn C D u v φ x y = ((x, y) ∈ C ×ˢ D ∧ IsLocalMaxOn (fun (q : ViscositySolns.DoubledPoint n) => u q.1 - v q.2 - φ q) (C ×ˢ D) (x, y))

def ViscositySolns.BlockMatrixRelation {n : ℕ} (lower upper : BlockHessian n) : Hessian n → Hessian n → Prop

The block matrix relation

lower ≤ [X 0; 0 -Y] ≤ upper.

This is the matrix part of the two-function maximum principle. In the theorem from the paper, lower is -((1 / ε) + ‖A‖) I, upper is A + ε A^2, and A is the Hessian of the twice continuously differentiable test function at the local maximum point.

Equations

• ViscositySolns.BlockMatrixRelation lower upper X Y = (lower ≤ ViscositySolns.comparisonBlockDiagonal X Y ∧ ViscositySolns.comparisonBlockDiagonal X Y ≤ upper)

def ViscositySolns.CILMatrixRelation {n : ℕ} (epsilon matrixNormBound : ℝ) (A : BlockHessian n) : Hessian n → Hessian n → Prop

The matrix relation appearing in CIL Theorem 3.2.

In standard mathematical terms, if A is the Hessian of the test function at the doubled maximum point, ε > 0, and μ is the matrix norm bound used in the theorem, then the conclusion is

-((ε⁻¹) + μ) I ≤ [X 0; 0 -Y] ≤ A + ε A^2.

Equations

• ViscositySolns.CILMatrixRelation epsilon matrixNormBound A = ViscositySolns.BlockMatrixRelation (-(epsilon⁻¹ + matrixNormBound) • ViscositySolns.blockDiagonalIdentity n) (A + epsilon • (A * A))

theorem ViscositySolns.HasDoubledLocalMaximumOn.sub_const_left {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {φ : DoubledPoint n → ℝ} {x y : Point n} {δ : ℝ} (h : HasDoubledLocalMaximumOn C D u v φ x y) : HasDoubledLocalMaximumOn C D (fun (z : Point n) => u z - δ) v φ x y

Subtracting a constant from the first function preserves doubled local maximum points.

In quantified mathematical form, for every real number δ, if (x, y) is a local maximum point on C × D of (x', y') ↦ u x' - v y' - φ (x', y'), then (x, y) is a local maximum point on C × D of (x', y') ↦ (u x' - δ) - v y' - φ (x', y').

theorem ViscositySolns.hasDoubledLocalMaximumOn_sub_const_left_iff {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {φ : DoubledPoint n → ℝ} {x y : Point n} {δ : ℝ} : HasDoubledLocalMaximumOn C D (fun (z : Point n) => u z - δ) v φ x y ↔ HasDoubledLocalMaximumOn C D u v φ x y

Subtracting a constant from the first function does not change doubled local maximum points.

In quantified mathematical form, for every real number δ, (x, y) is a local maximum point on C × D of (x', y') ↦ (u x' - δ) - v y' - φ (x', y') if and only if it is a local maximum point on C × D of (x', y') ↦ u x' - v y' - φ (x', y').

structure ViscositySolns.ClosedSemijetPairWithMatrixRelation {n : ℕ} (C D : Set (Point n)) (u v : Point n → ℝ) (x y p q : Point n) (matrixRel : Hessian n → Hessian n → Prop) : Type

The conclusion produced by the maximum principle at a fixed point (x, y).

The fields assert the existence of matrices X and Y such that:

• (p, X) belongs to the closed superjet of u at x relative to C;
• (q, Y) belongs to the closed subjet of v at y relative to D;
• X and Y satisfy the matrix relation specified by the caller.

• X : Hessian n

  The Hessian in the closed superjet of the first function.

• Y : Hessian n

  The Hessian in the closed subjet of the second function.

• superjet_mem : { gradient := p, hessian := self.X } ∈ ClosedSuperjet C u x
• subjet_mem : { gradient := q, hessian := self.Y } ∈ ClosedSubjet D v y
• matrix_relation : matrixRel self.X self.Y

def ViscositySolns.ClosedSemijetPairWithMatrixRelation.subConstLeft {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {x y p q : Point n} {matrixRel : Hessian n → Hessian n → Prop} {δ : ℝ} (h : ClosedSemijetPairWithMatrixRelation C D u v x y p q matrixRel) : ClosedSemijetPairWithMatrixRelation C D (fun (z : Point n) => u z - δ) v x y p q matrixRel

Subtracting a constant from the first function preserves a closed-semijet pair with a fixed matrix relation.

In quantified mathematical form, for every real number δ, if there exist matrices X and Y such that (p, X) ∈ \bar J^{2,+}_C u(x), (q, Y) ∈ \bar J^{2,-}_D v(y), and matrixRel X Y, then the same matrices satisfy (p, X) ∈ \bar J^{2,+}_C (u - δ)(x), (q, Y) ∈ \bar J^{2,-}_D v(y), and matrixRel X Y.

Equations

• h.subConstLeft = { X := h.X, Y := h.Y, superjet_mem := ⋯, subjet_mem := ⋯, matrix_relation := ⋯ }

def ViscositySolns.MaximumPrincipleConclusion {n : ℕ} (C D : Set (Point n)) (u v : Point n → ℝ) (x y p q : Point n) (matrixRel : Hessian n → Hessian n → Prop) : Prop

A precise predicate for the conclusion of the maximum principle from a doubled local maximum.

This is a declaration, not a proved theorem. A future theorem will prove this predicate under the hypotheses of the finite-dimensional maximum principle.

Equations

• ViscositySolns.MaximumPrincipleConclusion C D u v x y p q matrixRel = Nonempty (ViscositySolns.ClosedSemijetPairWithMatrixRelation C D u v x y p q matrixRel)

def ViscositySolns.DoubledMaximumPrincipleOn {n : ℕ} (C D : Set (Point n)) (u v : Point n → ℝ) (φ : DoubledPoint n → ℝ) (p q : DoubledPoint n → Point n) (matrixRel : DoubledPoint n → Hessian n → Hessian n → Prop) : Prop

The two-function maximum-principle theorem-shaped proposition.

In quantified mathematical form, this says: for every x ∈ C and y ∈ D, if (x, y) is a local maximum point, relative to C × D, of

(x', y') ↦ u x' - v y' - φ (x', y'),

then there exist symmetric matrices X and Y such that

(p x y, X) ∈ \bar J^{2,+}_C u(x),

(q x y, Y) ∈ \bar J^{2,-}_D v(y),

and matrixRel x y X Y.

For an actual C^2 test function φ, the intended choices are p x y = D_x φ(x, y), q x y = -D_y φ(x, y), and matrixRel x y is the block inequality obtained from D^2 φ(x, y).

Equations

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

def ViscositySolns.CILDoubledMaximumPrincipleOn {n : ℕ} (C D : Set (Point n)) (u v : Point n → ℝ) (φ : DoubledPoint n → ℝ) (p q : DoubledPoint n → Point n) (A : DoubledPoint n → BlockHessian n) (matrixNormBound : DoubledPoint n → ℝ) : Prop

The two-function maximum-principle theorem-shaped proposition with the matrix bounds from CIL Theorem 3.2.

In quantified mathematical form, this says: for every ε > 0, every local maximum point (x, y) of

(x', y') ↦ u x' - v y' - φ (x', y')

has closed semijets with first-order components p (x, y) and q (x, y), and with matrices X and Y satisfying

-((ε⁻¹) + μ(x, y)) I ≤ [X 0; 0 -Y] ≤ A(x, y) + ε A(x, y)^2.

Here A(x, y) is the Hessian matrix of φ at (x, y) in block form, and μ(x, y) is the corresponding matrix norm bound used in the CIL statement.

Equations

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

theorem ViscositySolns.MaximumPrincipleConclusion.sub_const_left {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {x y p q : Point n} {matrixRel : Hessian n → Hessian n → Prop} {δ : ℝ} (h : MaximumPrincipleConclusion C D u v x y p q matrixRel) : MaximumPrincipleConclusion C D (fun (z : Point n) => u z - δ) v x y p q matrixRel

Subtracting a constant from the first function preserves the conclusion of the maximum principle.

In quantified mathematical form, for every real number δ, if the maximum principle conclusion holds for u and v at (x, y), with gradients p, q, and matrix relation matrixRel, then the same conclusion holds for x ↦ u x - δ and v.

theorem ViscositySolns.DoubledMaximumPrincipleOn.sub_const_left {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {φ : DoubledPoint n → ℝ} {p q : DoubledPoint n → Point n} {matrixRel : DoubledPoint n → Hessian n → Hessian n → Prop} {δ : ℝ} (hMP : DoubledMaximumPrincipleOn C D u v φ p q matrixRel) : DoubledMaximumPrincipleOn C D (fun (z : Point n) => u z - δ) v φ p q matrixRel

Subtracting a constant from the first function preserves the two-function maximum-principle theorem-shaped proposition.

In quantified mathematical form, for every real number δ, suppose that for every local maximum point of (x', y') ↦ u x' - v y' - φ (x', y') on C × D, the maximum-principle conclusion holds. Then for every local maximum point of (x', y') ↦ (u x' - δ) - v y' - φ (x', y') on C × D, the corresponding maximum-principle conclusion holds for x ↦ u x - δ and v.

theorem ViscositySolns.MaximumPrincipleConclusion.exists_matrices {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {x y p q : Point n} {matrixRel : Hessian n → Hessian n → Prop} (h : MaximumPrincipleConclusion C D u v x y p q matrixRel) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := p, hessian := X } ∈ ClosedSuperjet C u x ∧ { gradient := q, hessian := Y } ∈ ClosedSubjet D v y ∧ matrixRel X Y

Unpack MaximumPrincipleConclusion into matrices X and Y.

def ViscositySolns.QuadraticPenaltyMatrixRelation {n : ℕ} (α : ℝ) (x y : Point n) : Hessian n → Hessian n → Prop

The matrix relation in the quadratic-penalty case: X and Y satisfy the block inequalities -(3 * α) [I 0; 0 I] ≤ [X 0; 0 -Y] ≤ 3 [α I -α I; -α I α I].

Equations

• ViscositySolns.QuadraticPenaltyMatrixRelation α x y X Y = ViscositySolns.IshiiMatrixRelation α x y X Y

theorem ViscositySolns.CILMatrixRelation.quadraticPenalty_of_pos {n : ℕ} {α : ℝ} (hα : 0 < α) {x y : Point n} {X Y : Hessian n} (h : CILMatrixRelation α⁻¹ (2 * α) (comparisonPenaltyBlock α) X Y) : QuadraticPenaltyMatrixRelation α x y X Y

The CIL matrix relation specializes to the Ishii matrix relation for the coordinate quadratic penalty.

In standard mathematical terms, for A = [α I -α I; -α I α I], the identities A^2 = 2α A and A + α⁻¹ A^2 = 3A convert

-((α⁻¹)⁻¹ + 2α) I ≤ [X 0; 0 -Y] ≤ A + α⁻¹ A^2

into

-3α I ≤ [X 0; 0 -Y] ≤ 3A.

def ViscositySolns.QuadraticPenaltyIshiiConclusion {n : ℕ} (C D : Set (Point n)) (u v : Point n → ℝ) (α : ℝ) (x y : Point n) : Prop

The conclusion of Ishii's lemma for the quadratic penalty (α / 2) * ∑ i, (x i - y i)^2, expressed through closed semijets.

Equations

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

theorem ViscositySolns.QuadraticPenaltyIshiiConclusion.sub_const_left {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} {δ : ℝ} (h : QuadraticPenaltyIshiiConclusion C D u v α x y) : QuadraticPenaltyIshiiConclusion C D (fun (z : Point n) => u z - δ) v α x y

Subtracting a constant from the first function preserves the quadratic-penalty conclusion of Ishii's lemma.

In quantified mathematical form, for every real number δ, if the quadratic-penalty conclusion holds for u and v at (x, y) with parameter α, then the same conclusion holds for x ↦ u x - δ and v.