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

Basic second-order jet calculus

theorem ViscositySolns.HasSecondOrderJet.closedSuperjet {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : HasSecondOrderJet f x p X) : { gradient := p, hessian := X } ∈ ClosedSuperjet Set.univ f x

The superjet part of a second-order jet belongs to the closed superjet.

theorem ViscositySolns.HasSecondOrderJet.closedSubjet {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : HasSecondOrderJet f x p X) : { gradient := p, hessian := X } ∈ ClosedSubjet Set.univ f x

The subjet part of a second-order jet belongs to the closed subjet.

theorem ViscositySolns.hasSecondOrderExpansionWithin_linear {n : ℕ} {C : Set (Point n)} (q x : Point n) : HasSecondOrderExpansionWithin C (fun (y : Point n) => q ⬝ᵥ y) x { gradient := q, hessian := 0 }

A linear function has its expected second-order expansion at every point.

In quantified mathematical form, for every q : R^n, the function x ↦ q · x has gradient q and Hessian 0 at every point.

theorem ViscositySolns.HasSecondOrderJet.of_linearPerturbation {n : ℕ} {f : Point n → ℝ} {x p q : Point n} {X : Hessian n} (h : HasSecondOrderJet (ViscositySolns.linearPerturbation f q) x p X) : HasSecondOrderJet f x (p - q) X

If f + q · x has a second-order jet at x, then subtracting the linear jet gives a second-order jet of f at x.

theorem ViscositySolns.HasSecondOrderJet.linearPerturbation {n : ℕ} {f : Point n → ℝ} {x p q : Point n} {X : Hessian n} (h : HasSecondOrderJet f x p X) : HasSecondOrderJet (ViscositySolns.linearPerturbation f q) x (p + q) X

If f has a second-order jet at x, then f + q · x has the corresponding second-order jet with gradient shifted by q.

theorem ViscositySolns.HasSecondOrderJet.of_semiconvexConvexification {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : HasSecondOrderJet (semiconvexConvexification lambda f) x p X) : HasSecondOrderJet f x ({ gradient := p, hessian := X } - quadraticModelJetAt 0 0 (lambda • 1) x).gradient ({ gradient := p, hessian := X } - quadraticModelJetAt 0 0 (lambda • 1) x).hessian

Subtracting the quadratic function used for semiconvex convexification converts a two-sided jet of the convexified function into a two-sided jet of the original function.

In quantified mathematical form, if g(x) = f(x) + (lambda / 2) * ∑ i, x_i^2 and (p, X) is an ordinary two-sided second-order jet of g at x, then subtracting the first and second derivatives of (lambda / 2) * ∑ i, x_i^2 at x gives an ordinary two-sided second-order jet of f at x.

theorem ViscositySolns.HasSomeSecondOrderJet.of_semiconvexConvexification {n : ℕ} {lambda : ℝ} {f : Point n → ℝ} {x : Point n} (h : HasSomeSecondOrderJet (semiconvexConvexification lambda f) x) : HasSomeSecondOrderJet f x

Existential form of the semiconvex-to-convex reduction for two-sided jets.

This is the jet-level version of the source proof's reduction from a semiconvex function to its convexification by adding a quadratic.

theorem ViscositySolns.HasSecondOrderJet.hasSecondOrderExpansionWithin {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : HasSecondOrderJet f x p X) : HasSecondOrderExpansionWithin Set.univ f x { gradient := p, hessian := X }

If (p, X) belongs both to the ordinary superjet and to the ordinary subjet of f at x, then f has the corresponding second-order expansion at x.

In quantified mathematical form, there exists a function ρ such that ρ(y) = o(|y - x|^2) as y -> x and, for all y sufficiently close to x,

f y = f x + p · (y - x) + (1 / 2) * ⟪X (y - x), y - x⟫ + ρ y.

theorem ViscositySolns.quadraticModel_line {n : ℕ} (x : Point n) (r t : ℝ) (p v : Point n) (X : Hessian n) : quadraticModel x r p X (x + t • v) = r + t * p ⬝ᵥ v + 1 / 2 * t ^ 2 * Matrix.mulVec X v ⬝ᵥ v

The restriction of a quadratic model to a line through its base point.

In quantified mathematical form, for every t : R and every vector v,

quadraticModel x r p X (x + t v) = r + t * p · v + (t^2 / 2) * ⟪X v, v⟫.

theorem ViscositySolns.quadraticModel_zero_zero_isBigO_norm_sq {n : ℕ} (x : Point n) (X : Hessian n) : (fun (y : Point n) => quadraticModel x 0 0 X y) =O[nhds x] fun (y : Point n) => ‖y - x‖ ^ 2

The quadratic part of a fixed Hessian is bounded by a constant multiple of |y - x|^2 near x.

In quantified mathematical form, for every matrix X, the function y ↦ (1 / 2) * ⟪X (y - x), y - x⟫ is O(|y - x|^2) as y -> x.

theorem ViscositySolns.quadraticModel_zero_zero_isLittleO_sub {n : ℕ} (x : Point n) (X : Hessian n) : (fun (y : Point n) => quadraticModel x 0 0 X y) =o[nhds x] fun (y : Point n) => y - x

The quadratic part of a fixed Hessian is first-order negligible at its base point.

In quantified mathematical form, for every matrix X,

(1 / 2) * ⟪X (y - x), y - x⟫ = o(|y - x|)

as y -> x.

theorem ViscositySolns.HasSecondOrderExpansionWithin.hasFDerivAt {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : HasSecondOrderExpansionWithin Set.univ f x { gradient := p, hessian := X }) : HasFDerivAt f (gradientLinearMap p) x

A second-order expansion gives the corresponding first Fréchet derivative.

In quantified mathematical form, if

f y = f x + p · (y - x) + (1 / 2) * ⟪X (y - x), y - x⟫ + o(|y - x|^2)

as y -> x, then the Fréchet derivative of f at x is the linear map h ↦ p · h.

theorem ViscositySolns.HasSecondOrderJet.gradient_eq_zero_of_isLocalMax {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (hmax : IsLocalMax f x) (h : HasSecondOrderJet f x p X) : p = 0

At a local maximum point, the gradient component of a two-sided ordinary jet is zero.

In quantified mathematical form, if f has a local maximum at x and (p, X) belongs both to the ordinary superjet and the ordinary subjet of f at x, then p = 0.

theorem ViscositySolns.HasSecondOrderJet.quadraticForm_nonpos_of_isLocalMax {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (hmax : IsLocalMax f x) (h : HasSecondOrderJet f x p X) (v : Point n) : Matrix.mulVec X v ⬝ᵥ v ≤ 0

At a local maximum point, the quadratic form determined by the Hessian component of a two-sided ordinary jet is nonpositive in every direction.

In quantified mathematical form, if f has a local maximum at x and (p, X) belongs both to the ordinary superjet and to the ordinary subjet of f at x, then for every v : R^n, ⟪X v, v⟫ ≤ 0.

theorem ViscositySolns.StrictLocalMax.isLocalMax {n : ℕ} {f : Point n → ℝ} {x0 : Point n} (h : StrictLocalMax f x0) : IsLocalMax f x0

If f has a strict local maximum at x0, then f has a local maximum at x0.

In quantified mathematical form, this says: if there is a neighborhood U of x0 such that every x ∈ U with x ≠ x0 satisfies f x < f x0, then there is a neighborhood V of x0 such that every x ∈ V satisfies f x ≤ f x0.

theorem ViscositySolns.StrictLocalMax.exists_closedBall_strict {n : ℕ} {f : Point n → ℝ} {x0 : Point n} (h : StrictLocalMax f x0) {R : ℝ} (hR : 0 < R) : ∃ (r : ℝ), 0 < r ∧ r ≤ R ∧ ∀ x ∈ Metric.closedBall x0 r, x ≠ x0 → f x < f x0

A strict local maximum is strict on a sufficiently small closed ball.

In quantified mathematical form, if x0 is a strict local maximum point of f and R > 0, then there exists r with 0 < r ≤ R such that, for every x ∈ closedBall x0 r, if x ≠ x0, then f x < f x0.

theorem ViscositySolns.superjet_zero_of_isLocalMax {n : ℕ} {f : Point n → ℝ} {x : Point n} (hmax : IsLocalMax f x) : { gradient := 0, hessian := 0 } ∈ Superjet Set.univ f x

At a local maximum point, the zero jet is a superjet.

In quantified mathematical form, if there is a neighborhood U of x such that f y ≤ f x for every y ∈ U, then (0, 0) belongs to J^{2,+}_{R^n} f(x).

theorem ViscositySolns.closedSuperjet_zero_of_isLocalMax {n : ℕ} {f : Point n → ℝ} {x : Point n} (hmax : IsLocalMax f x) : { gradient := 0, hessian := 0 } ∈ ClosedSuperjet Set.univ f x

At a local maximum point, the zero jet belongs to the closed superjet.

In quantified mathematical form, if there is a neighborhood U of x such that f y ≤ f x for every y ∈ U, then (0, 0) belongs to \overline J^{2,+}_{R^n} f(x).

def ViscositySolns.LocalMaxSecondOrderJetCalculusTheorem (n : ℕ) : Prop

The second-order calculus theorem needed after applying Jensen's lemma.

In quantified mathematical form, LocalMaxSecondOrderJetCalculusTheorem n means: for every function f : R^n -> R, every point x, every vector p, and every Hermitian matrix X, if f has a local maximum at x and (p, X) belongs both to the ordinary superjet and to the ordinary subjet of f at x, then p = 0 and X ≤ 0.

Equations

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

theorem ViscositySolns.HasSecondOrderJet.hessian_le_zero_of_isLocalMax {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (hX : Matrix.IsHermitian X) (hmax : IsLocalMax f x) (h : HasSecondOrderJet f x p X) : X ≤ 0

At a local maximum point, the Hermitian Hessian component of a two-sided ordinary jet is nonpositive in the Loewner order.

theorem ViscositySolns.localMaxSecondOrderJetCalculusTheorem {n : ℕ} : LocalMaxSecondOrderJetCalculusTheorem n

The local-maximum second-order calculus theorem for Hermitian Hessian components.

theorem ViscositySolns.LocalMaxSecondOrderJetCalculusTheorem.apply_linearPerturbation {n : ℕ} (hcalc : LocalMaxSecondOrderJetCalculusTheorem n) {f : Point n → ℝ} {x a q : Point n} {X : Hessian n} (hX : Matrix.IsHermitian X) (hmax : IsLocalMax (linearPerturbation f q) x) (hjet : HasSecondOrderJet f x a X) : a + q = 0 ∧ X ≤ 0

The local-maximum second-order calculus theorem applies after adding a linear perturbation.

In quantified mathematical form, assume the theorem LocalMaxSecondOrderJetCalculusTheorem n. If f has second-order jet (a, X) at x, the matrix X is Hermitian, and the function y ↦ f y + q · y has a local maximum at x, then a + q = 0 and X ≤ 0.