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

Locally uniform convergence infrastructure

This file packages mathlib's locally uniform convergence definitions and theorems in the concrete Point n -> Real setting used by the viscosity solution development.

@[reducible, inline]

abbrev ViscositySolns.LocallyUniformTendstoOn {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (u : Point n → ℝ) (l : Filter ι) (C : Set (Point n)) : Prop

Locally uniform convergence on a domain of functions Point n -> Real.

Equations

• ViscositySolns.LocallyUniformTendstoOn uᵢ u l C = TendstoLocallyUniformlyOn uᵢ u l C

@[reducible, inline]

abbrev ViscositySolns.UniformTendstoOn {n : ℕ} {ι : Type u_1} (uᵢ : ι → Point n → ℝ) (u : Point n → ℝ) (l : Filter ι) (C : Set (Point n)) : Prop

Uniform convergence on a domain of functions Point n -> Real.

Equations

• ViscositySolns.UniformTendstoOn uᵢ u l C = TendstoUniformlyOn uᵢ u l C

theorem ViscositySolns.locallyUniformTendstoOn_iff {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} : LocallyUniformTendstoOn uᵢ u l C ↔ ∀ ε > 0, ∀ x ∈ C, ∃ t ∈ nhdsWithin x C, ∀ᶠ (i : ι) in l, ∀ y ∈ t, dist (u y) (uᵢ i y) < ε

theorem ViscositySolns.uniformTendstoOn_iff {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} : UniformTendstoOn uᵢ u l C ↔ ∀ ε > 0, ∀ᶠ (i : ι) in l, ∀ x ∈ C, dist (u x) (uᵢ i x) < ε

theorem ViscositySolns.UniformTendstoOn.eventually_forall_abs_sub_lt {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} (h : UniformTendstoOn uᵢ u l C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ∀ x ∈ C, |uᵢ i x - u x| < ε

theorem ViscositySolns.UniformTendstoOn.eventually_forall_le_add {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} (h : UniformTendstoOn uᵢ u l C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ∀ x ∈ C, uᵢ i x ≤ u x + ε

theorem ViscositySolns.UniformTendstoOn.eventually_forall_sub_le {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} (h : UniformTendstoOn uᵢ u l C) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (i : ι) in l, ∀ x ∈ C, u x ≤ uᵢ i x + ε

theorem ViscositySolns.UniformTendstoOn.locallyUniformTendstoOn {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} (h : UniformTendstoOn uᵢ u l C) : LocallyUniformTendstoOn uᵢ u l C

theorem ViscositySolns.locallyUniformTendstoOn_mono {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C D : Set (Point n)} (h : LocallyUniformTendstoOn uᵢ u l C) (hDC : D ⊆ C) : LocallyUniformTendstoOn uᵢ u l D

theorem ViscositySolns.locallyUniformTendstoOn_tendsto_at {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} (h : LocallyUniformTendstoOn uᵢ u l C) (hx : x ∈ C) : Filter.Tendsto (fun (i : ι) => uᵢ i x) l (nhds (u x))

theorem ViscositySolns.locallyUniformTendstoOn_uniformTendstoOn_of_isCompact {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {K : Set (Point n)} (h : LocallyUniformTendstoOn uᵢ u l K) (hK : IsCompact K) : UniformTendstoOn uᵢ u l K

theorem ViscositySolns.locallyUniformTendstoOn_uniformTendstoOn_compact_subset {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C K : Set (Point n)} (h : LocallyUniformTendstoOn uᵢ u l C) (hKC : K ⊆ C) (hK : IsCompact K) : UniformTendstoOn uᵢ u l K

theorem ViscositySolns.locallyUniformTendstoOn_continuousOn {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} (h : LocallyUniformTendstoOn uᵢ u l C) (hcont : ∃ᶠ (i : ι) in l, ContinuousOn (uᵢ i) C) : ContinuousOn u C

theorem ViscositySolns.locallyUniformTendstoOn_tendsto_comp {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {xᵢ : ι → Point n} (h : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hx : x ∈ C) (hxᵢ : Filter.Tendsto xᵢ l (nhdsWithin x C)) : Filter.Tendsto (fun (i : ι) => uᵢ i (xᵢ i)) l (nhds (u x))

theorem ViscositySolns.locallyUniformTendstoOn_tendsto_comp_of_tendsto_nhds_eventually_mem {n : ℕ} {ι : Type u_1} {uᵢ : ι → Point n → ℝ} {u : Point n → ℝ} {l : Filter ι} {C : Set (Point n)} {x : Point n} {xᵢ : ι → Point n} (h : LocallyUniformTendstoOn uᵢ u l C) (hu : ContinuousWithinAt u C x) (hx : x ∈ C) (hxᵢ : Filter.Tendsto xᵢ l (nhds x)) (hmem : ∀ᶠ (i : ι) in l, xᵢ i ∈ C) : Filter.Tendsto (fun (i : ι) => uᵢ i (xᵢ i)) l (nhds (u x))

Moving-point scalar convergence under locally uniform convergence, stated with ordinary convergence plus eventual membership in the domain.