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

Half-relaxed stability theorems

This file contains the main viscosity stability theorems for upper and lower half-relaxed limits.

The main declarations are ViscositySubsolution.upperHalfRelaxedLimit and ViscositySupersolution.lowerHalfRelaxedLimit.

theorem ViscositySolns.ViscositySubsolution.upperHalfRelaxedLimit_of_eventually_tailClosureSuperjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator 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ᵢ)) (happrox : ∀ x ∈ C, ∀ J ∈ Superjet C (ViscositySolns.upperHalfRelaxedLimit uᵢ l C) x, ((x, ViscositySolns.upperHalfRelaxedLimit uᵢ l C x), J) ∈ TailClosureSuperjetGraph C uᵢ l) : ViscositySubsolution C F (ViscositySolns.upperHalfRelaxedLimit uᵢ l C)

Abstract half-relaxed stability for subsolutions.

Let upperLimit x = upperHalfRelaxedLimit uᵢ l C x. If the set of indices i for which uᵢ i is a viscosity subsolution of F = 0 on C belongs to l, and if for every x ∈ C and every J ∈ Superjet C upperLimit x the graph point ((x, upperLimit x), J) belongs to TailClosureSuperjetGraph C uᵢ l, then upperLimit is a viscosity subsolution of F = 0 on C. The other hypotheses are the operator continuity and boundedness assumptions used to prove upper semicontinuity of upperLimit.

theorem ViscositySolns.ViscositySupersolution.lowerHalfRelaxedLimit_of_eventually_tailClosureSubjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator n} {uᵢ : ι → Point n → ℝ} {l : Filter ι} (hF : OperatorContinuous F) (hsuper : ∀ᶠ (i : ι) in l, ViscositySupersolution C F (uᵢ i)) (hbddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddAbove : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (happrox : ∀ x ∈ C, ∀ J ∈ Subjet C (ViscositySolns.lowerHalfRelaxedLimit uᵢ l C) x, ((x, ViscositySolns.lowerHalfRelaxedLimit uᵢ l C x), J) ∈ TailClosureSubjetGraph C uᵢ l) : ViscositySupersolution C F (ViscositySolns.lowerHalfRelaxedLimit uᵢ l C)

Abstract half-relaxed stability for supersolutions.

Let lowerLimit x = lowerHalfRelaxedLimit uᵢ l C x. If the set of indices i for which uᵢ i is a viscosity supersolution of F = 0 on C belongs to l, and if for every x ∈ C and every J ∈ Subjet C lowerLimit x the graph point ((x, lowerLimit x), J) belongs to TailClosureSubjetGraph C uᵢ l, then lowerLimit is a viscosity supersolution of F = 0 on C. The other hypotheses are the operator continuity and boundedness assumptions used to prove lower semicontinuity of lowerLimit.

theorem ViscositySolns.ViscositySubsolution.upperHalfRelaxedLimit {n : ℕ} {ι : Type u_1} {C : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator 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ᵢ)) : ViscositySubsolution C F (ViscositySolns.upperHalfRelaxedLimit uᵢ l C)

Half-relaxed stability for subsolutions.

Let upperLimit x = upperHalfRelaxedLimit uᵢ l C x. If the set of indices i for which uᵢ i is a viscosity subsolution of F = 0 on C belongs to l, then upperLimit is a viscosity subsolution of F = 0 on C, under the operator continuity, local compactness, and boundedness hypotheses stated below.

theorem ViscositySolns.ViscositySupersolution.lowerHalfRelaxedLimit {n : ℕ} {ι : Type u_1} {C : Set (Point n)} [LocallyCompactSpace ↑C] {F : Operator n} {uᵢ : ι → Point n → ℝ} {l : Filter ι} (hF : OperatorContinuous F) (hsuper : ∀ᶠ (i : ι) in l, ViscositySupersolution C F (uᵢ i)) (hbddBelow : ∀ x ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hcobddAbove : ∀ x ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) : ViscositySupersolution C F (ViscositySolns.lowerHalfRelaxedLimit uᵢ l C)

Half-relaxed stability for supersolutions.

Let lowerLimit x = lowerHalfRelaxedLimit uᵢ l C x. If the set of indices i for which uᵢ i is a viscosity supersolution of F = 0 on C belongs to l, then lowerLimit is a viscosity supersolution of F = 0 on C, under the operator continuity, local compactness, and boundedness hypotheses stated below.

theorem ViscositySolns.upperHalfRelaxedLimit_eq_of_locallyUniform {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} [(halfRelaxedFilter l C x).NeBot] (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) : upperHalfRelaxedLimit uᵢ l C x = u x

Locally uniform convergence identifies the upper half-relaxed limit with the ordinary limit.

theorem ViscositySolns.lowerHalfRelaxedLimit_eq_of_locallyUniform {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} [(halfRelaxedFilter l C x).NeBot] (hlu : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hxC : x ∈ C) : lowerHalfRelaxedLimit uᵢ l C x = u x

Locally uniform convergence identifies the lower half-relaxed limit with the ordinary limit.