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

Abstract stability through tail-closed semijet graphs

This file isolates the closed-graph argument used in stability theorems. The analytic content of locally uniform convergence is separated into an approximation hypothesis saying that semijets of the limit lie in the tail closure of semijet graphs of the approximating functions.

def ViscositySolns.TailClosureSuperjetGraph {n : ℕ} {ι : Type u_1} (C : Set (Point n)) (uᵢ : ι → Point n → ℝ) (l : Filter ι) : Set ((Point n × ℝ) × Jet n)

Tail closure of the superjet graphs of a family uᵢ along a filter l.

A point z belongs to this set if, for every set of indices A with A ∈ l, the point z belongs to the closure of ⋃ i ∈ A, SuperjetGraph C (uᵢ i).

Equations

• ViscositySolns.TailClosureSuperjetGraph C uᵢ l = {z : (ViscositySolns.Point n × ℝ) × ViscositySolns.Jet n | ∀ A ∈ l, z ∈ closure (⋃ i ∈ A, ViscositySolns.SuperjetGraph C (uᵢ i))}

def ViscositySolns.TailClosureSubjetGraph {n : ℕ} {ι : Type u_1} (C : Set (Point n)) (uᵢ : ι → Point n → ℝ) (l : Filter ι) : Set ((Point n × ℝ) × Jet n)

Tail closure of the subjet graphs of a family uᵢ along a filter l.

Equations

• ViscositySolns.TailClosureSubjetGraph C uᵢ l = {z : (ViscositySolns.Point n × ℝ) × ViscositySolns.Jet n | ∀ A ∈ l, z ∈ closure (⋃ i ∈ A, ViscositySolns.SubjetGraph C (uᵢ i))}

theorem ViscositySolns.tailClosureSuperjetGraph_of_forall_nhds_exists {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {z : (Point n × ℝ) × Jet n} (h : ∀ A ∈ l, ∀ W ∈ nhds z, ∃ w ∈ W, w ∈ ⋃ i ∈ A, SuperjetGraph C (uᵢ i)) : z ∈ TailClosureSuperjetGraph C uᵢ l

Neighborhood criterion for tail closure of superjet graphs.

If, for every set of indices A with A ∈ l, every neighborhood of z contains a point of ⋃ i ∈ A, SuperjetGraph C (uᵢ i), then z belongs to TailClosureSuperjetGraph C uᵢ l.

theorem ViscositySolns.tailClosureSubjetGraph_of_forall_nhds_exists {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {z : (Point n × ℝ) × Jet n} (h : ∀ A ∈ l, ∀ W ∈ nhds z, ∃ w ∈ W, w ∈ ⋃ i ∈ A, SubjetGraph C (uᵢ i)) : z ∈ TailClosureSubjetGraph C uᵢ l

Neighborhood criterion for tail closure of subjet graphs.

If, for every set of indices A with A ∈ l, every neighborhood of z contains a point of ⋃ i ∈ A, SubjetGraph C (uᵢ i), then z belongs to TailClosureSubjetGraph C uᵢ l.

theorem ViscositySolns.tailClosureSuperjetGraph_of_forall_nhds_exists_components {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {x : Point n} {r : ℝ} {J : Jet n} (h : ∀ A ∈ l, ∀ W ∈ nhds ((x, r), J), ∃ i ∈ A, ∃ (y : Point n) (s : ℝ) (J' : Jet n), ((y, s), J') ∈ SuperjetGraph C (uᵢ i) ∧ ((y, s), J') ∈ W) : ((x, r), J) ∈ TailClosureSuperjetGraph C uᵢ l

Componentwise neighborhood criterion for tail closure of superjet graphs.

If every neighborhood of ((x, r), J) contains a graph point ((y, s), J') ∈ SuperjetGraph C (uᵢ i) with i ∈ A, for every set of indices A satisfying A ∈ l, then ((x, r), J) belongs to the tail closure.

theorem ViscositySolns.tailClosureSubjetGraph_of_forall_nhds_exists_components {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {x : Point n} {r : ℝ} {J : Jet n} (h : ∀ A ∈ l, ∀ W ∈ nhds ((x, r), J), ∃ i ∈ A, ∃ (y : Point n) (s : ℝ) (J' : Jet n), ((y, s), J') ∈ SubjetGraph C (uᵢ i) ∧ ((y, s), J') ∈ W) : ((x, r), J) ∈ TailClosureSubjetGraph C uᵢ l

Componentwise neighborhood criterion for tail closure of subjet graphs.

If every neighborhood of ((x, r), J) contains a graph point ((y, s), J') ∈ SubjetGraph C (uᵢ i) with i ∈ A, for every set of indices A satisfying A ∈ l, then ((x, r), J) belongs to the tail closure.

theorem ViscositySolns.isClosed_tailClosureSuperjetGraph {n : ℕ} {ι : Type u_1} (C : Set (Point n)) (uᵢ : ι → Point n → ℝ) (l : Filter ι) : IsClosed (TailClosureSuperjetGraph C uᵢ l)

Tail closures of superjet graphs are closed sets.

theorem ViscositySolns.isClosed_tailClosureSubjetGraph {n : ℕ} {ι : Type u_1} (C : Set (Point n)) (uᵢ : ι → Point n → ℝ) (l : Filter ι) : IsClosed (TailClosureSubjetGraph C uᵢ l)

Tail closures of subjet graphs are closed sets.

theorem ViscositySolns.tailClosureSuperjetGraph_of_tendsto_tailClosureSuperjetGraph {n : ℕ} {ι : Type u_1} {α : Type u_2} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {m : Filter α} [m.NeBot] {z : (Point n × ℝ) × Jet n} {zα : α → (Point n × ℝ) × Jet n} (hz : Filter.Tendsto zα m (nhds z)) (hmem : ∀ᶠ (a : α) in m, zα a ∈ TailClosureSuperjetGraph C uᵢ l) : z ∈ TailClosureSuperjetGraph C uᵢ l

A limit of tail-closed superjet graph points is tail-closed.

theorem ViscositySolns.tailClosureSubjetGraph_of_tendsto_tailClosureSubjetGraph {n : ℕ} {ι : Type u_1} {α : Type u_2} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {m : Filter α} [m.NeBot] {z : (Point n × ℝ) × Jet n} {zα : α → (Point n × ℝ) × Jet n} (hz : Filter.Tendsto zα m (nhds z)) (hmem : ∀ᶠ (a : α) in m, zα a ∈ TailClosureSubjetGraph C uᵢ l) : z ∈ TailClosureSubjetGraph C uᵢ l

A limit of tail-closed subjet graph points is tail-closed.

theorem ViscositySolns.tailClosureSuperjetGraph_of_nat_hessian_add_identity {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {x p : Point n} {r : ℝ} {X : Hessian n} (hmem : ∀ (k : ℕ), ((x, r), { gradient := p, hessian := X + (1 / (↑k + 1)) • 1 }) ∈ TailClosureSuperjetGraph C uᵢ l) : ((x, r), { gradient := p, hessian := X }) ∈ TailClosureSuperjetGraph C uᵢ l

If every positive identity-matrix perturbation along the sequence 1 / (k + 1) lies in the tail closure of the superjet graphs, then the unperturbed jet lies in the same tail closure.

theorem ViscositySolns.tailClosureSubjetGraph_of_nat_hessian_sub_identity {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {x p : Point n} {r : ℝ} {X : Hessian n} (hmem : ∀ (k : ℕ), ((x, r), { gradient := p, hessian := X - (1 / (↑k + 1)) • 1 }) ∈ TailClosureSubjetGraph C uᵢ l) : ((x, r), { gradient := p, hessian := X }) ∈ TailClosureSubjetGraph C uᵢ l

If every negative identity-matrix perturbation along the sequence 1 / (k + 1) lies in the tail closure of the subjet graphs, then the unperturbed jet lies in the same tail closure.

theorem ViscositySolns.tailClosureSuperjetGraph_of_tendsto_superjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {z : (Point n × ℝ) × Jet n} {zᵢ : ι → (Point n × ℝ) × Jet n} (hz : Filter.Tendsto zᵢ l (nhds z)) (hgraph : ∀ᶠ (i : ι) in l, zᵢ i ∈ SuperjetGraph C (uᵢ i)) : z ∈ TailClosureSuperjetGraph C uᵢ l

A convergent net of approximating superjet graph points gives a point in the tail closure of the approximating superjet graphs.

theorem ViscositySolns.tailClosureSubjetGraph_of_tendsto_subjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {z : (Point n × ℝ) × Jet n} {zᵢ : ι → (Point n × ℝ) × Jet n} (hz : Filter.Tendsto zᵢ l (nhds z)) (hgraph : ∀ᶠ (i : ι) in l, zᵢ i ∈ SubjetGraph C (uᵢ i)) : z ∈ TailClosureSubjetGraph C uᵢ l

A convergent net of approximating subjet graph points gives a point in the tail closure of the approximating subjet graphs.

theorem ViscositySolns.tailClosureSuperjetGraph_of_tendsto_superjetGraph_components {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {r : ℝ} {J : Jet n} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hx : Filter.Tendsto xᵢ l (nhds x)) (hr : Filter.Tendsto rᵢ l (nhds r)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph C (uᵢ i)) : ((x, r), J) ∈ TailClosureSuperjetGraph C uᵢ l

Componentwise convergence of selected approximating superjet graph triples gives tail-closure membership.

theorem ViscositySolns.tailClosureSubjetGraph_of_tendsto_subjetGraph_components {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {r : ℝ} {J : Jet n} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hx : Filter.Tendsto xᵢ l (nhds x)) (hr : Filter.Tendsto rᵢ l (nhds r)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph C (uᵢ i)) : ((x, r), J) ∈ TailClosureSubjetGraph C uᵢ l

Componentwise convergence of selected approximating subjet graph triples gives tail-closure membership.

theorem ViscositySolns.eventually_superjetGraph_of_eventually_superjetGraph_of_nhdsWithin_eq {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph K (uᵢ i)) (hnhds : ∀ᶠ (i : ι) in l, nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C) : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph C (uᵢ i)

Let K ⊆ C. If the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph K (uᵢ i) belongs to l, and the set of indices i for which nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C belongs to l, then the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph C (uᵢ i) belongs to l.

theorem ViscositySolns.eventually_subjetGraph_of_eventually_subjetGraph_of_nhdsWithin_eq {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph K (uᵢ i)) (hnhds : ∀ᶠ (i : ι) in l, nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C) : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph C (uᵢ i)

Let K ⊆ C. If the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph K (uᵢ i) belongs to l, and the set of indices i for which nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C belongs to l, then the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph C (uᵢ i) belongs to l.

theorem ViscositySolns.eventually_superjetGraph_of_eventually_superjetGraph_of_mem_nhdsWithin {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph K (uᵢ i)) (hKnhds : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C) : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph C (uᵢ i)

Let K ⊆ C. If the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph K (uᵢ i) belongs to l, and the set of indices i for which K ∈ nhdsWithin (xᵢ i) C belongs to l, then the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph C (uᵢ i) belongs to l.

theorem ViscositySolns.eventually_subjetGraph_of_eventually_subjetGraph_of_mem_nhdsWithin {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph K (uᵢ i)) (hKnhds : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C) : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph C (uᵢ i)

Let K ⊆ C. If the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph K (uᵢ i) belongs to l, and the set of indices i for which K ∈ nhdsWithin (xᵢ i) C belongs to l, then the set of indices i for which ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph C (uᵢ i) belongs to l.

theorem ViscositySolns.tailClosureSuperjetGraph_of_tendsto_superjetGraph_nhdsWithin_eq {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {r : ℝ} {J : Jet n} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hx : Filter.Tendsto xᵢ l (nhds x)) (hr : Filter.Tendsto rᵢ l (nhds r)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph K (uᵢ i)) (hnhds : ∀ᶠ (i : ι) in l, nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C) : ((x, r), J) ∈ TailClosureSuperjetGraph C uᵢ l

Selected convergent superjet graph triples on a local domain K give a tail-closure point for the ambient domain C, assuming that the set of indices i for which nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C belongs to l.

theorem ViscositySolns.tailClosureSubjetGraph_of_tendsto_subjetGraph_nhdsWithin_eq {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {r : ℝ} {J : Jet n} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hx : Filter.Tendsto xᵢ l (nhds x)) (hr : Filter.Tendsto rᵢ l (nhds r)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph K (uᵢ i)) (hnhds : ∀ᶠ (i : ι) in l, nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C) : ((x, r), J) ∈ TailClosureSubjetGraph C uᵢ l

Selected convergent subjet graph triples on a local domain K give a tail-closure point for the ambient domain C, assuming that the set of indices i for which nhdsWithin (xᵢ i) K = nhdsWithin (xᵢ i) C belongs to l.

theorem ViscositySolns.tailClosureSuperjetGraph_of_tendsto_superjetGraph_mem_nhdsWithin {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {r : ℝ} {J : Jet n} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hx : Filter.Tendsto xᵢ l (nhds x)) (hr : Filter.Tendsto rᵢ l (nhds r)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SuperjetGraph K (uᵢ i)) (hKnhds : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C) : ((x, r), J) ∈ TailClosureSuperjetGraph C uᵢ l

Selected convergent superjet graph triples on a local domain K give a tail-closure point for the ambient domain C when the set of indices i for which K ∈ nhdsWithin (xᵢ i) C belongs to l.

theorem ViscositySolns.tailClosureSubjetGraph_of_tendsto_subjetGraph_mem_nhdsWithin {n : ℕ} {ι : Type u_1} {K C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] {x : Point n} {r : ℝ} {J : Jet n} {xᵢ : ι → Point n} {rᵢ : ι → ℝ} {Jᵢ : ι → Jet n} (hKC : K ⊆ C) (hx : Filter.Tendsto xᵢ l (nhds x)) (hr : Filter.Tendsto rᵢ l (nhds r)) (hJ : Filter.Tendsto Jᵢ l (nhds J)) (hgraph : ∀ᶠ (i : ι) in l, ((xᵢ i, rᵢ i), Jᵢ i) ∈ SubjetGraph K (uᵢ i)) (hKnhds : ∀ᶠ (i : ι) in l, K ∈ nhdsWithin (xᵢ i) C) : ((x, r), J) ∈ TailClosureSubjetGraph C uᵢ l

Selected convergent subjet graph triples on a local domain K give a tail-closure point for the ambient domain C when the set of indices i for which K ∈ nhdsWithin (xᵢ i) C belongs to l.

theorem ViscositySolns.superjetGraph_subset_tailClosureSuperjetGraph_of_eventually_eqOn {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] (heq : ∀ᶠ (i : ι) in l, Set.EqOn (uᵢ i) u C) : SuperjetGraph C u ⊆ TailClosureSuperjetGraph C uᵢ l

If the set of indices i for which uᵢ i agrees with u on C belongs to l, then every superjet graph point of u belongs to the tail closure of the approximating superjet graphs.

theorem ViscositySolns.subjetGraph_subset_tailClosureSubjetGraph_of_eventually_eqOn {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] (heq : ∀ᶠ (i : ι) in l, Set.EqOn (uᵢ i) u C) : SubjetGraph C u ⊆ TailClosureSubjetGraph C uᵢ l

If the set of indices i for which uᵢ i agrees with u on C belongs to l, then every subjet graph point of u belongs to the tail closure of the approximating subjet graphs.

theorem ViscositySolns.tailClosureSuperjetGraph_induction {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {z : (Point n × ℝ) × Jet n} {S : Set ((Point n × ℝ) × Jet n)} (hclosed : IsClosed S) (hgraph : ∀ᶠ (i : ι) in l, ∀ y ∈ C, ∀ K ∈ Superjet C (uᵢ i) y, ((y, uᵢ i y), K) ∈ S) (hz : z ∈ TailClosureSuperjetGraph C uᵢ l) : z ∈ S

theorem ViscositySolns.tailClosureSubjetGraph_induction {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {z : (Point n × ℝ) × Jet n} {S : Set ((Point n × ℝ) × Jet n)} (hclosed : IsClosed S) (hgraph : ∀ᶠ (i : ι) in l, ∀ y ∈ C, ∀ K ∈ Subjet C (uᵢ i) y, ((y, uᵢ i y), K) ∈ S) (hz : z ∈ TailClosureSubjetGraph C uᵢ l) : z ∈ S

theorem ViscositySolns.ViscositySubsolution.of_eventually_tailClosureSuperjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} (husc : UpperSemicontinuousOn u C) (hF : OperatorContinuous F) (hsub : ∀ᶠ (i : ι) in l, ViscositySubsolution C F (uᵢ i)) (happrox : ∀ x ∈ C, ∀ J ∈ Superjet C u x, ((x, u x), J) ∈ TailClosureSuperjetGraph C uᵢ l) : ViscositySubsolution C F u

Abstract stability criterion for subsolutions. If every superjet of the limit is in the tail closure of the approximating superjet graphs, then eventual subsolutions pass to the limit for continuous operators.

theorem ViscositySolns.ViscositySupersolution.of_eventually_tailClosureSubjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} (hlsc : LowerSemicontinuousOn u C) (hF : OperatorContinuous F) (hsuper : ∀ᶠ (i : ι) in l, ViscositySupersolution C F (uᵢ i)) (happrox : ∀ x ∈ C, ∀ J ∈ Subjet C u x, ((x, u x), J) ∈ TailClosureSubjetGraph C uᵢ l) : ViscositySupersolution C F u

Abstract stability criterion for supersolutions. If every subjet of the limit is in the tail closure of the approximating subjet graphs, then eventual supersolutions pass to the limit for continuous operators.

theorem ViscositySolns.le_of_eventually_viscositySubsolution_tailClosureSuperjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {x : Point n} {J : Jet n} (hF : OperatorContinuous F) (hsub : ∀ᶠ (i : ι) in l, ViscositySubsolution C F (uᵢ i)) (hz : ((x, u x), J) ∈ TailClosureSuperjetGraph C uᵢ l) : F x (u x) J.gradient J.hessian ≤ 0

Pointwise closed-graph consequence for subsolutions. If the set of indices i for which uᵢ i is a viscosity subsolution belongs to l, then any tail-closure point of the approximating superjet graphs satisfies the limiting operator inequality.

theorem ViscositySolns.nonneg_of_eventually_viscositySupersolution_tailClosureSubjetGraph {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {x : Point n} {J : Jet n} (hF : OperatorContinuous F) (hsuper : ∀ᶠ (i : ι) in l, ViscositySupersolution C F (uᵢ i)) (hz : ((x, u x), J) ∈ TailClosureSubjetGraph C uᵢ l) : 0 ≤ F x (u x) J.gradient J.hessian

Pointwise closed-graph consequence for supersolutions. If the set of indices i for which uᵢ i is a viscosity supersolution belongs to l, then any tail-closure point of the approximating subjet graphs satisfies the limiting operator inequality.

theorem ViscositySolns.ViscositySubsolution.of_eventually_eqOn {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] (husc : UpperSemicontinuousOn u C) (hF : OperatorContinuous F) (hsub : ∀ᶠ (i : ι) in l, ViscositySubsolution C F (uᵢ i)) (heq : ∀ᶠ (i : ι) in l, Set.EqOn (uᵢ i) u C) : ViscositySubsolution C F u

If the set of indices i for which uᵢ i agrees with u on C belongs to l, then the tail-closure approximation hypothesis holds. Consequently, if the set of indices i for which uᵢ i is a subsolution belongs to l, then u is a subsolution.

theorem ViscositySolns.ViscositySupersolution.of_eventually_eqOn {n : ℕ} {ι : Type u_1} {C : Set (Point n)} {F : Operator n} {u : Point n → ℝ} {uᵢ : ι → Point n → ℝ} {l : Filter ι} [l.NeBot] (hlsc : LowerSemicontinuousOn u C) (hF : OperatorContinuous F) (hsuper : ∀ᶠ (i : ι) in l, ViscositySupersolution C F (uᵢ i)) (heq : ∀ᶠ (i : ι) in l, Set.EqOn (uᵢ i) u C) : ViscositySupersolution C F u

If the set of indices i for which uᵢ i agrees with u on C belongs to l, then the tail-closure approximation hypothesis holds. Consequently, if the set of indices i for which uᵢ i is a supersolution belongs to l, then u is a supersolution.