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

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

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.superjet_left_of_superjet_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} {J : Jet (n + n)} (hJ : J ∈ Superjet Set.univ (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) 0) : { gradient := leftPointGradient J.gradient, hessian := leftPointHessian J.hessian } ∈ Superjet Set.univ G 0

Restrict a superjet of a separated difference to the left coordinate slice.

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

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

Restrict a superjet of a separated difference to the right coordinate slice.

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

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

Restrict a subjet of a separated difference to the left coordinate slice.

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

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

Restrict a subjet of a separated difference to the right coordinate slice.

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

theorem ViscositySolns.Continuous.blockFunctionToPointFunction {n : ℕ} {F : BlockPoint n → ℝ} (hF : Continuous F) : Continuous (ViscositySolns.blockFunctionToPointFunction F)

Pulling a continuous function on R^n × R^n back to R^(n+n) gives a continuous function.

noncomputable def ViscositySolns.doubledQuadraticExpansionAt {n : ℕ} (x0 y0 : Point n) (φ0 : ℝ) (P : BlockPoint n) (A : BlockHessian n) (q : DoubledPoint n) : ℝ

The quadratic expansion of a test function at a doubled point, written in translated block coordinates.

In standard mathematical terms, at the base point (x0, y0) this is

`φ0 + ⟪P, (x - x0, y - y0)⟫

• (1 / 2) * ⟪A (x - x0, y - y0), (x - x0, y - y0)⟫`.

Equations

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

def ViscositySolns.normalizedLeftOfBlockGradient {n : ℕ} (u : Point n → ℝ) (x0 : Point n) (P : BlockPoint n) (x : Point n) : ℝ

The left normalized function used after translating the doubled maximum point to the origin and subtracting the affine part of the test function.

In standard mathematical terms this is x ↦ u(x0 + x) - u(x0) - ⟪P_x, x⟫.

Equations

• ViscositySolns.normalizedLeftOfBlockGradient u x0 P x = u (x0 + x) - u x0 - ViscositySolns.blockPointLeft P ⬝ᵥ x

@[simp]

theorem ViscositySolns.normalizedLeftOfBlockGradient_zero {n : ℕ} (u : Point n → ℝ) (x0 : Point n) (P : BlockPoint n) : normalizedLeftOfBlockGradient u x0 P 0 = 0

def ViscositySolns.normalizedRightOfBlockGradient {n : ℕ} (v : Point n → ℝ) (y0 : Point n) (P : BlockPoint n) (y : Point n) : ℝ

The right normalized function used after translating the doubled maximum point to the origin and subtracting the affine part of the test function.

If P_y is the derivative of the test function with respect to the second variable, this is y ↦ v(y0 + y) - v(y0) + ⟪P_y, y⟫. Equivalently, it subtracts the subjet gradient -P_y.

Equations

• ViscositySolns.normalizedRightOfBlockGradient v y0 P y = v (y0 + y) - v y0 + ViscositySolns.blockPointRight P ⬝ᵥ y

@[simp]

theorem ViscositySolns.normalizedRightOfBlockGradient_zero {n : ℕ} (v : Point n → ℝ) (y0 : Point n) (P : BlockPoint n) : normalizedRightOfBlockGradient v y0 P 0 = 0

theorem ViscositySolns.closedSuperjet_of_closedSuperjet_normalizedLeftOfBlockGradient {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x0 : Point n} {P : BlockPoint n} {X : Hessian n} (hJ : { gradient := 0, hessian := X } ∈ ClosedSuperjet K (normalizedLeftOfBlockGradient u x0 P) 0) : { gradient := blockPointLeft P, hessian := X } ∈ ClosedSuperjet ((fun (x : Point n) => x0 + x) '' K) u x0

Closed superjets of the left normalized function transfer back to closed superjets of the original function with the affine gradient restored.

In quantified mathematical form, if

u_norm(x) = u(x0+x) - u(x0) - ⟪P_x, x⟫

and (0, X) ∈ \overline J^{2,+}_K u_norm(0), then (P_x, X) ∈ \overline J^{2,+}_{x0+K} u(x0).

theorem ViscositySolns.closedSubjet_of_closedSubjet_normalizedRightOfBlockGradient {n : ℕ} {L : Set (Point n)} {v : Point n → ℝ} {y0 : Point n} {P : BlockPoint n} {Y : Hessian n} (hJ : { gradient := 0, hessian := Y } ∈ ClosedSubjet L (normalizedRightOfBlockGradient v y0 P) 0) : { gradient := -blockPointRight P, hessian := Y } ∈ ClosedSubjet ((fun (y : Point n) => y0 + y) '' L) v y0

Closed subjets of the right normalized function transfer back to closed subjets of the original function with the affine gradient restored.

In quantified mathematical form, if

v_norm(y) = v(y0+y) - v(y0) + ⟪P_y, y⟫

and (0, Y) ∈ \overline J^{2,-}_L v_norm(0), then (-P_y, Y) ∈ \overline J^{2,-}_{y0+L} v(y0).

theorem ViscositySolns.upperSemicontinuousOn_normalizedLeftOfBlockGradient {n : ℕ} {K : Set (Point n)} {u : Point n → ℝ} {x0 : Point n} {P : BlockPoint n} (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) : UpperSemicontinuousOn (normalizedLeftOfBlockGradient u x0 P) K

Upper semicontinuity is preserved by translating the argument and subtracting the affine part used in the normalized maximum-principle reduction.

theorem ViscositySolns.lowerSemicontinuousOn_normalizedRightOfBlockGradient {n : ℕ} {L : Set (Point n)} {v : Point n → ℝ} {y0 : Point n} {P : BlockPoint n} (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) : LowerSemicontinuousOn (normalizedRightOfBlockGradient v y0 P) L

Lower semicontinuity is preserved by translating the argument and adding the affine part used in the normalized maximum-principle reduction.

theorem ViscositySolns.normalizedLeft_sub_normalizedRight_eq {n : ℕ} {u v : Point n → ℝ} {x0 y0 : Point n} {P : BlockPoint n} (x y : Point n) : normalizedLeftOfBlockGradient u x0 P x - normalizedRightOfBlockGradient v y0 P y = u (x0 + x) - v (y0 + y) - (u x0 - v y0) - P ⬝ᵥ doubledPointToBlockPoint (x, y)

The difference of the two normalized functions is the original doubled difference with the base value and affine test part subtracted.

theorem ViscositySolns.normalized_pointwise_bound_of_isMaxOn_doubledQuadraticExpansionAt {n : ℕ} {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (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)) (x : Point n) : x ∈ K → ∀ y ∈ L, normalizedLeftOfBlockGradient u x0 P x - normalizedRightOfBlockGradient v y0 P y ≤ blockQuadraticModel A (doubledPointToBlockPoint (x, y))

A maximum of the doubled difference minus a quadratic expansion gives the normalized pointwise quadratic bound.

In standard mathematical terms, suppose (x0, y0) is a maximum, relative to the translated set {(x0 + x, y0 + y) | x ∈ K, y ∈ L}, of

`(x, y) ↦ u(x) - v(y)

• [φ0 + ⟪P, (x - x0, y - y0)⟫
  • (1 / 2) * ⟪A(x - x0, y - y0), (x - x0, y - y0)⟫]`.

Then for every x ∈ K and y ∈ L,

`u(x0 + x) - u(x0) - ⟪P_x, x⟫

• [v(y0 + y) - v(y0) + ⟪P_y, y⟫] ≤ (1 / 2) * ⟪A(x, y), (x, y)⟫`.

theorem ViscositySolns.isMaxOn_translated_product_of_isMaxOn_superset {n : ℕ} {K L : Set (Point n)} {P : Set (DoubledPoint n)} {f : DoubledPoint n → ℝ} {x0 y0 : Point n} (hmax : IsMaxOn f P (x0, y0)) (hsubset : {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} ⊆ P) : IsMaxOn f {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)

Restrict a doubled maximum to a translated product set.

In standard mathematical terms, if (x0, y0) is a maximum point of f on a set P, and every pair (x, y) satisfying x - x0 ∈ K and y - y0 ∈ L belongs to P, then (x0, y0) is a maximum point of f on that translated product set.

def ViscositySolns.BlockCoordinateSemiconvexOn {n : ℕ} (lambda : ℝ) (C : Set (BlockPoint n)) (F : BlockPoint n → ℝ) : Prop

The semiconvexity inequality on R^n × R^n, written in block coordinates.

In quantified mathematical form, a function F : R^n × R^n -> R satisfies BlockCoordinateSemiconvexOn lambda C F if for every x, y ∈ C and every real numbers a, b with 0 ≤ a, 0 ≤ b, and a + b = 1, whenever a x + b y ∈ C, one has

F (a x + b y) ≤ a F x + b F y + (lambda / 2) a b |x - y|^2.

Equations

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

theorem ViscositySolns.BlockCoordinateSemiconvexOn.coordinateSemiconvexOn_blockFunctionToPointFunction {n : ℕ} {lambda : ℝ} {F : BlockPoint n → ℝ} (hsemi : BlockCoordinateSemiconvexOn lambda Set.univ F) : CoordinateSemiconvexOn lambda Set.univ (blockFunctionToPointFunction F)

Writing a block-coordinate semiconvex function in R^(n+n) coordinates preserves the semiconvexity inequality.

In quantified mathematical form, if F : R^n × R^n -> R satisfies the semiconvexity inequality with constant lambda on all of R^n × R^n, then z ↦ F(z_1, z_2), regarded as a function on R^(n+n), satisfies the same semiconvexity inequality with constant lambda on all of R^(n+n).

theorem ViscositySolns.BlockCoordinateSemiconvexOn.continuous_univ {n : ℕ} {lambda : ℝ} {F : BlockPoint n → ℝ} (hsemi : BlockCoordinateSemiconvexOn lambda Set.univ F) : Continuous F

Block-coordinate semiconvexity on all of R^n × R^n implies continuity.

In standard mathematical terms, this is the continuity of a semiconvex function on the finite-dimensional product space.

theorem ViscositySolns.BlockCoordinateSemiconvexOn.left_right_add {n : ℕ} {lambda : ℝ} {f g : Point n → ℝ} (hf : CoordinateSemiconvexOn lambda Set.univ f) (hg : CoordinateSemiconvexOn lambda Set.univ g) : BlockCoordinateSemiconvexOn lambda Set.univ fun (q : BlockPoint n) => f (blockPointLeft q) + g (blockPointRight q)

If two functions on R^n are semiconvex with the same constant, then their sum as a function on R^n × R^n is semiconvex with that same constant.

In standard mathematical terms, if f and g satisfy the semiconvexity inequality with constant lambda, then (x, y) ↦ f(x) + g(y) satisfies the semiconvexity inequality with constant lambda on the product space, because |(x_1, y_1) - (x_2, y_2)|^2 = |x_1 - x_2|^2 + |y_1 - y_2|^2.