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

Semijet calculus (QuadraticControl)

Part of the calculus lemmas for second-order superjets and subjets. Split from Calculus.lean; see the umbrella module docstring.

theorem ViscositySolns.tendsto_div_self_of_isLittleO_sq {rho : ℝ → ℝ} (hrho : rho =o[nhds 0] fun (t : ℝ) => t ^ 2) (l : Filter ℝ) (hl : l ≤ nhdsWithin 0 {t : ℝ | t ≠ 0}) (hl_nhds : l ≤ nhds 0) : Filter.Tendsto (fun (t : ℝ) => rho t / t) l (nhds 0)

If rho(t) = o(t^2), then rho(t) / t -> 0 along any filter approaching 0 through nonzero points.

theorem ViscositySolns.eq_zero_of_eventually_nonneg_linear_add_sq_add_isLittleO_sq {a b : ℝ} {rho : ℝ → ℝ} (hrho : rho =o[nhds 0] fun (t : ℝ) => t ^ 2) (hineq : ∀ᶠ (t : ℝ) in nhds 0, 0 ≤ a * t + b * t ^ 2 + rho t) : a = 0

First-order scalar coefficient extraction from a two-sided neighborhood.

If rho(t) = o(t^2) and 0 <= a t + b t^2 + rho(t) for all t sufficiently close to 0, then a = 0. The proof divides by t on the right and left one-sided neighborhoods and compares the two limits.

theorem ViscositySolns.nonpos_of_eventually_mul_sq_le_isLittleO_sq {c : ℝ} {f : ℝ → ℝ} (hf : f =o[nhds 0] fun (t : ℝ) => t ^ 2) (hle : ∀ᶠ (t : ℝ) in nhds 0, c * t ^ 2 ≤ f t) : c ≤ 0

A scalar o(t^2) comparison lemma for extracting second-order coefficients.

In standard mathematical terms, if f(t) = o(t^2) as t -> 0 and c t^2 <= f(t) for all t sufficiently close to 0, then c <= 0. The proof works on the punctured neighborhood of 0, divides by t^2, and passes to the limit.

theorem ViscositySolns.superjet_zero_univ_gradient_eq_zero {n : ℕ} {x : Point n} {J : Jet n} (hJ : J ∈ Superjet Set.univ (fun (x : Point n) => 0) x) : J.gradient = 0

A full-neighborhood superjet of the zero function has zero gradient.

The proof restricts the superjet inequality to every affine line through the base point and applies the scalar first-order extraction lemma.

theorem ViscositySolns.superjet_zero_univ_quadraticForm_nonneg_of_gradient_eq_zero {n : ℕ} {x : Point n} {J : Jet n} (hJ : J ∈ Superjet Set.univ (fun (x : Point n) => 0) x) (hgrad : J.gradient = 0) (v : Point n) : 0 ≤ Matrix.mulVec J.hessian v ⬝ᵥ v

The Hessian quadratic form of a zero-function superjet is nonnegative once the gradient part is known to vanish.

This is the line-restriction step needed to control quadratic bumps. Applied to a superjet of a quadratic model after subtracting the recentered quadratic expansion, it gives the quadratic-form inequalities that imply Loewner order under the necessary Hermitian hypothesis.

theorem ViscositySolns.superjet_zero_univ_hessian_nonneg_of_gradient_eq_zero {n : ℕ} {x : Point n} {J : Jet n} (hJ : J ∈ Superjet Set.univ (fun (x : Point n) => 0) x) (hgrad : J.gradient = 0) (hHerm : Matrix.IsHermitian J.hessian) : 0 ≤ J.hessian

A zero-function superjet with zero gradient has nonnegative Hessian, provided the Hessian is Hermitian.

The Hermitian hypothesis is the unavoidable bridge from scalar quadratic-form inequalities to mathlib's Loewner order on real matrices.

theorem ViscositySolns.quadraticModel_superjet_hessian_le_of_gradient_eq_of_isHermitian_sub {n : ℕ} {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} {J : Jet n} (hJ : J ∈ Superjet Set.univ (fun (y : Point n) => quadraticModel x0 r p X y) x) (hgrad : J.gradient = (quadraticModelJetAt x0 p X x).gradient) (hHerm : Matrix.IsHermitian (J.hessian - (quadraticModelJetAt x0 p X x).hessian)) : (quadraticModelJetAt x0 p X x).hessian ≤ J.hessian

Hessian control for a full-neighborhood superjet of a quadratic model, after the first-order part has been identified.

Subtracting the exact recentered quadratic expansion turns the superjet into a zero-function superjet. The preceding zero-function lemma then gives nonnegative Hessian difference, hence the desired Loewner inequality.

theorem ViscositySolns.quadraticModel_superjet_control_of_isHermitian_sub {n : ℕ} {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} {J : Jet n} (hJ : J ∈ Superjet Set.univ (fun (y : Point n) => quadraticModel x0 r p X y) x) (hHerm : Matrix.IsHermitian (J.hessian - (quadraticModelJetAt x0 p X x).hessian)) : J.gradient = (quadraticModelJetAt x0 p X x).gradient ∧ (quadraticModelJetAt x0 p X x).hessian ≤ J.hessian

Full-neighborhood superjet control for a quadratic model, up to the necessary Hermitian hypothesis on the Hessian difference.

The gradient equality is forced by subtracting the exact quadratic expansion and applying superjet_zero_univ_gradient_eq_zero; the Hessian inequality is then the preceding Loewner-control lemma.

theorem ViscositySolns.superjet_eq_univ_of_mem_interior {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} (hx : x ∈ interior C) : Superjet C u x = Superjet Set.univ u x

At an interior point of the domain, ordinary superjets over the domain are the same as full-neighborhood superjets.

theorem ViscositySolns.quadraticModel_superjet_control_of_mem_interior_of_isHermitian_sub {n : ℕ} {C : Set (Point n)} {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} {J : Jet n} (hx : x ∈ interior C) (hJ : J ∈ Superjet C (fun (y : Point n) => quadraticModel x0 r p X y) x) (hHerm : Matrix.IsHermitian (J.hessian - (quadraticModelJetAt x0 p X x).hessian)) : J.gradient = (quadraticModelJetAt x0 p X x).gradient ∧ (quadraticModelJetAt x0 p X x).hessian ≤ J.hessian

Interior-domain superjet control for a quadratic model.

This is the local version used by smooth Perron bumps: once the base point is interior to the PDE domain, superjets relative to the domain can be read as full-neighborhood superjets and controlled by the canonical recentered quadratic jet.

theorem ViscositySolns.superjet_symHessian {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Superjet C u x) : { gradient := J.gradient, hessian := symHessian J.hessian } ∈ Superjet C u x

Symmetrizing the Hessian component of a superjet preserves superjet membership.

The defining quadratic model only sees the symmetric part of the Hessian.

theorem ViscositySolns.subjet_symHessian {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Subjet C u x) : { gradient := J.gradient, hessian := symHessian J.hessian } ∈ Subjet C u x

Symmetrizing the Hessian component of a subjet preserves subjet membership.

theorem ViscositySolns.quadraticModel_superjet_control_symHessian_of_mem_interior {n : ℕ} {C : Set (Point n)} {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} {J : Jet n} (hx : x ∈ interior C) (hX : Matrix.IsHermitian X) (hJ : J ∈ Superjet C (fun (y : Point n) => quadraticModel x0 r p X y) x) : J.gradient = (quadraticModelJetAt x0 p X x).gradient ∧ (quadraticModelJetAt x0 p X x).hessian ≤ symHessian J.hessian

Interior-domain superjet control for a quadratic model after symmetrizing the tested Hessian.

This avoids asking every raw superjet Hessian difference to be Hermitian. Instead, the quadratic's own Hessian is Hermitian and the arbitrary tested Hessian is replaced by its symmetric part, which defines the same quadratic touching polynomial.

theorem ViscositySolns.hessian_le_of_forall_quadraticForm_le_of_isHermitian_sub {n : ℕ} {X Y : Hessian n} (hHerm : Matrix.IsHermitian (Y - X)) (hquad : ∀ (v : Point n), Matrix.mulVec X v ⬝ᵥ v ≤ Matrix.mulVec Y v ⬝ᵥ v) : X ≤ Y

Recover Loewner order from quadratic-form inequalities, once the Hessian difference is known to be Hermitian.

The Hermitian hypothesis is essential in the current jet setup: quadratic models only see the symmetric part of a matrix, while mathlib's Loewner order is an order on Hermitian differences.

theorem ViscositySolns.superjet_add {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} {J K : Jet n} (hJ : J ∈ Superjet C u x) (hK : K ∈ Superjet C v x) : J + K ∈ Superjet C (fun (y : Point n) => u y + v y) x

If J is a superjet of u and K is a superjet of v, then J + K is a superjet of u + v. This is the formal version of CIL Remark 2.6(ii)'s inclusion J^{2,+}(u+v) ⊇ J^{2,+}u + J^{2,+}v.

theorem ViscositySolns.subjet_add {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} {J K : Jet n} (hJ : J ∈ Subjet C u x) (hK : K ∈ Subjet C v x) : J + K ∈ Subjet C (fun (y : Point n) => u y + v y) x

If J is a subjet of u and K is a subjet of v, then J + K is a subjet of u + v.

theorem ViscositySolns.superjet_max_of_left {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Superjet C (fun (y : Point n) => max (u y) (v y)) x) (hactive : max (u x) (v x) = u x) : J ∈ Superjet C u x

A superjet of max u v at a point where u is an active branch is a superjet of u.

theorem ViscositySolns.superjet_max_of_right {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Superjet C (fun (y : Point n) => max (u y) (v y)) x) (hactive : max (u x) (v x) = v x) : J ∈ Superjet C v x

A superjet of max u v at a point where v is an active branch is a superjet of v.

theorem ViscositySolns.subjet_min_of_left {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Subjet C (fun (y : Point n) => min (u y) (v y)) x) (hactive : min (u x) (v x) = u x) : J ∈ Subjet C u x

A subjet of min u v at a point where u is an active branch is a subjet of u.

theorem ViscositySolns.subjet_min_of_right {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Subjet C (fun (y : Point n) => min (u y) (v y)) x) (hactive : min (u x) (v x) = v x) : J ∈ Subjet C v x

A subjet of min u v at a point where v is an active branch is a subjet of v.

theorem ViscositySolns.superjet_congr_eqOn {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} (h : Set.EqOn u v C) (hx : x ∈ C) : Superjet C u x = Superjet C v x

Superjet fibers depend only on the values of the function on the domain C.

theorem ViscositySolns.subjet_congr_eqOn {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} (h : Set.EqOn u v C) (hx : x ∈ C) : Subjet C u x = Subjet C v x

Subjet fibers depend only on the values of the function on the domain C.

theorem ViscositySolns.superjet_sub_const_iff {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} : J ∈ Superjet C (fun (y : Point n) => u y - δ) x ↔ J ∈ Superjet C u x

Subtracting a constant from a function does not change its superjet fibers.

In quantified mathematical form, for every real number δ, J ∈ J^{2,+}_C (u - δ)(x) if and only if J ∈ J^{2,+}_C u(x).

theorem ViscositySolns.subjet_sub_const_iff {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} : J ∈ Subjet C (fun (y : Point n) => u y - δ) x ↔ J ∈ Subjet C u x

Subtracting a constant from a function does not change its subjet fibers.

In quantified mathematical form, for every real number δ, J ∈ J^{2,-}_C (u - δ)(x) if and only if J ∈ J^{2,-}_C u(x).

theorem ViscositySolns.superjet_convexCombination {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J K : Jet n} {a b : ℝ} (hJ : J ∈ Superjet C u x) (hK : K ∈ Superjet C u x) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • J + b • K ∈ Superjet C u x

Convex combinations of superjets remain superjets. This is the concrete form of convexity of the fiber J^{2,+}_C u(x).

theorem ViscositySolns.subjet_convexCombination {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J K : Jet n} {a b : ℝ} (hJ : J ∈ Subjet C u x) (hK : K ∈ Subjet C u x) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • J + b • K ∈ Subjet C u x

Convex combinations of subjets remain subjets. This is the concrete form of convexity of the fiber J^{2,-}_C u(x).

theorem ViscositySolns.convex_superjet {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x : Point n) : Convex ℝ (Superjet C u x)

Ordinary superjet fibers are convex.

theorem ViscositySolns.convex_subjet {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x : Point n) : Convex ℝ (Subjet C u x)

Ordinary subjet fibers are convex.