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

Second-order semijets

This file contains superjets, subjets, their excess characterizations, and the abstract test-function bridge for semijets.

def ViscositySolns.Superjet {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x0 : Point n) : Set (Jet n)

The second-order superjet J^{2,+}_C u(x0).

The inequality is the CIL condition u x <= u x0 + <p, x - x0> + 1/2 <X (x - x0), x - x0> + o(|x - x0|^2) as C ∋ x -> x0.

Equations

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

def ViscositySolns.Subjet {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x0 : Point n) : Set (Jet n)

The second-order subjet J^{2,-}_C u(x0).

This is the sign-reversed companion to Superjet: the same quadratic expansion supports u from below, up to an o(|x - x0|^2) error.

Equations

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

theorem ViscositySolns.superjet_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {u : Point n → ℝ} {x : Point n} (h : nhdsWithin x C = nhdsWithin x D) : Superjet C u x = Superjet D u x

Superjet fibers only depend on the germ of the domain at the base point.

theorem ViscositySolns.subjet_congr_nhdsWithin {n : ℕ} {C D : Set (Point n)} {u : Point n → ℝ} {x : Point n} (h : nhdsWithin x C = nhdsWithin x D) : Subjet C u x = Subjet D u x

Subjet fibers only depend on the germ of the domain at the base point.

noncomputable def ViscositySolns.SuperjetExcess {n : ℕ} (u : Point n → ℝ) (x : Point n) (J : Jet n) (y : Point n) : ℝ

The normalized numerator for the superjet condition. Superjets make this excess nonpositive up to an o(|y - x|^2) error.

Equations

• ViscositySolns.SuperjetExcess u x J y = u y - ViscositySolns.quadraticModel x (u x) J.gradient J.hessian y

noncomputable def ViscositySolns.SubjetExcess {n : ℕ} (u : Point n → ℝ) (x : Point n) (J : Jet n) (y : Point n) : ℝ

The normalized numerator for the subjet condition. Subjets make this excess nonpositive up to an o(|y - x|^2) error.

Equations

• ViscositySolns.SubjetExcess u x J y = ViscositySolns.quadraticModel x (u x) J.gradient J.hessian y - u y

theorem ViscositySolns.continuous_superjetExcess_jet {n : ℕ} (u : Point n → ℝ) (x y : Point n) : Continuous fun (J : Jet n) => SuperjetExcess u x J y

For fixed base point and evaluation point, the superjet excess depends continuously on the jet variables.

theorem ViscositySolns.continuous_subjetExcess_jet {n : ℕ} (u : Point n → ℝ) (x y : Point n) : Continuous fun (J : Jet n) => SubjetExcess u x J y

For fixed base point and evaluation point, the subjet excess depends continuously on the jet variables.

theorem ViscositySolns.superjetExcess_eq_add_quadraticModel_sub {n : ℕ} (u : Point n → ℝ) (x : Point n) (J K : Jet n) (y : Point n) : SuperjetExcess u x J y = SuperjetExcess u x K y + quadraticModel x 0 (K - J).gradient (K - J).hessian y

Changing the jet in the superjet excess adds exactly the quadratic model of the difference jet. This is the algebraic estimate used before introducing the singular ‖y - x‖^2 scale.

theorem ViscositySolns.subjetExcess_eq_add_quadraticModel_sub {n : ℕ} (u : Point n → ℝ) (x : Point n) (J K : Jet n) (y : Point n) : SubjetExcess u x J y = SubjetExcess u x K y + quadraticModel x 0 (J - K).gradient (J - K).hessian y

Changing the jet in the subjet excess adds exactly the quadratic model of the difference jet.

def ViscositySolns.SecondOrderNonposWithin {n : ℕ} (C : Set (Point n)) (x : Point n) (excess : Point n → ℝ) : Prop

An excess is second-order nonpositive at x relative to C: for every positive ε, the set of points y satisfying excess y <= ε * ‖y - x‖^2 is a relative neighborhood of x in C.

This is the epsilon form of the limsup characterization of semijets.

Equations

• ViscositySolns.SecondOrderNonposWithin C x excess = ∀ (ε : ℝ), 0 < ε → ∀ᶠ (y : ViscositySolns.Point n) in nhdsWithin x C, excess y ≤ ε * ‖y - x‖ ^ 2

theorem ViscositySolns.superjetExcess_secondOrderNonposWithin {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Superjet C u x) : SecondOrderNonposWithin C x (SuperjetExcess u x J)

theorem ViscositySolns.subjetExcess_secondOrderNonposWithin {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (hJ : J ∈ Subjet C u x) : SecondOrderNonposWithin C x (SubjetExcess u x J)

theorem ViscositySolns.secondOrderNonposWithin_positivePart_isLittleO {n : ℕ} {C : Set (Point n)} {x : Point n} {excess : Point n → ℝ} (h : SecondOrderNonposWithin C x excess) : SemijetRemainder C x fun (y : Point n) => max (excess y) 0

theorem ViscositySolns.superjet_of_superjetExcess_secondOrderNonposWithin {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (h : SecondOrderNonposWithin C x (SuperjetExcess u x J)) : J ∈ Superjet C u x

theorem ViscositySolns.subjet_of_subjetExcess_secondOrderNonposWithin {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} (h : SecondOrderNonposWithin C x (SubjetExcess u x J)) : J ∈ Subjet C u x

theorem ViscositySolns.superjet_iff_superjetExcess_secondOrderNonposWithin {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} : J ∈ Superjet C u x ↔ SecondOrderNonposWithin C x (SuperjetExcess u x J)

theorem ViscositySolns.subjet_iff_subjetExcess_secondOrderNonposWithin {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {J : Jet n} : J ∈ Subjet C u x ↔ SecondOrderNonposWithin C x (SubjetExcess u x J)

theorem ViscositySolns.superjet_of_eventually_le_of_hasSecondOrderExpansionWithinAtValue {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (h_le : ∀ᶠ (x : Point n) in nhdsWithin x0 C, u x ≤ φ x) (hφ : HasSecondOrderExpansionWithinAtValue C φ x0 (u x0) J) : J ∈ Superjet C u x0

theorem ViscositySolns.subjet_of_eventually_le_of_hasSecondOrderExpansionWithinAtValue {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (h_le : ∀ᶠ (x : Point n) in nhdsWithin x0 C, φ x ≤ u x) (hφ : HasSecondOrderExpansionWithinAtValue C φ x0 (u x0) J) : J ∈ Subjet C u x0

theorem ViscositySolns.superjet_iff_exists_eventually_le_hasSecondOrderExpansionWithinAtValue {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x0 : Point n} {J : Jet n} : J ∈ Superjet C u x0 ↔ ∃ (φ : Point n → ℝ), (∀ᶠ (x : Point n) in nhdsWithin x0 C, u x ≤ φ x) ∧ HasSecondOrderExpansionWithinAtValue C φ x0 (u x0) J

theorem ViscositySolns.subjet_iff_exists_eventually_le_hasSecondOrderExpansionWithinAtValue {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x0 : Point n} {J : Jet n} : J ∈ Subjet C u x0 ↔ ∃ (φ : Point n → ℝ), (∀ᶠ (x : Point n) in nhdsWithin x0 C, φ x ≤ u x) ∧ HasSecondOrderExpansionWithinAtValue C φ x0 (u x0) J

theorem ViscositySolns.superjet_of_touchesAbove_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (htouch : TouchesAboveOn C u φ x0) (hφ : HasSecondOrderExpansionWithin C φ x0 J) : J ∈ Superjet C u x0

theorem ViscositySolns.subjet_of_touchesBelow_hasSecondOrderExpansionWithin {n : ℕ} {C : Set (Point n)} {u φ : Point n → ℝ} {x0 : Point n} {J : Jet n} (htouch : TouchesBelowOn C u φ x0) (hφ : HasSecondOrderExpansionWithin C φ x0 J) : J ∈ Subjet C u x0