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

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

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.exists_isMaxOn_mem_nhdsWithin_of_isLocalMaxOn {α : Type u_1} {β : Type u_2} [TopologicalSpace α] [Preorder β] {f : α → β} {S : Set α} {a : α} (ha : a ∈ S) (hlocal : IsLocalMaxOn f S a) : ∃ P ∈ nhdsWithin a S, a ∈ P ∧ P ⊆ S ∧ IsMaxOn f P a

A local maximum on a set is a maximum on a smaller relative neighborhood.

In quantified mathematical form, if a ∈ S and a is a local maximum point of f relative to S, then there is a set P such that P is a neighborhood of a relative to S, a ∈ P, P ⊆ S, and a is a maximum point of f on P.

def ViscositySolns.blockFunctionToPointFunction {n : ℕ} (F : BlockPoint n → ℝ) : Point (n + n) → ℝ

View a function on R^n × R^n as a function on the coordinate space R^(n+n).

Equations

• ViscositySolns.blockFunctionToPointFunction F z = F ((ViscositySolns.pointSumEquivBlockPoint n) z)

theorem ViscositySolns.continuous_pointSumEquivBlockPoint {n : ℕ} : Continuous ⇑(pointSumEquivBlockPoint n)

The coordinate map from R^(n+n) to R^n × R^n is continuous.

def ViscositySolns.leftBlockPoint {n : ℕ} (x : Point n) : BlockPoint n

The point (x, 0) in the product coordinate space R^n × R^n.

Equations

• ViscositySolns.leftBlockPoint x = Sum.elim x 0

def ViscositySolns.rightBlockPoint {n : ℕ} (y : Point n) : BlockPoint n

The point (0, y) in the product coordinate space R^n × R^n.

Equations

• ViscositySolns.rightBlockPoint y = Sum.elim 0 y

def ViscositySolns.leftPointEmbedding {n : ℕ} (x : Point n) : Point (n + n)

The point (x, 0), written in R^(n+n) coordinates.

Equations

• ViscositySolns.leftPointEmbedding x = (ViscositySolns.pointSumEquivBlockPoint n).symm (ViscositySolns.leftBlockPoint x)

def ViscositySolns.rightPointEmbedding {n : ℕ} (y : Point n) : Point (n + n)

The point (0, y), written in R^(n+n) coordinates.

Equations

• ViscositySolns.rightPointEmbedding y = (ViscositySolns.pointSumEquivBlockPoint n).symm (ViscositySolns.rightBlockPoint y)

def ViscositySolns.pointLeft {n : ℕ} (z : Point (n + n)) : Point n

The left R^n coordinate of a point of R^(n+n) = R^n × R^n.

Equations

• ViscositySolns.pointLeft z = ViscositySolns.blockPointLeft ((ViscositySolns.pointSumEquivBlockPoint n) z)

def ViscositySolns.pointRight {n : ℕ} (z : Point (n + n)) : Point n

The right R^n coordinate of a point of R^(n+n) = R^n × R^n.

Equations

• ViscositySolns.pointRight z = ViscositySolns.blockPointRight ((ViscositySolns.pointSumEquivBlockPoint n) z)

def ViscositySolns.pointWithLeft {n : ℕ} (z : Point (n + n)) (x : Point n) : Point (n + n)

The point obtained from z = (x0, y0) by replacing its left coordinate with x, giving (x, y0).

Equations

• ViscositySolns.pointWithLeft z x = (ViscositySolns.pointSumEquivBlockPoint n).symm (Sum.elim x (ViscositySolns.pointRight z))

def ViscositySolns.pointWithRight {n : ℕ} (z : Point (n + n)) (y : Point n) : Point (n + n)

The point obtained from z = (x0, y0) by replacing its right coordinate with y, giving (x0, y).

Equations

• ViscositySolns.pointWithRight z y = (ViscositySolns.pointSumEquivBlockPoint n).symm (Sum.elim (ViscositySolns.pointLeft z) y)

theorem ViscositySolns.continuous_leftPointEmbedding {n : ℕ} : Continuous leftPointEmbedding

theorem ViscositySolns.continuous_rightPointEmbedding {n : ℕ} : Continuous rightPointEmbedding

theorem ViscositySolns.continuous_pointLeft {n : ℕ} : Continuous pointLeft

theorem ViscositySolns.continuous_pointRight {n : ℕ} : Continuous pointRight

theorem ViscositySolns.continuous_pointWithLeft {n : ℕ} (z : Point (n + n)) : Continuous (pointWithLeft z)

theorem ViscositySolns.continuous_pointWithRight {n : ℕ} (z : Point (n + n)) : Continuous (pointWithRight z)

def ViscositySolns.leftPointGradient {n : ℕ} (p : Point (n + n)) : Point n

The left R^n component of a vector written in R^(n+n) coordinates.

Equations

• ViscositySolns.leftPointGradient p i = p (Fin.castAdd n i)

def ViscositySolns.rightPointGradient {n : ℕ} (p : Point (n + n)) : Point n

The right R^n component of a vector written in R^(n+n) coordinates.

Equations

• ViscositySolns.rightPointGradient p i = p (Fin.natAdd n i)

@[simp]

theorem ViscositySolns.leftPointGradient_smul {n : ℕ} (a : ℝ) (p : Point (n + n)) : leftPointGradient (a • p) = a • leftPointGradient p

@[simp]

theorem ViscositySolns.rightPointGradient_smul {n : ℕ} (a : ℝ) (p : Point (n + n)) : rightPointGradient (a • p) = a • rightPointGradient p

def ViscositySolns.leftPointHessian {n : ℕ} (X : Hessian (n + n)) : Hessian n

The left-left block of a Hessian written in R^(n+n) coordinates.

Equations

• ViscositySolns.leftPointHessian X = Matrix.submatrix X (Fin.castAdd n) (Fin.castAdd n)

def ViscositySolns.rightPointHessian {n : ℕ} (X : Hessian (n + n)) : Hessian n

The right-right block of a Hessian written in R^(n+n) coordinates.

Equations

• ViscositySolns.rightPointHessian X = Matrix.submatrix X (Fin.natAdd n) (Fin.natAdd n)

def ViscositySolns.leftPointJet {n : ℕ} (J : Jet (n + n)) : Jet n

The left coordinate projection of a jet on R^n × R^n.

Equations

• ViscositySolns.leftPointJet J = { gradient := ViscositySolns.leftPointGradient J.gradient, hessian := ViscositySolns.leftPointHessian J.hessian }

def ViscositySolns.rightPointJet {n : ℕ} (J : Jet (n + n)) : Jet n

The right coordinate projection of a jet on R^n × R^n.

Equations

• ViscositySolns.rightPointJet J = { gradient := ViscositySolns.rightPointGradient J.gradient, hessian := ViscositySolns.rightPointHessian J.hessian }

theorem ViscositySolns.continuous_leftPointJet {n : ℕ} : Continuous leftPointJet

theorem ViscositySolns.continuous_rightPointJet {n : ℕ} : Continuous rightPointJet

theorem ViscositySolns.tendsto_leftPointJet_of_tendsto {n : ℕ} {ι : Type u_1} {l : Filter ι} {JSeq : ι → Jet (n + n)} {J : Jet (n + n)} (hJ : Filter.Tendsto JSeq l (nhds J)) : Filter.Tendsto (fun (i : ι) => leftPointJet (JSeq i)) l (nhds (leftPointJet J))

Convergence of block jets implies convergence of their left-coordinate projected jets.

theorem ViscositySolns.tendsto_rightPointJet_neg_of_tendsto {n : ℕ} {ι : Type u_1} {l : Filter ι} {JSeq : ι → Jet (n + n)} {J : Jet (n + n)} (hJ : Filter.Tendsto JSeq l (nhds J)) : Filter.Tendsto (fun (i : ι) => (rightPointJet (JSeq i)).neg) l (nhds (rightPointJet J).neg)

Convergence of block jets implies convergence of the negated right-coordinate projected jets.

In standard mathematical terms, if J_i -> J as jets on R^n × R^n, then the jets obtained by taking the right coordinate component and negating both the gradient and Hessian also converge: -(right J_i) -> -(right J).

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_leftPointEmbedding {n : ℕ} (x : Point n) : (pointSumEquivBlockPoint n) (leftPointEmbedding x) = leftBlockPoint x

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_rightPointEmbedding {n : ℕ} (y : Point n) : (pointSumEquivBlockPoint n) (rightPointEmbedding y) = rightBlockPoint y

@[simp]

theorem ViscositySolns.leftBlockPoint_smul {n : ℕ} (a : ℝ) (x : Point n) : leftBlockPoint (a • x) = a • leftBlockPoint x

@[simp]

theorem ViscositySolns.rightBlockPoint_smul {n : ℕ} (a : ℝ) (y : Point n) : rightBlockPoint (a • y) = a • rightBlockPoint y

@[simp]

theorem ViscositySolns.leftPointEmbedding_smul {n : ℕ} (a : ℝ) (x : Point n) : leftPointEmbedding (a • x) = a • leftPointEmbedding x

@[simp]

theorem ViscositySolns.rightPointEmbedding_smul {n : ℕ} (a : ℝ) (y : Point n) : rightPointEmbedding (a • y) = a • rightPointEmbedding y

@[simp]

theorem ViscositySolns.blockPointLeft_leftBlockPoint {n : ℕ} (x : Point n) : blockPointLeft (leftBlockPoint x) = x

@[simp]

theorem ViscositySolns.blockPointRight_leftBlockPoint {n : ℕ} (x : Point n) : blockPointRight (leftBlockPoint x) = 0

@[simp]

theorem ViscositySolns.blockPointLeft_rightBlockPoint {n : ℕ} (y : Point n) : blockPointLeft (rightBlockPoint y) = 0

@[simp]

theorem ViscositySolns.blockPointRight_rightBlockPoint {n : ℕ} (y : Point n) : blockPointRight (rightBlockPoint y) = y

@[simp]

theorem ViscositySolns.leftBlockPoint_single {n : ℕ} (i : Fin n) : leftBlockPoint (Pi.single i 1) = Pi.single (Sum.inl i) 1

@[simp]

theorem ViscositySolns.rightBlockPoint_single {n : ℕ} (j : Fin n) : rightBlockPoint (Pi.single j 1) = Pi.single (Sum.inr j) 1

theorem ViscositySolns.finSumFinEquiv_symm_castAdd {n : ℕ} (i : Fin n) : finSumFinEquiv.symm (Fin.castAdd n i) = Sum.inl i

theorem ViscositySolns.finSumFinEquiv_symm_natAdd {n : ℕ} (i : Fin n) : finSumFinEquiv.symm (Fin.natAdd n i) = Sum.inr i

@[simp]

theorem ViscositySolns.finSumFinEquiv_symm_addNat {n : ℕ} (i : Fin n) : finSumFinEquiv.symm (i.addNat n) = Sum.inr i

@[simp]

theorem ViscositySolns.pointLeft_zero {n : ℕ} : pointLeft 0 = 0

@[simp]

theorem ViscositySolns.pointRight_zero {n : ℕ} : pointRight 0 = 0

@[simp]

theorem ViscositySolns.pointLeft_leftPointEmbedding {n : ℕ} (x : Point n) : pointLeft (leftPointEmbedding x) = x

@[simp]

theorem ViscositySolns.pointRight_leftPointEmbedding {n : ℕ} (x : Point n) : pointRight (leftPointEmbedding x) = 0

@[simp]

theorem ViscositySolns.pointLeft_rightPointEmbedding {n : ℕ} (y : Point n) : pointLeft (rightPointEmbedding y) = 0

@[simp]

theorem ViscositySolns.pointRight_rightPointEmbedding {n : ℕ} (y : Point n) : pointRight (rightPointEmbedding y) = y

@[simp]

theorem ViscositySolns.pointLeft_add_leftPointEmbedding {n : ℕ} (z : Point (n + n)) (x : Point n) : pointLeft (z + leftPointEmbedding x) = pointLeft z + x

@[simp]

theorem ViscositySolns.pointRight_add_leftPointEmbedding {n : ℕ} (z : Point (n + n)) (x : Point n) : pointRight (z + leftPointEmbedding x) = pointRight z

@[simp]

theorem ViscositySolns.pointLeft_add_rightPointEmbedding {n : ℕ} (z : Point (n + n)) (y : Point n) : pointLeft (z + rightPointEmbedding y) = pointLeft z

@[simp]

theorem ViscositySolns.pointRight_add_rightPointEmbedding {n : ℕ} (z : Point (n + n)) (y : Point n) : pointRight (z + rightPointEmbedding y) = pointRight z + y

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_pointWithLeft {n : ℕ} (z : Point (n + n)) (x : Point n) : (pointSumEquivBlockPoint n) (pointWithLeft z x) = Sum.elim x (pointRight z)

@[simp]

theorem ViscositySolns.pointSumEquivBlockPoint_pointWithRight {n : ℕ} (z : Point (n + n)) (y : Point n) : (pointSumEquivBlockPoint n) (pointWithRight z y) = Sum.elim (pointLeft z) y

@[simp]

theorem ViscositySolns.pointLeft_pointWithLeft {n : ℕ} (z : Point (n + n)) (x : Point n) : pointLeft (pointWithLeft z x) = x

@[simp]

theorem ViscositySolns.pointRight_pointWithLeft {n : ℕ} (z : Point (n + n)) (x : Point n) : pointRight (pointWithLeft z x) = pointRight z

@[simp]

theorem ViscositySolns.pointLeft_pointWithRight {n : ℕ} (z : Point (n + n)) (y : Point n) : pointLeft (pointWithRight z y) = pointLeft z

@[simp]

theorem ViscositySolns.pointRight_pointWithRight {n : ℕ} (z : Point (n + n)) (y : Point n) : pointRight (pointWithRight z y) = y

@[simp]

theorem ViscositySolns.pointWithLeft_self {n : ℕ} (z : Point (n + n)) : pointWithLeft z (pointLeft z) = z

@[simp]

theorem ViscositySolns.pointWithRight_self {n : ℕ} (z : Point (n + n)) : pointWithRight z (pointRight z) = z

theorem ViscositySolns.pointWithLeft_sub_self {n : ℕ} (z : Point (n + n)) (x : Point n) : pointWithLeft z x - z = leftPointEmbedding (x - pointLeft z)

theorem ViscositySolns.pointWithRight_sub_self {n : ℕ} (z : Point (n + n)) (y : Point n) : pointWithRight z y - z = rightPointEmbedding (y - pointRight z)

@[simp]

theorem ViscositySolns.leftPointEmbedding_zero {n : ℕ} : leftPointEmbedding 0 = 0

@[simp]

theorem ViscositySolns.rightPointEmbedding_zero {n : ℕ} : rightPointEmbedding 0 = 0

@[simp]

theorem ViscositySolns.leftPointEmbedding_apply_castAdd {n : ℕ} (x : Point n) (i : Fin n) : leftPointEmbedding x (Fin.castAdd n i) = x i

theorem ViscositySolns.leftPointEmbedding_apply_natAdd {n : ℕ} (x : Point n) (i : Fin n) : leftPointEmbedding x (Fin.natAdd n i) = 0

@[simp]

theorem ViscositySolns.rightPointEmbedding_apply_castAdd {n : ℕ} (y : Point n) (i : Fin n) : rightPointEmbedding y (Fin.castAdd n i) = 0

theorem ViscositySolns.rightPointEmbedding_apply_natAdd {n : ℕ} (y : Point n) (i : Fin n) : rightPointEmbedding y (Fin.natAdd n i) = y i

@[simp]

theorem ViscositySolns.leftPointEmbedding_apply_addNat {n : ℕ} (x : Point n) (i : Fin n) : leftPointEmbedding x (i.addNat n) = 0

The left embedding vanishes on the right coordinate block.

@[simp]

theorem ViscositySolns.rightPointEmbedding_apply_addNat {n : ℕ} (y : Point n) (i : Fin n) : rightPointEmbedding y (i.addNat n) = y i

The right embedding recovers the original right coordinate.

@[simp]

theorem ViscositySolns.dotProduct_leftPointGradient {n : ℕ} (p : Point (n + n)) (x : Point n) : p ⬝ᵥ leftPointEmbedding x = leftPointGradient p ⬝ᵥ x

@[simp]

theorem ViscositySolns.dotProduct_rightPointGradient {n : ℕ} (p : Point (n + n)) (y : Point n) : p ⬝ᵥ rightPointEmbedding y = rightPointGradient p ⬝ᵥ y

theorem ViscositySolns.norm_leftPointEmbedding_le {n : ℕ} (x : Point n) : ‖leftPointEmbedding x‖ ≤ ‖x‖

theorem ViscositySolns.norm_rightPointEmbedding_le {n : ℕ} (y : Point n) : ‖rightPointEmbedding y‖ ≤ ‖y‖

theorem ViscositySolns.norm_pointWithLeft_sub_self_le {n : ℕ} (z : Point (n + n)) (x : Point n) : ‖pointWithLeft z x - z‖ ≤ ‖x - pointLeft z‖

theorem ViscositySolns.norm_pointWithRight_sub_self_le {n : ℕ} (z : Point (n + n)) (y : Point n) : ‖pointWithRight z y - z‖ ≤ ‖y - pointRight z‖

@[simp]

theorem ViscositySolns.quadraticModel_leftPointEmbedding {n : ℕ} (r : ℝ) (p : Point (n + n)) (X : Hessian (n + n)) (x : Point n) : quadraticModel 0 r p X (leftPointEmbedding x) = quadraticModel 0 r (leftPointGradient p) (leftPointHessian X) x

@[simp]

theorem ViscositySolns.quadraticModel_rightPointEmbedding {n : ℕ} (r : ℝ) (p : Point (n + n)) (X : Hessian (n + n)) (y : Point n) : quadraticModel 0 r p X (rightPointEmbedding y) = quadraticModel 0 r (rightPointGradient p) (rightPointHessian X) y

@[simp]

theorem ViscositySolns.quadraticModel_pointWithLeft {n : ℕ} (z : Point (n + n)) (r : ℝ) (p : Point (n + n)) (X : Hessian (n + n)) (x : Point n) : quadraticModel z r p X (pointWithLeft z x) = quadraticModel (pointLeft z) r (leftPointGradient p) (leftPointHessian X) x

@[simp]

theorem ViscositySolns.quadraticModel_pointWithRight {n : ℕ} (z : Point (n + n)) (r : ℝ) (p : Point (n + n)) (X : Hessian (n + n)) (y : Point n) : quadraticModel z r p X (pointWithRight z y) = quadraticModel (pointRight z) r (rightPointGradient p) (rightPointHessian X) y

theorem ViscositySolns.quadraticModel_mixed_second_difference_left_right {n : ℕ} (z : Point (n + n)) (r : ℝ) (p : Point (n + n)) (X : Hessian (n + n)) (x y : Point n) : quadraticModel z r p X (z + leftPointEmbedding x + rightPointEmbedding y) - quadraticModel z r p X (z + leftPointEmbedding x) - quadraticModel z r p X (z + rightPointEmbedding y) + quadraticModel z r p X z = 1 / 2 * (Matrix.mulVec X (leftPointEmbedding x) ⬝ᵥ rightPointEmbedding y + Matrix.mulVec X (rightPointEmbedding y) ⬝ᵥ leftPointEmbedding x)

The mixed second difference of a quadratic model in a left direction and a right direction depends only on the mixed Hessian terms.

In standard mathematical terms, for a quadratic polynomial on R^n × R^n, the expression

q(z + (x, 0) + (0, y)) - q(z + (x, 0)) - q(z + (0, y)) + q(z)

is

(1 / 2) * (⟪X(x, 0), (0, y)⟫ + ⟪X(0, y), (x, 0)⟫).

theorem ViscositySolns.dotProduct_mulVec_leftPointEmbedding_rightPointEmbedding {n : ℕ} (Z : Hessian (n + n)) (x y : Point n) : Matrix.mulVec Z (leftPointEmbedding x) ⬝ᵥ rightPointEmbedding y = Matrix.mulVec (pointHessianToBlockHessian Z) (leftBlockPoint x) ⬝ᵥ rightBlockPoint y

The cross term between a left increment and a right increment may be computed in block coordinates.

In standard mathematical terms, reindexing the Hessian Z from R^{2n} to R^n × R^n does not change the bilinear expression ⟪Z(x, 0), (0, y)⟫.

theorem ViscositySolns.dotProduct_mulVec_rightPointEmbedding_leftPointEmbedding {n : ℕ} (Z : Hessian (n + n)) (x y : Point n) : Matrix.mulVec Z (rightPointEmbedding y) ⬝ᵥ leftPointEmbedding x = Matrix.mulVec (pointHessianToBlockHessian Z) (rightBlockPoint y) ⬝ᵥ leftBlockPoint x

The cross term between a right increment and a left increment may be computed in block coordinates.

In standard mathematical terms, reindexing the Hessian Z from R^{2n} to R^n × R^n does not change the bilinear expression ⟪Z(0, y), (x, 0)⟫.

theorem ViscositySolns.dotProduct_mulVec_leftBlockPoint_single_rightBlockPoint_single {n : ℕ} (A : BlockHessian n) (i j : Fin n) : Matrix.mulVec A (Pi.single (Sum.inl i) 1) ⬝ᵥ Pi.single (Sum.inr j) 1 = A (Sum.inr j) (Sum.inl i)

The left-right cross term against coordinate basis vectors is the corresponding matrix entry.

In standard mathematical terms, for a block Hessian A,

⟪A e_i^L, e_j^R⟫ = A_{R_j,L_i}.

theorem ViscositySolns.dotProduct_mulVec_rightBlockPoint_single_leftBlockPoint_single {n : ℕ} (A : BlockHessian n) (i j : Fin n) : Matrix.mulVec A (Pi.single (Sum.inr j) 1) ⬝ᵥ Pi.single (Sum.inl i) 1 = A (Sum.inl i) (Sum.inr j)

The right-left cross term against coordinate basis vectors is the corresponding matrix entry.

In standard mathematical terms, for a block Hessian A,

⟪A e_j^R, e_i^L⟫ = A_{L_i,R_j}.