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

Product-coordinate consequences of the semiconvex matrix lemma (RegularizedConvolution)

Part of the product-coordinate development connecting the semiconvex matrix conclusion on the coordinate space R^(n+n) to the block-matrix notation on R^n × R^n. Split from ProductCoordinates.lean; see the umbrella module docstring.

noncomputable def ViscositySolns.regularizedDoubledConvolution {n : ℕ} (lambda : ℝ) (K L : Set (Point n)) (u v : Point n → ℝ) : BlockPoint n → ℝ

The regularized two-function expression used before applying the semiconvex matrix lemma.

In standard mathematical notation this is

(ξ, η) ↦ sup { u(x) - (lambda / 2) |x - ξ|^2 | x ∈ K } - inf { v(y) + (lambda / 2) |y - η|^2 | y ∈ L }.

Equations

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

theorem ViscositySolns.regularizedDoubledConvolution_eq_sup_add_sup_neg {n : ℕ} {lambda : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} : regularizedDoubledConvolution lambda K L u v = fun (q : BlockPoint n) => compactSupConvolution lambda K u (blockPointLeft q) + compactSupConvolution lambda L (fun (x : Point n) => -v x) (blockPointRight q)

The regularized two-function expression is a sum of two compact sup-convolutions.

theorem ViscositySolns.blockCoordinateSemiconvexOn_regularizedDoubledConvolution_of_isCompact {n : ℕ} {lambda : ℝ} {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) : BlockCoordinateSemiconvexOn lambda Set.univ (regularizedDoubledConvolution lambda K L u v)

The regularized two-function expression is semiconvex on R^n × R^n.

In standard mathematical terms, if K and L are nonempty compact sets, u is upper semicontinuous on K, and v is lower semicontinuous on L, then the function

(ξ, η) ↦ sup_K (u(x) - (lambda / 2)|x - ξ|^2) - inf_L (v(y) + (lambda / 2)|y - η|^2)

satisfies the semiconvexity inequality with constant lambda.

theorem ViscositySolns.continuous_regularizedDoubledConvolution_of_isCompact {n : ℕ} {lambda : ℝ} {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) : Continuous (regularizedDoubledConvolution lambda K L u v)

The regularized two-function expression is continuous on R^n × R^n.

theorem ViscositySolns.closedSemijets_and_blockBounds_of_regularizedDoubledConvolution {n : ℕ} {lambda : ℝ} {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) {Z : Hessian (n + n)} {X Y : Hessian n} {lower upper : BlockHessian n} (hdiag : pointHessianToBlockHessian Z = comparisonBlockDiagonal X Y) (hlower : lower ≤ pointHessianToBlockHessian Z) (hupper : pointHessianToBlockHessian Z ≤ upper) (hJ : { gradient := 0, hessian := Z } ∈ ClosedSuperjet Set.univ (blockFunctionToPointFunction (regularizedDoubledConvolution lambda K L u v)) 0) : { gradient := 0, hessian := X } ∈ ClosedSuperjet Set.univ (fun (ξ : Point n) => compactSupConvolution lambda K u ξ) 0 ∧ { gradient := 0, hessian := Y } ∈ ClosedSubjet Set.univ (fun (η : Point n) => compactInfConvolution lambda L v η) 0 ∧ lower ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ upper

Closed semijets and matrix bounds for a regularized doubled convolution from a selected block diagonal Hessian.

In quantified mathematical form, let K and L be nonempty compact subsets of R^n, let u be upper semicontinuous on K, and let v be lower semicontinuous on L. Suppose (0, Z) belongs to the closed superjet at (0, 0) of

`(ξ, η) ↦ compactSupConvolution lambda K u ξ

• compactInfConvolution lambda L v η`,

and suppose that the block-coordinate form of Z is [X 0; 0 -Y]. If this block-coordinate matrix lies between lower and upper in the Loewner order, then (0, X) belongs to the closed superjet at 0 of the compact sup-convolution of u, (0, Y) belongs to the closed subjet at 0 of the compact inf-convolution of v, and lower ≤ [X 0; 0 -Y] ≤ upper.

theorem ViscositySolns.regularizedDoubledConvolution_eq_kernels_of_isMaxOn_isMinOn {n : ℕ} {lambda : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {ξ η x y : Point n} (hx : x ∈ K) (hy : y ∈ L) (hmax : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda u ξ z) K x) (hmin : IsMinOn (fun (z : Point n) => infConvolutionKernel lambda v η z) L y) : regularizedDoubledConvolution lambda K L u v (doubledPointToBlockPoint (ξ, η)) = supConvolutionKernel lambda u ξ x - infConvolutionKernel lambda v η y

If x is a maximum point for the sup-convolution kernel on K, and y is a minimum point for the inf-convolution kernel on L, then the regularized two-function value at (ξ, η) is the difference between the two selected kernel values.

In quantified mathematical form, if x ∈ K, y ∈ L,

u(z) - (lambda / 2) * |z - ξ|^2 ≤ u(x) - (lambda / 2) * |x - ξ|^2

for every z ∈ K, and

v(y) + (lambda / 2) * |y - η|^2 ≤ v(z) + (lambda / 2) * |z - η|^2

for every z ∈ L, then

regularizedDoubledConvolution lambda K L u v (ξ, η) = supConvolutionKernel lambda u ξ x - infConvolutionKernel lambda v η y.

theorem ViscositySolns.regularizedDoubledConvolution_eq_values_of_isMaxOn_isMinOn {n : ℕ} {lambda : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {ξ η x y : Point n} (hx : x ∈ K) (hy : y ∈ L) (hmax : IsMaxOn (fun (z : Point n) => supConvolutionKernel lambda u ξ z) K x) (hmin : IsMinOn (fun (z : Point n) => infConvolutionKernel lambda v η z) L y) : regularizedDoubledConvolution lambda K L u v (doubledPointToBlockPoint (ξ, η)) = u x - v y - lambda / 2 * (x - ξ) ⬝ᵥ (x - ξ) - lambda / 2 * (y - η) ⬝ᵥ (y - η)

The value identity from regularizedDoubledConvolution_eq_kernels_of_isMaxOn_isMinOn, expanded in terms of u, v, and the two quadratic penalties.

theorem ViscositySolns.regularizedDoubledConvolution_zero_of_pointwise_bound_and_quadratic_control {n : ℕ} {lambda : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {A : BlockHessian n} (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hu0 : u 0 = 0) (hv0 : v 0 = 0) (hbound : ∀ x ∈ K, ∀ y ∈ L, u x - v y ≤ blockQuadraticModel A (doubledPointToBlockPoint (x, y))) (hquad0 : ∀ (z : BlockPoint n), blockQuadraticModel A z ≤ lambda / 2 * z ⬝ᵥ z) : regularizedDoubledConvolution lambda K L u v 0 = 0

The compact regularized doubled convolution has value 0 at the origin when the normalized functions vanish at the origin, the origin belongs to both compact sets, and the quadratic upper bound is dominated by the convolution penalty.

In quantified mathematical form, assume K and L are nonempty compact subsets of R^n, 0 ∈ K, 0 ∈ L, u is upper semicontinuous on K, v is lower semicontinuous on L, u(0) = 0, v(0) = 0, and

u(x) - v(y) ≤ quadratic_A(x, y)

for every x ∈ K and y ∈ L. If, for every z ∈ R^(n+n),

quadratic_A(z) ≤ (lambda / 2) * |z|^2,

then

regularizedDoubledConvolution lambda K L u v 0 = 0.

theorem ViscositySolns.regularizedDoubledConvolution_zero_of_pointwise_bound_and_cil_quadratic {n : ℕ} {epsilon mu : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hu0 : u 0 = 0) (hv0 : v 0 = 0) (hbound : ∀ x ∈ K, ∀ y ∈ L, u x - v y ≤ blockQuadraticModel A (doubledPointToBlockPoint (x, y))) : regularizedDoubledConvolution (epsilon⁻¹ + mu) K L u v 0 = 0

The origin-value normalization in the CIL quadratic estimate.

In quantified mathematical form, suppose A is symmetric, epsilon > 0, and A ≤ mu I. If the normalized functions vanish at 0, the origin belongs to both compact sets, and

u(x) - v(y) ≤ quadratic_A(x, y)

for every x ∈ K and y ∈ L, then the compact regularized doubled convolution with parameter epsilon⁻¹ + mu has value 0 at the origin.

theorem ViscositySolns.regularizedDoubledConvolution_le_blockQuadratic_of_pointwise_bound {n : ℕ} {lambda : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {A B : BlockHessian n} (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) (hbound : ∀ x ∈ K, ∀ y ∈ L, u x - v y ≤ blockQuadraticModel A (doubledPointToBlockPoint (x, y))) (hquad : ∀ (z ξ : BlockPoint n), blockQuadraticModel A z ≤ blockQuadraticModel B ξ + lambda / 2 * (z - ξ) ⬝ᵥ (z - ξ)) (ξ : BlockPoint n) : regularizedDoubledConvolution lambda K L u v ξ ≤ blockQuadraticModel B ξ

Pointwise quadratic bounds pass to the regularized doubled convolution.

In standard mathematical terms, suppose that for every x ∈ K and y ∈ L,

u(x) - v(y) ≤ (1 / 2) * ⟪A (x, y), (x, y)⟫,

and suppose that for every z, ξ ∈ R^n × R^n,

(1 / 2) * ⟪A z, z⟫ ≤ (1 / 2) * ⟪B ξ, ξ⟫ + (lambda / 2) * |z - ξ|^2.

If K and L are nonempty compact sets, u is upper semicontinuous on K, and v is lower semicontinuous on L, then for every ξ ∈ R^n × R^n,

regularizedDoubledConvolution lambda K L u v ξ ≤ (1 / 2) * ⟪B ξ, ξ⟫.

This is the compact real-valued version of the sup-convolution estimate used in the proof of the CIL maximum principle.

theorem ViscositySolns.isMaxOn_sub_blockQuadraticModel_zero_of_le {n : ℕ} {F : BlockPoint n → ℝ} {B : BlockHessian n} (hle : ∀ (ξ : BlockPoint n), F ξ ≤ blockQuadraticModel B ξ) (hzero : F 0 = 0) : IsMaxOn (fun (ξ : BlockPoint n) => F ξ - blockQuadraticModel B ξ) Set.univ 0

An upper bound by a quadratic form gives a maximum of the difference at the origin, provided equality holds at the origin.

In standard mathematical terms, if F(ξ) ≤ (1 / 2) * ⟪B ξ, ξ⟫ for every ξ ∈ R^n × R^n, and F(0) = 0, then

ξ ↦ F(ξ) - (1 / 2) * ⟪B ξ, ξ⟫

has a maximum at 0.

theorem ViscositySolns.isMaxOn_regularizedDoubledConvolution_sub_blockQuadratic_of_pointwise_bound {n : ℕ} {lambda : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {A B : BlockHessian n} (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) (hbound : ∀ x ∈ K, ∀ y ∈ L, u x - v y ≤ blockQuadraticModel A (doubledPointToBlockPoint (x, y))) (hquad : ∀ (z ξ : BlockPoint n), blockQuadraticModel A z ≤ blockQuadraticModel B ξ + lambda / 2 * (z - ξ) ⬝ᵥ (z - ξ)) (hzero : regularizedDoubledConvolution lambda K L u v 0 = 0) : IsMaxOn (fun (ξ : BlockPoint n) => regularizedDoubledConvolution lambda K L u v ξ - blockQuadraticModel B ξ) Set.univ 0

The compact regularized doubled convolution satisfies the maximum condition used before applying the semiconvex matrix lemma, once the pointwise quadratic bound and the quadratic comparison estimate have been proved.

In standard mathematical terms, under the hypotheses of regularizedDoubledConvolution_le_blockQuadratic_of_pointwise_bound, if the regularized doubled convolution has value 0 at the origin, then

ξ ↦ regularizedDoubledConvolution lambda K L u v ξ - (1 / 2) * ⟪B ξ, ξ⟫

has a maximum at 0.

theorem ViscositySolns.isMaxOn_regularizedDoubledConvolution_sub_cilQuadratic_of_pointwise_bound {n : ℕ} {epsilon mu : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u K) (hv : LowerSemicontinuousOn v L) (hbound : ∀ x ∈ K, ∀ y ∈ L, u x - v y ≤ blockQuadraticModel A (doubledPointToBlockPoint (x, y))) (hzero : regularizedDoubledConvolution (epsilon⁻¹ + mu) K L u v 0 = 0) : IsMaxOn (fun (ξ : BlockPoint n) => regularizedDoubledConvolution (epsilon⁻¹ + mu) K L u v ξ - blockQuadraticModel (A + epsilon • (A * A)) ξ) Set.univ 0

The compact regularized doubled convolution satisfies the maximum condition with the CIL quadratic matrix A + ε A^2.

In standard mathematical terms, assume that A is symmetric, ε > 0, and A ≤ μ I. If the localized functions satisfy

u(x) - v(y) ≤ (1 / 2) * ⟪A(x, y), (x, y)⟫

on K × L, and if the regularized doubled convolution with parameter ε⁻¹ + μ has value 0 at the origin, then

ξ ↦ regularizedDoubledConvolution (ε⁻¹ + μ) K L u v ξ - (1 / 2) * ⟪(A + ε A^2)ξ, ξ⟫

has a maximum at 0.

theorem ViscositySolns.isMaxOn_regularizedDoubledConvolution_normalized_sub_cilQuadratic_of_isMaxOn_expansion {n : ℕ} {epsilon mu : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn (normalizedLeftOfBlockGradient u x0 P) K) (hv : LowerSemicontinuousOn (normalizedRightOfBlockGradient v y0 P) L) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) (hzero : regularizedDoubledConvolution (epsilon⁻¹ + mu) K L (normalizedLeftOfBlockGradient u x0 P) (normalizedRightOfBlockGradient v y0 P) 0 = 0) : IsMaxOn (fun (ξ : BlockPoint n) => regularizedDoubledConvolution (epsilon⁻¹ + mu) K L (normalizedLeftOfBlockGradient u x0 P) (normalizedRightOfBlockGradient v y0 P) ξ - blockQuadraticModel (A + epsilon • (A * A)) ξ) Set.univ 0

The translated and affine-normalized form of the regularized maximum condition used in the CIL proof.

In standard mathematical terms, suppose (x0, y0) is a maximum on the translated compact set {(x0 + x, y0 + y) | x ∈ K, y ∈ L} of the doubled difference minus the quadratic expansion with value φ0, gradient P, and Hessian A. If A is symmetric, ε > 0, A ≤ μI, and the normalized compact regularization has value 0 at the origin, then subtracting quadratic_{A + εA^2} from that regularization gives a function with a maximum at the origin.

theorem ViscositySolns.isMaxOn_regularizedDoubledConvolution_normalized_sub_cilQuadratic_of_mem_zero {n : ℕ} {epsilon mu : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn (normalizedLeftOfBlockGradient u x0 P) K) (hv : LowerSemicontinuousOn (normalizedRightOfBlockGradient v y0 P) L) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : IsMaxOn (fun (ξ : BlockPoint n) => regularizedDoubledConvolution (epsilon⁻¹ + mu) K L (normalizedLeftOfBlockGradient u x0 P) (normalizedRightOfBlockGradient v y0 P) ξ - blockQuadraticModel (A + epsilon • (A * A)) ξ) Set.univ 0

The normalized regularized maximum condition without an additional origin-value hypothesis.

In standard mathematical terms, if the translated compact sets contain the origin and the normalized functions vanish at the origin, then the value 0 of the compact regularized doubled convolution at the origin follows from the maximum inequality and the CIL quadratic estimate.

theorem ViscositySolns.isMaxOn_regularizedDoubledConvolution_normalized_sub_cilQuadratic_of_isMaxOn_expansion' {n : ℕ} {epsilon mu : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) (hzero : regularizedDoubledConvolution (epsilon⁻¹ + mu) K L (normalizedLeftOfBlockGradient u x0 P) (normalizedRightOfBlockGradient v y0 P) 0 = 0) : IsMaxOn (fun (ξ : BlockPoint n) => regularizedDoubledConvolution (epsilon⁻¹ + mu) K L (normalizedLeftOfBlockGradient u x0 P) (normalizedRightOfBlockGradient v y0 P) ξ - blockQuadraticModel (A + epsilon • (A * A)) ξ) Set.univ 0

The previous theorem, with semicontinuity hypotheses stated for the original functions on the translated compact neighborhoods.

In standard mathematical terms, upper semicontinuity of u on {x0 + x | x ∈ K} and lower semicontinuity of v on {y0 + y | y ∈ L} imply the corresponding semicontinuity hypotheses for the translated affine-normalized functions on K and L.

theorem ViscositySolns.isMaxOn_regularizedDoubledConvolution_normalized_sub_cilQuadratic_of_translated_mem_zero {n : ℕ} {epsilon mu : ℝ} {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : IsMaxOn (fun (ξ : BlockPoint n) => regularizedDoubledConvolution (epsilon⁻¹ + mu) K L (normalizedLeftOfBlockGradient u x0 P) (normalizedRightOfBlockGradient v y0 P) ξ - blockQuadraticModel (A + epsilon • (A * A)) ξ) Set.univ 0

The translated-neighborhood version of the normalized regularized maximum condition without an additional origin-value hypothesis.

In standard mathematical terms, if u and v are semicontinuous on the translated compact neighborhoods, if those neighborhoods contain the base points after translation, and if (x0, y0) is the maximum point of the doubled difference minus the quadratic expansion, then the regularized maximum condition follows directly.