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

Strictification and jet bridges for the Aleksandrov--Jensen argument (StrictifiedObjective)

Part of the quartic strictification, compact Hessian, and jet transport development used before the contact-set and approximation arguments in SemiconvexJensen. Split from Strictification.lean; see the umbrella module docstring.

def ViscositySolns.hessianEntryBox (n : ℕ) (R : ℝ) : Set (Hessian n)

The entrywise closed box of Hessian matrices with entries in [-R, R].

Equations

• ViscositySolns.hessianEntryBox n R = {A : ViscositySolns.Hessian n | ∀ (i j : Fin n), A i j ∈ Set.Icc (-R) R}

theorem ViscositySolns.isCompact_hessianEntryBox {n : ℕ} (R : ℝ) : IsCompact (hessianEntryBox n R)

The entrywise closed box of Hessian matrices is compact.

theorem ViscositySolns.exists_hessian_subsequence_tendsto_of_eventually_entrywise_abs_le {n : ℕ} {A : ℕ → Hessian n} {R : ℝ} (hbound : ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (i j : Fin n), |A k i j| ≤ R) : ∃ (Z : Hessian n) (φ : ℕ → ℕ), StrictMono φ ∧ Filter.Tendsto (fun (k : ℕ) => A (φ k)) Filter.atTop (nhds Z)

Every eventually entrywise-bounded sequence of Hessian matrices has a convergent subsequence.

In standard mathematical terms, if there is a real number R such that |A_k i j| ≤ R for every pair of coordinates (i,j) and all sufficiently large k, then there exist a Hessian Z and a strictly increasing sequence of indices φ : Nat -> Nat such that A_{φ(k)} -> Z.

theorem ViscositySolns.abs_hessian_entry_le_half_diag_sum_of_posSemidef {n : ℕ} {A : Hessian n} (hA : Matrix.PosSemidef A) (i j : Fin n) : |A i j| ≤ (A i i + A j j) / 2

For a positive semidefinite Hessian matrix, every off-diagonal entry is bounded in absolute value by half the sum of the corresponding diagonal entries.

In standard mathematical terms, if A is positive semidefinite, then |A_{ij}| ≤ (A_{ii} + A_{jj}) / 2. This follows by applying nonnegativity of the quadratic form associated to A to the two vectors e_i + e_j and e_i - e_j.

theorem ViscositySolns.abs_hessian_entry_le_of_posSemidef_of_diag_le {n : ℕ} {A : Hessian n} {R : ℝ} (hA : Matrix.PosSemidef A) (hdiag : ∀ (i : Fin n), A i i ≤ R) (i j : Fin n) : |A i j| ≤ R

If 0 ≤ A and all diagonal entries of A are bounded above by R, then all entries of A are bounded in absolute value by R.

theorem ViscositySolns.exists_eventually_entrywise_abs_le_of_posSemidef_le_add_tendsto_zero {n : ℕ} {A Q : ℕ → Hessian n} {B : Hessian n} (hA : ∀ (k : ℕ), Matrix.PosSemidef (A k)) (hupper : ∀ (k : ℕ), A k ≤ Q k + B) (hQ : Filter.Tendsto Q Filter.atTop (nhds 0)) : ∃ (R : ℝ), ∀ᶠ (k : ℕ) in Filter.atTop, ∀ (i j : Fin n), |A k i j| ≤ R

Uniform Loewner lower and upper bounds give eventual entrywise boundedness when the upper-error matrices converge entrywise to zero.

In standard mathematical terms, if A_k is positive semidefinite for every k, if A_k ≤ Q_k + B for every k, and if Q_k -> 0, then there is a real number R such that |A_k i j| ≤ R for every pair of coordinates (i,j) and all sufficiently large k.

theorem ViscositySolns.continuous_hessian_quadraticForm {n : ℕ} (v : Point n) : Continuous fun (A : Hessian n) => v ⬝ᵥ Matrix.mulVec A v

The quadratic form associated to a Hessian matrix is continuous in the matrix.

theorem ViscositySolns.hessian_isHermitian_of_tendsto_isHermitian {n : ℕ} {A : ℕ → Hessian n} {Z : Hessian n} (hA : Filter.Tendsto A Filter.atTop (nhds Z)) (hHerm : ∀ (k : ℕ), Matrix.IsHermitian (A k)) : Matrix.IsHermitian Z

Hermitian Hessian matrices are closed under sequential limits.

In standard mathematical terms, if A_k -> Z entrywise and every A_k is Hermitian, then Z is Hermitian.

theorem ViscositySolns.hessian_le_of_tendsto_le {n : ℕ} {A C : ℕ → Hessian n} {Z W : Hessian n} (hA : Filter.Tendsto A Filter.atTop (nhds Z)) (hC : Filter.Tendsto C Filter.atTop (nhds W)) (hZ : Matrix.IsHermitian Z) (hW : Matrix.IsHermitian W) (hle : ∀ᶠ (k : ℕ) in Filter.atTop, A k ≤ C k) : Z ≤ W

Loewner inequalities are closed under sequential limits.

In standard mathematical terms, if A_k -> Z, C_k -> W, and A_k ≤ C_k for all sufficiently large k, then Z ≤ W, provided Z and W are Hermitian.

theorem ViscositySolns.hessian_nonneg_of_tendsto_nonneg {n : ℕ} {A : ℕ → Hessian n} {Z : Hessian n} (hA : Filter.Tendsto A Filter.atTop (nhds Z)) (hZ : Matrix.IsHermitian Z) (hnonneg : ∀ᶠ (k : ℕ) in Filter.atTop, 0 ≤ A k) : 0 ≤ Z

Positive semidefiniteness is closed under sequential limits of Hermitian Hessian matrices.

def ViscositySolns.quarticStrictification {n : ℕ} (f : Point n → ℝ) : Point n → ℝ

Subtract the coordinate quartic from a function.

Equations

• ViscositySolns.quarticStrictification f x = f x - ViscositySolns.coordinateQuartic x

theorem ViscositySolns.strictLocalMax_quarticStrictification_of_isMaxOn_univ {n : ℕ} {f : Point n → ℝ} (hmax : IsMaxOn f Set.univ 0) : StrictLocalMax (quarticStrictification f) 0

If f has a global maximum at the origin, then x ↦ f x - (∑ i, x_i^2)^2 has a strict local maximum at the origin.

noncomputable def ViscositySolns.strictifiedQuadraticObjective {n : ℕ} (g : Point n → ℝ) (B : Hessian n) : Point n → ℝ

The strictified quadratic objective used in the proof of the convex matrix theorem.

In quantified mathematical form, this is x ↦ g x - (1 / 2) * ⟪B x, x⟫ - (∑ i, x_i^2)^2.

Equations

• ViscositySolns.strictifiedQuadraticObjective g B = ViscositySolns.quarticStrictification (ViscositySolns.semiconvexQuadraticObjective g B)

theorem ViscositySolns.coordinateSemiconvexOn_strictifiedQuadraticObjective_closedBall_of_entrywise_abs_le {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {r eta : ℝ} (hconv : ConvexOn ℝ Set.univ g) (hr : 0 ≤ r) (heta : 0 ≤ eta) (hB : ∀ (i j : Fin n), |B i j| ≤ eta) : CoordinateSemiconvexOn (eta * ↑n * ↑n + 2 * (4 * ↑n ^ 2 * r ^ 2 + 2 * ↑n * r ^ 2)) (Metric.closedBall 0 r) (strictifiedQuadraticObjective g B)

The strictified quadratic objective is semiconvex on every closed ball, with an explicit constant from an entrywise bound on the quadratic matrix.

In quantified mathematical form, suppose g is convex on R^n, 0 ≤ r, 0 ≤ η, and |Bᵢⱼ| ≤ η for every matrix entry. Then

x ↦ g x - (1 / 2) * ⟪B x, x⟫ - (∑ i x_i^2)^2

satisfies the coordinate semiconvexity inequality on closedBall 0 r with constant

η n^2 + 2 * (4 n^2 r^2 + 2 n r^2).

theorem ViscositySolns.exists_coordinateSemiconvexOn_strictifiedQuadraticObjective_closedBall {n : ℕ} {g : Point n → ℝ} (B : Hessian n) {r : ℝ} (hconv : ConvexOn ℝ Set.univ g) (hr : 0 ≤ r) : ∃ (lambda : ℝ), CoordinateSemiconvexOn lambda (Metric.closedBall 0 r) (strictifiedQuadraticObjective g B)

The strictified quadratic objective is semiconvex on every closed ball.

In quantified mathematical form, if g is convex on R^n and 0 ≤ r, then there exists a real number lambda such that

x ↦ g x - (1 / 2) * ⟪B x, x⟫ - (∑ i x_i^2)^2

satisfies the coordinate semiconvexity inequality with constant lambda on closedBall 0 r.

theorem ViscositySolns.strictLocalMax_strictifiedQuadraticObjective_of_isMaxOn_univ {n : ℕ} {g : Point n → ℝ} {B : Hessian n} (hmax : IsMaxOn (semiconvexQuadraticObjective g B) Set.univ 0) : StrictLocalMax (strictifiedQuadraticObjective g B) 0

If x ↦ g x - (1 / 2) * ⟪B x, x⟫ has a maximum at 0 on all of R^n, then the strictified quadratic objective has a strict local maximum at 0.

theorem ViscositySolns.HasSecondOrderJet.superjet_semiconvexQuadraticObjective_of_strictified {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {x a : Point n} {X : Hessian n} (h : HasSecondOrderJet (strictifiedQuadraticObjective g B) x a X) : { gradient := a, hessian := X } + coordinateQuarticJetAt x ∈ Superjet Set.univ (semiconvexQuadraticObjective g B) x

Adding back the coordinate quartic converts a superjet of the strictified quadratic objective into a superjet of the unstrictified quadratic objective.

theorem ViscositySolns.HasSecondOrderJet.subjet_semiconvexQuadraticObjective_of_strictified {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {x a : Point n} {X : Hessian n} (h : HasSecondOrderJet (strictifiedQuadraticObjective g B) x a X) : { gradient := a, hessian := X } + coordinateQuarticJetAt x ∈ Subjet Set.univ (semiconvexQuadraticObjective g B) x

Adding back the coordinate quartic converts a subjet of the strictified quadratic objective into a subjet of the unstrictified quadratic objective.

theorem ViscositySolns.HasSecondOrderJet.superjet_of_strictifiedQuadraticObjective {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {x a : Point n} {X : Hessian n} (h : HasSecondOrderJet (strictifiedQuadraticObjective g B) x a X) : { gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x ∈ Superjet Set.univ g x

Adding back both smooth terms converts a two-sided jet of the strictified quadratic objective into a superjet of the original function.

theorem ViscositySolns.HasSecondOrderJet.subjet_of_strictifiedQuadraticObjective {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {x a : Point n} {X : Hessian n} (h : HasSecondOrderJet (strictifiedQuadraticObjective g B) x a X) : { gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x ∈ Subjet Set.univ g x

Adding back both smooth terms converts a two-sided jet of the strictified quadratic objective into a subjet of the original function.

theorem ViscositySolns.HasSecondOrderJet.of_strictifiedQuadraticObjective {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {x a : Point n} {X : Hessian n} (h : HasSecondOrderJet (strictifiedQuadraticObjective g B) x a X) : HasSecondOrderJet g x ({ gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x).gradient ({ gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x).hessian

Adding back the quartic and quadratic terms converts a two-sided jet of the strictified quadratic objective into a two-sided jet of the original function.

theorem ViscositySolns.HasSecondOrderJet.of_eq_strictifiedQuadraticObjectiveJet {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {x a : Point n} {X : Hessian n} {J : Jet n} (h : HasSecondOrderJet (strictifiedQuadraticObjective g B) x a X) (hJ : J = { gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x) : HasSecondOrderJet g x J.gradient J.hessian

The selected jet obtained by adding back the quartic and quadratic terms is an ordinary two-sided jet of the original function.

theorem ViscositySolns.HasSecondOrderJet.closedSuperjet_of_strictifiedQuadraticObjective {n : ℕ} {g : Point n → ℝ} {B : Hessian n} {x a : Point n} {X : Hessian n} (h : HasSecondOrderJet (strictifiedQuadraticObjective g B) x a X) : { gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x ∈ ClosedSuperjet Set.univ g x

A two-sided jet of the strictified quadratic objective gives a closed superjet of the original function after adding back the quartic and quadratic jets.

theorem ViscositySolns.strictifiedQuadraticObjective_closedSuperjetJet_hessian {n : ℕ} (B : Hessian n) (x a : Point n) (X : Hessian n) : ({ gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x).hessian = X + (coordinateQuarticJetAt x).hessian + B

The Hessian component of the closed-superjet jet obtained by adding back the quartic and quadratic terms.

theorem ViscositySolns.strictifiedQuadraticObjective_closedSuperjetJet_hessian_isHermitian {n : ℕ} {B : Hessian n} {x a : Point n} {X : Hessian n} (hX : Matrix.IsHermitian X) (hB : Matrix.IsHermitian B) : Matrix.IsHermitian ({ gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x).hessian

If the Hessian from the two-sided jet and the quadratic matrix are Hermitian, then the Hessian component of the resulting closed-superjet jet is Hermitian.

theorem ViscositySolns.strictifiedQuadraticObjective_closedSuperjetJet_hessian_le {n : ℕ} {B : Hessian n} {x a : Point n} {X : Hessian n} (hX : X ≤ 0) : ({ gradient := a, hessian := X } + coordinateQuarticJetAt x + quadraticModelJetAt 0 0 B x).hessian ≤ (coordinateQuarticJetAt x).hessian + B

The local-maximum inequality X ≤ 0 gives the upper bound for the Hessian of the closed-superjet jet obtained from the strictified quadratic objective.