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

Quadratic gluing data for the Perron bump step (AnnulusSelectionPatches)

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.PerronLowerEnvelopeBentQuadraticSourceCompactInactivePatchAt {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

Source-radius compact-inactive data for the localized bent quadratic.

This is the finite-selection version of the source bump construction. The patch ball carries the strict quadratic branch. On the compact inactive set, including the Dirichlet boundary, local Perron-family branches dominate the bent quadratic; finite selection then produces one old Perron branch for the global max patch.

Equations

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

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

Source-radius compact-inactive data at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatchAt {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

Source-radius transition-annulus selection data.

The compact set K only has to control the transition region where the piecewise patch crosses the sphere. For inactive points, the caller supplies the local alternative outside the patch ball or in K; finite selection on K then makes the patch agree locally with the selected old branch.

Equations

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

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

Source-radius transition-annulus selection data at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatchAt {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

Concrete closed-annulus source-radius transition data.

The transition compact set is the explicit closed annulus r / 2 <= dist z x <= r. The bridge below proves the remaining local alternative: any point of C outside the open patch ball is eventually either outside that ball or inside this annulus.

Equations

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

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

Concrete closed-annulus source-radius transition data at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatchAt {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

Source-radius closed-annulus data with pointwise Perron-family branch selection.

At each point of the explicit annulus, the caller only selects one Perron-family branch that is strictly above the bent quadratic at that point and lower semicontinuous relative to the annulus there. The bridge below turns this into the local domination required by PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatchAt.

Equations

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

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

Closed-annulus lower-semicontinuous branch selection data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatchAt.closedAnnulusSelectionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatchAt C boundary F g B x J

Lower semicontinuity plus a pointwise strict gap gives local branch domination on the explicit annulus.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatch.closedAnnulusSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatch C boundary F g B

Global lower-semicontinuous closed-annulus branch selection data supplies the closed-annulus local-domination interface.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatchAt {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

Source-radius closed-annulus data from strict Perron-envelope approximation.

The source annulus estimate naturally gives information against the Perron supremum. This interface records the additional regularity needed to turn strict Perron-envelope approximation into the lower-semicontinuous branch selection used by the finite Perron patch: the Perron-family values are bounded above at annulus points, the bent quadratic is strictly below the Perron envelope there, and Perron-family branches are lower semicontinuous on the annulus.

Equations

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

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

Strict Perron-envelope closed-annulus approximation data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatchAt.lscSelectionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatchAt C boundary F g B x J

Strict approximation by the Perron envelope, plus lower semicontinuity of the approximating Perron branches on the annulus, supplies the LSC branch-selection interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatch.lscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatch C boundary F g B

Global strict Perron-envelope closed-annulus approximation data supplies the LSC branch-selection interface.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatchAt {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

Source-radius closed-annulus data from strict Perron-envelope approximation, with Perron-family boundedness discharged by an annulus-domain condition.

If every point of the explicit annulus lies in C ∪ boundary, the upper barrier bounds every Perron-family member there, so the Perron envelope can be approximated from below without asking the caller for a separate boundedness proof.

Equations

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

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

Domain-controlled strict Perron-envelope closed-annulus approximation data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatchAt.envelopeLscSelectionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatchAt C boundary F g B x J

The annulus-domain condition lets the upper barrier provide the pointwise boundedness needed for strict approximation by the Perron envelope.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatch.envelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatch C boundary F g B

Global domain-controlled strict Perron-envelope data supplies the bounded strict Perron-envelope approximation interface.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatchAt {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

Source-radius closed-annulus data with the source proof's geometric domain condition.

The caller supplies the closed patch ball inside C and the Dirichlet boundary outside C. These imply both that the explicit annulus lies in the Dirichlet domain and that the open patch ball avoids the boundary.

Equations

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

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

Closed-ball source-geometry strict Perron-envelope data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatchAt.domainEnvelopeLscSelectionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatchAt C boundary F g B x J

Closed-ball source geometry supplies the domain-controlled closed-annulus strict Perron-envelope interface.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatch.domainEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatch C boundary F g B

Global closed-ball source-geometry data supplies the domain-controlled closed-annulus strict Perron-envelope interface.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallLowerEnvelopeLscSelectionPatchAt {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

Source-radius closed-ball data with annulus strictness stated against the lower relaxed Perron envelope.

The closed ball condition later converts the lower-envelope inequality to a Perron-envelope inequality using local lower boundedness of the Perron envelope.

Equations

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

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

Closed-ball lower-envelope annulus data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallLowerEnvelopeLscSelectionPatchAt.closedBallEnvelopeLscSelectionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallLowerEnvelopeLscSelectionPatchAt C boundary F g B x J) (hlowerBddBelow : ∀ z ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin z C) B.lower) : PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatchAt C boundary F g B x J

Local lower boundedness turns strict annulus domination of the lower envelope into strict annulus domination of the Perron envelope.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallLowerEnvelopeLscSelectionPatch.closedBallEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallLowerEnvelopeLscSelectionPatch C boundary F g B) (hlowerBddBelow : ∀ z ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin z C) B.lower) : PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatch C boundary F g B

Global closed-ball lower-envelope annulus data supplies the closed-ball Perron-envelope interface.

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatchAt {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

Source-radius closed-ball data with annulus strictness on the outer transition annulus.

The transition region for the piecewise patch only needs to cover points near the boundary of the patch ball. Using 3 * r / 4 <= dist z x <= r leaves a strict quadratic margin for the source subjet estimate while preserving the metric transition argument.

Equations

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

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

Outer-transition closed-ball lower-envelope annulus data without Perron-family branch lower-semicontinuity.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatchAt {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

Legacy source-radius closed-ball data with annulus strictness on the outer transition annulus, plus the branch lower-semicontinuity field used by the older selection route.

Equations

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

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

Outer-transition closed-ball lower-envelope annulus data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatchAt.lowerEnvelopePatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} {J : Jet n} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatchAt C boundary F g B x J) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatchAt C boundary F g B x J

Forget the branch lower-semicontinuity field from the legacy outer-annulus package.

theorem ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch.lowerEnvelopePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch C boundary F g B) : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch C boundary F g B

Forget the branch lower-semicontinuity field from the legacy global outer-annulus package.