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

Quadratic gluing data for the Perron bump step (GluingSkeleton)

Part of the quadratic-gluing development connecting the lifted quadratic supplied by operator continuity to the strict local max-patch formulation. Split from QuadraticGluing.lean; see the umbrella module docstring.

def ViscositySolns.pointwiseMaxList {n : ℕ} (base : Point n → ℝ) : List (Point n → ℝ) → Point n → ℝ

Finite pointwise maximum, with a base branch used for the empty list.

The compact part of the Perron bump argument selects finitely many old Perron members and then replaces them by their pointwise maximum. Keeping the base branch explicit avoids a nonempty-list side condition in later selection lemmas.

Equations

• ViscositySolns.pointwiseMaxList base [] = base
• ViscositySolns.pointwiseMaxList base (u :: us) = fun (x : ViscositySolns.Point n) => max (u x) (ViscositySolns.pointwiseMaxList base us x)

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

Local quadratic active-branch gluing data at a failed lower-envelope contact.

This is the point at which the source proof's branch separation is visible: the patched function max old q is locally equal either to the old Perron member or to the lifted quadratic branch, and the lifted quadratic branch has already been certified as a viscosity subsolution.

Equations

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

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

Local quadratic active-branch gluing data at every failed lower-envelope subjet inequality.

Equations

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

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

Local quadratic gluing data stated in terms of local viscosity-subsolution germs for the patched function.

This is the branch-separation form of the source bump construction: after the lifted quadratic has been chosen, an old Perron-class branch is selected so that max old q has local subsolution representatives, satisfies the boundary condition, and stays below the upper barrier.

Equations

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

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

Local quadratic gluing data at every failed lower-envelope subjet inequality.

Equations

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

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

Local quadratic branch-gluing data at a failed lower-envelope contact.

Unlike PerronLowerEnvelopeLocalQuadraticActiveGluingAt, this does not ask the lifted quadratic to be a global subsolution. It only asks for local subsolution representatives on the region where the quadratic branch is allowed to be active.

Equations

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

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

Local quadratic branch-gluing data at every failed lower-envelope subjet inequality.

Equations

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

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

Selection data for the source patch step once the lifted quadratic has been chosen by continuity.

For every certified local lifted quadratic, this asks for the old Perron branch and the local branch/boundary/upper-barrier facts needed to glue the quadratic into the Perron family.

Equations

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

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

Selection data for every failed lower-envelope subjet inequality.

Equations

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

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

Compact-inactive selection data for the source bump construction.

This is a weaker and more source-shaped old-branch obligation than PerronLowerEnvelopeLocalQuadraticPatchSelectionAt. The caller chooses a compact inactive set K containing the points of C outside the active quadratic neighborhood V; finite Perron selection builds one old branch dominating the lifted quadratic near every point of K. Inside V, the max patch is certified by taking the maximum of the old branch and the local quadratic subsolution representative, so no branch ordering is required there.

Equations

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

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

Compact-inactive selection data at every failed lower-envelope subjet inequality.

Equations

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

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

Compact-inactive max-patch data with genuinely local active representatives.

After the old Perron branch is selected from the compact inactive set, the caller supplies local-domain subsolution representatives for the patched function max old q on the active quadratic neighborhood. Outside the active neighborhood, finite selection makes max old q locally equal to old.

Equations

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

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

Compact-inactive local max-patch data at every failed lower-envelope subjet inequality.

Equations

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

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

Compact-inactive patch data before comparison with the upper barrier.

This is the source-shaped variant of PerronLowerEnvelopeLocalQuadraticCompactInactivePatchAt: after finite selection of the old branch, the caller only has to certify that the patched function is locally a viscosity subsolution and satisfies the boundary subsolution inequality. The upper-barrier bound is later supplied by the abstract Dirichlet comparison principle.

Equations

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

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

Compact-inactive local subsolution-patch data at every failed lower-envelope subjet inequality.

Equations

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

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

Compact-inactive data where the active branch is the lifted quadratic itself.

Compared with PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatchAt, the active input is no longer a local representative for max old q. Instead it supplies a relative-open local domain on which the lifted quadratic q is a viscosity subsolution; max-stability with the old Perron branch then builds the patched local representative.

Equations

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

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

Compact-inactive quadratic-active patch data at every failed lower-envelope subjet inequality.

Equations

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

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

Compact-inactive data with certified active domains for the lifted quadratic.

This is one step closer to the analytic bump construction than PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatchAt: on the active side, the caller supplies only relative-open interior domains contained in the strict negativity region. Degenerate ellipticity and symmetric Hessian-invariance certify the lifted quadratic as a viscosity subsolution on those domains.

Equations

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

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

Compact-inactive certified active-domain data at every failed lower-envelope subjet inequality.

Equations

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

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

Compact-inactive certified active-domain data without assuming the failed jet Hessian is already symmetric.

The active domains are the same geometric data as in PerronLowerEnvelopeLocalQuadraticCompactInactiveCertifiedPatchAt, but the quadratic subsolution certification is later applied to symHessian J.hessian and transported back using quadraticModel_symHessian.

Equations

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

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

Compact-inactive symmetrized certified active-domain data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronClass.of_locally_eventuallyEq {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper 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) (husc : UpperSemicontinuousOn u (C ∪ boundary)) (hlower : ∀ x ∈ C ∪ boundary, lower x ≤ u x) (hupper : ∀ x ∈ C ∪ boundary, u x ≤ upper x) : PerronClass C boundary F g lower upper u

Perron-class membership can be proved from local viscosity-subsolution germs plus the global Dirichlet and order bounds.

This is the gluing skeleton used by the localized Perron bump construction: the analytic branch proof supplies the local representatives, while the boundary and barrier inequalities are checked separately.

theorem ViscositySolns.PerronClass.of_locally_eventuallyEqOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper 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) (husc : UpperSemicontinuousOn u (C ∪ boundary)) (hlower : ∀ x ∈ C ∪ boundary, lower x ≤ u x) (hupper : ∀ x ∈ C ∪ boundary, u x ≤ upper x) : PerronClass C boundary F g lower upper u

Perron-class membership can be proved from local-domain viscosity-subsolution germs plus the global Dirichlet and order bounds.

Compared with PerronClass.of_locally_eventuallyEq, each local representative only has to be a subsolution on a relative neighborhood of the point.

theorem ViscositySolns.PerronClass.max_patch_of_locally_eventuallyEq {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) (hlocal : ∀ x ∈ C, ∃ (v : Point n → ℝ), ViscositySubsolution C F v ∧ Max.max (old x) (bump x) = v x ∧ (fun (y : Point n) => Max.max (old y) (bump y)) =ᶠ[nhdsWithin x C] v) (hboundary : BoundarySubsolutionOn boundary g fun (y : Point n) => Max.max (old y) (bump y)) (husc : UpperSemicontinuousOn (fun (y : Point n) => Max.max (old y) (bump y)) (C ∪ boundary)) (hupper : ∀ x ∈ C ∪ boundary, Max.max (old x) (bump x) ≤ upper x) : PerronClass C boundary F g lower upper fun (y : Point n) => Max.max (old y) (bump y)

Local viscosity-subsolution germs for a max patch are enough to certify the patched function as Perron-admissible, provided the upper and boundary bounds are supplied. The lower bound follows from the old Perron-class branch.

theorem ViscositySolns.PerronClass.max_patch_of_locally_eventuallyEqOn {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) (hlocal : ∀ x ∈ C, ∃ (D : Set (Point n)) (v : Point n → ℝ), D ⊆ C ∧ D ∈ nhdsWithin x C ∧ ViscositySubsolution D F v ∧ Max.max (old x) (bump x) = v x ∧ (fun (y : Point n) => Max.max (old y) (bump y)) =ᶠ[nhdsWithin x C] v) (hboundary : BoundarySubsolutionOn boundary g fun (y : Point n) => Max.max (old y) (bump y)) (husc : UpperSemicontinuousOn (fun (y : Point n) => Max.max (old y) (bump y)) (C ∪ boundary)) (hupper : ∀ x ∈ C ∪ boundary, Max.max (old x) (bump x) ≤ upper x) : PerronClass C boundary F g lower upper fun (y : Point n) => Max.max (old y) (bump y)

Local-domain viscosity-subsolution germs for a max patch are enough to certify the patched function as Perron-admissible.

This is the patching form closest to the source bump argument: in the active ball the representative may be a subsolution only on that local ball, while outside the ball it can be the old Perron branch.

theorem ViscositySolns.PerronClass.max_patch_of_active_branches {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) (hbumpSub : ViscositySubsolution C F bump) (hactive : ∀ x ∈ C, (bump x ≤ old x ∧ ∀ᶠ (y : Point n) in nhdsWithin x C, bump y ≤ old y) ∨ old x ≤ bump x ∧ ∀ᶠ (y : Point n) in nhdsWithin x C, old y ≤ bump y) (hboundary : BoundarySubsolutionOn boundary g fun (y : Point n) => Max.max (old y) (bump y)) (husc : UpperSemicontinuousOn (fun (y : Point n) => Max.max (old y) (bump y)) (C ∪ boundary)) (hupper : ∀ x ∈ C ∪ boundary, Max.max (old x) (bump x) ≤ upper x) : PerronClass C boundary F g lower upper fun (y : Point n) => Max.max (old y) (bump y)

Active-branch separation gives the local viscosity-subsolution germs needed to certify a max patch as Perron-admissible.

theorem ViscositySolns.le_pointwiseMaxList_base {n : ℕ} {base : Point n → ℝ} {us : List (Point n → ℝ)} {x : Point n} : base x ≤ pointwiseMaxList base us x

The base branch lies below the finite pointwise maximum.

theorem ViscositySolns.le_pointwiseMaxList_of_mem {n : ℕ} {base u : Point n → ℝ} {us : List (Point n → ℝ)} {x : Point n} (hu : u ∈ us) : u x ≤ pointwiseMaxList base us x

Every listed branch lies below the finite pointwise maximum.

theorem ViscositySolns.pointwiseMaxList_le {n : ℕ} {base : Point n → ℝ} {us : List (Point n → ℝ)} {x : Point n} {a : ℝ} (hbase : base x ≤ a) (hus : ∀ u ∈ us, u x ≤ a) : pointwiseMaxList base us x ≤ a

A finite pointwise maximum is bounded above if every branch is.

theorem ViscositySolns.PerronClass.pointwiseMaxList {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper base : Point n → ℝ} {us : List (Point n → ℝ)} (hbase : PerronClass C boundary F g lower upper base) (hus : ∀ u ∈ us, PerronClass C boundary F g lower upper u) : PerronClass C boundary F g lower upper (ViscositySolns.pointwiseMaxList base us)

Finite pointwise maxima of Perron-class members remain Perron-admissible.

theorem ViscositySolns.PerronFamily.pointwiseMaxList_mem {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper : Point n → ℝ} (base : PerronFamily C boundary F g lower upper) (ws : List (PerronFamily C boundary F g lower upper)) : PerronClass C boundary F g lower upper (pointwiseMaxList base.fun (List.map «fun» ws))

Finite maxima of Perron-family witnesses remain Perron-admissible.

This is the form used after compact selection has produced a finite list of Perron-family members.

theorem ViscositySolns.PerronFamily.fun_le_pointwiseMaxList_of_mem {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper : Point n → ℝ} {base w : PerronFamily C boundary F g lower upper} {ws : List (PerronFamily C boundary F g lower upper)} {x : Point n} (hw : w ∈ ws) : w.fun x ≤ pointwiseMaxList base.fun (List.map «fun» ws) x

A listed Perron-family branch lies below the finite maximum of the list.

theorem ViscositySolns.DirichletBarrierPair.exists_perronClass_dominate_on_isCompact {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {K : Set (Point n)} {q : Point n → ℝ} (hKcompact : IsCompact K) (hlocal : ∀ z ∈ K, ∃ (w : PerronFamily C boundary F g B.lower B.upper), ∀ᶠ (y : Point n) in nhdsWithin z K, q y ≤ w.fun y) : ∃ (old : Point n → ℝ), PerronClass C boundary F g B.lower B.upper old ∧ ∀ y ∈ K, q y ≤ old y

Compact finite-selection step for old Perron branches.

If every point of a compact set has a local Perron-family branch dominating a candidate q, then finitely many of those branches can be replaced by one old Perron-class function dominating q on the whole compact set. This is the finite-subcover core of the source Perron patch argument.

theorem ViscositySolns.DirichletBarrierPair.exists_perronClass_eventually_dominate_on_isCompact {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {K : Set (Point n)} {q : Point n → ℝ} (hKcompact : IsCompact K) (hKnhds : ∀ z ∈ K, K ∈ nhdsWithin z C) (hlocal : ∀ z ∈ K, ∃ (w : PerronFamily C boundary F g B.lower B.upper), ∀ᶠ (y : Point n) in nhdsWithin z K, q y ≤ w.fun y) : ∃ (old : Point n → ℝ), PerronClass C boundary F g B.lower B.upper old ∧ ∀ z ∈ K, q z ≤ old z ∧ ∀ᶠ (y : Point n) in nhdsWithin z C, q y ≤ old y

Compact finite-selection step with eventual domination in the ambient domain.

This is the version needed by the inactive annulus in the Perron bump construction. If every point of a compact set has a local Perron-family branch dominating the candidate bump on that compact set, and the compact set is itself a relative neighborhood of each point under consideration, then the finite maximum branch dominates the bump eventually in nhdsWithin z C.

theorem ViscositySolns.DirichletBarrierPair.exists_perronFamily_gt_of_lt_perronEnvelope_of_bddAbove {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} {a : ℝ} (hbdd : BddAbove {r : ℝ | ∃ (w : Point n → ℝ), PerronClass C boundary F g B.lower B.upper w ∧ r = w x}) (ha : a < perronEnvelope C boundary F g B.lower B.upper x) : ∃ (w : PerronFamily C boundary F g B.lower B.upper), a < w.fun x

Approximate the Perron envelope from below at a point where the Perron-family values are bounded above.

Unlike DirichletBarrierPair.exists_perronClass_gt_of_lt_perronEnvelope, this version does not require the point to lie in C ∪ boundary; the needed boundedness is supplied directly.