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

Ishii lemma declarations

This file names the precise quadratic-penalty specialization of the maximum principle. It does not assert Ishii's lemma as a theorem.

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

The statement that (x, y) is a local maximum point of

(x', y') ↦ u x' - v y' - (α / 2) * ∑ i, (x' i - y' i)^2

relative to C × D.

Equations

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

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

Subtracting a constant from the first function preserves quadratic-penalty 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' - (α / 2) * ∑ i, (x' i - y' i)^2, then (x, y) is a local maximum point on C × D of (x', y') ↦ (u x' - δ) - v y' - (α / 2) * ∑ i, (x' i - y' i)^2.

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

Subtracting a constant from the first function does not change quadratic-penalty 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' - (α / 2) * ∑ i, (x' i - y' i)^2 if and only if it is a local maximum point on C × D of (x', y') ↦ u x' - v y' - (α / 2) * ∑ i, (x' i - y' i)^2.

theorem ViscositySolns.hasQuadraticPenaltyLocalMaximumOn_of_isMaxOn_doubledObjective {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} (hxy : (x, y) ∈ C ×ˢ D) (hmax : IsMaxOn (fun (q : DoubledPoint n) => doubledObjective u v α q) (C ×ˢ D) (x, y)) : HasQuadraticPenaltyLocalMaximumOn C D u v α x y

If (x, y) ∈ C × D is a maximum point on C × D of the doubled objective u x - v y - (α / 2) * ∑ i, (x i - y i)^2, then (x, y) satisfies the local maximum hypothesis used in the quadratic Ishii lemma.

theorem ViscositySolns.exists_hasQuadraticPenaltyLocalMaximumOn_of_isCompact {n : ℕ} {K L : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) : ∃ x ∈ K, ∃ y ∈ L, HasQuadraticPenaltyLocalMaximumOn K L u v α x y

If the doubled objective attains a maximum on K × L, then there are x ∈ K and y ∈ L satisfying the local maximum hypothesis used in the quadratic Ishii lemma.

def ViscositySolns.QuadraticPenaltyIshiiLemmaOn {n : ℕ} (C D : Set (Point n)) (u v : Point n → ℝ) : Prop

The theorem-shaped proposition corresponding to Ishii's lemma for the quadratic doubled-variable penalty.

It says that for every α > 0 and every local maximum point (x, y) of u x - v y - (α / 2) * ∑ i, (x i - y i)^2 on C × D, there exist matrices X and Y such that (α • (x - y), X) belongs to the closed superjet of u at x, (α • (x - y), Y) belongs to the closed subjet of v at y, and X, Y satisfy the Ishii block matrix inequality.

Equations

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

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.of_doubledMaximumPrinciple {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} (hMP : ∀ (α : ℝ), 0 < α → DoubledMaximumPrincipleOn C D u v (fun (q : DoubledPoint n) => quadraticPenalty α q.1 q.2) (fun (q : DoubledPoint n) => quadraticPenaltyGradientLeft α q.1 q.2) (fun (q : DoubledPoint n) => -quadraticPenaltyGradientRight α q.1 q.2) fun (q : DoubledPoint n) => QuadraticPenaltyMatrixRelation α q.1 q.2) : QuadraticPenaltyIshiiLemmaOn C D u v

The two-function maximum principle specialized to the quadratic penalty gives the quadratic-penalty Ishii lemma.

In quantified mathematical form, suppose that for every α > 0, every x : Point n, and every y : Point n, whenever (x, y) is a local maximum point on C × D of

(x', y') ↦ u x' - v y' - (α / 2) * ∑ i, (x' i - y' i)^2,

there exist matrices X and Y such that

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

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

and the Ishii block matrix inequality holds. Then QuadraticPenaltyIshiiLemmaOn C D u v.

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.of_quadraticPenaltyCILMaximumPrinciple {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} (hMP : ∀ (α : ℝ), 0 < α → DoubledMaximumPrincipleOn C D u v (fun (q : DoubledPoint n) => quadraticPenalty α q.1 q.2) (fun (q : DoubledPoint n) => quadraticPenaltyGradientLeft α q.1 q.2) (fun (q : DoubledPoint n) => -quadraticPenaltyGradientRight α q.1 q.2) fun (_q : DoubledPoint n) => CILMatrixRelation α⁻¹ (2 * α) (comparisonPenaltyBlock α)) : QuadraticPenaltyIshiiLemmaOn C D u v

The two-function maximum principle with the CIL matrix bounds gives the quadratic-penalty Ishii lemma.

In quantified mathematical form, suppose that for every α > 0, every local maximum point of

(x', y') ↦ u x' - v y' - (α / 2) * ∑ i, (x' i - y' i)^2

has closed semijets satisfying the CIL matrix bounds

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

where A = [α I -α I; -α I α I]. Then the same maximum point satisfies the quadratic-penalty Ishii conclusion.

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.of_quadraticPenaltyCILDoubledMaximumPrinciple {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} (hMP : ∀ (α : ℝ), 0 < α → CILDoubledMaximumPrincipleOn C D u v (fun (q : DoubledPoint n) => quadraticPenalty α q.1 q.2) (fun (q : DoubledPoint n) => quadraticPenaltyGradientLeft α q.1 q.2) (fun (q : DoubledPoint n) => -quadraticPenaltyGradientRight α q.1 q.2) (fun (_q : DoubledPoint n) => comparisonPenaltyBlock α) fun (_q : DoubledPoint n) => 2 * α) : QuadraticPenaltyIshiiLemmaOn C D u v

The CIL two-function maximum principle specialized to the coordinate quadratic penalty gives the quadratic-penalty Ishii lemma.

In quantified mathematical form, suppose that for every α > 0 the CIL two-function maximum principle holds for

φ(x, y) = (α / 2) * ∑ i, (x i - y i)^2,

with the superjet first-order component D_x φ(x, y) = α(x - y), the subjet first-order component -D_y φ(x, y) = α(x - y), Hessian A = [α I -α I; -α I α I], and matrix norm bound 2α. Then QuadraticPenaltyIshiiLemmaOn C D u v.

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.sub_const_left {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {δ : ℝ} (hIshii : QuadraticPenaltyIshiiLemmaOn C D u v) : QuadraticPenaltyIshiiLemmaOn C D (fun (z : Point n) => u z - δ) v

Subtracting a constant from the first function preserves the quadratic-penalty Ishii lemma hypothesis.

In quantified mathematical form, for every real number δ, suppose that for every α > 0 and every (x, y) which is a local maximum point on C × D of (x', y') ↦ u x' - v y' - (α / 2) * ∑ i, (x' i - y' i)^2, the quadratic-penalty Ishii conclusion holds for u and v. Then, for every α > 0 and every (x, y) which is a local maximum point on C × D of (x', y') ↦ (u x' - δ) - v y' - (α / 2) * ∑ i, (x' i - y' i)^2, the quadratic-penalty Ishii conclusion holds for x ↦ u x - δ and v.

theorem ViscositySolns.exists_quadraticPenaltyIshiiConclusion_of_isCompact {n : ℕ} {K L : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} (hIshii : QuadraticPenaltyIshiiLemmaOn K L u v) (hα : 0 < α) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) : ∃ x ∈ K, ∃ y ∈ L, QuadraticPenaltyIshiiConclusion K L u v α x y

Assume QuadraticPenaltyIshiiLemmaOn K L u v. If the doubled objective attains a maximum on K × L, as it does when K and L are nonempty compact sets and u is upper semicontinuous on K while v is lower semicontinuous on L, then there exist x ∈ K and y ∈ L such that QuadraticPenaltyIshiiConclusion K L u v α x y holds.

theorem ViscositySolns.QuadraticPenaltyIshiiConclusion.exists_matrices {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} (h : QuadraticPenaltyIshiiConclusion C D u v α x y) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := quadraticPenaltyGradientLeft α x y, hessian := X } ∈ ClosedSuperjet C u x ∧ { gradient := quadraticPenaltyGradientLeft α x y, hessian := Y } ∈ ClosedSubjet D v y ∧ IshiiMatrixRelation α x y X Y

Unpack QuadraticPenaltyIshiiConclusion into the matrices X and Y.

theorem ViscositySolns.QuadraticPenaltyIshiiConclusion.exists_matrices_with_bounds {n : ℕ} {C D : Set (Point n)} {u v : Point n → ℝ} {α : ℝ} {x y : Point n} (h : QuadraticPenaltyIshiiConclusion C D u v α x y) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := quadraticPenaltyGradientLeft α x y, hessian := X } ∈ ClosedSuperjet C u x ∧ { gradient := quadraticPenaltyGradientLeft α x y, hessian := Y } ∈ ClosedSubjet D v y ∧ IshiiMatrixRelation α x y X Y ∧ -(3 * α) • 1 ≤ X ∧ X ≤ (3 * α) • 1 ∧ -(3 * α) • 1 ≤ Y ∧ Y ≤ (3 * α) • 1

Unpack QuadraticPenaltyIshiiConclusion into matrices X and Y, together with the individual Loewner-order bounds implied by the Ishii block matrix inequality.

In quantified mathematical form, if the quadratic-penalty conclusion holds at (x, y) with parameter α, then there exist matrices X and Y such that (α(x - y), X) belongs to the closed superjet of u at x, (α(x - y), Y) belongs to the closed subjet of v at y, X and Y satisfy the Ishii block matrix inequality, and

-(3α) I ≤ X ≤ 3α I, -(3α) I ≤ Y ≤ 3α I.