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

Perron-family assembly interfaces

Perron existence theorems using the canonical Perron-family upper side and several lower bump interfaces.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_strictSubsolutionPatch {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 : PerronLowerEnvelopeStrictSubsolutionPatch 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 upper side represented canonically by the Perron family and the top filter.

This is the source-shaped assembly interface: comparison remains an explicit DirichletComparisonPrinciple, the upper-envelope subsolution property comes from supremum stability applied to the Perron family, and the lower-envelope supersolution property comes from the strict bumped-subsolution form of the Perron bump lemma.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_pointwiseStrictSubsolutionPatch {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 : PerronLowerEnvelopePointwiseStrictSubsolutionPatch 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 pointwise-lower-semicontinuous form of the lower bump lemma.

This is the most local source-shaped interface in this file: the analytic bump construction only has to produce a Dirichlet subsolution patch whose value at the failed contact lies strictly above W_* and is lower semicontinuous there.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_continuousStrictPatch {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 : PerronLowerEnvelopeContinuousStrictSubsolutionPatch 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 continuous pointwise form of the lower bump lemma.

This is the smooth-bump-facing assembly interface: the lower-side analytic input may provide a continuous Dirichlet subsolution patch at the failed contact, rather than an already-neighborhood-strict patch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_continuousBump {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 : PerronLowerEnvelopeContinuousBump 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 continuous Dirichlet-bump form of the lower bump lemma.

The analytic input only has to produce a continuous Dirichlet subsolution bump strictly above W_* at each failed contact. The lower barrier is inserted by the formal max-patching bridge in Bump.lean.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_continuousMaxPatch {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 : PerronLowerEnvelopeContinuousMaxPatch 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 continuous max-patch form of the lower bump lemma.

The remaining analytic input is now localized around the patched function: for each failed contact, produce a continuous bump w strictly above W_* such that max lower w is a Dirichlet subsolution.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_localMaxPatch {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 : PerronLowerEnvelopeContinuousLocalMaxPatch 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 continuous local max-patch form of the lower bump lemma.

This exposes the local gluing obligation for the patched function max lower w: prove its boundary inequality and supply local subsolution germs around each point of C.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_branchMaxPatch {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 : PerronLowerEnvelopeContinuousBranchMaxPatch 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 continuous max-patch form of the lower bump lemma.

This is a branchwise gluing interface: around each point the patched function max lower w may be certified by the lower-barrier branch or by another local viscosity-subsolution branch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_activeMaxPatch {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 : PerronLowerEnvelopeContinuousActiveMaxPatch 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 active-branch continuous max-patch form of the lower bump lemma.

This exposes the usual local max-gluing inequalities: near each point, either the lower barrier dominates the bump or the bump branch dominates and agrees with a local subsolution representative.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_strictActivePatch {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 : PerronLowerEnvelopeContinuousStrictActiveMaxPatch 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 active-branch continuous max-patch form of the lower bump lemma.

This is a strict branch-separation gluing interface: near each point, either the bump is strictly below the lower barrier, or it is strictly above and agrees with a local subsolution branch.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_strictActiveSubsolutionBump {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 : PerronLowerEnvelopeContinuousStrictActiveSubsolutionBump 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 active subsolution-bump form of the lower bump lemma.

In this interface the raw bump is already a viscosity subsolution, so the upper active branch of max lower bump uses the bump itself as its local subsolution representative.

theorem ViscositySolns.PerronMethodExistenceTheorem.of_perronFamily_top_and_strictActiveDirichletBump {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 : PerronLowerEnvelopeContinuousStrictActiveDirichletBump 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 active Dirichlet-bump form of the lower bump lemma.

Here the raw bump is a Dirichlet subsolution. The only max-gluing input left is strict branch separation between the bump and the lower barrier.

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

Perron's method with the canonical Perron-family upper side and source-shaped interior quadratic bump data for the lower side.

This is the quadratic-bump version of the lower Lemma 4.4 interface: each failed lower-envelope subjet inequality supplies a certified quadratic bump, and the Perron assembly turns that into existence using only the abstract comparison principle.