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

Perron bump interface bridges

Implications between the local and global Perron lower-envelope bump interfaces.

theorem ViscositySolns.PerronLowerEnvelopeContinuousStrictSubsolutionPatchAt.pointwiseStrict {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} (hpatch : PerronLowerEnvelopeContinuousStrictSubsolutionPatchAt C boundary F g B x) : PerronLowerEnvelopePointwiseStrictSubsolutionPatchAt C boundary F g B x

A continuous strict bump is in particular a lower-semicontinuous strict bump.

theorem ViscositySolns.DirichletBarrierPair.continuousMaxPatchAt_of_continuousBumpAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hbump : PerronLowerEnvelopeContinuousBumpAt C boundary F g B x) : PerronLowerEnvelopeContinuousMaxPatchAt C boundary F g B x

A continuous Dirichlet bump gives continuous max-patch data after maxing with the lower barrier.

theorem ViscositySolns.DirichletBarrierPair.continuousMaxPatchAt_of_continuousLocalMaxPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hpatch : PerronLowerEnvelopeContinuousLocalMaxPatchAt C boundary F g B x) : PerronLowerEnvelopeContinuousMaxPatchAt C boundary F g B x

The local-germ max-patch formulation assembles the global continuous max-patch datum.

theorem ViscositySolns.DirichletBarrierPair.localizedImprovementAt_of_continuousMaxPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hne : (nhdsWithin x C).NeBot) (hupperBddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hpatch : PerronLowerEnvelopeContinuousMaxPatchAt C boundary F g B x) : PerronLowerEnvelopeLocalizedImprovementAt C boundary F g B x

Continuous max-patch data gives localized-improvement data. The lower-envelope selection supplies points near the contact where W lies below an intermediate level, while continuity of the raw bump keeps the patched max above that level.

theorem ViscositySolns.DirichletBarrierPair.localizedImprovementAt_of_pointwiseStrictSubsolutionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hne : (nhdsWithin x C).NeBot) (hupperBddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hpatch : PerronLowerEnvelopePointwiseStrictSubsolutionPatchAt C boundary F g B x) : PerronLowerEnvelopeLocalizedImprovementAt C boundary F g B x

Pointwise lower-semicontinuous strict subsolution patch data gives localized improvement data.

theorem ViscositySolns.DirichletBarrierPair.localizedImprovementAt_of_neighborhoodImprovementAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (himprove : PerronLowerEnvelopeNeighborhoodImprovementAt C boundary F g B x) : PerronLowerEnvelopeLocalizedImprovementAt C boundary F g B x

The neighborhood-form improvement is exactly strong enough to give the frequent localized-improvement formulation used by the formal contradiction.

theorem ViscositySolns.DirichletBarrierPair.continuousLocalMaxPatchAt_of_branchMaxPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hpatch : PerronLowerEnvelopeContinuousBranchMaxPatchAt C boundary F g B x) : PerronLowerEnvelopeContinuousLocalMaxPatchAt C boundary F g B x

Branch-local max-patch data supplies the local-germ max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.branchMaxPatchAt_of_activeMaxPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hpatch : PerronLowerEnvelopeContinuousActiveMaxPatchAt C boundary F g B x) : PerronLowerEnvelopeContinuousBranchMaxPatchAt C boundary F g B x

Active-branch max-patch data supplies the branch-local max-patch formulation.

theorem ViscositySolns.DirichletBarrierPair.activeMaxPatchAt_of_strictActiveMaxPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hpatch : PerronLowerEnvelopeContinuousStrictActiveMaxPatchAt C boundary F g B x) : PerronLowerEnvelopeContinuousActiveMaxPatchAt C boundary F g B x

Strict active-branch data implies active-branch data by weakening the strict branch inequalities.

theorem ViscositySolns.DirichletBarrierPair.strictActiveMaxPatchAt_of_strictActiveSubsolutionBumpAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hbump : PerronLowerEnvelopeContinuousStrictActiveSubsolutionBumpAt C boundary F g B x) : PerronLowerEnvelopeContinuousStrictActiveMaxPatchAt C boundary F g B x

If the strict active bump is already a viscosity subsolution, it supplies the strict active max-patch data by taking the bump itself as the upper active local branch.

theorem ViscositySolns.DirichletBarrierPair.strictActiveSubsolutionBumpAt_of_strictActiveDirichletBumpAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hbump : PerronLowerEnvelopeContinuousStrictActiveDirichletBumpAt C boundary F g B x) : PerronLowerEnvelopeContinuousStrictActiveSubsolutionBumpAt C boundary F g B x

A strict active Dirichlet bump supplies the strict active subsolution-bump formulation. The max-patch boundary inequality is just the boundary part of the maximum of the lower barrier with the raw bump.

theorem ViscositySolns.DirichletBarrierPair.strictSubsolutionPatchAt_of_continuousMaxPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hpatch : PerronLowerEnvelopeContinuousMaxPatchAt C boundary F g B x) : PerronLowerEnvelopeStrictSubsolutionPatchAt C boundary F g B x

Continuous max-patch bump data gives the source-shaped strict subsolution patch data.

theorem ViscositySolns.DirichletBarrierPair.strictSubsolutionPatchAt_of_continuousBumpAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hbump : PerronLowerEnvelopeContinuousBumpAt C boundary F g B x) : PerronLowerEnvelopeStrictSubsolutionPatchAt C boundary F g B x

Maxing a continuous Dirichlet bump with the lower barrier gives the source-shaped strict subsolution patch data.

theorem ViscositySolns.DirichletBarrierPair.strictSubsolutionPatchAt_of_pointwiseStrictSubsolutionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hpatch : PerronLowerEnvelopePointwiseStrictSubsolutionPatchAt C boundary F g B x) : PerronLowerEnvelopeStrictSubsolutionPatchAt C boundary F g B x

Lower semicontinuity upgrades pointwise strictness at the failed contact into the neighborhood-strict patch data used by the Perron contradiction.

theorem ViscositySolns.DirichletBarrierPair.strictPatchAt_of_strictSubsolutionPatchAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hcomparison : DirichletComparisonPrinciple C boundary F g) {x : Point n} (hpatch : PerronLowerEnvelopeStrictSubsolutionPatchAt C boundary F g B x) : PerronLowerEnvelopeStrictPatchAt C boundary F g B x

Comparison with the upper barrier turns source-shaped strict subsolution patch data into Perron-class strict patch data.