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

Envelope infrastructure for Perron's method

This file contains the upper and lower semicontinuous envelopes used in Section 4 and the first pointwise order facts for the Perron envelope. The definitions use nhdsWithin filters rather than metric balls; in finite dimension this is the same local operation and is a better fit for the existing semijet/stability infrastructure.

noncomputable def ViscositySolns.upperEnvelope {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : Point n → ℝ

The upper semicontinuous envelope of u relative to the domain C.

Equations

• ViscositySolns.upperEnvelope C u x = Filter.limsup u (nhdsWithin x C)

noncomputable def ViscositySolns.lowerEnvelope {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) : Point n → ℝ

The lower semicontinuous envelope of u relative to the domain C.

Equations

• ViscositySolns.lowerEnvelope C u x = Filter.liminf u (nhdsWithin x C)

theorem ViscositySolns.upperEnvelope_def {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x : Point n) : upperEnvelope C u x = Filter.limsup u (nhdsWithin x C)

theorem ViscositySolns.lowerEnvelope_def {n : ℕ} (C : Set (Point n)) (u : Point n → ℝ) (x : Point n) : lowerEnvelope C u x = Filter.liminf u (nhdsWithin x C)

theorem ViscositySolns.frequently_lt_upperEnvelope {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {a : ℝ} (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) (ha : a < upperEnvelope C u x) : ∃ᶠ (y : Point n) in nhdsWithin x C, a < u y

If a level lies strictly below the upper envelope at x, then points of C arbitrarily close to x have values above that level.

theorem ViscositySolns.frequently_lowerEnvelope_lt {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {a : ℝ} (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) (ha : lowerEnvelope C u x < a) : ∃ᶠ (y : Point n) in nhdsWithin x C, u y < a

If the lower envelope at x lies strictly below a level, then points of C arbitrarily close to x have values below that level.

theorem ViscositySolns.exists_mem_nhdsWithin_lt_upperEnvelope {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {a : ℝ} (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) (ha : a < upperEnvelope C u x) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ y ∈ V, a < u y

Every relative neighborhood of x contains a point whose value is above a strict level below the upper envelope.

theorem ViscositySolns.exists_mem_nhdsWithin_lowerEnvelope_lt {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {a : ℝ} (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) (ha : lowerEnvelope C u x < a) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ y ∈ V, u y < a

Every relative neighborhood of x contains a point whose value is below a strict level above the lower envelope.

theorem ViscositySolns.exists_upperEnvelope_sub_lt {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {ε : ℝ} (hε : 0 < ε) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ y ∈ V, upperEnvelope C u x - ε < u y

For every positive ε, every relative neighborhood of x contains a point with value above upperEnvelope C u x - ε.

theorem ViscositySolns.exists_lt_lowerEnvelope_add {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} {ε : ℝ} (hε : 0 < ε) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) {V : Set (Point n)} (hV : V ∈ nhdsWithin x C) : ∃ y ∈ V, u y < lowerEnvelope C u x + ε

For every positive ε, every relative neighborhood of x contains a point with value below lowerEnvelope C u x + ε.

theorem ViscositySolns.upperSemicontinuousOn_upperEnvelope_on {n : ℕ} {C S : Set (Point n)} {u : Point n → ℝ} (hbddAbove : ∀ x ∈ S, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) (hcobddBelow : ∀ x ∈ S, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) : UpperSemicontinuousOn (upperEnvelope C u) S

The upper envelope is upper semicontinuous on any set where its defining filters satisfy the real-valued limsup boundedness conditions. In particular, the set may include boundary points of C.

theorem ViscositySolns.lowerSemicontinuousOn_lowerEnvelope_on {n : ℕ} {C S : Set (Point n)} {u : Point n → ℝ} (hbddBelow : ∀ x ∈ S, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) (hcobddAbove : ∀ x ∈ S, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) : LowerSemicontinuousOn (lowerEnvelope C u) S

The lower envelope is lower semicontinuous also at boundary points, provided its defining filters satisfy the real-valued liminf bounds.

theorem ViscositySolns.upperSemicontinuousOn_upperEnvelope {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) (hcobddBelow : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) : UpperSemicontinuousOn (upperEnvelope C u) C

The upper envelope is upper semicontinuous on C, under local boundedness.

theorem ViscositySolns.lowerSemicontinuousOn_lowerEnvelope {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} (hbddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) (hcobddAbove : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) : LowerSemicontinuousOn (lowerEnvelope C u) C

The lower envelope is lower semicontinuous on C, under local boundedness.

def ViscositySolns.BoundaryLowerTraceOn {n : ℕ} (C boundary : Set (Point n)) (g u : Point n → ℝ) : Prop

Lower semicontinuous boundary trace of a function relative to C.

Equations

• ViscositySolns.BoundaryLowerTraceOn C boundary g u = ∀ x ∈ boundary, ViscositySolns.lowerEnvelope C u x = g x

def ViscositySolns.BoundaryUpperTraceOn {n : ℕ} (C boundary : Set (Point n)) (g u : Point n → ℝ) : Prop

Upper semicontinuous boundary trace of a function relative to C.

Equations

• ViscositySolns.BoundaryUpperTraceOn C boundary g u = ∀ x ∈ boundary, ViscositySolns.upperEnvelope C u x = g x

theorem ViscositySolns.upperEnvelope_le_of_eventually_le {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} (h : ∀ᶠ (y : Point n) in nhdsWithin x C, u y ≤ v y) (hu : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) (hv : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) v) : upperEnvelope C u x ≤ upperEnvelope C v x

theorem ViscositySolns.lowerEnvelope_le_of_eventually_le {n : ℕ} {C : Set (Point n)} {u v : Point n → ℝ} {x : Point n} (h : ∀ᶠ (y : Point n) in nhdsWithin x C, u y ≤ v y) (hu : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) (hv : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) v) : lowerEnvelope C u x ≤ lowerEnvelope C v x

theorem ViscositySolns.lowerEnvelope_le_upperEnvelope {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} [(nhdsWithin x C).NeBot] (hbddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) (hbddBelow : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) : lowerEnvelope C u x ≤ upperEnvelope C u x

theorem ViscositySolns.le_upperEnvelope {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} (hx : x ∈ C) (hbddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) u) : u x ≤ upperEnvelope C u x

theorem ViscositySolns.lowerEnvelope_le {n : ℕ} {C : Set (Point n)} {u : Point n → ℝ} {x : Point n} (hx : x ∈ C) (hbddBelow : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) u) : lowerEnvelope C u x ≤ u x

theorem ViscositySolns.DirichletBarrierPair.lower_le_perronEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hx : x ∈ C ∪ boundary) : B.lower x ≤ perronEnvelope C boundary F g B.lower B.upper x

theorem ViscositySolns.DirichletBarrierPair.perronEnvelope_le_upper {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hx : x ∈ C ∪ boundary) : perronEnvelope C boundary F g B.lower B.upper x ≤ B.upper x

theorem ViscositySolns.DirichletBarrierPair.lowerEnvelope_le_perronEnvelope_lowerEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hlower : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hperron : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)) : lowerEnvelope C B.lower x ≤ lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x

theorem ViscositySolns.DirichletBarrierPair.perronEnvelope_upperEnvelope_le_upperEnvelope {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hperron : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)) (hupper : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) : upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x ≤ upperEnvelope C B.upper x

theorem ViscositySolns.DirichletBarrierPair.perronEnvelope_isBoundedUnder_le {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hupper : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)

theorem ViscositySolns.DirichletBarrierPair.perronEnvelope_isBoundedUnder_ge {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} (hlower : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)

theorem ViscositySolns.DirichletBarrierPair.perronEnvelope_isCoboundedUnder_le {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} [(nhdsWithin x C).NeBot] (hlower : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)

theorem ViscositySolns.DirichletBarrierPair.perronEnvelope_isCoboundedUnder_ge {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} [(nhdsWithin x C).NeBot] (hupper : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)

theorem ViscositySolns.DirichletBarrierPair.perronUpperEnvelope_upperSemicontinuousOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupper : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlower : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) : UpperSemicontinuousOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (C ∪ boundary)

Barrier bounds give upper semicontinuity of the Perron upper envelope throughout the domain and boundary.

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_lowerSemicontinuousOn {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hne : ∀ x ∈ C ∪ boundary, (nhdsWithin x C).NeBot) (hupper : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlower : ∀ x ∈ C ∪ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) : LowerSemicontinuousOn (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (C ∪ boundary)

Barrier bounds give lower semicontinuity of the Perron lower envelope throughout the domain and boundary.

theorem ViscositySolns.DirichletBarrierPair.perronUpperEnvelope_boundarySubsolution {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (htrace : BoundaryUpperTraceOn C boundary g B.upper) (hperron : ∀ x ∈ boundary, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)) (hupper : ∀ x ∈ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) : BoundarySubsolutionOn boundary g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

theorem ViscositySolns.DirichletBarrierPair.perronLowerEnvelope_boundarySupersolution {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (htrace : BoundaryLowerTraceOn C boundary g B.lower) (hlower : ∀ x ∈ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hperron : ∀ x ∈ boundary, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)) : BoundarySupersolutionOn boundary g (lowerEnvelope C (perronEnvelope C boundary F g B.lower B.upper))