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

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

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.pointHessianToBlockHessian_eq_comparisonBlockDiagonal_of_mixed_dot_zero {n : ℕ} {Z : Hessian (n + n)} (hZ : Matrix.IsHermitian Z) (hmix : ∀ (x y : Point n), Matrix.mulVec Z (leftPointEmbedding x) ⬝ᵥ rightPointEmbedding y + Matrix.mulVec Z (rightPointEmbedding y) ⬝ᵥ leftPointEmbedding x = 0) : pointHessianToBlockHessian Z = comparisonBlockDiagonal (leftPointHessian Z) (-rightPointHessian Z)

Vanishing of the mixed bilinear expression gives the selected block diagonal Hessian.

In standard mathematical terms, let Z be a symmetric Hessian matrix on R^n × R^n. Suppose that for all x, y ∈ R^n,

⟪Z(x, 0), (0, y)⟫ + ⟪Z(0, y), (x, 0)⟫ = 0.

Then the block-coordinate form of Z is

[X 0; 0 -Y],

where X is the left-left block of Z and Y is the negative of the right-right block of Z.

theorem ViscositySolns.separatedFunction_mixed_second_difference_left_right {n : ℕ} (G H : Point n → ℝ) (z : Point (n + n)) (x y : Point n) : blockFunctionToPointFunction (fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) (z + leftPointEmbedding x + rightPointEmbedding y) - blockFunctionToPointFunction (fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) (z + leftPointEmbedding x) - blockFunctionToPointFunction (fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) (z + rightPointEmbedding y) + blockFunctionToPointFunction (fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) z = 0

The mixed second difference of a separated function is zero.

In standard mathematical terms, if F(ξ, η) = G(ξ) - H(η), then for every base point (ξ₀, η₀) and all increments x, y ∈ R^n,

`F((ξ₀ + x), (η₀ + y)) - F((ξ₀ + x), η₀)

• F(ξ₀, (η₀ + y)) + F(ξ₀, η₀) = 0`.

theorem ViscositySolns.mixed_dot_zero_of_hasSecondOrderExpansionWithin_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} {z p : Point (n + n)} {Z : Hessian (n + n)} (hF : HasSecondOrderExpansionWithin Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) z { gradient := p, hessian := Z }) (x y : Point n) : Matrix.mulVec Z (leftPointEmbedding x) ⬝ᵥ rightPointEmbedding y + Matrix.mulVec Z (rightPointEmbedding y) ⬝ᵥ leftPointEmbedding x = 0

A second-order expansion of a separated function has zero mixed Hessian bilinear expression.

In standard mathematical terms, let F(ξ, η) = G(ξ) - H(η). If F has a second-order expansion at (ξ₀, η₀) with Hessian Z, then for every x, y ∈ R^n,

⟪Z(x, 0), (0, y)⟫ + ⟪Z(0, y), (x, 0)⟫ = 0.

theorem ViscositySolns.superjet_left_of_superjet_blockFunctionToPointFunction_sub_at {n : ℕ} {G H : Point n → ℝ} {z : Point (n + n)} {J : Jet (n + n)} (hJ : J ∈ Superjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) z) : { gradient := leftPointGradient J.gradient, hessian := leftPointHessian J.hessian } ∈ Superjet Set.univ G (pointLeft z)

Restrict a superjet of a separated difference to the left coordinate slice at an arbitrary base point.

In standard mathematical terms, if (p, Z) is a superjet at (x0, y0) of (ξ, η) ↦ G(ξ) - H(η), then the left component of p and the left-left block of Z form a superjet of G at x0.

theorem ViscositySolns.subjet_right_of_superjet_blockFunctionToPointFunction_sub_at {n : ℕ} {G H : Point n → ℝ} {z : Point (n + n)} {J : Jet (n + n)} (hJ : J ∈ Superjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) z) : { gradient := -rightPointGradient J.gradient, hessian := -rightPointHessian J.hessian } ∈ Subjet Set.univ H (pointRight z)

Restrict a superjet of a separated difference to the right coordinate slice at an arbitrary base point.

In standard mathematical terms, if (p, Z) is a superjet at (x0, y0) of (ξ, η) ↦ G(ξ) - H(η), then the negative right component of p and the negative right-right block of Z form a subjet of H at y0.

theorem ViscositySolns.subjet_left_of_subjet_blockFunctionToPointFunction_sub_at {n : ℕ} {G H : Point n → ℝ} {z : Point (n + n)} {J : Jet (n + n)} (hJ : J ∈ Subjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) z) : { gradient := leftPointGradient J.gradient, hessian := leftPointHessian J.hessian } ∈ Subjet Set.univ G (pointLeft z)

Restrict a subjet of a separated difference to the left coordinate slice at an arbitrary base point.

In standard mathematical terms, if (p, Z) is a subjet at (x0, y0) of (ξ, η) ↦ G(ξ) - H(η), then the left component of p and the left-left block of Z form a subjet of G at x0.

theorem ViscositySolns.superjet_right_of_subjet_blockFunctionToPointFunction_sub_at {n : ℕ} {G H : Point n → ℝ} {z : Point (n + n)} {J : Jet (n + n)} (hJ : J ∈ Subjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) z) : { gradient := -rightPointGradient J.gradient, hessian := -rightPointHessian J.hessian } ∈ Superjet Set.univ H (pointRight z)

Restrict a subjet of a separated difference to the right coordinate slice at an arbitrary base point.

In standard mathematical terms, if (p, Z) is a subjet at (x0, y0) of (ξ, η) ↦ G(ξ) - H(η), then the negative right component of p and the negative right-right block of Z form a superjet of H at y0.

theorem ViscositySolns.closedSuperjet_left_of_closedSuperjet_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} (hH : Continuous H) {J : Jet (n + n)} (hJ : J ∈ ClosedSuperjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) 0) : leftPointJet J ∈ ClosedSuperjet Set.univ G 0

Closed-superjet restriction to the left coordinate for a separated difference.

In standard mathematical terms, assume H is continuous. If (p, Z) belongs to the closed superjet at (0, 0) of (ξ, η) ↦ G(ξ) - H(η), then the left component of p and the left-left block of Z belong to the closed superjet of G at 0.

theorem ViscositySolns.closedSubjet_right_of_closedSuperjet_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} (hG : Continuous G) {J : Jet (n + n)} (hJ : J ∈ ClosedSuperjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) 0) : (rightPointJet J).neg ∈ ClosedSubjet Set.univ H 0

Closed-subjet restriction to the right coordinate for a separated difference.

In standard mathematical terms, assume G is continuous. If (p, Z) belongs to the closed superjet at (0, 0) of (ξ, η) ↦ G(ξ) - H(η), then the negative right component of p and the negative right-right block of Z belong to the closed subjet of H at 0.

theorem ViscositySolns.closedSemijets_of_closedSuperjet_blockFunctionToPointFunction_sub_of_blockDiagonal {n : ℕ} {G H : Point n → ℝ} (hG : Continuous G) (hH : Continuous H) {Z : Hessian (n + n)} {X Y : Hessian n} (hdiag : pointHessianToBlockHessian Z = comparisonBlockDiagonal X Y) (hJ : { gradient := 0, hessian := Z } ∈ ClosedSuperjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) 0) : { gradient := 0, hessian := X } ∈ ClosedSuperjet Set.univ G 0 ∧ { gradient := 0, hessian := Y } ∈ ClosedSubjet Set.univ H 0

Separated closed semijets obtained from a selected block diagonal Hessian.

In quantified mathematical form, let G, H : R^n -> R be continuous functions, let Z be a Hessian matrix on R^n × R^n, and let X and Y be Hessian matrices on R^n. Suppose that (0, Z) belongs to the closed superjet at (0, 0) of

(ξ, η) ↦ G(ξ) - H(η),

and suppose that, after writing Z in block coordinates,

Z = [X 0; 0 -Y].

Then (0, X) belongs to the closed superjet of G at 0, and (0, Y) belongs to the closed subjet of H at 0.

theorem ViscositySolns.closedSemijets_and_blockBounds_of_blockDiagonal_closedSuperjet {n : ℕ} {G H : Point n → ℝ} (hG : Continuous G) (hH : Continuous H) {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 fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) 0) : { gradient := 0, hessian := X } ∈ ClosedSuperjet Set.univ G 0 ∧ { gradient := 0, hessian := Y } ∈ ClosedSubjet Set.univ H 0 ∧ lower ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ upper

Separated closed semijets together with inherited block matrix bounds.

In quantified mathematical form, let G, H : R^n -> R be continuous functions, let (0, Z) belong to the closed superjet at (0, 0) of (ξ, η) ↦ G(ξ) - H(η), and suppose that the block form of Z is [X 0; 0 -Y]. If the block form of Z lies between matrices lower and upper in the Loewner order, then (0, X) belongs to the closed superjet of G at 0, (0, Y) belongs to the closed subjet of H at 0, and

lower ≤ [X 0; 0 -Y] ≤ upper.