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

Strict-boundary Perron interfaces (BentAnnulusPatches)

Part of Dirichlet-data specializations of the Perron method theorem in the forms closest to the source document. Split from StrictBoundary.lean; see the umbrella module docstring.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticPatchSelection {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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 : PerronLowerEnvelopeLocalQuadraticPatchSelection C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using operator continuity for the lifted quadratic and an explicit patch-selection input for the remaining local gluing step.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticCompactInactivePatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactivePatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using operator continuity for the lifted quadratic and compact-inactive local patch data for the remaining source bump step.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticCompactInactiveSubsolution {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using operator continuity for the lifted quadratic, compact-inactive local subsolution-patch data, and comparison for the upper-barrier bound.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticCompactInactiveQuadratic {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using compact-inactive data whose active branch is the lifted quadratic itself on relative-open local subsolution domains.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticCompactInactiveCertified {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveCertifiedPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using certified compact-inactive active domains for the lifted quadratic. The quadratic subsolution certification is discharged from degenerate ellipticity and Hessian-symmetric invariance.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_compactInactiveSymCertified {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveSymCertifiedPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using symmetrized certified compact-inactive active-domain data. Hessian-symmetric invariance removes the need to assume the failed subjet Hessian is Hermitian.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_compactInactiveBoundary {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveBoundaryPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using boundary-safe compact-inactive data. The boundary condition is checked only for the lifted quadratic branch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_compactInactiveCovered {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveCoveredPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using boundary-covered compact-inactive data. Boundary domination is supplied by the selected old Perron branch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_compactInactiveExterior {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant 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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveExteriorPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using exterior compact-inactive data. The active quadratic neighborhood is separated from the boundary, and the inactive compact covers the exterior in C ∪ boundary.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_barrierExterior {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hF : OperatorContinuous F) (hFell : DegenerateElliptic F) (hFinv : HessianSymmetricInvariant 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) (hpatch : PerronLowerEnvelopeLocalQuadraticBarrierExteriorPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using lower-barrier exterior compact-inactive data. On the inactive compact, the lower barrier itself supplies the old Perron branch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_openBarrierExterior {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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 : PerronLowerEnvelopeLocalQuadraticOpenBarrierExteriorPatch C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Strict-boundary Perron theorem in Dirichlet form, using open-active lower-barrier exterior data. Operator continuity supplies the open active quadratic neighborhood, and openness of C supplies the active local domain.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentOpenBarrierExterior {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using the bent open-active lower-barrier exterior data from the source bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentLocalizedLowerPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using the localized bent lower-barrier piecewise patch data from the source bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentOpenPiecewisePatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using open patch-set data for the localized bent lower-barrier piecewise patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentBoundaryAwayOpenPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using boundary-away open patch-set data for the localized bent lower-barrier piecewise patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentBallPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using ball-shaped patch data for the localized bent lower-barrier piecewise patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentClosedBallAnnulusPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using closed-ball annulus data for the localized bent lower-barrier patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentShrinkingClosedBallAnnulusPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using shrinking closed-ball annulus data for the localized bent lower-barrier patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSmallRadiusClosedBallAnnulusPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using small-radius closed-ball annulus data for the localized bent lower-barrier patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceClosedBallAnnulusPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using the source-radius closed-ball annulus data from the localized lower bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceCompactInactivePatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using the source-radius compact-inactive lower bump package with finite old-branch selection.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceAnnulusSelectionPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using the source-radius transition-annulus lower bump package.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceClosedAnnulusSelectionPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using the source-radius closed-annulus transition package.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceClosedAnnulusLscSelectionPatch {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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))

Strict-boundary Perron theorem in Dirichlet form, using the lower-semicontinuous pointwise branch version of the source-radius closed-annulus transition package.