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

Perron-family lower conclusion interfaces (BentSourcePatches)

Part of the Perron existence development using the canonical Perron-family upper side and lower-side conclusions from the bump argument. Split from LowerInterfaces.lean; see the umbrella module docstring.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentOpenBarrierExterior {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticOpenBarrierExteriorPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the source-shaped bent open-active lower-barrier exterior patch input.

This matches the bump in the source proof more closely than the unbent quadratic interface: operator continuity supplies a positive vertical lift and a positive downward identity-Hessian bend, while the remaining input is the exterior annulus where the bent quadratic is locally below the lower barrier.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentLocalizedLowerPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticLocalizedLowerPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the localized bent lower-barrier piecewise patch input.

This is the source-shaped endpoint closest to the piecewise construction in Section 4: the patch is locally max(lower, q) on the active neighborhood and locally the lower barrier away from it.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentOpenPiecewisePatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticOpenPiecewisePatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using open patch-set data for the localized bent lower-barrier piecewise patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentBoundaryAwayOpenPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticBoundaryAwayOpenPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using boundary-away open patch-set data for the localized bent lower-barrier piecewise patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentBallPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticBallPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using ball-shaped patch data for the localized bent lower-barrier piecewise patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentClosedBallAnnulusPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticClosedBallAnnulusPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using closed-ball annulus data for the localized bent lower-barrier patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentShrinkingClosedBallAnnulusPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticShrinkingClosedBallAnnulusPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using shrinking closed-ball annulus data for the localized bent lower-barrier patch.

This is the source-shaped ball route: the patch ball is allowed to be smaller than the open strict-negativity neighborhood supplied by operator continuity.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSmallRadiusClosedBallAnnulusPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSmallRadiusClosedBallAnnulusPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using small-radius closed-ball annulus data for the localized bent lower-barrier patch.

The radius is chosen small enough to lie in the operator-continuity strict-negativity neighborhood, then the existing shrinking-annulus route performs the gluing.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceClosedBallAnnulusPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallAnnulusPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the source-radius closed-ball annulus lower bump package.

Here the lift of the bent quadratic is chosen together with the patch radius as in the source proof, rather than being quantified over independently.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceCompactInactivePatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceCompactInactivePatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the source-radius compact-inactive lower bump package.

This route performs the finite old-branch selection inside the Perron proof: local Perron-family domination on the inactive compact set is converted to one old Perron branch, then maxed with the bent source quadratic.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceAnnulusSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the source-radius transition-annulus lower bump package.

Finite old-branch selection is required only on the compact transition set; outside the patch ball the piecewise patch is already the old branch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceClosedAnnulusSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the concrete closed-annulus version of the source-radius transition package.

The metric transition across the patch sphere is discharged by the bridge to PerronLowerEnvelopeBentQuadraticSourceAnnulusSelectionPatch; the caller only supplies local Perron-family domination on the explicit annulus r / 2 <= dist z x <= r.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceClosedAnnulusLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the lower-semicontinuous pointwise branch version of the closed-annulus source package.

The pointwise strict branch gap and lower semicontinuity are converted into local branch domination on the explicit annulus before applying the closed-annulus theorem.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceClosedAnnulusEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using strict Perron-envelope approximation on the explicit closed annulus plus lower-semicontinuity of Perron-family branches there.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceClosedAnnulusDomainEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using strict Perron-envelope approximation on the closed annulus and deriving the required pointwise Perron-family boundedness from the annulus-domain condition.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceClosedBallEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using closed-ball source geometry to supply the domain-controlled closed-annulus package.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceOuterClosedBallLowerEnvelopePatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the outer-transition closed-ball annulus package.

The lower bump input is stated on 3 * r / 4 <= dist z x <= r, which is still enough for the piecewise patch transition near the patch sphere and leaves room for the source subjet estimate.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceOuterClosedBallLowerEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Legacy outer-transition closed-ball annulus package implies the no-LSC method input by forgetting the branch lower-semicontinuity field.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceOuterClosedBallOpenGeometry {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hboundaryOutside : ∀ z ∈ boundary, z ∉ C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, where operator continuity and open-domain geometry supply the source outer-closed-ball lower-envelope patch package directly.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceOuterClosedBallSemijetLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using semijet-driven outer-transition source data.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using small-radius semijet-driven outer-transition source data.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceOuterClosedBallGeometricSemijetLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using geometric small-radius semijet outer-transition source data. Operator continuity supplies the source strict-negativity scale.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceOuterAnnulusLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hboundaryOutside : ∀ z ∈ boundary, z ∉ C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceOuterAnnulusLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using pure outer-annulus branch lower-semicontinuity data. Openness of the domain supplies the closed-ball geometry.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_perronFamilyLowerSemicontinuousOnDomain {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hboundaryOutside : ∀ z ∈ boundary, z ∉ C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hreg : PerronFamilyLowerSemicontinuousOnDomain C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using the named domain lower-semicontinuity regularity of Perron-family branches. Openness of the domain converts this branch regularity into the source outer-annulus LSC package used by the quadratic bump assembly.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bentSourceClosedBallLowerEnvelopeLscSelectionPatch {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant F) (hCopen : IsOpen C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hpatch : PerronLowerEnvelopeBentQuadraticSourceClosedBallLowerEnvelopeLscSelectionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, using closed-ball source geometry and annulus strictness against the lower relaxed Perron envelope.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localQuadraticCompactInactiveSelection {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hselect : PerronLowerEnvelopeLocalQuadraticCompactInactiveSelection C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side, where operator continuity supplies the lifted quadratic and the remaining input is the compact-inactive selection step.

This is closer to the source bump construction than the branch-separation patch-selection interface: outside the active quadratic neighborhood, finite Perron selection makes the old branch dominate; inside the active neighborhood, the max of the old branch and the local quadratic subsolution representative certifies the local germ.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localQuadraticActiveGluing {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hactive : PerronLowerEnvelopeLocalQuadraticActiveGluing C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron's method with the canonical Perron-family upper side and the active-branch quadratic gluing form of the lower bump construction.