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

Perron-family lower conclusion interfaces (CoreInterfaces)

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.perronFamily_top_upperEnvelope_eqOn_domain {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) : Set.EqOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (perronEnvelope C boundary F g B.lower B.upper) C

With the canonical Perron-family upper side, the upper envelope is admissible and therefore equals the pointwise Perron envelope on the PDE domain.

This is the maximality step used in the source proof before the lower bump is applied directly to W.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_lowerViscosity {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) (hlowerVisc : ViscositySupersolution C F (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))) (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 and a supplied lower-envelope viscosity supersolution property.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bumpInequality {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) (hineq : PerronLowerEnvelopeSubjetInequality 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 lower subjet inequality supplied by the bump argument.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_bumpContradiction {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) (hbump : PerronLowerEnvelopeBumpContradiction 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 formal bump contradiction as the lower-side input.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localizedImprovement {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) (himprove : PerronLowerEnvelopeLocalizedImprovement 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 localized improvement form of the lower bump lemma.

This is close to the payload of CIL Lemma 4.4: every failed lower-envelope subjet inequality produces a Dirichlet subsolution above the lower barrier that beats the Perron envelope at points arbitrarily near the failed contact.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_upperEnvelopeLocalizedImprovement {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) (himprove : PerronUpperEnvelopeLocalizedImprovement 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 a direct localized improvement over W^*.

The method layer first proves the source-proof maximality identity W^* = W on C, then converts the direct improvement into the ordinary Perron localized-improvement interface.

theorem ViscositySolns.PerronMethodExistenceTheorem.upperEnvelopeLocalizedImprovement_of_strictPatch {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) (hpatch : PerronLowerEnvelopeStrictPatch C boundary F g B) : PerronUpperEnvelopeLocalizedImprovement C boundary F g B

For the canonical Perron-family upper side, source-style strict patch data supplies direct localized improvement over W^*.

The method layer first recovers the source maximality identity W^* = W on the domain, and the bump layer then transfers the strict patch improvement from W to W^*.

theorem ViscositySolns.PerronMethodExistenceTheorem.upperEnvelopeLocalizedImprovement_of_sourceOuterClosedBallLowerEnvelope {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) : PerronUpperEnvelopeLocalizedImprovement C boundary F g B

For the canonical Perron-family upper side, source outer-annulus lower-envelope data supplies direct localized improvement over W^*.

This instantiates the direct bump bridge with old = W^*: upper stability and comparison make W^* admissible, maximality gives W^* = W on C, and the source annulus estimate patches over W^* without selecting Perron-family branches.

theorem ViscositySolns.PerronMethodExistenceTheorem.upperEnvelopeLocalizedImprovement_of_sourceOuterClosedBallLowerEnvelopeLscSelection {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) : PerronUpperEnvelopeLocalizedImprovement C boundary F g B

Legacy source outer-annulus lower-envelope data still supplies the direct localized improvement after forgetting the branch lower-semicontinuity field.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_neighborhoodImprovement {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) (himprove : PerronLowerEnvelopeNeighborhoodImprovement 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 neighborhood-form localized improvement input.

This exposes the source-document formulation directly: every failed contact has an improved Dirichlet subsolution that beats the Perron envelope in every relative neighborhood of that contact.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_strictPatch {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) (hpatch : PerronLowerEnvelopeStrictPatch 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 source-shaped strict patch form of the lower bump lemma.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_maxPatchBump {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) (hbump : PerronLowerEnvelopeMaxPatchBump 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 max-patch form of the lower bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_strictLocalPatch {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) (hpatch : PerronLowerEnvelopeStrictLocalPatch 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 strict local-patch form of the lower bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localQuadraticMaxPatch {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) (hpatch : PerronLowerEnvelopeLocalQuadraticMaxPatch 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 source-shaped local quadratic max-patch form of the lower bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localQuadraticGluing {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) (hglue : PerronLowerEnvelopeLocalQuadraticGluing 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 local-germ quadratic gluing form of the lower bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localQuadraticBranchGluing {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) (hbranch : PerronLowerEnvelopeLocalQuadraticBranchGluing 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 branch-local quadratic gluing form of the lower bump construction.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localQuadraticPatchSelection {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 : PerronLowerEnvelopeLocalQuadraticPatchSelection 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 explicit patch-selection step.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localQuadraticCompactInactivePatch {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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactivePatch 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 compact-inactive local max-patch data.

This endpoint permits the active quadratic branch to be certified only on local domains, which is the natural form produced by a localized bump.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_compactInactiveSubsolution {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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveSubsolutionPatch 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, finite inactive selection supplies the old branch, and comparison with the upper barrier supplies the global upper bound for the patched subsolution.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_compactInactiveQuadratic {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) (hpatch : PerronLowerEnvelopeLocalQuadraticCompactInactiveQuadraticPatch 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 the active compact-inactive patch input only has to certify the lifted quadratic itself as a local subsolution on relative-open domains.

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

Perron's method with the canonical Perron-family upper side, where the active compact-inactive input supplies only certified local domains for the lifted quadratic. Degenerate ellipticity and Hessian-symmetric invariance certify the quadratic active branch as a viscosity subsolution on those domains.

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

Perron's method with the canonical Perron-family upper side, using symmetrized certified active-domain compact-inactive data. This removes the need for failed subjet Hessians to be supplied as Hermitian.

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

Perron's method with the canonical Perron-family upper side, using boundary-safe compact-inactive data. The caller only proves the boundary subsolution inequality for the lifted quadratic; the max patch inherits it from the old Perron branch.

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

Perron's method with the canonical Perron-family upper side, using boundary-covered compact-inactive data. Covering the boundary by the inactive compact set lets finite Perron selection make the old branch dominate there, so no separate boundary inequality is required for the quadratic branch.

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

Perron's method with the canonical Perron-family upper side, using exterior compact-inactive data. The active quadratic neighborhood is kept away from the Dirichlet boundary, so the inactive compact covers the exterior in C ∪ boundary and hence supplies the boundary-covered datum.

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

Perron's method with the canonical Perron-family upper side, using lower-barrier exterior compact-inactive data. On the inactive compact the lifted quadratic is locally below the lower barrier, which is already a Perron-family member.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_openBarrierExterior {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 : PerronLowerEnvelopeLocalQuadraticOpenBarrierExteriorPatch 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 open-active lower-barrier exterior patch input.

Operator continuity supplies an open active strict-negativity neighborhood; when C is open, the active local domain is C ∩ V. The remaining exterior annulus data is stated only for open active neighborhoods.