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

Semijet calculus (ShiftsClosedness)

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

theorem ViscositySolns.superjet_add_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J A : Jet n} (hJ : J ∈ Superjet C u x) (hφ : HasSecondOrderExpansionWithin C φ x A) : J + A ∈ Superjet C (fun (y : Point n) => u y + φ y) x

Adding a function with second-order expansion shifts superjets by its jet.

theorem ViscositySolns.subjet_add_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J A : Jet n} (hJ : J ∈ Subjet C u x) (hφ : HasSecondOrderExpansionWithin C φ x A) : J + A ∈ Subjet C (fun (y : Point n) => u y + φ y) x

Adding a function with second-order expansion shifts subjets by its jet.

theorem ViscositySolns.superjet_sub_of_add_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J A : Jet n} (hJ : J ∈ Superjet C (fun (y : Point n) => u y + φ y) x) (hφ : HasSecondOrderExpansionWithin C φ x A) : J - A ∈ Superjet C u x

Subtracting the jet of a function with second-order expansion pulls back a superjet of u + φ to a superjet of u.

theorem ViscositySolns.subjet_sub_of_add_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J A : Jet n} (hJ : J ∈ Subjet C (fun (y : Point n) => u y + φ y) x) (hφ : HasSecondOrderExpansionWithin C φ x A) : J - A ∈ Subjet C u x

Subtracting the jet of a function with second-order expansion pulls back a subjet of u + φ to a subjet of u.

theorem ViscositySolns.superjet_add_hasSecondOrderExpansionWithin_iff {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J A : Jet n} (hφ : HasSecondOrderExpansionWithin C φ x A) : J ∈ Superjet C (fun (y : Point n) => u y + φ y) x ↔ J - A ∈ Superjet C u x

Shift equivalence for superjets under addition of a function with second-order expansion.

theorem ViscositySolns.subjet_add_hasSecondOrderExpansionWithin_iff {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x : Point n} {J A : Jet n} (hφ : HasSecondOrderExpansionWithin C φ x A) : J ∈ Subjet C (fun (y : Point n) => u y + φ y) x ↔ J - A ∈ Subjet C u x

Shift equivalence for subjets under addition of a function with second-order expansion.

theorem ViscositySolns.superjet_mono_hessian {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {Y : Hessian n} (hJ : J ∈ Superjet C u x) (hXY : J.hessian ≤ Y) : { gradient := J.gradient, hessian := Y } ∈ Superjet C u x

Enlarging the Hessian of a superjet preserves membership. This is the basic Loewner-order monotonicity of second-order superjets.

theorem ViscositySolns.subjet_mono_hessian {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {Y : Hessian n} (hJ : J ∈ Subjet C u x) (hYX : Y ≤ J.hessian) : { gradient := J.gradient, hessian := Y } ∈ Subjet C u x

Shrinking the Hessian of a subjet preserves membership. This is the subjet counterpart to superjet_mono_hessian.

theorem ViscositySolns.eventually_le_quadraticModel_hessian_add_identity_of_superjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} (hδ : 0 < δ) (hJ : J ∈ Superjet C u x) : ∀ᶠ (y : Point n) in nhdsWithin x C, u y ≤ quadraticModel x (u x) J.gradient (J.hessian + δ • 1) y

A positive identity-Hessian perturbation turns a superjet into an eventual ordinary upper support with no remainder term.

theorem ViscositySolns.eventually_quadraticModel_hessian_sub_identity_le_of_subjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ : ℝ} (hδ : 0 < δ) (hJ : J ∈ Subjet C u x) : ∀ᶠ (y : Point n) in nhdsWithin x C, quadraticModel x (u x) J.gradient (J.hessian - δ • 1) y ≤ u y

A positive identity-Hessian subtraction turns a subjet into an eventual ordinary lower support with no remainder term.

theorem ViscositySolns.eventually_quadraticModel_lift_hessian_sub_identity_lt_of_subjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {δ γ : ℝ} (hγ : 0 < γ) (hJ : J ∈ Subjet C u x) : ∀ᶠ (y : Point n) in nhdsWithin x C, δ < 1 / 4 * γ * ‖y - x‖ ^ 2 → quadraticModel x (u x + δ) J.gradient (J.hessian - γ • 1) y < u y

A lifted, downward-bent subjet quadratic is strictly below the function at nearby points where the vertical lift is smaller than the bend margin.

The constant 1 / 4 leaves half of the identity-Hessian bend to absorb the subjet o(|y-x|^2) remainder and half as a strict gap. This is the local estimate needed before choosing annulus radii in the Perron bump argument.

theorem ViscositySolns.eventually_forall_quadraticModel_lift_hessian_sub_identity_lt_of_subjet {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} {γ : ℝ} (hγ : 0 < γ) (hJ : J ∈ Subjet C u x) : ∀ᶠ (y : Point n) in nhdsWithin x C, ∀ δ < 1 / 4 * γ * ‖y - x‖ ^ 2, quadraticModel x (u x + δ) J.gradient (J.hessian - γ • 1) y < u y

Uniform version of eventually_quadraticModel_lift_hessian_sub_identity_lt_of_subjet: for a fixed downward identity-Hessian bend, one relative neighborhood works for all vertical lifts that fit inside the bend margin at the evaluation point.

theorem ViscositySolns.superjet_of_forall_add_pos_smul_one {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : ∀ (δ : ℝ), 0 < δ → { gradient := p, hessian := X + δ • 1 } ∈ Superjet C u x) : { gradient := p, hessian := X } ∈ Superjet C u x

If all positive identity-Hessian enlargements of a fixed-gradient jet are superjets, then the limiting jet is a superjet. This is the asymptotic half of CIL Remark 2.6(i)'s fixed-gradient closedness statement.

theorem ViscositySolns.subjet_of_forall_sub_pos_smul_one {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : ∀ (δ : ℝ), 0 < δ → { gradient := p, hessian := X - δ • 1 } ∈ Subjet C u x) : { gradient := p, hessian := X } ∈ Subjet C u x

If all positive identity-Hessian shrinkings of a fixed-gradient jet are subjets, then the limiting jet is a subjet.

theorem ViscositySolns.isClosed_superjet_hessian_slice {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x p : Point n) : IsClosed {X : Hessian n | { gradient := p, hessian := X } ∈ Superjet C u x}

For fixed gradient p, the Hessian slice of an ordinary superjet fiber is closed. This is CIL Remark 2.6(i)'s closedness statement for {X | (p, X) ∈ J^{2,+} u(x)}.

theorem ViscositySolns.isClosed_subjet_hessian_slice {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x p : Point n) : IsClosed {X : Hessian n | { gradient := p, hessian := X } ∈ Subjet C u x}

For fixed gradient p, the Hessian slice of an ordinary subjet fiber is closed.

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

Neg duality for superjets (CIL Remark 2.6): J is a superjet of u at x if and only if the negated jet J.neg is a subjet of -u at x.

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

Neg duality for subjets (CIL Remark 2.6): J is a subjet of u at x if and only if the negated jet J.neg is a superjet of -u at x.