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

Perron quadratic bump certification

Quadratic and max-patching lemmas used at the beginning of the Perron bump construction.

theorem ViscositySolns.OperatorContinuous.eventually_quadraticModelJetAt_lt_of_lt {n : ℕ} {F : Operator n} (hF : OperatorContinuous F) {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hneg : F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian < 0) : ∀ᶠ (z : Point n) in nhds x, F z (quadraticModel x0 r p X z) (quadraticModelJetAt x0 p X z).gradient (quadraticModelJetAt x0 p X z).hessian < 0

Strict operator negativity for a quadratic model persists in a neighborhood of the base point.

This is the continuity ingredient used in the Perron bump construction after a failed lower-envelope subjet inequality has produced a strict negative value of F at the contact jet.

theorem ViscositySolns.OperatorContinuous.exists_pos_eventually_quadraticModelJetAt_lift_lt_of_lt {n : ℕ} {F : Operator n} (hF : OperatorContinuous F) {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hneg : F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian < 0) : ∃ (κ : ℝ), 0 < κ ∧ ∀ᶠ (z : Point n) in nhds x, F z (quadraticModel x0 (r + κ) p X z) (quadraticModelJetAt x0 p X z).gradient (quadraticModelJetAt x0 p X z).hessian < 0

Strict operator negativity for a quadratic model persists after a sufficiently small positive vertical lift of the model, and then in a neighborhood of the base point.

The lift parameter is the height of the Perron bump. Continuity of F first chooses a positive height that keeps the contact inequality strict; the preceding theorem then spreads that strict inequality to nearby points.

theorem ViscositySolns.ViscositySubsolution.quadraticModelJetAt_le {n : ℕ} {C : Set (Point n)} {F : Operator n} {x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hsub : ViscositySubsolution C F fun (y : Point n) => quadraticModel x0 r p X y) {x : Point n} (hx : x ∈ C) : F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian ≤ 0

A viscosity subsolution quadratic satisfies the operator inequality at its canonical recentered quadratic jet.

theorem ViscositySolns.ViscositySupersolution.quadraticModelJetAt_nonneg {n : ℕ} {C : Set (Point n)} {F : Operator n} {x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hsuper : ViscositySupersolution C F fun (y : Point n) => quadraticModel x0 r p X y) {x : Point n} (hx : x ∈ C) : 0 ≤ F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian

A viscosity supersolution quadratic satisfies the operator inequality at its canonical recentered quadratic jet.

theorem ViscositySolns.ViscositySubsolution.of_superjetControl {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (husc : UpperSemicontinuousOn u C) (hFell : DegenerateElliptic F) (A : Point n → Jet n) (hcontrol : ∀ x ∈ C, ∀ J ∈ Superjet C u x, J.gradient = (A x).gradient ∧ (A x).hessian ≤ J.hessian) (hineq : ∀ x ∈ C, F x (u x) (A x).gradient (A x).hessian ≤ 0) : ViscositySubsolution C F u

Subsolution certification from a controlled jet field.

If every superjet of u has the same gradient as a chosen jet field A and a larger Hessian, then degenerate ellipticity reduces the viscosity subsolution check to the operator inequality on A.

theorem ViscositySolns.ViscositySupersolution.of_subjetControl {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hlsc : LowerSemicontinuousOn u C) (hFell : DegenerateElliptic F) (A : Point n → Jet n) (hcontrol : ∀ x ∈ C, ∀ J ∈ Subjet C u x, J.gradient = (A x).gradient ∧ J.hessian ≤ (A x).hessian) (hineq : ∀ x ∈ C, 0 ≤ F x (u x) (A x).gradient (A x).hessian) : ViscositySupersolution C F u

Supersolution certification from a controlled jet field.

For subjets the Hessian inequality is reversed: a controlled subjet has the same gradient as A and a smaller Hessian. Degenerate ellipticity then moves the operator inequality from A to the tested subjet.

theorem ViscositySolns.ViscositySubsolution.quadraticModel_of_superjetControl {n : ℕ} {C : Set (Point n)} {F : Operator n} {x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hFell : DegenerateElliptic F) (hcontrol : ∀ x ∈ C, ∀ 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 ≤ J.hessian) (hineq : ∀ x ∈ C, F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian ≤ 0) : ViscositySubsolution C F fun (y : Point n) => quadraticModel x0 r p X y

Quadratic subsolution certification from superjet control.

This is the bump-facing specialization of ViscositySubsolution.of_superjetControl: once the remaining analytic work identifies superjets of a quadratic bump with larger-Hessian perturbations of the recentered quadratic jet, checking the PDE on the recentered jet proves that the bump is a viscosity subsolution.

theorem ViscositySolns.ViscositySubsolution.quadraticModel_of_mem_interior_of_isHermitian_sub {n : ℕ} {C : Set (Point n)} {F : Operator n} {x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hFell : DegenerateElliptic F) (hinterior : ∀ x ∈ C, x ∈ interior C) (hHerm : ∀ x ∈ C, ∀ J ∈ Superjet C (fun (y : Point n) => quadraticModel x0 r p X y) x, Matrix.IsHermitian (J.hessian - (quadraticModelJetAt x0 p X x).hessian)) (hineq : ∀ x ∈ C, F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian ≤ 0) : ViscositySubsolution C F fun (y : Point n) => quadraticModel x0 r p X y

Quadratic subsolution certification on an interior domain.

This is the bump-facing version of the shared semijet control theorem: interior points let us replace relative superjets by full-neighborhood superjets, and the Hermitian hypothesis converts scalar quadratic-form control into the Loewner order needed for degenerate ellipticity.

theorem ViscositySolns.ViscositySubsolution.quadraticModel_of_mem_interior_of_hessianSymmetricInvariant {n : ℕ} {C : Set (Point n)} {F : Operator n} {x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hX : Matrix.IsHermitian X) (hinterior : ∀ x ∈ C, x ∈ interior C) (hineq : ∀ x ∈ C, F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian ≤ 0) : ViscositySubsolution C F fun (y : Point n) => quadraticModel x0 r p X y

Quadratic subsolution certification on an interior domain, using symmetric Hessians.

If the quadratic Hessian is Hermitian and the operator ignores skew Hessian parts, then arbitrary superjet Hessians can be symmetrized before applying degenerate ellipticity. This is closer to the classical Perron bump argument, where second derivatives are symmetric matrices.

theorem ViscositySolns.ViscositySupersolution.quadraticModel_of_subjetControl {n : ℕ} {C : Set (Point n)} {F : Operator n} {x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hFell : DegenerateElliptic F) (hcontrol : ∀ x ∈ C, ∀ J ∈ Subjet C (fun (y : Point n) => quadraticModel x0 r p X y) x, J.gradient = (quadraticModelJetAt x0 p X x).gradient ∧ J.hessian ≤ (quadraticModelJetAt x0 p X x).hessian) (hineq : ∀ x ∈ C, 0 ≤ F x (quadraticModel x0 r p X x) (quadraticModelJetAt x0 p X x).gradient (quadraticModelJetAt x0 p X x).hessian) : ViscositySupersolution C F fun (y : Point n) => quadraticModel x0 r p X y

Quadratic supersolution certification from subjet control.

theorem ViscositySolns.superjet_congr_eventuallyEq {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} (hx : u x = v x) (h : u =ᶠ[nhdsWithin x C] v) : Superjet C u x = Superjet C v x

Superjet fibers depend only on the germ of the function at the base point, together with the value at the base point.

theorem ViscositySolns.subjet_congr_eventuallyEq {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} (hx : u x = v x) (h : u =ᶠ[nhdsWithin x C] v) : Subjet C u x = Subjet C v x

Subjet fibers depend only on the germ of the function at the base point, together with the value at the base point.

theorem ViscositySolns.ViscositySubsolution.of_locally_eventuallyEq {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hlocal : ∀ x ∈ C, ∃ (v : Point n → ℝ), ViscositySubsolution C F v ∧ u x = v x ∧ u =ᶠ[nhdsWithin x C] v) : ViscositySubsolution C F u

A viscosity subsolution can be checked locally in the germ of the function at each point of the PDE domain.

theorem ViscositySolns.ViscositySubsolution.of_locally_eventuallyEqOn {n : ℕ} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hlocal : ∀ x ∈ C, ∃ (D : Set (Point n)) (v : Point n → ℝ), D ⊆ C ∧ D ∈ nhdsWithin x C ∧ ViscositySubsolution D F v ∧ u x = v x ∧ u =ᶠ[nhdsWithin x C] v) : ViscositySubsolution C F u

A viscosity subsolution can be checked from genuinely local domain germs.

This is the locality form needed for Perron patching: near each point of the PDE domain C, the candidate only has to agree with a subsolution on a relative neighborhood D of that point. The semijet domain-germ lemma then transfers the local subsolution inequality back to C.

theorem ViscositySolns.ViscositySubsolution.restrict_of_subset_of_mem_nhdsWithin {n : ℕ} {C D : Set (Point n)} {F : Operator n} {u : Point n → ℝ} (hu : ViscositySubsolution C F u) (hDC : D ⊆ C) (hDnhds : ∀ x ∈ D, D ∈ nhdsWithin x C) : ViscositySubsolution D F u

A viscosity subsolution restricts to a relatively open subdomain.

This local restriction form is useful in the Perron patch: an old Perron branch is known to be a subsolution on C, while the quadratic bump is only certified on a smaller relative neighborhood D.

theorem ViscositySolns.DirichletSubsolutionOn.of_locally_eventuallyEq {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hlocal : ∀ x ∈ C, ∃ (v : Point n → ℝ), ViscositySubsolution C F v ∧ u x = v x ∧ u =ᶠ[nhdsWithin x C] v) (hboundary : BoundarySubsolutionOn boundary g u) : UpperSemicontinuousOn u (C ∪ boundary) → DirichletSubsolutionOn C boundary F g u

A Dirichlet subsolution can be assembled from local viscosity-subsolution germs and a separately supplied boundary inequality.

theorem ViscositySolns.DirichletSubsolutionOn.of_locally_eventuallyEqOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u : Point n → ℝ} (hlocal : ∀ x ∈ C, ∃ (D : Set (Point n)) (v : Point n → ℝ), D ⊆ C ∧ D ∈ nhdsWithin x C ∧ ViscositySubsolution D F v ∧ u x = v x ∧ u =ᶠ[nhdsWithin x C] v) (hboundary : BoundarySubsolutionOn boundary g u) : UpperSemicontinuousOn u (C ∪ boundary) → DirichletSubsolutionOn C boundary F g u

A Dirichlet subsolution can be assembled from local-domain viscosity-subsolution germs and a separately supplied boundary inequality.

theorem ViscositySolns.UpperSemicontinuousOn.of_eqOn_compl_closed_patch {n : ℕ} {C boundary K : Set (Point n)} {u v : Point n → ℝ} (hCopen : IsOpen C) (hKclosed : IsClosed K) (hbase : UpperSemicontinuousOn u (C ∪ boundary)) (hpatchUSC : UpperSemicontinuousOn v C) (hEq : Set.EqOn v u Kᶜ) (hboundaryAvoid : ∀ x ∈ boundary, x ∉ K) : UpperSemicontinuousOn v (C ∪ boundary)

Union semicontinuity for a patch whose changes are confined to a compact subset of an open domain. Interior points use the assembled subsolution's USC; boundary points have a neighborhood disjoint from the compact support and inherit USC from the original Dirichlet function.

theorem ViscositySolns.UpperSemicontinuousOn.union_of_isOpen_domain {n : ℕ} {C boundary : Set (Point n)} {u : Point n → ℝ} (hC : IsOpen C) (hu : UpperSemicontinuousOn u C) (hb : ∀ x ∈ boundary, UpperSemicontinuousWithinAt u (C ∪ boundary) x) : UpperSemicontinuousOn u (C ∪ boundary)

Interior USC and boundary USC assemble on an open domain and its boundary.

theorem ViscositySolns.UpperSemicontinuousOn.piecewise_max_boundary {n : ℕ} {S P : Set (Point n)} {u q : Point n → ℝ} {x : Point n} (hu : UpperSemicontinuousOn u S) (hq : Continuous q) (hx : x ∈ S) (hboundary : x ∉ closure P ∨ q x ≤ u x) : UpperSemicontinuousWithinAt (fun (y : Point n) => if y ∈ P then max (u y) (q y) else u y) S x

A piecewise maximum preserves boundary USC if its support stays away from the boundary point or its continuous branch lies below the base there.

theorem ViscositySolns.DirichletSubsolutionOn.max {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g u v : Point n → ℝ} (hu : DirichletSubsolutionOn C boundary F g u) (hv : DirichletSubsolutionOn C boundary F g v) : DirichletSubsolutionOn C boundary F g fun (x : Point n) => Max.max (u x) (v x)

The maximum of two Dirichlet subsolutions is a Dirichlet subsolution.

theorem ViscositySolns.PerronClass.max {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper u v : Point n → ℝ} (hu : PerronClass C boundary F g lower upper u) (hv : PerronClass C boundary F g lower upper v) : PerronClass C boundary F g lower upper fun (x : Point n) => Max.max (u x) (v x)

Membership in the Perron class is closed under pointwise maximum.

theorem ViscositySolns.PerronClass.max_patch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper old bump : Point n → ℝ} (hold : PerronClass C boundary F g lower upper old) (hbump : PerronClass C boundary F g lower upper bump) : PerronClass C boundary F g lower upper fun (x : Point n) => Max.max (old x) (bump x)

If a new local candidate is itself an admissible Perron-class member, max patching with an old Perron-class member remains admissible. This is the algebraic part of the localized bump construction; the analytic work is to produce such a candidate and prove it agrees with the old function near the patch boundary.

theorem ViscositySolns.PerronClass.le_perronEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper w : Point n → ℝ} (hw : PerronClass C boundary F g lower upper w) {x : Point n} (hbdd : BddAbove {r : ℝ | ∃ (v : Point n → ℝ), PerronClass C boundary F g lower upper v ∧ r = v x}) : w x ≤ perronEnvelope C boundary F g lower upper x

Every Perron-class member lies below the pointwise Perron envelope.

theorem ViscositySolns.DirichletBarrierPair.perronClass_le_perronEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g w : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hw : PerronClass C boundary F g B.lower B.upper w) {x : Point n} (hx : x ∈ C ∪ boundary) : w x ≤ perronEnvelope C boundary F g B.lower B.upper x

The upper barrier supplies the boundedness needed to compare a Perron-class member with the pointwise Perron envelope.

theorem ViscositySolns.DirichletBarrierPair.not_perronEnvelope_lt_perronClass {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g w : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hw : PerronClass C boundary F g B.lower B.upper w) {x : Point n} (hx : x ∈ C ∪ boundary) : ¬perronEnvelope C boundary F g B.lower B.upper x < w x

It is impossible for a Perron-class member to exceed the Perron envelope at a Dirichlet-domain point.

theorem ViscositySolns.DirichletBarrierPair.exists_perronClass_gt_of_lt_perronEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hx : x ∈ C ∪ boundary) {a : ℝ} (ha : a < perronEnvelope C boundary F g B.lower B.upper x) : ∃ (w : Point n → ℝ), PerronClass C boundary F g B.lower B.upper w ∧ a < w x

Approximate the Perron envelope from below by a member of the Perron class at a fixed point.