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

Matrix inequalities for comparison (QuadraticModel)

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

noncomputable def ViscositySolns.blockQuadraticModel {n : ℕ} (A : BlockHessian n) (q : BlockPoint n) : ℝ

The pure quadratic expression associated to a block Hessian on R^n × R^n.

Equations

• ViscositySolns.blockQuadraticModel A q = 1 / 2 * Matrix.mulVec A q ⬝ᵥ q

theorem ViscositySolns.dotProduct_mulVec_comm_of_isHermitian {n : ℕ} {A : BlockHessian n} (hA : Matrix.IsHermitian A) (x y : BlockPoint n) : Matrix.mulVec A x ⬝ᵥ y = Matrix.mulVec A y ⬝ᵥ x

Symmetry of the bilinear form associated to a Hermitian real matrix.

In standard mathematical terms, if A is symmetric, then ⟪Ax, y⟫ = ⟪Ay, x⟫.

theorem ViscositySolns.blockQuadraticModel_add {n : ℕ} {A : BlockHessian n} (hA : Matrix.IsHermitian A) (ξ h : BlockPoint n) : blockQuadraticModel A (ξ + h) = blockQuadraticModel A ξ + Matrix.mulVec A ξ ⬝ᵥ h + blockQuadraticModel A h

Expansion of a Hermitian quadratic form at a translated point.

In standard mathematical terms, if A is symmetric, then for every ξ, h ∈ R^n × R^n,

(1 / 2) * ⟪A(ξ + h), ξ + h⟫ = (1 / 2) * ⟪Aξ, ξ⟫ + ⟪Aξ, h⟫ + (1 / 2) * ⟪Ah, h⟫.

theorem ViscositySolns.blockQuadraticModel_add_smul_mul_self {n : ℕ} {A : BlockHessian n} (hA : Matrix.IsHermitian A) (epsilon : ℝ) (ξ : BlockPoint n) : blockQuadraticModel (A + epsilon • (A * A)) ξ = blockQuadraticModel A ξ + epsilon / 2 * Matrix.mulVec A ξ ⬝ᵥ Matrix.mulVec A ξ

The quadratic form associated to A + ε A^2.

In standard mathematical terms, if A is symmetric, then

(1 / 2) * ⟪(A + ε A^2)ξ, ξ⟫ = (1 / 2) * ⟪Aξ, ξ⟫ + (ε / 2) * |Aξ|^2.

theorem ViscositySolns.blockQuadraticModel_le_of_le_smul_identity {n : ℕ} {A : BlockHessian n} {mu : ℝ} (hA : A ≤ mu • blockDiagonalIdentity n) (h : BlockPoint n) : blockQuadraticModel A h ≤ mu / 2 * h ⬝ᵥ h

A Loewner upper bound by a scalar multiple of the identity gives the corresponding quadratic-form upper bound.

In standard mathematical terms, if A ≤ μ I, then

(1 / 2) * ⟪Ah, h⟫ ≤ (μ / 2) * |h|^2

for every vector h.

theorem ViscositySolns.blockQuadraticModel_le_add_smul_mul_self_add_of_bounds {n : ℕ} {A : BlockHessian n} (hA : Matrix.IsHermitian A) {epsilon mu : ℝ} (hbound : ∀ (h : BlockPoint n), blockQuadraticModel A h ≤ mu / 2 * h ⬝ᵥ h) (hyoung : ∀ (ξ h : BlockPoint n), Matrix.mulVec A ξ ⬝ᵥ h ≤ epsilon / 2 * Matrix.mulVec A ξ ⬝ᵥ Matrix.mulVec A ξ + epsilon⁻¹ / 2 * h ⬝ᵥ h) (z ξ : BlockPoint n) : blockQuadraticModel A z ≤ blockQuadraticModel (A + epsilon • (A * A)) ξ + (epsilon⁻¹ + mu) / 2 * (z - ξ) ⬝ᵥ (z - ξ)

The CIL quadratic comparison estimate, separated from the scalar inequalities used to prove it.

In standard mathematical terms, let A be symmetric. Suppose that

(1 / 2) * ⟪Ah, h⟫ ≤ (μ / 2) * |h|^2

for every h, and suppose that

⟪Aξ, h⟫ ≤ (ε / 2) * |Aξ|^2 + (ε⁻¹ / 2) * |h|^2

for every ξ and h. Then for every z and ξ,

`(1 / 2) * ⟪Az, z⟫ ≤ (1 / 2) * ⟪(A + ε A^2)ξ, ξ⟫

• ((ε⁻¹ + μ) / 2) * |z - ξ|^2`.

theorem ViscositySolns.blockQuadraticModel_le_add_smul_mul_self_add_of_le_smul_identity {n : ℕ} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) {epsilon mu : ℝ} (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (z ξ : BlockPoint n) : blockQuadraticModel A z ≤ blockQuadraticModel (A + epsilon • (A * A)) ξ + (epsilon⁻¹ + mu) / 2 * (z - ξ) ⬝ᵥ (z - ξ)

The CIL quadratic comparison estimate obtained from a Loewner upper bound A ≤ μ I.

In standard mathematical terms, if A is symmetric, ε > 0, and A ≤ μ I, then for every z and ξ,

`(1 / 2) * ⟪Az, z⟫ ≤ (1 / 2) * ⟪(A + ε A^2)ξ, ξ⟫

• ((ε⁻¹ + μ) / 2) * |z - ξ|^2`.

theorem ViscositySolns.blockQuadraticModel_pointHessianToBlockHessian_pointSumEquivBlockPoint {n : ℕ} (A : Hessian (n + n)) (z : Point (n + n)) : blockQuadraticModel (pointHessianToBlockHessian A) ((pointSumEquivBlockPoint n) z) = quadraticModel 0 0 0 A z

The pure quadratic model at the origin is unchanged by the coordinate equivalence between R^(n+n) and R^n × R^n.

theorem ViscositySolns.blockQuadraticModel_comparisonBlockDiagonal_doubledPoint {n : ℕ} (X Y : Hessian n) (q : DoubledPoint n) : blockQuadraticModel (comparisonBlockDiagonal X Y) (doubledPointToBlockPoint q) = quadraticModel 0 0 0 X q.1 - quadraticModel 0 0 0 Y q.2

The quadratic expression of a block diagonal Hessian on R^n × R^n.

In quantified mathematical form, for every x, y : R^n,

1 / 2 * ⟪[X 0; 0 -Y] (x, y), (x, y)⟫ = 1 / 2 * ⟪X x, x⟫ - 1 / 2 * ⟪Y y, y⟫.

theorem ViscositySolns.blockQuadraticModel_comparisonPenaltyBlock_doubledPoint {n : ℕ} (α : ℝ) (q : DoubledPoint n) : blockQuadraticModel (comparisonPenaltyBlock α) (doubledPointToBlockPoint q) = quadraticPenalty α q.1 q.2

The block Hessian of the coordinate quadratic penalty gives the coordinate quadratic penalty.

In quantified mathematical form, for every x, y : R^n,

1 / 2 * ⟪[α I -α I; -α I α I] (x, y), (x, y)⟫ = (α / 2) * ∑ i, (x i - y i)^2.

theorem ViscositySolns.comparisonPenaltyBlock_le_two_smul_blockDiagonalIdentity {n : ℕ} {α : ℝ} (hα : 0 ≤ α) : comparisonPenaltyBlock α ≤ (2 * α) • blockDiagonalIdentity n

The coordinate quadratic-penalty Hessian is bounded above by 2α times the block identity.

In quantified mathematical form, if 0 ≤ α, then

[αI -αI; -αI αI] ≤ 2α [I 0; 0 I]

in the Loewner order.

theorem ViscositySolns.comparisonPenaltyBlock_mulVec_doubledPoint {n : ℕ} (α : ℝ) (q : DoubledPoint n) : Matrix.mulVec (comparisonPenaltyBlock α) (doubledPointToBlockPoint q) = doubledPointToBlockPoint (quadraticPenaltyGradientLeft α q.1 q.2, quadraticPenaltyGradientRight α q.1 q.2)

The first derivative of the coordinate quadratic penalty in block form.

In standard mathematical terms, if

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

then A (x, y) = (α(x - y), -α(x - y)).

theorem ViscositySolns.blockPointLeft_comparisonPenaltyBlock_mulVec_doubledPoint {n : ℕ} (α : ℝ) (q : DoubledPoint n) : blockPointLeft (Matrix.mulVec (comparisonPenaltyBlock α) (doubledPointToBlockPoint q)) = quadraticPenaltyGradientLeft α q.1 q.2

The left component of the first derivative of the coordinate quadratic penalty is α(x - y).

theorem ViscositySolns.blockPointRight_comparisonPenaltyBlock_mulVec_doubledPoint {n : ℕ} (α : ℝ) (q : DoubledPoint n) : blockPointRight (Matrix.mulVec (comparisonPenaltyBlock α) (doubledPointToBlockPoint q)) = quadraticPenaltyGradientRight α q.1 q.2

The right component of the first derivative of the coordinate quadratic penalty is -α(x - y).

theorem ViscositySolns.blockQuadraticModel_ishiiUpperBlock_doubledPoint {n : ℕ} (α : ℝ) (q : DoubledPoint n) : blockQuadraticModel (ishiiUpperBlock α) (doubledPointToBlockPoint q) = 3 * quadraticPenalty α q.1 q.2

The upper Ishii block has quadratic expression equal to three times the coordinate quadratic penalty.

theorem ViscositySolns.comparisonPenaltyBlock_mulVec_doubledSameVector {n : ℕ} (α : ℝ) (z : Fin n → ℝ) : Matrix.mulVec (comparisonPenaltyBlock α) (doubledSameVector z) = 0

For every vector z : Fin n -> Real, the Hessian matrix of (α / 2) * ∑ i, (x i - y i)^2 sends (z, z) to zero.

theorem ViscositySolns.ishiiUpperBlock_quadratic_doubledSameVector {n : ℕ} (α : ℝ) (z : Fin n → ℝ) : doubledSameVector z ⬝ᵥ Matrix.mulVec (ishiiUpperBlock α) (doubledSameVector z) = 0

For every vector z : Fin n -> Real, the quadratic form of the upper Ishii block on (z, z) is zero.

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

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

zᵀ X z ≤ zᵀ Y z.

theorem ViscositySolns.IshiiMatrixRelation.left_le_right {n : ℕ} {α : ℝ} {x y : Point n} {X Y : Hessian n} (h : IshiiMatrixRelation α x y X Y) : X ≤ Y

If X and Y satisfy IshiiMatrixRelation α x y X Y, then X ≤ Y in the Loewner order.

theorem ViscositySolns.IshiiMatrixRelation.left_lower_bound {n : ℕ} {α : ℝ} {x y : Point n} {X Y : Hessian n} (h : IshiiMatrixRelation α x y X Y) : -(3 * α) • 1 ≤ X

The lower Ishii block bound implies -(3 * α) I ≤ X.

theorem ViscositySolns.IshiiMatrixRelation.left_upper_bound {n : ℕ} {α : ℝ} {x y : Point n} {X Y : Hessian n} (h : IshiiMatrixRelation α x y X Y) : X ≤ (3 * α) • 1

The upper Ishii block bound implies X ≤ 3α I.

theorem ViscositySolns.IshiiMatrixRelation.right_lower_bound {n : ℕ} {α : ℝ} {x y : Point n} {X Y : Hessian n} (h : IshiiMatrixRelation α x y X Y) : -(3 * α) • 1 ≤ Y

The upper Ishii block bound implies -(3 * α) I ≤ Y.

theorem ViscositySolns.IshiiMatrixRelation.right_upper_bound {n : ℕ} {α : ℝ} {x y : Point n} {X Y : Hessian n} (h : IshiiMatrixRelation α x y X Y) : Y ≤ (3 * α) • 1

The lower Ishii block bound implies Y ≤ 3α I.

@[simp]

theorem ViscositySolns.comparisonBlockDiagonal_apply_left_left {n : ℕ} (X Y : Hessian n) (i j : Fin n) : comparisonBlockDiagonal X Y (Sum.inl i) (Sum.inl j) = X i j

@[simp]

theorem ViscositySolns.comparisonBlockDiagonal_apply_left_right {n : ℕ} (X Y : Hessian n) (i j : Fin n) : comparisonBlockDiagonal X Y (Sum.inl i) (Sum.inr j) = 0

@[simp]

theorem ViscositySolns.comparisonBlockDiagonal_apply_right_left {n : ℕ} (X Y : Hessian n) (i j : Fin n) : comparisonBlockDiagonal X Y (Sum.inr i) (Sum.inl j) = 0

@[simp]

theorem ViscositySolns.comparisonBlockDiagonal_apply_right_right {n : ℕ} (X Y : Hessian n) (i j : Fin n) : comparisonBlockDiagonal X Y (Sum.inr i) (Sum.inr j) = -Y i j

@[simp]

theorem ViscositySolns.blockDiagonalIdentity_apply_left_left {n : ℕ} (i j : Fin n) : blockDiagonalIdentity n (Sum.inl i) (Sum.inl j) = 1 i j

@[simp]

theorem ViscositySolns.blockDiagonalIdentity_apply_right_right {n : ℕ} (i j : Fin n) : blockDiagonalIdentity n (Sum.inr i) (Sum.inr j) = 1 i j

@[simp]

theorem ViscositySolns.comparisonPenaltyBlock_apply_left_left {n : ℕ} (α : ℝ) (i j : Fin n) : comparisonPenaltyBlock α (Sum.inl i) (Sum.inl j) = (α • 1) i j

@[simp]

theorem ViscositySolns.comparisonPenaltyBlock_apply_left_right {n : ℕ} (α : ℝ) (i j : Fin n) : comparisonPenaltyBlock α (Sum.inl i) (Sum.inr j) = (-α • 1) i j

@[simp]

theorem ViscositySolns.comparisonPenaltyBlock_apply_right_left {n : ℕ} (α : ℝ) (i j : Fin n) : comparisonPenaltyBlock α (Sum.inr i) (Sum.inl j) = (-α • 1) i j

@[simp]

theorem ViscositySolns.comparisonPenaltyBlock_apply_right_right {n : ℕ} (α : ℝ) (i j : Fin n) : comparisonPenaltyBlock α (Sum.inr i) (Sum.inr j) = (α • 1) i j