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

Convex jet Hessian estimates

theorem ViscositySolns.Superjet.quadraticForm_nonneg_of_convexOn_closedBall {n : ℕ} {g : Point n → ℝ} {x x0 : Point n} {r : ℝ} {J : Jet n} (hconv : ConvexOn ℝ (Metric.closedBall x0 r) g) (hx : x ∈ Metric.ball x0 r) (hJ : J ∈ Superjet Set.univ g x) (v : Point n) : 0 ≤ Matrix.mulVec J.hessian v ⬝ᵥ v

For a function convex on a closed ball, the Hessian component of an ordinary superjet at an interior point of that ball has nonnegative quadratic form in every direction.

In quantified mathematical form, if g is convex on closedBall x0 r, x ∈ ball x0 r, (p, X) ∈ J^{2,+}_{R^n} g(x), and v ∈ R^n, then 0 ≤ ⟪Xv, v⟫.

theorem ViscositySolns.Superjet.hessian_nonneg_of_convexOn_closedBall {n : ℕ} {g : Point n → ℝ} {x x0 : Point n} {r : ℝ} {J : Jet n} (hconv : ConvexOn ℝ (Metric.closedBall x0 r) g) (hx : x ∈ Metric.ball x0 r) (hJ : J ∈ Superjet Set.univ g x) (hHerm : Matrix.IsHermitian J.hessian) : 0 ≤ J.hessian

For a function convex on a closed ball, a Hermitian Hessian component of an ordinary superjet at an interior point is nonnegative in the Loewner order.

theorem ViscositySolns.Superjet.quadraticForm_nonneg_of_convexOn {n : ℕ} {g : Point n → ℝ} {x : Point n} {J : Jet n} (hconv : ConvexOn ℝ Set.univ g) (hJ : J ∈ Superjet Set.univ g x) (v : Point n) : 0 ≤ Matrix.mulVec J.hessian v ⬝ᵥ v

For a convex function, the Hessian component of an ordinary superjet has nonnegative quadratic form in every direction.

In quantified mathematical form, if g : R^n -> R is convex, if (p, X) belongs to J^{2,+}_{R^n} g(x), and if v ∈ R^n, then 0 ≤ ⟪Xv, v⟫.

theorem ViscositySolns.Superjet.hessian_nonneg_of_convexOn {n : ℕ} {g : Point n → ℝ} {x : Point n} {J : Jet n} (hconv : ConvexOn ℝ Set.univ g) (hJ : J ∈ Superjet Set.univ g x) (hHerm : Matrix.IsHermitian J.hessian) : 0 ≤ J.hessian

For a convex function, a Hermitian Hessian component of an ordinary superjet is nonnegative in the Loewner order.

theorem ViscositySolns.ClosedSuperjet.quadraticForm_nonneg_of_convexOn {n : ℕ} {g : Point n → ℝ} {x : Point n} {J : Jet n} (hconv : ConvexOn ℝ Set.univ g) (hJ : J ∈ ClosedSuperjet Set.univ g x) (v : Point n) : 0 ≤ Matrix.mulVec J.hessian v ⬝ᵥ v

For a convex function, the Hessian component of a closed superjet has nonnegative quadratic form in every direction.

In quantified mathematical form, if g : R^n -> R is convex, if (p, X) belongs to \overline J^{2,+}_{R^n} g(x), and if v ∈ R^n, then 0 ≤ ⟪Xv, v⟫.

theorem ViscositySolns.ClosedSuperjet.hessian_nonneg_of_convexOn {n : ℕ} {g : Point n → ℝ} {x : Point n} {J : Jet n} (hconv : ConvexOn ℝ Set.univ g) (hJ : J ∈ ClosedSuperjet Set.univ g x) (hHerm : Matrix.IsHermitian J.hessian) : 0 ≤ J.hessian

For a convex function, a Hermitian Hessian component of a closed superjet is nonnegative in the Loewner order.