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

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

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.

theorem ViscositySolns.semiconvexQuadraticObjective_blockFunctionToPointFunction {n : ℕ} (F : BlockPoint n → ℝ) (B : BlockHessian n) (z : Point (n + n)) : semiconvexQuadraticObjective (blockFunctionToPointFunction F) (blockHessianToPointHessian B) z = F ((pointSumEquivBlockPoint n) z) - blockQuadraticModel B ((pointSumEquivBlockPoint n) z)

The quadratic objective on R^(n+n) associated to a reindexed block Hessian is the pullback of the corresponding block-coordinate quadratic objective.

In quantified mathematical form, for every z : R^(n+n),

F(z_block) - (1 / 2) ⟪B z_block, z_block⟫

equals

F(z_block) - (1 / 2) ⟪B_point z, z⟫,

where z_block is the image of z in R^n × R^n and B_point is the matrix B written in R^(n+n) coordinates.

theorem ViscositySolns.isMaxOn_semiconvexQuadraticObjective_blockFunctionToPointFunction {n : ℕ} {F : BlockPoint n → ℝ} {B : BlockHessian n} (hmax : IsMaxOn (fun (q : BlockPoint n) => F q - blockQuadraticModel B q) Set.univ 0) : IsMaxOn (semiconvexQuadraticObjective (blockFunctionToPointFunction F) (blockHessianToPointHessian B)) Set.univ 0

A global maximum of the block-coordinate quadratic objective pulls back to a global maximum of the corresponding objective on R^(n+n).

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

The matrix part of a semiconvex matrix conclusion transported from R^(n+n) to R^n × R^n.

In quantified mathematical form, suppose that SemiconvexMatrixConclusion lambda f B holds on R^(n+n). Then there exists a matrix Z on R^(n+n) such that (0, Z) ∈ \overline J^{2,+}_{R^(n+n)} f(0), and after identifying R^(n+n) with R^n × R^n, the reindexed matrix Z_block satisfies

-lambda [I 0; 0 I] ≤ Z_block ≤ B_block.

theorem ViscositySolns.SemiconvexMatrixLemmaOn.exists_reindexed_block_bounds {n : ℕ} {lambda : ℝ} (hlemma : SemiconvexMatrixLemmaOn lambda) (hlambda : 0 ≤ lambda) {f : Point (n + n) → ℝ} (hf : Continuous f) {B : Hessian (n + n)} (hB : Matrix.IsHermitian B) (hsemi : CoordinateSemiconvexOn lambda Set.univ f) (hmax : IsMaxOn (semiconvexQuadraticObjective f B) Set.univ 0) : ∃ (Z : Hessian (n + n)), { gradient := 0, hessian := Z } ∈ ClosedSuperjet Set.univ f 0 ∧ -lambda • blockDiagonalIdentity n ≤ pointHessianToBlockHessian Z ∧ pointHessianToBlockHessian Z ≤ pointHessianToBlockHessian B

Apply the semiconvex matrix lemma on R^(n+n) and immediately transport its matrix inequalities to block coordinates on R^n × R^n.

In quantified mathematical form, if the semiconvex matrix lemma holds in dimension n + n, if 0 ≤ lambda, if f : R^(n+n) -> R is continuous and semiconvex with constant lambda, and if B is Hermitian and ξ ↦ f ξ - (1 / 2) * ⟪B ξ, ξ⟫ has a maximum at 0, then there exists a matrix Z such that (0, Z) belongs to the closed superjet of f at 0 and

-lambda [I 0; 0 I] ≤ Z_block ≤ B_block.

theorem ViscositySolns.SemiconvexMatrixLemmaOn.exists_reindexed_block_bounds_of_block {n : ℕ} {lambda : ℝ} (hlemma : SemiconvexMatrixLemmaOn lambda) (hlambda : 0 ≤ lambda) {F : BlockPoint n → ℝ} (hF : Continuous F) {B : BlockHessian n} (hB : Matrix.IsHermitian B) (hsemi : BlockCoordinateSemiconvexOn lambda Set.univ F) (hmax : IsMaxOn (fun (q : BlockPoint n) => F q - blockQuadraticModel B q) Set.univ 0) : ∃ (Z : Hessian (n + n)), { gradient := 0, hessian := Z } ∈ ClosedSuperjet Set.univ (blockFunctionToPointFunction F) 0 ∧ -lambda • blockDiagonalIdentity n ≤ pointHessianToBlockHessian Z ∧ pointHessianToBlockHessian Z ≤ B

Apply the semiconvex matrix lemma to a function on R^n × R^n, after writing that function in R^(n+n) coordinates.

In quantified mathematical form, suppose that the semiconvex matrix lemma holds in dimension n + n, that 0 ≤ lambda, that F : R^n × R^n -> R is continuous and satisfies the semiconvexity inequality with constant lambda, that B is Hermitian, and that

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

has a maximum at 0. Then there exists a matrix Z on R^(n+n) such that (0, Z) belongs to the closed superjet at 0 of the function z ↦ F(z_1, z_2), and after writing Z in R^n × R^n coordinates,

-lambda [I 0; 0 I] ≤ Z_block ≤ B.

theorem ViscositySolns.SemiconvexMatrixLemmaOn.regularizedDoubledConvolution_block_bounds {n : ℕ} {epsilon mu : ℝ} (hlemma : SemiconvexMatrixLemmaOn (epsilon⁻¹ + mu)) (hlambda : 0 ≤ 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)) : ∃ (Z : Hessian (n + n)), { gradient := 0, hessian := Z } ∈ ClosedSuperjet Set.univ (blockFunctionToPointFunction (regularizedDoubledConvolution (epsilon⁻¹ + mu) K L (normalizedLeftOfBlockGradient u x0 P) (normalizedRightOfBlockGradient v y0 P))) 0 ∧ -(epsilon⁻¹ + mu) • blockDiagonalIdentity n ≤ pointHessianToBlockHessian Z ∧ pointHessianToBlockHessian Z ≤ A + epsilon • (A * A)

Apply the semiconvex matrix lemma to the compact regularized doubled convolution after translating the doubled maximum point to the origin.

In quantified mathematical form, assume:

• K and L are nonempty compact subsets of R^n;
• u is upper semicontinuous on {x0 + x | x ∈ K};
• v is lower semicontinuous on {y0 + y | y ∈ L};
• (x0, y0) is a maximum point on the translated product set of u(x) - v(y) minus the quadratic polynomial with Hessian A;
• A is symmetric, ε > 0, A ≤ μ [I 0; 0 I], and 0 ≤ ε⁻¹ + μ.

Then the semiconvex matrix lemma applied to

ξ ↦ regularizedDoubledConvolution (ε⁻¹ + μ) K L u_norm v_norm ξ

produces a closed superjet at 0 whose reindexed Hessian lies between -(ε⁻¹ + μ)[I 0; 0 I] and A + ε A^2.