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

Perron bump contradiction

Conversion from bump interfaces to the lower-envelope contradiction, subjet inequality, and supersolution conclusion.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_bumpContradictionAt_of_strictPatchAt {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 : PerronLowerEnvelopeStrictPatchAt C boundary F g B x) : ∃ y ∈ C ∪ boundary, ∃ (w : Point n → ℝ), PerronClass C boundary F g B.lower B.upper w ∧ perronEnvelope C boundary F g B.lower B.upper y < w y

Strict patch data implies the formal bump contradiction at the same failed contact point.

theorem ViscositySolns.DirichletBarrierPair.neighborhoodImprovementAt_of_strictPatchAt {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 : PerronLowerEnvelopeStrictPatchAt C boundary F g B x) : PerronLowerEnvelopeNeighborhoodImprovementAt C boundary F g B x

Strict patch data gives the neighborhood-form localized improvement at the same failed contact point.

Given any relative neighborhood of the contact, intersect it with the patch neighborhood and the domain. The lower-envelope selection lemma finds a point there where W is below the strict level, while the patch is above that level.

def ViscositySolns.PerronLowerEnvelopeStrictPatch {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

Strict patch data at every failed subjet inequality.

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.DirichletBarrierPair.strictPatch_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) (hpatch : PerronLowerEnvelopeStrictSubsolutionPatch C boundary F g B) : PerronLowerEnvelopeStrictPatch C boundary F g B

Comparison turns source-shaped strict subsolution patch data into strict patch data for Perron's contradiction.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_bumpContradiction_of_strictPatch {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) (hpatch : PerronLowerEnvelopeStrictPatch C boundary F g B) : PerronLowerEnvelopeBumpContradiction C boundary F g B

The source-shaped strict patch formulation gives the formal bump contradiction.

theorem ViscositySolns.DirichletBarrierPair.neighborhoodImprovement_of_strictPatch {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) (hpatch : PerronLowerEnvelopeStrictPatch C boundary F g B) : PerronLowerEnvelopeNeighborhoodImprovement C boundary F g B

Strict patch data at every failed contact supplies the neighborhood-form localized improvement.

theorem ViscositySolns.DirichletBarrierPair.upperEnvelopeLocalizedImprovementAt_of_strictPatchAt {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) (hEq : Set.EqOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (perronEnvelope C boundary F g B.lower B.upper) C) (hpatch : PerronLowerEnvelopeStrictPatchAt C boundary F g B x) : PerronUpperEnvelopeLocalizedImprovementAt C boundary F g B x

Strict patch data gives a direct localized improvement over W^* once W^* = W on the domain.

theorem ViscositySolns.DirichletBarrierPair.upperEnvelopeLocalizedImprovement_of_strictPatch {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) (hEq : Set.EqOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (perronEnvelope C boundary F g B.lower B.upper) C) (hpatch : PerronLowerEnvelopeStrictPatch C boundary F g B) : PerronUpperEnvelopeLocalizedImprovement C boundary F g B

Global strict patch data gives direct localized improvement over W^* once W^* = W on the domain.

theorem ViscositySolns.DirichletBarrierPair.neighborhoodImprovement_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) (hne : ∀ x ∈ C, (nhdsWithin x C).NeBot) (hupperBddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hpatch : PerronLowerEnvelopeStrictSubsolutionPatch C boundary F g B) : PerronLowerEnvelopeNeighborhoodImprovement C boundary F g B

Comparison turns source-shaped strict subsolution patch data into the neighborhood-form localized improvement.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_bumpContradictionAt_of_localizedImprovementAt {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} (himprove : PerronLowerEnvelopeLocalizedImprovementAt C boundary F g B x) : ∃ y ∈ C ∪ boundary, ∃ (w : Point n → ℝ), PerronClass C boundary F g B.lower B.upper w ∧ perronEnvelope C boundary F g B.lower B.upper y < w y

Localized-improvement data at a failed contact gives the formal bump contradiction at that contact.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_bumpContradiction_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) (himprove : PerronLowerEnvelopeLocalizedImprovement C boundary F g B) : PerronLowerEnvelopeBumpContradiction C boundary F g B

Localized-improvement data at every failed contact gives the formal bump contradiction.

theorem ViscositySolns.PerronUpperEnvelopeLocalizedImprovementAt.lowerEnvelopeLocalizedImprovementAt {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} {x : Point n} (himprove : PerronUpperEnvelopeLocalizedImprovementAt C boundary F g B x) (hEq : Set.EqOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (perronEnvelope C boundary F g B.lower B.upper) C) : PerronLowerEnvelopeLocalizedImprovementAt C boundary F g B x

An improvement over W^* gives the usual Perron localized improvement once W^* = W on the domain.

theorem ViscositySolns.PerronUpperEnvelopeLocalizedImprovement.lowerEnvelopeLocalizedImprovement {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} {B : DirichletBarrierPair C boundary F g} (himprove : PerronUpperEnvelopeLocalizedImprovement C boundary F g B) (hEq : Set.EqOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (perronEnvelope C boundary F g B.lower B.upper) C) : PerronLowerEnvelopeLocalizedImprovement C boundary F g B

Global direct improvement over W^* gives the usual Perron localized improvement once W^* = W on the domain.

def ViscositySolns.PerronLowerEnvelopeStrictLocalPatchAt {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) (x : Point n) : Prop

A local strict-patch datum at a failed lower-envelope contact.

The analytic bump construction should eventually supply such data: a level a strictly above W_* x, a relative neighborhood on which the bump is above a, and an admissible max-patch Perron member. The lower-envelope selection lemma then chooses a nearby point where W < a, hence where the patch exceeds the Perron envelope.

Equations

• One or more equations did not get rendered due to their size.

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

The older max-patch strict-local formulation implies the source-shaped strict patch formulation by taking the patched Perron-class member itself.

theorem ViscositySolns.DirichletBarrierPair.neighborhoodImprovementAt_of_strictLocalPatchAt {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 : PerronLowerEnvelopeStrictLocalPatchAt C boundary F g B x) : PerronLowerEnvelopeNeighborhoodImprovementAt C boundary F g B x

The older strict-local max-patch formulation gives the neighborhood-form localized improvement at the same failed contact.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_maxPatchBumpAt_of_strictLocalPatchAt {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 : PerronLowerEnvelopeStrictLocalPatchAt C boundary F g B x) : PerronLowerEnvelopeMaxPatchBumpAt C boundary F g B x

The local strict-patch formulation implies the concrete max-patch output at the same failed contact point.

def ViscositySolns.PerronLowerEnvelopeStrictLocalPatch {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g : Point n → ℝ) (B : DirichletBarrierPair C boundary F g) : Prop

A strict local patch at every failed subjet inequality.

Equations

• One or more equations did not get rendered due to their size.

theorem ViscositySolns.DirichletBarrierPair.neighborhoodImprovement_of_strictLocalPatch {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) (hpatch : PerronLowerEnvelopeStrictLocalPatch C boundary F g B) : PerronLowerEnvelopeNeighborhoodImprovement C boundary F g B

The older strict-local max-patch formulation supplies the neighborhood-form localized improvement.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_maxPatchBump_of_strictLocalPatch {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) (hpatch : PerronLowerEnvelopeStrictLocalPatch C boundary F g B) : PerronLowerEnvelopeMaxPatchBump C boundary F g B

The strict local-patch formulation supplies the max-patch bump formulation, provided the Perron envelope is locally bounded above by the upper barrier at each interior contact point.

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

A max-patch bump output gives the formal bump contradiction.