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

Strict-boundary Perron interfaces (SubsolutionPatches)

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_strictSubsolutionPatch {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 : PerronLowerEnvelopeStrictSubsolutionPatch 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 used in the source document, with comparison kept as an explicit hypothesis.

The remaining analytic input is the source-shaped strict subsolution patch form of the bump lemma: every failed lower-envelope subjet inequality produces a Dirichlet subsolution patch above the lower barrier. This theorem packages the completed Perron assembly around that input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localizedImprovement {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) (himprove : PerronLowerEnvelopeLocalizedImprovement 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-improvement version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_upperEnvelopeLocalizedImprovement {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) (himprove : PerronUpperEnvelopeLocalizedImprovement 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 a direct localized improvement over the upper Perron envelope. The method layer proves W^* = W on the domain before converting this to the usual localized improvement contradiction.

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

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

Strict-boundary Perron theorem in Dirichlet form, using an already proved lower-envelope viscosity supersolution property.

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

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

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_pointwiseStrictSubsolutionPatch {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 : PerronLowerEnvelopePointwiseStrictSubsolutionPatch 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 pointwise-lower-semicontinuous version of the bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_continuousStrictPatch {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 : PerronLowerEnvelopeContinuousStrictSubsolutionPatch 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 continuous pointwise version of the bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_continuousBump {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) (hbump : PerronLowerEnvelopeContinuousBump 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 continuous Dirichlet-bump version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_continuousMaxPatch {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 : PerronLowerEnvelopeContinuousMaxPatch 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 continuous max-patch version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localMaxPatch {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 : PerronLowerEnvelopeContinuousLocalMaxPatch 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 continuous local max-patch version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_branchMaxPatch {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 : PerronLowerEnvelopeContinuousBranchMaxPatch 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 branch-local continuous max-patch version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_activeMaxPatch {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 : PerronLowerEnvelopeContinuousActiveMaxPatch 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 continuous max-patch version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_strictActivePatch {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 : PerronLowerEnvelopeContinuousStrictActiveMaxPatch 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 strict active-branch continuous max-patch version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_strictActiveSubsolutionBump {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) (hbump : PerronLowerEnvelopeContinuousStrictActiveSubsolutionBump 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 strict active subsolution-bump version of the lower bump input.

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_strictActiveDirichletBump {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) (hbump : PerronLowerEnvelopeContinuousStrictActiveDirichletBump 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 strict active Dirichlet-bump version of the lower bump input.

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

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

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

theorem ViscositySolns.PerronMethodExistenceTheorem.strictBoundary_of_localQuadraticMaxPatch {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 : PerronLowerEnvelopeLocalQuadraticMaxPatch 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-shaped local quadratic max-patch version of the lower bump input.

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

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