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

Perron bump supersolution consequences

Conversion from lower-envelope contradiction interfaces to lower-envelope subjet inequalities and Dirichlet supersolution conclusions.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_subjetInequality_of_bumpContradiction {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hbump : PerronLowerEnvelopeBumpContradiction C boundary F g B) : PerronLowerEnvelopeSubjetInequality C boundary F g B

The bump contradiction supplies the lower Perron envelope subjet inequality.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_viscositySupersolution_of_subjetInequality {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hperronBddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)) (hperronCobddAbove : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)) (hineq : PerronLowerEnvelopeSubjetInequality C boundary F g B) : ViscositySupersolution C F (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

The lower Perron envelope is a viscosity supersolution once the bump argument has supplied the subjet inequality.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_viscositySupersolution_of_bumpInequality {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hne : ∀ x ∈ C, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlowerBddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hineq : PerronLowerEnvelopeSubjetInequality C boundary F g B) : ViscositySupersolution C F (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Barrier-local-bounded version of the lower-envelope supersolution criterion.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_bumpInequality {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution criterion after boundary trace inheritance.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_bumpContradiction {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the formal bump contradiction.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_strictPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the source-shaped strict patch form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_localizedImprovement {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the localized-improvement form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_neighborhoodImprovement {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the neighborhood-form localized improvement version of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_strictSubsolutionPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the source-shaped strict subsolution patch form of the Perron bump lemma.

The analytic bump construction only has to produce a Dirichlet subsolution patch above the lower barrier. The comparison principle supplies the missing upper-barrier bound needed to place the patch in the Perron class.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_pointwiseStrictPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the pointwise-lower-semicontinuous form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_continuousStrictPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the continuous pointwise form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_continuousBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the continuous Dirichlet bump form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_continuousMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the continuous max-patch form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_localMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the continuous local max-patch form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_branchMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the branch-local continuous max-patch form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_activeMaxPatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the active-branch continuous max-patch form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_strictActivePatch {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the strict active-branch continuous max-patch form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_strictActiveBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the strict active subsolution-bump form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_strictActiveDirichletBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from the strict active Dirichlet-bump form of the Perron bump lemma.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_interiorQuadraticBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) (hFell : DegenerateElliptic F) (hinterior : ∀ z ∈ C, z ∈ interior C) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from source-shaped interior quadratic bump data.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_dirichletSupersolution_of_maxPatchBump {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hlowerTrace : BoundaryLowerTraceOn C boundary g B.lower) (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) : DirichletSupersolutionOn C boundary F g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet lower-envelope supersolution from a max-patch localized bump construction.