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

Quadratic gluing data for the Perron bump step (CompactInactivePatches)

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

Boundary-safe symmetrized compact-inactive data.

This is the same active/inactive geometric datum as PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatchAt, but the boundary condition is stated only for the lifted quadratic q. Since every old Perron branch already satisfies the boundary subsolution inequality, max old q then satisfies the boundary inequality automatically.

Equations

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

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

Boundary-safe symmetrized 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.PerronLowerEnvelopeLocalQuadraticCompactInactiveCoveredPatchAt {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 whose inactive compact also covers the boundary.

After finite Perron selection, the selected old branch dominates the lifted quadratic on the whole inactive compact. The extra boundary cover therefore makes the max patch equal to the old Perron branch on the boundary, so the boundary subsolution inequality needs no separate check for q.

Equations

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

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

Boundary-covered 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.PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatchAt {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 whose inactive compact covers the exterior of the active quadratic neighborhood in C ∪ boundary.

This is closer to the source proof: the active bump is chosen away from the Dirichlet boundary, and the inactive compact covers every point of the domain or boundary outside the active neighborhood. The boundary-covered interface is then obtained by applying the boundary-away field.

Equations

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

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

Exterior 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.PerronLowerEnvelopeLocalQuadraticBarrierExteriorPatchAt {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

Exterior compact-inactive data using the lower barrier as the inactive branch.

This is the source-style annulus input: outside the active quadratic neighborhood, the lifted quadratic is locally below the lower barrier. Since the lower barrier is itself a Perron-family member, this discharges the local Perron-branch selection field required by PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatchAt.

Equations

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

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

Lower-barrier exterior 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.PerronLowerEnvelopeLocalQuadraticOpenBarrierExteriorPatchAt {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

Open-active lower-barrier exterior data.

This is the source-shaped annulus input for the bump produced directly by operator continuity: it only has to handle open active neighborhoods V, and therefore does not carry the local active-domain field. When C is open, the active domain is supplied later by C ∩ V.

Equations

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

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

Open-active lower-barrier exterior data at every failed lower-envelope subjet inequality.

Equations

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

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

Open-active exterior data for the bent source quadratic.

Compared with PerronLowerEnvelopeLocalQuadraticOpenBarrierExteriorPatchAt, the active branch is the lifted and downward-bent quadratic J.hessian - γ • I. This matches the quadratic used in the source annulus argument.

Equations

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

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

Bent open-active exterior data at every failed lower-envelope subjet inequality.

Equations

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

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

Bent quadratic max-patch data at a failed lower-envelope contact.

This endpoint is intentionally independent of PerronLowerEnvelopeLocalQuadraticMaxPatchAt, whose public payload records the unbent Hessian J.hessian. The bent patch still feeds the generic Perron contradiction through PerronLowerEnvelopeStrictLocalPatchAt.

Equations

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

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

Bent quadratic 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.PerronLowerEnvelopeBentQuadraticLocalizedLowerPatchAt {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

Localized lower-barrier piecewise patch data for the bent source quadratic.

The outside branch is the lower barrier itself. The caller supplies a patched function which is locally max lower q on the active neighborhood and locally the lower barrier off that neighborhood. This is the Lean-facing form of the source piecewise definition.

Equations

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

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

Localized lower-barrier piecewise patch data at every failed lower-envelope subjet inequality.

Equations

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

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

Open patch-set data for the localized bent source quadratic.

The caller supplies an open patch region P containing the active strict-negativity neighborhood V. Openness makes P a relative neighborhood of every active point, so only the inactive and boundary lower-barrier domination estimates remain.

Equations

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

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

Open patch-set data at every failed lower-envelope subjet inequality.

Equations

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

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

Boundary-away open patch-set data for the localized bent source quadratic.

This is the direct source shape when the patch region is chosen strictly inside the domain: the open patch set contains the active neighborhood, is disjoint from the Dirichlet boundary, and satisfies lower-barrier domination wherever points of C lie outside the active neighborhood.

Equations

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

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

Boundary-away open patch-set data at every failed lower-envelope subjet inequality.

Equations

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

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

Ball patch data for the localized bent source quadratic.

This is the ball-shaped source patch: the patch region is the open metric ball Metric.ball x r, it contains the active strict-negativity neighborhood V, it is disjoint from the Dirichlet boundary, and the bent quadratic is locally below the lower barrier whenever a point of C lies outside V.

Equations

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

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

Ball patch data at every failed lower-envelope subjet inequality.

Equations

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

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

Closed-ball annulus data for the localized bent source quadratic.

The patch region is still the open ball Metric.ball x r, but the inactive estimate only needs to be supplied on the closed ball. Points outside the closed ball are automatically eventually outside the open patch ball.

Equations

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

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

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

Equations

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

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

Shrinkable localized lower-barrier piecewise patch data for the bent source quadratic.

The strict-negativity neighborhood V comes from operator continuity. The actual patch region P may be a smaller open relative neighborhood of the contact point contained in V; this matches the source proof, which shrinks to a ball before patching.

Equations

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

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

Shrinkable localized lower-barrier patch data at every failed lower-envelope subjet inequality.

Equations

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

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

Shrinking closed-ball annulus data for the localized bent source quadratic.

The chosen ball is contained in the operator-continuity neighborhood V. Lower-barrier domination is required only on the closed-ball annulus outside the open patch ball; outside the closed ball, metric separation makes the patch locally inactive.

Equations

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

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

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

Equations

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

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

Small-radius closed-ball annulus data for the localized bent source quadratic.

The analytic estimates are required only below some positive radius bound. The bridge to the shrinkable annulus package intersects this bound with the radius forced by the open strict-negativity neighborhood supplied by operator continuity.

Equations

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

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

Small-radius closed-ball annulus data at every failed lower-envelope subjet inequality.

Equations

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

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

Chosen localized lower-barrier patch data for one bent lifted quadratic.

Unlike the compatibility interfaces above, this is existential in the lift, bend, active neighborhood, and patch set. It is the right target for the source proof, where the lift is chosen together with the patch radius.

Equations

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

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

Chosen localized lower-barrier patch data at every failed lower-envelope subjet inequality.

Equations

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

def ViscositySolns.PerronLowerEnvelopeBentQuadraticSourceClosedBallAnnulusPatchAt {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 annulus data for the localized bent quadratic.

This matches the expanded source proof: the vertical lift is tied to the patch radius by δ = γ * r ^ 2 / 8, and lower-barrier domination is only needed on the closed-ball sphere where the open patch ball becomes inactive.

Equations

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

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

Source-radius closed-ball annulus data at every failed lower-envelope subjet inequality.

Equations

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

theorem ViscositySolns.eventually_not_mem_ball_of_not_mem_closedBall {n : ℕ} {C : Set (Point n)} {x z : Point n} {r : ℝ} (hz : z ∉ Metric.closedBall x r) : ∀ᶠ (y : Point n) in nhdsWithin z C, y ∉ Metric.ball x r

Outside a closed metric ball, one is eventually outside the corresponding open ball, even relative to an arbitrary set C.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatchAt.coveredPatchAt {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 : PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatchAt C boundary F g B x J) : PerronLowerEnvelopeLocalQuadraticCompactInactiveCoveredPatchAt C boundary F g B x J

Exterior compact-inactive data supplies the boundary-covered compact-inactive datum.

theorem ViscositySolns.PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatch.coveredPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatch C boundary F g B) : PerronLowerEnvelopeLocalQuadraticCompactInactiveCoveredPatch C boundary F g B

Global exterior compact-inactive data supplies global boundary-covered compact-inactive data.

theorem ViscositySolns.eventually_not_mem_ball_or_mem_outerAnnulus {n : ℕ} {C : Set (Point n)} {x z : Point n} {r : ℝ} (hr : 0 < r) (hzNotBall : z ∉ Metric.ball x r) : ∀ᶠ (y : Point n) in nhdsWithin z C, y ∉ Metric.ball x r ∨ 3 * r / 4 ≤ dist y x ∧ dist y x ≤ r

Near a point outside an open ball, points inside the ball lie in its outer annulus.