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

Supremum stability for Perron's method

This file should house the formal version of Section 4, Lemma 4.2: the upper semicontinuous envelope of a locally bounded supremum of subsolutions is again a subsolution. It may reuse the half-relaxed-limit semijet approximation machinery, but it must not depend on the concrete comparison proof.

noncomputable def ViscositySolns.pointwiseSup {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) : Point n → ℝ

Pointwise supremum of an indexed family of real-valued functions.

Equations

• ViscositySolns.pointwiseSup uᵢ x = sSup {r : ℝ | ∃ (i : ι), r = uᵢ i x}

theorem ViscositySolns.le_pointwiseSup {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {x : Point n} {i : ι} (hbdd : BddAbove {r : ℝ | ∃ (j : ι), r = uᵢ j x}) : uᵢ i x ≤ pointwiseSup uᵢ x

theorem ViscositySolns.pointwiseSup_le {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {x : Point n} {a : ℝ} (hne : (Set.range fun (i : ι) => uᵢ i x).Nonempty) (hle : ∀ (i : ι), uᵢ i x ≤ a) : pointwiseSup uᵢ x ≤ a

theorem ViscositySolns.limsup_pointwiseSup_comp_snd_top {n : ℕ} {ι : Type u_1} [Nonempty ι] (uᵢ : ι → Point n → ℝ) (C : Set (Point n)) (x : Point n) : Filter.limsup (fun (q : ι × Point n) => pointwiseSup uᵢ q.2) (⊤ ×ˢ nhdsWithin x C) = upperEnvelope C (pointwiseSup uᵢ) x

Taking the limsup of the pointwise supremum along nhdsWithin is the same as taking the limsup of its pullback along the second projection of the top-index product filter.

theorem ViscositySolns.frequently_lt_halfRelaxedValue_top_of_frequently_lt_pointwiseSup {n : ℕ} {ι : Type u_1} [Nonempty ι] {uᵢ : ι → Point n → ℝ} {C : Set (Point n)} {x : Point n} {a : ℝ} (hbddPoint : ∀ᶠ (y : Point n) in nhdsWithin x C, BddAbove {r : ℝ | ∃ (i : ι), r = uᵢ i y}) (hfreq : ∃ᶠ (y : Point n) in nhdsWithin x C, a < pointwiseSup uᵢ y) : ∃ᶠ (q : ι × Point n) in ⊤ ×ˢ nhdsWithin x C, a < uᵢ q.1 q.2

If the pointwise supremum is frequently above a level, then the indexed family is frequently above that level along the ⊤-index half-relaxed filter.

theorem ViscositySolns.upperHalfRelaxedLimit_top_le_upperEnvelope_pointwiseSup {n : ℕ} {ι : Type u_1} [Nonempty ι] {uᵢ : ι → Point n → ℝ} {C : Set (Point n)} {x : Point n} (hbddPoint : ∀ᶠ (y : Point n) in nhdsWithin x C, BddAbove {r : ℝ | ∃ (i : ι), r = uᵢ i y}) (hpointBddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (pointwiseSup uᵢ)) (hhrCobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter ⊤ C x) (halfRelaxedValue uᵢ)) : upperHalfRelaxedLimit uᵢ ⊤ C x ≤ upperEnvelope C (pointwiseSup uᵢ) x

The upper half-relaxed limit over the ⊤ index filter is bounded above by the upper envelope of the indexed pointwise supremum.

theorem ViscositySolns.upperEnvelope_pointwiseSup_le_upperHalfRelaxedLimit_top {n : ℕ} {ι : Type u_1} [Nonempty ι] {uᵢ : ι → Point n → ℝ} {C : Set (Point n)} {x : Point n} (hbddPoint : ∀ᶠ (y : Point n) in nhdsWithin x C, BddAbove {r : ℝ | ∃ (i : ι), r = uᵢ i y}) (hpointCobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (pointwiseSup uᵢ)) (hhrCobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter ⊤ C x) (halfRelaxedValue uᵢ)) (hhrBddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter ⊤ C x) (halfRelaxedValue uᵢ)) : upperEnvelope C (pointwiseSup uᵢ) x ≤ upperHalfRelaxedLimit uᵢ ⊤ C x

The upper envelope of the indexed pointwise supremum is bounded above by the upper half-relaxed limit over the ⊤ index filter.

theorem ViscositySolns.upperEnvelope_pointwiseSup_eq_upperHalfRelaxedLimit_top {n : ℕ} {ι : Type u_1} [Nonempty ι] {uᵢ : ι → Point n → ℝ} {C : Set (Point n)} {x : Point n} (hbddPoint : ∀ᶠ (y : Point n) in nhdsWithin x C, BddAbove {r : ℝ | ∃ (i : ι), r = uᵢ i y}) (hpointBddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (pointwiseSup uᵢ)) (hpointCobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (pointwiseSup uᵢ)) (hhrCobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter ⊤ C x) (halfRelaxedValue uᵢ)) (hhrBddAbove : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter ⊤ C x) (halfRelaxedValue uᵢ)) : upperEnvelope C (pointwiseSup uᵢ) x = upperHalfRelaxedLimit uᵢ ⊤ C x

The upper envelope of a nonempty pointwise supremum is canonically represented as an upper half-relaxed limit over the top filter on the index type.

def ViscositySolns.PerronFamily {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g lower upper : Point n → ℝ) : Type

The subtype indexing the Perron family between a fixed barrier pair.

Equations

• ViscositySolns.PerronFamily C boundary F g lower upper = { w : ViscositySolns.Point n → ℝ // ViscositySolns.PerronClass C boundary F g lower upper w }

def ViscositySolns.PerronFamily.fun {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper : Point n → ℝ} (w : PerronFamily C boundary F g lower upper) : Point n → ℝ

The function represented by an indexed Perron-family member.

Equations

• w.fun = ↑w

theorem ViscositySolns.PerronFamily.mem {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper : Point n → ℝ} (w : PerronFamily C boundary F g lower upper) : PerronClass C boundary F g lower upper w.fun

theorem ViscositySolns.DirichletBarrierPair.perronFamily_nonempty {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) : Nonempty (PerronFamily C boundary F g B.lower B.upper)

The Perron family is nonempty because it contains the lower barrier.

theorem ViscositySolns.perronEnvelope_eq_pointwiseSup_perronFamily {n : ℕ} (C boundary : Set (Point n)) (F : Operator n) (g lower upper : Point n → ℝ) : perronEnvelope C boundary F g lower upper = pointwiseSup fun (w : PerronFamily C boundary F g lower upper) => w.fun

The pointwise Perron envelope is the indexed pointwise supremum over the subtype of Perron-class members.

theorem ViscositySolns.perronFamily_eventually_viscositySubsolution {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g lower upper : Point n → ℝ} {l : Filter (PerronFamily C boundary F g lower upper)} : ∀ᶠ (w : PerronFamily C boundary F g lower upper) in l, ViscositySubsolution C F w.fun

theorem ViscositySolns.DirichletBarrierPair.perronFamily_pointwise_bddAbove_eventually {n : ℕ} {C boundary : Set (Point n)} {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {x : Point n} : ∀ᶠ (y : Point n) in nhdsWithin x C, BddAbove {r : ℝ | ∃ (w : PerronFamily C boundary F g B.lower B.upper), r = w.fun y}

The upper barrier pointwise-bounds the Perron-family values near every point of C, hence the family supremum is pointwise bounded above there.

theorem ViscositySolns.DirichletBarrierPair.perronFamily_halfRelaxed_isBoundedUnder_le_top {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) (halfRelaxedFilter ⊤ C x) (halfRelaxedValue fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun)

Local upper-barrier boundedness bounds the Perron-family half-relaxed values above.

theorem ViscositySolns.DirichletBarrierPair.perronFamily_halfRelaxed_isBoundedUnder_ge_top {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) (halfRelaxedFilter ⊤ C x) (halfRelaxedValue fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun)

Local lower-barrier boundedness bounds the Perron-family half-relaxed values below.

theorem ViscositySolns.DirichletBarrierPair.pointwiseSup_perronFamily_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) (pointwiseSup fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun)

The Perron-family pointwise supremum has the same local upper bound as the upper barrier.

theorem ViscositySolns.DirichletBarrierPair.pointwiseSup_perronFamily_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) (pointwiseSup fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun)

The Perron-family pointwise supremum has the same local lower bound as the lower barrier.

theorem ViscositySolns.DirichletBarrierPair.upperEnvelope_perronEnvelope_eq_upperHalfRelaxedLimit_top {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) (hupper : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hlower : Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) : upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper) x = upperHalfRelaxedLimit (fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun) ⊤ C x

The Perron upper envelope is the upper half-relaxed limit of the Perron family with the top filter on the Perron class.

theorem ViscositySolns.ViscositySubsolution.upperEnvelope_of_eq_upperHalfRelaxedLimit {n : ℕ} {ι : Type u_1} {C : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {w : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} (hF : OperatorContinuous F) (hsub : ∀ᶠ (i : ι) in l, ViscositySubsolution C F (uᵢ i)) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddBelow : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hEq : upperEnvelope C w = ViscositySolns.upperHalfRelaxedLimit uᵢ l C) : ViscositySubsolution C F (upperEnvelope C w)

Supremum stability in the form consumed by Perron's method.

If the upper envelope of a candidate w is identified with an upper half-relaxed limit of eventually subsolution approximants, then the envelope is a viscosity subsolution. The separate equality hypothesis lets later Perron code choose whatever enumeration/selection of the Perron family is most convenient.

theorem ViscositySolns.DirichletBarrierPair.perronUpperEnvelope_viscositySubsolution {n : ℕ} {ι : Type u_1} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {uᵢ : ι → Point n → ℝ} {l : Filter ι} (hF : OperatorContinuous F) (hsub : ∀ᶠ (i : ι) in l, ViscositySubsolution C F (uᵢ i)) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddBelow : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hEq : upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper) = upperHalfRelaxedLimit uᵢ l C) : ViscositySubsolution C F (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

The same stability adapter specialized to the Perron envelope. The substantive selection work is isolated in the equality with an upper half-relaxed limit; once that representation is available, the viscosity inequality is supplied by the existing stability theorem.

theorem ViscositySolns.DirichletBarrierPair.perronUpperEnvelope_viscositySubsolution_of_perronFamily {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {l : Filter (PerronFamily C boundary F g B.lower B.upper)} (hF : OperatorContinuous F) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun)) (hcobddBelow : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun)) (hEq : upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper) = upperHalfRelaxedLimit (fun (w : PerronFamily C boundary F g B.lower B.upper) => w.fun) l C) : ViscositySubsolution C F (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron upper-envelope stability specialized to the Perron family as the approximating index type. The eventual subsolution hypothesis is automatic from membership in the Perron class.

theorem ViscositySolns.DirichletBarrierPair.perronUpperEnvelope_viscositySubsolution_of_perronFamily_top {n : ℕ} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) (hF : OperatorContinuous F) (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) : ViscositySubsolution C F (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Perron upper-envelope stability using the Perron family itself, indexed by the top filter. This removes the need for callers to provide a separate half-relaxed-limit representation of the Perron envelope on C.

theorem ViscositySolns.DirichletBarrierPair.perronUpperEnvelope_dirichletSubsolution {n : ℕ} {ι : Type u_1} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {uᵢ : ι → Point n → ℝ} {l : Filter ι} (hF : OperatorContinuous F) (hsub : ∀ᶠ (i : ι) in l, ViscositySubsolution C F (uᵢ i)) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddBelow : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hEq : upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper) = upperHalfRelaxedLimit uᵢ l C) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hperronCobddBelowOnBoundary : ∀ x ∈ boundary, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) (perronEnvelope C boundary F g B.lower B.upper)) (hupperBddAboveOnBoundary : ∀ x ∈ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hupperSemi : UpperSemicontinuousOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (C ∪ boundary)) : DirichletSubsolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet version of Perron upper-envelope stability.

The viscosity subsolution property comes from the half-relaxed-limit representation, while the boundary inequality is inherited from the upper barrier trace.

theorem ViscositySolns.DirichletBarrierPair.perronUpperEnvelope_dirichletSubsolution_of_barrierLocalBounded {n : ℕ} {ι : Type u_1} {C boundary : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {g : Point n → ℝ} (B : DirichletBarrierPair C boundary F g) {uᵢ : ι → Point n → ℝ} {l : Filter ι} (hF : OperatorContinuous F) (hsub : ∀ᶠ (i : ι) in l, ViscositySubsolution C F (uᵢ i)) (hbddAbove : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddBelow : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hEq : upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper) = upperHalfRelaxedLimit uᵢ l C) (hupperTrace : BoundaryUpperTraceOn C boundary g B.upper) (hneBoundary : ∀ x ∈ boundary, (nhdsWithin x C).NeBot) (hlowerBddBelowOnBoundary : ∀ x ∈ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (nhdsWithin x C) B.lower) (hupperBddAboveOnBoundary : ∀ x ∈ boundary, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (nhdsWithin x C) B.upper) (hupperSemi : UpperSemicontinuousOn (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper)) (C ∪ boundary)) : DirichletSubsolutionOn C boundary F g (upperEnvelope C (perronEnvelope C boundary F g B.lower B.upper))

Dirichlet Perron upper-envelope stability with boundary coboundedness inherited from the lower barrier.