English
If δseq is a sequence of radii tending to 0 and E ⊆ α, then thickenedIndicatorAux(δseq(n), E) converges pointwise to the indicator of closure E.
Русский
Если δ_seq(n) → 0 и E ⊆ α, то thickenedIndicatorAux(δ_seq(n), E) сходится по точкам к индикатору замыкания E.
LaTeX
$$$\text{Let } (δ_n) \to 0 \text{ in } \mathbb{R}.\; \operatorname{thickenedIndicatorAux}(δ_n,E) \to \mathbf{1}_{\overline{E}} \text{ pointwise on } α$$$
Lean4
/-- As the thickening radius δ tends to 0, the δ-thickened indicator of a set E (in α) tends
pointwise (i.e., w.r.t. the product topology on `α → ℝ≥0∞`) to the indicator function of the
closure of E.
This statement is for the unbundled `ℝ≥0∞`-valued functions `thickenedIndicatorAux δ E`, see
`thickenedIndicator_tendsto_indicator_closure` for the version for bundled `ℝ≥0`-valued
bounded continuous functions. -/
theorem thickenedIndicatorAux_tendsto_indicator_closure {δseq : ℕ → ℝ} (δseq_lim : Tendsto δseq atTop (𝓝 0))
(E : Set α) :
Tendsto (fun n => thickenedIndicatorAux (δseq n) E) atTop (𝓝 (indicator (closure E) fun _ => (1 : ℝ≥0∞))) :=
by
rw [tendsto_pi_nhds]
intro x
by_cases x_mem_closure : x ∈ closure E
· simp_rw [thickenedIndicatorAux_one_of_mem_closure _ E x_mem_closure]
rw [show (indicator (closure E) fun _ => (1 : ℝ≥0∞)) x = 1 by simp only [x_mem_closure, indicator_of_mem]]
exact tendsto_const_nhds
· rw [show (closure E).indicator (fun _ => (1 : ℝ≥0∞)) x = 0 by
simp only [x_mem_closure, indicator_of_notMem, not_false_iff]]
rcases exists_real_pos_lt_infEdist_of_notMem_closure x_mem_closure with ⟨ε, ⟨ε_pos, ε_lt⟩⟩
rw [Metric.tendsto_nhds] at δseq_lim
specialize δseq_lim ε ε_pos
simp only [dist_zero_right, Real.norm_eq_abs, eventually_atTop] at δseq_lim
rcases δseq_lim with ⟨N, hN⟩
apply tendsto_atTop_of_eventually_const (i₀ := N)
intro n n_large
have key : x ∉ thickening ε E := by simpa only [thickening, mem_setOf_eq, not_lt] using ε_lt.le
refine le_antisymm ?_ bot_le
apply (thickenedIndicatorAux_mono (lt_of_abs_lt (hN n n_large)).le E x).trans
exact (thickenedIndicatorAux_zero ε_pos E key).le
