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

The CIL maximum principle for quadratic test functions

This file assembles the compact localization, regularized doubled convolution, and semiconvex matrix theorem into the CIL maximum-principle conclusion for test functions which are represented globally by their quadratic expansion at each base point. The coordinate quadratic penalty is the main intended instance.

theorem ViscositySolns.CILDoubledMaximumPrincipleOn.of_global_doubledQuadraticExpansion {n : ℕ} (hJensen : JensenContactSetPositiveMeasureOnClosedBallTheorem (n + n)) (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} {φ : DoubledPoint n → ℝ} {P : DoubledPoint n → BlockPoint n} {A : DoubledPoint n → BlockHessian n} {μ : DoubledPoint n → ℝ} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v D) (hφ : ∀ (z w : DoubledPoint n), φ w = doubledQuadraticExpansionAt z.1 z.2 (φ z) (P z) (A z) w) (hHerm : ∀ (z : DoubledPoint n), Matrix.IsHermitian (A z)) (hA : ∀ (z : DoubledPoint n), A z ≤ μ z • blockDiagonalIdentity n) (hμ : ∀ (z : DoubledPoint n), 0 ≤ μ z) : CILDoubledMaximumPrincipleOn C D u v φ (fun (z : DoubledPoint n) => blockPointLeft (P z)) (fun (z : DoubledPoint n) => -blockPointRight (P z)) A μ

The CIL two-function maximum principle for a test function which is globally equal to its quadratic expansion at every base point.

In quantified mathematical form, assume:

• u is upper semicontinuous on C;
• v is lower semicontinuous on D;
• the relative topologies on C and D are locally compact;
• for every base point z = (x, y), the function φ satisfies φ(w) = doubledQuadraticExpansionAt x y (φ z) (P z) (A z) w for every w;
• each matrix A z is symmetric;
• A z ≤ μ(z) [I 0; 0 I] and 0 ≤ μ(z).

Then the CIL maximum-principle conclusion holds with first-order components blockPointLeft (P z) and -blockPointRight (P z), Hessian A z, and matrix norm bound μ(z).

theorem ViscositySolns.CILDoubledMaximumPrincipleOn.of_aleksandrov_global_doubledQuadraticExpansion {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} {φ : DoubledPoint n → ℝ} {P : DoubledPoint n → BlockPoint n} {A : DoubledPoint n → BlockHessian n} {μ : DoubledPoint n → ℝ} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v D) (hφ : ∀ (z w : DoubledPoint n), φ w = doubledQuadraticExpansionAt z.1 z.2 (φ z) (P z) (A z) w) (hHerm : ∀ (z : DoubledPoint n), Matrix.IsHermitian (A z)) (hA : ∀ (z : DoubledPoint n), A z ≤ μ z • blockDiagonalIdentity n) (hμ : ∀ (z : DoubledPoint n), 0 ≤ μ z) : CILDoubledMaximumPrincipleOn C D u v φ (fun (z : DoubledPoint n) => blockPointLeft (P z)) (fun (z : DoubledPoint n) => -blockPointRight (P z)) A μ

The CIL two-function maximum principle for globally quadratic test functions follows from the localized Aleksandrov second-differentiability theorem in dimension n + n, because the localized Jensen contact-set theorem has already been proved.

theorem ViscositySolns.CILDoubledMaximumPrincipleOn.of_selectedTwoSidedJets_global_doubledQuadraticExpansion {n : ℕ} (hselected : SelectedTwoSidedJetsForRegularizedDoubledConvolutionTheorem n) {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} {φ : DoubledPoint n → ℝ} {P : DoubledPoint n → BlockPoint n} {A : DoubledPoint n → BlockHessian n} {μ : DoubledPoint n → ℝ} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v D) (hφ : ∀ (z w : DoubledPoint n), φ w = doubledQuadraticExpansionAt z.1 z.2 (φ z) (P z) (A z) w) (hHerm : ∀ (z : DoubledPoint n), Matrix.IsHermitian (A z)) (hA : ∀ (z : DoubledPoint n), A z ≤ μ z • blockDiagonalIdentity n) (hμ : ∀ (z : DoubledPoint n), 0 ≤ μ z) : CILDoubledMaximumPrincipleOn C D u v φ (fun (z : DoubledPoint n) => blockPointLeft (P z)) (fun (z : DoubledPoint n) => -blockPointRight (P z)) A μ

The CIL two-function maximum principle from the selected two-sided-jet theorem.

In quantified mathematical form, this is CILDoubledMaximumPrincipleOn.of_global_doubledQuadraticExpansion with the analytic input replaced by the selected two-sided-jet theorem for the compact regularized doubled convolution.

theorem ViscositySolns.quadraticPenalty_eq_doubledQuadraticExpansionAt {n : ℕ} (α : ℝ) (z w : DoubledPoint n) : quadraticPenalty α w.1 w.2 = doubledQuadraticExpansionAt z.1 z.2 (quadraticPenalty α z.1 z.2) (Matrix.mulVec (comparisonPenaltyBlock α) (doubledPointToBlockPoint z)) (comparisonPenaltyBlock α) w

The coordinate quadratic penalty is equal to its quadratic expansion at every base point.

In quantified mathematical form, for every α, every base point z, and every point w,

quadraticPenalty α w.1 w.2

is equal to the quadratic polynomial at w with value quadraticPenalty α z.1 z.2, first derivative [αI -αI; -αI αI] (z.1, z.2), and Hessian [αI -αI; -αI αI].

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.of_localized_jensen_aleksandrov {n : ℕ} (hJensen : JensenContactSetPositiveMeasureOnClosedBallTheorem (n + n)) (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v D) : QuadraticPenaltyIshiiLemmaOn C D u v

The quadratic-penalty Ishii lemma follows from the localized Jensen and Aleksandrov analytic inputs.

In quantified mathematical form, assume u is upper semicontinuous on C, v is lower semicontinuous on D, and the relative topologies on C and D are locally compact. If the localized Jensen contact-set theorem and the localized Aleksandrov second-differentiability theorem are available in dimension n + n, then for every α > 0 and every local maximum point of

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

relative to C × D, the usual quadratic-penalty Ishii conclusion holds.

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.of_aleksandrov {n : ℕ} (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v D) : QuadraticPenaltyIshiiLemmaOn C D u v

The quadratic-penalty Ishii lemma follows from the localized Aleksandrov second-differentiability theorem in dimension n + n, because the localized Jensen contact-set theorem has already been proved.

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.proof {n : ℕ} {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v D) : QuadraticPenaltyIshiiLemmaOn C D u v

The quadratic-penalty Ishii lemma with the analytic inputs discharged.

theorem ViscositySolns.QuadraticPenaltyIshiiLemmaOn.of_selectedTwoSidedJets {n : ℕ} (hselected : SelectedTwoSidedJetsForRegularizedDoubledConvolutionTheorem n) {C D : Set (Point n)} [LocallyCompactSpace ↑C] [LocallyCompactSpace ↑D] {u v : Point n → ℝ} (hu : UpperSemicontinuousOn u C) (hv : LowerSemicontinuousOn v D) : QuadraticPenaltyIshiiLemmaOn C D u v

The quadratic-penalty Ishii lemma follows from the selected two-sided-jet theorem for compact regularized doubled convolutions.

In quantified mathematical form, assume u is upper semicontinuous on C, v is lower semicontinuous on D, and the relative topologies on C and D are locally compact. If SelectedTwoSidedJetsForRegularizedDoubledConvolutionTheorem n holds, then for every α > 0 and every local maximum point of

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

relative to C × D, the usual quadratic-penalty Ishii conclusion holds.