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

Semijet approximation for half-relaxed limits

This file proves that ordinary semijets of half-relaxed limits belong to the tail closures of the approximating semijet graphs.

theorem ViscositySolns.tailClosureSuperjetGraph_upperHalfRelaxedLimit_of_strictContact {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {JAt : Point n → Jet n} (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddAbove : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddBelow : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (hJAt : ContinuousWithinAt JAt K x) (hφexp : ∀ y ∈ K, HasSecondOrderExpansionWithin K φ y (JAt y)) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → upperHalfRelaxedLimit uᵢ l C y - φ y ≤ upperHalfRelaxedLimit uᵢ l C x - φ x - δ) : ((x, upperHalfRelaxedLimit uᵢ l C x), JAt x) ∈ TailClosureSuperjetGraph C uᵢ l

If the hypotheses in exists_isMaxOn_hasSecondOrderExpansionWithin_mem_nhds_upperHalfRelaxedLimit hold for every set of indices A with A ∈ l and every neighborhood of ((x, upperHalfRelaxedLimit uᵢ l C x), JAt x), then that graph point belongs to TailClosureSuperjetGraph C uᵢ l.

theorem ViscositySolns.tailClosureSubjetGraph_lowerHalfRelaxedLimit_of_strictContact {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {φ : Point n → ℝ} {JAt : Point n → Jet n} (hxC : x ∈ C) (hKne : K.Nonempty) (hKcompact : IsCompact K) (hKC : K ⊆ C) (hKnhds : K ∈ nhdsWithin x C) (hbddBelow : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddAbove : Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C x) (halfRelaxedValue uᵢ)) (hφC : ContinuousOn φ C) (hφK : ContinuousOn φ K) (hJAt : ContinuousWithinAt JAt K x) (hφexp : ∀ y ∈ K, HasSecondOrderExpansionWithin K φ y (JAt y)) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) K) (hstrict : ∀ V ∈ nhds x, ∃ δ > 0, ∀ y ∈ K, y ∉ V → lowerHalfRelaxedLimit uᵢ l C x - φ x + δ ≤ lowerHalfRelaxedLimit uᵢ l C y - φ y) : ((x, lowerHalfRelaxedLimit uᵢ l C x), JAt x) ∈ TailClosureSubjetGraph C uᵢ l

If the hypotheses in exists_isMinOn_hasSecondOrderExpansionWithin_mem_nhds_lowerHalfRelaxedLimit hold for every set of indices A with A ∈ l and every neighborhood of ((x, lowerHalfRelaxedLimit uᵢ l C x), JAt x), then that graph point belongs to TailClosureSubjetGraph C uᵢ l.

theorem ViscositySolns.tailClosureSuperjetGraph_upperHalfRelaxedLimit_superjet_hessian_add_identity {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} [LocallyCompactSpace ↑C] {x : Point n} {J : Jet n} {δ : ℝ} (hxC : x ∈ C) (hbddAbove : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddBelow : ∀ y ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) C) (hδ : 0 < δ) (hJ : J ∈ Superjet C (upperHalfRelaxedLimit uᵢ l C) x) : ((x, upperHalfRelaxedLimit uᵢ l C x), { gradient := J.gradient, hessian := J.hessian + δ • 1 }) ∈ TailClosureSuperjetGraph C uᵢ l

Let upperLimit x = upperHalfRelaxedLimit uᵢ l C x. If J ∈ Superjet C upperLimit x and δ > 0, then the graph point with the same value and gradient as J and Hessian J.hessian + δ I belongs to TailClosureSuperjetGraph C uᵢ l.

The proof uses the superjet inequality with Hessian J.hessian + (δ / 2) I to obtain a compact set K ⊆ C on which the quadratic polynomial with Hessian J.hessian + δ I has strict maximum contact with upperLimit at x.

theorem ViscositySolns.tailClosureSubjetGraph_lowerHalfRelaxedLimit_subjet_hessian_sub_identity {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} [LocallyCompactSpace ↑C] {x : Point n} {J : Jet n} {δ : ℝ} (hxC : x ∈ C) (hbddBelow : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddAbove : ∀ y ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) C) (hδ : 0 < δ) (hJ : J ∈ Subjet C (lowerHalfRelaxedLimit uᵢ l C) x) : ((x, lowerHalfRelaxedLimit uᵢ l C x), { gradient := J.gradient, hessian := J.hessian - δ • 1 }) ∈ TailClosureSubjetGraph C uᵢ l

Let lowerLimit x = lowerHalfRelaxedLimit uᵢ l C x. If J ∈ Subjet C lowerLimit x and δ > 0, then the graph point with the same value and gradient as J and Hessian J.hessian - δ I belongs to TailClosureSubjetGraph C uᵢ l.

The proof uses the subjet inequality with Hessian J.hessian - (δ / 2) I to obtain a compact set K ⊆ C on which the quadratic polynomial with Hessian J.hessian - δ I has strict minimum contact with lowerLimit at x.

theorem ViscositySolns.tailClosureSuperjetGraph_upperHalfRelaxedLimit_superjet {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} [LocallyCompactSpace ↑C] {x : Point n} {J : Jet n} (hxC : x ∈ C) (hbddAbove : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddBelow : ∀ y ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≤ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (husc : ∀ᶠ (i : ι) in l, UpperSemicontinuousOn (uᵢ i) C) (hJ : J ∈ Superjet C (upperHalfRelaxedLimit uᵢ l C) x) : ((x, upperHalfRelaxedLimit uᵢ l C x), J) ∈ TailClosureSuperjetGraph C uᵢ l

Let upperLimit x = upperHalfRelaxedLimit uᵢ l C x. If J ∈ Superjet C upperLimit x, then ((x, upperLimit x), J) belongs to TailClosureSuperjetGraph C uᵢ l.

theorem ViscositySolns.tailClosureSubjetGraph_lowerHalfRelaxedLimit_subjet {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C : Set (Point n)} [LocallyCompactSpace ↑C] {x : Point n} {J : Jet n} (hxC : x ∈ C) (hbddBelow : ∀ y ∈ C, Filter.IsBoundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hcobddAbove : ∀ y ∈ C, Filter.IsCoboundedUnder (fun (x1 x2 : ℝ) => x1 ≥ x2) (halfRelaxedFilter l C y) (halfRelaxedValue uᵢ)) (hlsc : ∀ᶠ (i : ι) in l, LowerSemicontinuousOn (uᵢ i) C) (hJ : J ∈ Subjet C (lowerHalfRelaxedLimit uᵢ l C) x) : ((x, lowerHalfRelaxedLimit uᵢ l C x), J) ∈ TailClosureSubjetGraph C uᵢ l

Let lowerLimit x = lowerHalfRelaxedLimit uᵢ l C x. If J ∈ Subjet C lowerLimit x, then ((x, lowerLimit x), J) belongs to TailClosureSubjetGraph C uᵢ l.

theorem ViscositySolns.tailClosureSuperjetGraph_upperHalfRelaxedLimit_of_forall_nhds_exists_isMaxOn {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {J : Jet n} {φ : Point n → ℝ} (hKC : K ⊆ C) (h : ∀ A ∈ l, ∀ W ∈ nhds ((x, upperHalfRelaxedLimit uᵢ l C x), J), ∃ i ∈ A, ∃ z ∈ K, ∃ (Jᵢ : Jet n), K ∈ nhdsWithin z C ∧ IsMaxOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ HasSecondOrderExpansionWithin K φ z Jᵢ ∧ ((z, uᵢ i z), Jᵢ) ∈ W) : ((x, upperHalfRelaxedLimit uᵢ l C x), J) ∈ TailClosureSuperjetGraph C uᵢ l

Compact-contact neighborhood criterion for half-relaxed superjet approximation.

Let upperLimit x = upperHalfRelaxedLimit uᵢ l C x. Suppose that for every set of indices A with A ∈ l and every neighborhood W of ((x, upperLimit x), J), there exist i ∈ A, z ∈ K, and a jet Jᵢ such that K is a relative neighborhood of z in C, z is a maximum point of uᵢ i - φ on K, φ has second-order expansion Jᵢ at z within K, and ((z, uᵢ i z), Jᵢ) ∈ W. Then ((x, upperLimit x), J) belongs to the tail closure of the approximating superjet graphs on C.

theorem ViscositySolns.tailClosureSubjetGraph_lowerHalfRelaxedLimit_of_forall_nhds_exists_isMinOn {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} {x : Point n} {J : Jet n} {φ : Point n → ℝ} (hKC : K ⊆ C) (h : ∀ A ∈ l, ∀ W ∈ nhds ((x, lowerHalfRelaxedLimit uᵢ l C x), J), ∃ i ∈ A, ∃ z ∈ K, ∃ (Jᵢ : Jet n), K ∈ nhdsWithin z C ∧ IsMinOn (fun (y : Point n) => uᵢ i y - φ y) K z ∧ HasSecondOrderExpansionWithin K φ z Jᵢ ∧ ((z, uᵢ i z), Jᵢ) ∈ W) : ((x, lowerHalfRelaxedLimit uᵢ l C x), J) ∈ TailClosureSubjetGraph C uᵢ l

Compact-contact neighborhood criterion for half-relaxed subjet approximation.

Let lowerLimit x = lowerHalfRelaxedLimit uᵢ l C x. Suppose that for every set of indices A with A ∈ l and every neighborhood W of ((x, lowerLimit x), J), there exist i ∈ A, z ∈ K, and a jet Jᵢ such that K is a relative neighborhood of z in C, z is a minimum point of uᵢ i - φ on K, φ has second-order expansion Jᵢ at z within K, and ((z, uᵢ i z), Jᵢ) ∈ W. Then ((x, lowerLimit x), J) belongs to the tail closure of the approximating subjet graphs on C.