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

Strict-boundary Perron interfaces (EnvelopeAssembly)

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_bentSourceClosedAnnulusEnvelopeLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusEnvelopeLscSelectionPatch 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 strict Perron-envelope approximation on the explicit closed annulus plus lower-semicontinuity of Perron-family branches there.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceClosedAnnulusDomainEnvelopeLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceClosedAnnulusDomainEnvelopeLscSelectionPatch 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 domain-controlled strict Perron-envelope approximation package on the explicit closed annulus.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceClosedBallEnvelopeLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceClosedBallEnvelopeLscSelectionPatch 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 source geometry for the explicit closed-annulus lower bump package.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceClosedBallLowerEnvelopeLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceClosedBallLowerEnvelopeLscSelectionPatch 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 source geometry with annulus strictness against the lower relaxed Perron envelope.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceOuterClosedBallLowerEnvelopePatch {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopePatch 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 outer-transition closed-ball annulus package.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceOuterClosedBallLowerEnvelopeLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallLowerEnvelopeLscSelectionPatch 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 legacy outer-transition closed-ball annulus package with branch lower-semicontinuity.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceOuterClosedBallOpenGeometry {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) (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))

Strict-boundary Perron theorem in Dirichlet form, where operator continuity and open-domain geometry supply the source outer-closed-ball lower-envelope patch package directly.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceOuterClosedBallSemijetLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSemijetLscSelectionPatch 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 semijet-driven outer-transition source package.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallSmallRadiusSemijetLscSelectionPatch 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 small-radius semijet-driven outer-transition source package.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceOuterClosedBallGeometricSemijetLscSelectionPatch {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 : PerronLowerEnvelopeBentQuadraticSourceOuterClosedBallGeometricSemijetLscSelectionPatch 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 geometric small-radius semijet-driven outer-transition source package.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_bentSourceOuterAnnulusLscSelectionPatch {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) (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))

Strict-boundary Perron theorem in Dirichlet form, using pure outer-annulus branch lower-semicontinuity data.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_perronFamilyLowerSemicontinuousOnDomain {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) (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))

Strict-boundary Perron theorem in Dirichlet form, using domain lower-semicontinuity of the Perron-family branches as the remaining branch regularity input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticCompactInactiveSelection {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 : PerronLowerEnvelopeLocalQuadraticCompactInactiveSelection 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 selection for the remaining source bump gluing step.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticActiveGluing {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) (hactive : PerronLowerEnvelopeLocalQuadraticActiveGluing 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 active-branch quadratic gluing version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_interiorQuadraticBump {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) (hinterior : ∀ z ∈ C, z ∈ interior 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) (hbump : PerronLowerEnvelopeInteriorQuadraticBump 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 source-shaped interior quadratic bump data for the lower-side construction.

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

Packaged hypotheses for the Section 4 Perron existence theorem with Dirichlet data g.

The comparison principle remains abstract here, preserving the Perron/comparison import boundary. Operator continuity, open-domain geometry, and boundary separation supply the source outer-closed-ball lower-envelope annulus package internally. The method layer proves the maximality identity W^* = W on the domain and patches directly over W^*, so this final wrapper does not expose the lower bump or abstract localized-improvement payload.

• comparison : DirichletComparisonPrinciple C boundary F g
• operator_continuous : OperatorContinuous F
• degenerate_elliptic : DegenerateElliptic F
• hessian_symmetric_invariant : HessianSymmetricInvariant F
• domain_open : IsOpen C
• boundary_outside_domain (z : Point n) : z ∈ boundary → z ∉ C
• lower_trace : BoundaryLowerTraceOn C boundary g B.lower
• upper_trace : BoundaryUpperTraceOn C boundary g B.upper
• nontrivial_nhds (x : Point n) : x ∈ C ∪ boundary → (nhdsWithin x C).NeBot
• upper_locally_bounded (x : Point n) : x ∈ C ∪ boundary → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper
• lower_locally_bounded (x : Point n) : x ∈ C ∪ boundary → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower

structure ViscositySolns.PerronStrictBoundaryZeroSection4Hypotheses {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (B : DirichletBarrierPair C boundary F fun (x : Point n) => 0) : Prop

Packaged hypotheses for the zero-boundary Section 4 Perron existence theorem. These are the hypotheses of PerronStrictBoundarySection4Hypotheses with g = 0.

• comparison : DirichletComparisonPrinciple C boundary F fun (x : Point n) => 0
• operator_continuous : OperatorContinuous F
• degenerate_elliptic : DegenerateElliptic F
• hessian_symmetric_invariant : HessianSymmetricInvariant F
• domain_open : IsOpen C
• boundary_outside_domain (z : Point n) : z ∈ boundary → z ∉ C
• lower_trace : BoundaryLowerTraceOn C boundary (fun (x : Point n) => 0) B.lower
• upper_trace : BoundaryUpperTraceOn C boundary (fun (x : Point n) => 0) B.upper
• nontrivial_nhds (x : Point n) : x ∈ C ∪ boundary → (nhdsWithin x C).NeBot
• upper_locally_bounded (x : Point n) : x ∈ C ∪ boundary → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper
• lower_locally_bounded (x : Point n) : x ∈ C ∪ boundary → Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary {n : ℕ} {g : Point n → ℝ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F g) (h : PerronStrictBoundarySection4Hypotheses C boundary F g B) : DirichletSolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Final Perron existence theorem in the Section 4 shape, with Dirichlet data g.

This is the stable public wrapper around the Perron assembly: upper stability, comparison with the upper barrier, operator-continuous quadratic bumping, and open-domain source geometry combine to produce the Perron solution.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_zero {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} (B : DirichletBarrierPair C boundary F fun (x : Point n) => 0) (h : PerronStrictBoundaryZeroSection4Hypotheses C boundary F B) : DirichletSolutionOn C boundary F (fun (x : Point n) => 0) (upperEnvelope C (perronEnvelope C boundary F (fun (x : Point n) => 0) B.lower B.upper))

Final zero-boundary Perron existence theorem in the Section 4 shape: the case g = 0 of strictBoundary.