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

Perron bump definitions

Local and global formulations of the Perron lower-envelope bump input, plus quadratic bump certification interfaces.

def ViscositySolns.PerronLowerEnvelopeSubjetInequality {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

The subjet inequality for the lower Perron envelope.

This is the analytic conclusion supplied by the localized bump contradiction: if the inequality failed at an interior subjet of W_*, one could construct a larger admissible Perron-class member, contradicting the definition of the envelope.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBumpContradiction {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

The formal output expected from the localized bump construction.

If the lower-envelope subjet inequality fails at an interior point, the bump argument should produce an admissible Perron-class member that is strictly larger than the pointwise Perron envelope at that same point.

Equations

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

def ViscositySolns.PerronLowerEnvelopeLocalizedImprovementAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Localized improvement output of the Perron bump construction at one failed lower-envelope contact.

This is a direct Lean version of the payload of CIL Lemma 4.4: construct a Dirichlet subsolution above the lower barrier that is strictly above the Perron envelope at points arbitrarily close to the failed contact. Comparison with the upper barrier turns this Dirichlet subsolution into a Perron-class member, giving the formal contradiction.

Equations

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

def ViscositySolns.PerronLowerEnvelopeNeighborhoodImprovementAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Neighborhood-form localized improvement at one failed contact.

This is the same payload as PerronLowerEnvelopeLocalizedImprovementAt, but with the source-document phrasing made explicit: every relative neighborhood of the failed contact contains a point where the improved subsolution beats the Perron envelope.

Equations

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

def ViscositySolns.PerronLowerEnvelopeMaxPatchBumpAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (_x : Point n) : Prop

Concrete max-patch output of the localized bump construction at one failed subjet inequality.

The analytic construction should produce an old admissible Perron member and a local bump such that their pointwise maximum is still admissible and strictly exceeds the Perron envelope at some Dirichlet-domain point.

Equations

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

def ViscositySolns.PerronLowerEnvelopeMaxPatchBump {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

The bump construction localized at every failed subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeLocalizedImprovement {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

Localized improvement output at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronUpperEnvelopeLocalizedImprovementAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Direct localized improvement over the upper Perron envelope at one failed lower-envelope contact.

This is the source-proof bump payload after the maximality step has identified W^* with the pointwise Perron envelope on the domain. The analytic bump can be constructed against the already-subsolution upper envelope; the method layer later converts this into the ordinary Perron localized-improvement interface using W^* = W on C.

Equations

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

def ViscositySolns.PerronUpperEnvelopeLocalizedImprovement {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

Direct localized improvement over W^* at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeNeighborhoodImprovement {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

Neighborhood-form localized improvement at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeStrictPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Source-shaped strict patch data at a failed lower-envelope contact.

This is the part of Lemma 4.4 that is actually needed for Perron's contradiction: construct an admissible Perron-class member that lies above a strict level on a relative neighborhood of the contact point, where that level is above the lower envelope value W_* x.

Equations

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

def ViscositySolns.PerronLowerEnvelopeStrictSubsolutionPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Source-shaped strict bump data before applying comparison with the upper barrier.

Lemma 4.4 constructs a Dirichlet subsolution patch. In Perron's method, the upper-barrier bound needed for membership in the Perron class comes from the abstract comparison principle.

Equations

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

def ViscositySolns.PerronLowerEnvelopePointwiseStrictSubsolutionPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Pointwise strict subsolution patch data at a failed lower-envelope contact.

This is closer to the analytic output of the bump construction: it is enough to build a Dirichlet subsolution patch that is lower semicontinuous at the contact point and whose value there is strictly above W_* x. Lower semicontinuity turns the pointwise strict inequality into a strict relative neighborhood, giving PerronLowerEnvelopeStrictSubsolutionPatchAt.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousStrictSubsolutionPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Continuous pointwise strict subsolution patch data at a failed lower-envelope contact.

This is the form naturally produced by a smooth local bump: continuity at the contact point, pointwise strict improvement over W_*, the Dirichlet subsolution property, and the lower-barrier bound.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousBumpAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Continuous Dirichlet bump data at a failed lower-envelope contact.

This removes one global burden from the analytic bump construction. The bump only has to be a Dirichlet subsolution and be continuous and strictly above W_* at the contact point; maxing with the lower barrier supplies the global lower-barrier bound required by the Perron class.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousMaxPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Continuous max-patch bump data at a failed lower-envelope contact.

Here the raw bump only has to be continuous and strictly above W_* at the contact. The analytic gluing argument may prove directly that the patched function max lower bump is a Dirichlet subsolution.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousLocalMaxPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Continuous local max-patch bump data at a failed lower-envelope contact.

This is a gluing-oriented form of the bump step: the raw bump is continuous and strictly above W_* at the contact, the boundary inequality is supplied for the patched function, and the viscosity subsolution property of max lower w is checked by local germ representatives.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousBranchMaxPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Branch-local continuous max-patch data at a failed lower-envelope contact.

This is the form closest to a local gluing proof: around each point of C, the patched function either agrees with the lower barrier branch, or agrees with a supplied viscosity subsolution branch.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousActiveMaxPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Active-branch continuous max-patch data at a failed lower-envelope contact.

This spells out the inequalities that make one branch of max lower w locally active. Near each point of C, either the lower barrier dominates the raw bump, or the raw bump dominates the lower barrier and agrees locally with a viscosity subsolution representative.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousStrictActiveMaxPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Strict active-branch continuous max-patch data at a failed lower-envelope contact.

This records the common gluing situation with strict local branch separation: locally either the raw bump lies strictly below the lower barrier, or it lies strictly above the lower barrier and agrees with a local subsolution branch.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousStrictActiveSubsolutionBumpAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Strict active-branch bump data where the raw bump is itself a viscosity subsolution.

This is the usual special case needed after a smooth local bump has already been certified as a subsolution: the max patch is verified by strict branch separation, and the upper active branch uses the bump itself as the local subsolution representative.

Equations

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

def ViscositySolns.PerronLowerEnvelopeContinuousStrictActiveDirichletBumpAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

Strict active-branch bump data where the raw bump is a Dirichlet subsolution.

Compared with PerronLowerEnvelopeContinuousStrictActiveSubsolutionBumpAt, this asks for the ordinary Dirichlet boundary inequality for the raw bump. The boundary inequality for max lower bump then follows from the Dirichlet max lemma.

Equations

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

theorem ViscositySolns.DirichletBarrierPair.strictActiveDirichletBumpAt_of_quadraticModel {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hFell : DegenerateElliptic F) (hcontrol : ∀ z ∈ C, ∀ J ∈ Superjet C (fun (y : Point n) => quadraticModel x0 r p X y) z, J.gradient = (quadraticModelJetAt x0 p X z).gradient ∧ (quadraticModelJetAt x0 p X z).hessian ≤ J.hessian) (hineq : ∀ z ∈ C, F z (quadraticModel x0 r p X z) (quadraticModelJetAt x0 p X z).gradient (quadraticModelJetAt x0 p X z).hessian ≤ 0) (hWlt : lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x < quadraticModel x0 r p X x) (hboundary : BoundarySubsolutionOn boundary g fun (y : Point n) => quadraticModel x0 r p X y) (hactive : ∀ z ∈ C, (quadraticModel x0 r p X z < B.lower z ∧ ∀ᶠ (y : Point n) in nhdsWithin z C, quadraticModel x0 r p X y < B.lower y) ∨ B.lower z < quadraticModel x0 r p X z ∧ ∀ᶠ (y : Point n) in nhdsWithin z C, B.lower y < quadraticModel x0 r p X y) : PerronLowerEnvelopeContinuousStrictActiveDirichletBumpAt C boundary F g B x

A certified quadratic bump supplies the strict active Dirichlet-bump interface.

This packages the analytic checks needed once a failed lower-envelope contact has produced a concrete quadratic: superjet control plus degenerate ellipticity certifies viscosity subsolution status, while the caller supplies the boundary inequality and strict active-branch separation from the lower barrier.

theorem ViscositySolns.DirichletBarrierPair.strictActiveDirichletBumpAt_of_interior_quadraticModel {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x x0 : Point n} {r : ℝ} {p : Point n} {X : Hessian n} (hFell : DegenerateElliptic F) (hinterior : ∀ z ∈ C, z ∈ interior C) (hHerm : ∀ z ∈ C, ∀ J ∈ Superjet C (fun (y : Point n) => quadraticModel x0 r p X y) z, Matrix.IsHermitian (J.hessian - (quadraticModelJetAt x0 p X z).hessian)) (hineq : ∀ z ∈ C, F z (quadraticModel x0 r p X z) (quadraticModelJetAt x0 p X z).gradient (quadraticModelJetAt x0 p X z).hessian ≤ 0) (hWlt : lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x < quadraticModel x0 r p X x) (hboundary : BoundarySubsolutionOn boundary g fun (y : Point n) => quadraticModel x0 r p X y) (hactive : ∀ z ∈ C, (quadraticModel x0 r p X z < B.lower z ∧ ∀ᶠ (y : Point n) in nhdsWithin z C, quadraticModel x0 r p X y < B.lower y) ∨ B.lower z < quadraticModel x0 r p X z ∧ ∀ᶠ (y : Point n) in nhdsWithin z C, B.lower y < quadraticModel x0 r p X y) : PerronLowerEnvelopeContinuousStrictActiveDirichletBumpAt C boundary F g B x

An interior-domain certified quadratic bump supplies the strict active Dirichlet-bump interface.

Compared with strictActiveDirichletBumpAt_of_quadraticModel, this discharges the explicit superjet-control input using the shared local/full-neighborhood quadratic superjet theorem.

def ViscositySolns.PerronLowerEnvelopeInteriorQuadraticBump {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

Source-shaped interior quadratic bump data at every failed lower-envelope subjet inequality.

This packages the analytic payload of the quadratic part of Lemma 4.4: from a failed lower-envelope subjet inequality, produce a quadratic bump that is strictly above the lower envelope at the contact, satisfies the differential subsolution inequality throughout C, obeys the boundary condition, and has strict local branch separation from the lower barrier.

Equations

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