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

Matrix inequalities for comparison (BlockStructure)

Part of the block-matrix development used in the doubling-of-variables proof of comparison. Split from MatrixInequalities.lean; see the umbrella module docstring.

@[reducible, inline]

abbrev ViscositySolns.BlockHessian (n : ℕ) : Type

Hessian matrices on the product coordinate space R^n × R^n.

Equations

• ViscositySolns.BlockHessian n = Matrix (Fin n ⊕ Fin n) (Fin n ⊕ Fin n) ℝ

@[reducible, inline]

abbrev ViscositySolns.BlockPoint (n : ℕ) : Type

Coordinate vectors on the product space R^n × R^n.

Equations

• ViscositySolns.BlockPoint n = (Fin n ⊕ Fin n → ℝ)

def ViscositySolns.doubledPointToBlockPoint {n : ℕ} (q : DoubledPoint n) : BlockPoint n

Convert a pair of R^n points into one point of the product coordinate space.

Equations

• ViscositySolns.doubledPointToBlockPoint q = Sum.elim q.1 q.2

def ViscositySolns.pointSumEquivBlockPoint (n : ℕ) : Point (n + n) ≃ BlockPoint n

Identify the product coordinate space R^n × R^n, indexed by Fin n ⊕ Fin n, with the coordinate space indexed by Fin (n + n).

Equations

• ViscositySolns.pointSumEquivBlockPoint n = Equiv.piCongrLeft (fun (x : Fin n ⊕ Fin n) => ℝ) finSumFinEquiv.symm

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_apply {n : ℕ} (z : Point (n + n)) (i : Fin (n + n)) : (pointSumEquivBlockPoint n) z (finSumFinEquiv.symm i) = z i

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_symm_apply {n : ℕ} (z : BlockPoint n) (i : Fin (n + n)) : (pointSumEquivBlockPoint n).symm z i = z (finSumFinEquiv.symm i)

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_apply_inl {n : ℕ} (z : Point (n + n)) (i : Fin n) : (pointSumEquivBlockPoint n) z (Sum.inl i) = z (Fin.castAdd n i)

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_apply_inr {n : ℕ} (z : Point (n + n)) (i : Fin n) : (pointSumEquivBlockPoint n) z (Sum.inr i) = z (Fin.natAdd n i)

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_zero {n : ℕ} : (pointSumEquivBlockPoint n) 0 = 0

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_add {n : ℕ} (x y : Point (n + n)) : (pointSumEquivBlockPoint n) (x + y) = (pointSumEquivBlockPoint n) x + (pointSumEquivBlockPoint n) y

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_sub {n : ℕ} (x y : Point (n + n)) : (pointSumEquivBlockPoint n) (x - y) = (pointSumEquivBlockPoint n) x - (pointSumEquivBlockPoint n) y

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_smul {n : ℕ} (a : ℝ) (x : Point (n + n)) : (pointSumEquivBlockPoint n) (a • x) = a • (pointSumEquivBlockPoint n) x

def ViscositySolns.pointHessianToBlockHessian {n : ℕ} (A : Hessian (n + n)) : BlockHessian n

Reindex a Hessian on R^(n+n) as a block Hessian on R^n × R^n.

Equations

• ViscositySolns.pointHessianToBlockHessian A = Matrix.submatrix A ⇑finSumFinEquiv ⇑finSumFinEquiv

def ViscositySolns.blockHessianToPointHessian {n : ℕ} (A : BlockHessian n) : Hessian (n + n)

Reindex a block Hessian on R^n × R^n as a Hessian on R^(n+n).

Equations

• ViscositySolns.blockHessianToPointHessian A = Matrix.submatrix A ⇑finSumFinEquiv.symm ⇑finSumFinEquiv.symm

@[simp]

theorem ViscositySolns.pointHessianToBlockHessian_apply {n : ℕ} (A : Hessian (n + n)) (i j : Fin n ⊕ Fin n) : pointHessianToBlockHessian A i j = A (finSumFinEquiv i) (finSumFinEquiv j)

@[simp]

theorem ViscositySolns.blockHessianToPointHessian_apply {n : ℕ} (A : BlockHessian n) (i j : Fin (n + n)) : blockHessianToPointHessian A i j = A (finSumFinEquiv.symm i) (finSumFinEquiv.symm j)

@[simp]

theorem ViscositySolns.pointHessianToBlockHessian_blockHessianToPointHessian {n : ℕ} (A : BlockHessian n) : pointHessianToBlockHessian (blockHessianToPointHessian A) = A

@[simp]

theorem ViscositySolns.blockHessianToPointHessian_pointHessianToBlockHessian {n : ℕ} (A : Hessian (n + n)) : blockHessianToPointHessian (pointHessianToBlockHessian A) = A

theorem ViscositySolns.Matrix.IsHermitian.pointHessianToBlockHessian {n : ℕ} {A : Hessian (n + n)} (hA : Matrix.IsHermitian A) : Matrix.IsHermitian (ViscositySolns.pointHessianToBlockHessian A)

Reindexing a Hermitian Hessian on R^(n+n) as a block Hessian on R^n × R^n preserves Hermitian symmetry.

theorem ViscositySolns.Matrix.IsHermitian.blockHessianToPointHessian {n : ℕ} {A : BlockHessian n} (hA : Matrix.IsHermitian A) : Matrix.IsHermitian (ViscositySolns.blockHessianToPointHessian A)

Reindexing a Hermitian block Hessian on R^n × R^n as a Hessian on R^(n+n) preserves Hermitian symmetry.

theorem ViscositySolns.dotProduct_pointSumEquivBlockPoint {n : ℕ} (z w : Point (n + n)) : (pointSumEquivBlockPoint n) z ⬝ᵥ (pointSumEquivBlockPoint n) w = z ⬝ᵥ w

The coordinate reindexing from Point (n + n) to BlockPoint n preserves dot products.

theorem ViscositySolns.pointHessianToBlockHessian_mulVec_pointSumEquivBlockPoint {n : ℕ} (A : Hessian (n + n)) (z : Point (n + n)) : Matrix.mulVec (pointHessianToBlockHessian A) ((pointSumEquivBlockPoint n) z) = (pointSumEquivBlockPoint n) (Matrix.mulVec A z)

Matrix-vector multiplication is preserved by reindexing a Hessian on R^(n+n) as a block Hessian on R^n × R^n.

theorem ViscositySolns.quadraticForm_pointHessianToBlockHessian_pointSumEquivBlockPoint {n : ℕ} (A : Hessian (n + n)) (z : Point (n + n)) : (pointSumEquivBlockPoint n) z ⬝ᵥ Matrix.mulVec (pointHessianToBlockHessian A) ((pointSumEquivBlockPoint n) z) = z ⬝ᵥ Matrix.mulVec A z

The quadratic form of a Hessian is unchanged by the coordinate equivalence between R^(n+n) and R^n × R^n.

def ViscositySolns.blockPointLeft {n : ℕ} (q : BlockPoint n) : Point n

The first coordinate of a point of R^n × R^n.

Equations

• ViscositySolns.blockPointLeft q = q ∘ Sum.inl

def ViscositySolns.blockPointRight {n : ℕ} (q : BlockPoint n) : Point n

The second coordinate of a point of R^n × R^n.

Equations

• ViscositySolns.blockPointRight q = q ∘ Sum.inr

@[simp]

theorem ViscositySolns.blockPointLeft_doubledPointToBlockPoint {n : ℕ} (q : DoubledPoint n) : blockPointLeft (doubledPointToBlockPoint q) = q.1

@[simp]

theorem ViscositySolns.blockPointRight_doubledPointToBlockPoint {n : ℕ} (q : DoubledPoint n) : blockPointRight (doubledPointToBlockPoint q) = q.2

@[simp]

theorem ViscositySolns.doubledPointToBlockPoint_left_right {n : ℕ} (q : BlockPoint n) : doubledPointToBlockPoint (blockPointLeft q, blockPointRight q) = q

theorem ViscositySolns.quadraticForm_mono_of_matrix_le {m : Type u_1} [Fintype m] {A B : Matrix m m ℝ} (hAB : A ≤ B) (z : m → ℝ) : z ⬝ᵥ A.mulVec z ≤ z ⬝ᵥ B.mulVec z

Loewner order implies the corresponding inequality of quadratic forms: if A ≤ B, then for every vector z, z · A z ≤ z · B z.

theorem ViscositySolns.matrix_le_submatrix {m : Type u_1} {k : Type u_2} {A B : Matrix m m ℝ} (hAB : A ≤ B) (e : k → m) : A.submatrix e e ≤ B.submatrix e e

Taking the same principal submatrix on both sides preserves the Loewner order.

theorem ViscositySolns.pointHessianToBlockHessian_mono {n : ℕ} {A B : Hessian (n + n)} (hAB : A ≤ B) : pointHessianToBlockHessian A ≤ pointHessianToBlockHessian B

The coordinate reindexing from R^(n+n) to R^n × R^n preserves the Loewner order.

def ViscositySolns.comparisonBlockDiagonal {n : ℕ} (X Y : Hessian n) : BlockHessian n

The block diagonal matrix [X 0; 0 -Y].

Equations

• ViscositySolns.comparisonBlockDiagonal X Y = Matrix.fromBlocks X 0 0 (-Y)

def ViscositySolns.blockDiagonalIdentity (n : ℕ) : BlockHessian n

The block identity matrix [I 0; 0 I].

Equations

• ViscositySolns.blockDiagonalIdentity n = Matrix.fromBlocks 1 0 0 1

theorem ViscositySolns.blockDiagonalIdentity_eq_one {n : ℕ} : blockDiagonalIdentity n = 1

The block identity matrix is the ordinary identity matrix on Fin n ⊕ Fin n.

theorem ViscositySolns.pointHessianToBlockHessian_one {n : ℕ} : pointHessianToBlockHessian 1 = blockDiagonalIdentity n

The identity matrix on R^(n+n) becomes the block identity matrix on R^n × R^n.

theorem ViscositySolns.pointHessianToBlockHessian_smul_one {n : ℕ} (a : ℝ) : pointHessianToBlockHessian (a • 1) = a • blockDiagonalIdentity n

A scalar multiple of the identity matrix on R^(n+n) becomes the same scalar multiple of the block identity matrix on R^n × R^n.

theorem ViscositySolns.pointHessianToBlockHessian_bounds_of_scalar_identity_bounds {n : ℕ} {a : ℝ} {A B : Hessian (n + n)} (hlower : a • 1 ≤ A) (hupper : A ≤ B) : a • blockDiagonalIdentity n ≤ pointHessianToBlockHessian A ∧ pointHessianToBlockHessian A ≤ pointHessianToBlockHessian B

Reindex the two-sided matrix bounds supplied by the semiconvex matrix theorem from R^(n+n) to R^n × R^n.

In quantified mathematical form, if a I ≤ A ≤ B as matrices on R^(n+n), then, after identifying R^(n+n) with R^n × R^n, a [I 0; 0 I] ≤ A_block ≤ B_block.

def ViscositySolns.comparisonPenaltyBlock {n : ℕ} (α : ℝ) : BlockHessian n

The Hessian matrix of the quadratic penalty (α / 2) * ∑ i, (x i - y i)^2, written in block form.

Equations

• ViscositySolns.comparisonPenaltyBlock α = Matrix.fromBlocks (α • 1) (-α • 1) (-α • 1) (α • 1)

theorem ViscositySolns.comparisonPenaltyBlock_mul_self {n : ℕ} (α : ℝ) : comparisonPenaltyBlock α * comparisonPenaltyBlock α = (2 * α) • comparisonPenaltyBlock α

The square of the Hessian matrix of the coordinate quadratic penalty.

In standard mathematical notation, if

A = [ α I -α I ], [ -α I α I ]

then A^2 = 2α A.

theorem ViscositySolns.comparisonPenaltyBlock_add_inv_smul_mul_self {n : ℕ} {α : ℝ} (hα : α ≠ 0) : comparisonPenaltyBlock α + α⁻¹ • (comparisonPenaltyBlock α * comparisonPenaltyBlock α) = 3 • comparisonPenaltyBlock α

The quadratic-penalty Hessian algebra used in the proof of Ishii's lemma.

In standard mathematical notation, if

A = [ α I -α I ], [ -α I α I ]

and α ≠ 0, then A + α⁻¹ A^2 = 3A.

def ViscositySolns.ishiiLowerBlock {n : ℕ} (α : ℝ) : BlockHessian n

The lower matrix bound -(3 * α) [I 0; 0 I].

Equations

• ViscositySolns.ishiiLowerBlock α = -(3 * α) • ViscositySolns.blockDiagonalIdentity n

def ViscositySolns.ishiiUpperBlock {n : ℕ} (α : ℝ) : BlockHessian n

The upper matrix bound 3 times the Hessian of the quadratic penalty.

Equations

• ViscositySolns.ishiiUpperBlock α = 3 • ViscositySolns.comparisonPenaltyBlock α

def ViscositySolns.IshiiMatrixRelation {n : ℕ} (α : ℝ) (_x _y : Point n) (X Y : Hessian n) : Prop

The matrix relation appearing in the comparison theorem.

For α > 0, matrices X and Y satisfy this relation if [X 0; 0 -Y] lies between the two block matrices displayed at the top of this file. The points x and y are arguments so that this relation can be used as a ComparisonMatrixRelation; the inequality itself does not depend on them.

Equations

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

def ViscositySolns.doubledSameVector {n : ℕ} (z : Fin n → ℝ) : Fin n ⊕ Fin n → ℝ

The vector (z, z) in the product coordinate space R^n × R^n.

Equations

• ViscositySolns.doubledSameVector z = Sum.elim z z

theorem ViscositySolns.IshiiMatrixRelation.quadraticForm_lower {n : ℕ} {α : ℝ} {x y : Point n} {X Y : Hessian n} (h : IshiiMatrixRelation α x y X Y) (z : Fin n ⊕ Fin n → ℝ) : z ⬝ᵥ Matrix.mulVec (ishiiLowerBlock α) z ≤ z ⬝ᵥ Matrix.mulVec (comparisonBlockDiagonal X Y) z

If X and Y satisfy IshiiMatrixRelation α x y X Y, then for every z : Fin n ⊕ Fin n -> Real,

zᵀ (ishiiLowerBlock α) z ≤ zᵀ (comparisonBlockDiagonal X Y) z.

theorem ViscositySolns.IshiiMatrixRelation.quadraticForm_upper {n : ℕ} {α : ℝ} {x y : Point n} {X Y : Hessian n} (h : IshiiMatrixRelation α x y X Y) (z : Fin n ⊕ Fin n → ℝ) : z ⬝ᵥ Matrix.mulVec (comparisonBlockDiagonal X Y) z ≤ z ⬝ᵥ Matrix.mulVec (ishiiUpperBlock α) z

If X and Y satisfy IshiiMatrixRelation α x y X Y, then for every z : Fin n ⊕ Fin n -> Real,

zᵀ (comparisonBlockDiagonal X Y) z ≤ zᵀ (ishiiUpperBlock α) z.

theorem ViscositySolns.comparisonBlockDiagonal_quadratic_doubledSameVector {n : ℕ} (X Y : Hessian n) (z : Fin n → ℝ) : doubledSameVector z ⬝ᵥ Matrix.mulVec (comparisonBlockDiagonal X Y) (doubledSameVector z) = z ⬝ᵥ Matrix.mulVec X z - z ⬝ᵥ Matrix.mulVec Y z

For every vector z : Fin n -> Real, the quadratic form of comparisonBlockDiagonal X Y on (z, z) is zᵀ X z - zᵀ Y z.

theorem ViscositySolns.dotProduct_self_nonneg {m : Type u_1} [Fintype m] (x : m → ℝ) : 0 ≤ x ⬝ᵥ x

The coordinate dot product of a vector with itself is nonnegative.

theorem ViscositySolns.hessian_quadraticForm_le_of_entrywise_abs_le {n : ℕ} (A : Hessian n) {eta : ℝ} (heta : 0 ≤ eta) (hA : ∀ (i j : Fin n), |A i j| ≤ eta) (v : Point n) : Matrix.mulVec A v ⬝ᵥ v ≤ eta * ↑n * ↑n * v ⬝ᵥ v

A finite entrywise bound on a Hessian gives an upper bound for its quadratic form.

In quantified mathematical form, if η ≥ 0 and |Aᵢⱼ| ≤ η for every matrix entry, then for every vector v,

⟪Av, v⟫ ≤ η n^2 ⟪v, v⟫.

theorem ViscositySolns.exists_hessian_le_smul_one_of_isHermitian {n : ℕ} {A : Hessian n} (hA : Matrix.IsHermitian A) : ∃ (mu : ℝ), A ≤ mu • 1

Every real symmetric Hessian is bounded above by a scalar multiple of the identity in the Loewner order.

In quantified mathematical form, for every symmetric matrix A on R^n, there exists μ ∈ R such that A ≤ μ I.

theorem ViscositySolns.exists_blockHessian_le_smul_blockDiagonalIdentity_of_isHermitian {n : ℕ} {A : BlockHessian n} (hA : Matrix.IsHermitian A) : ∃ (mu : ℝ), A ≤ mu • blockDiagonalIdentity n

Every real symmetric block Hessian on R^n × R^n is bounded above by a scalar multiple of the block identity in the Loewner order.

In quantified mathematical form, for every symmetric matrix A on R^n × R^n, there exists μ ∈ R such that

A ≤ μ [I 0; 0 I].

theorem ViscositySolns.dotProduct_le_young {m : Type u_1} [Fintype m] {epsilon : ℝ} (hepsilon : 0 < epsilon) (u v : m → ℝ) : u ⬝ᵥ v ≤ epsilon / 2 * u ⬝ᵥ u + epsilon⁻¹ / 2 * v ⬝ᵥ v

Young's inequality for the coordinate dot product.

In standard mathematical terms, for ε > 0 and finite-coordinate vectors u and v,

⟪u, v⟫ ≤ (ε / 2) * |u|^2 + (ε⁻¹ / 2) * |v|^2.