English
As δseq → 0, the thickened indicator of E tends to the indicator of closure E (for the unbundled indicatorAux).
Русский
При δ_seq → 0 толщина индикатора E стремится к индикатору замыкания E (для несобранного thickenedIndicatorAux).
LaTeX
$$$\text{Let } δseq: \mathbb{N}→\mathbb{R}, δseq\to 0:\; \operatorname{thickenedIndicatorAux}(δseq(n),E) \to \mathbf{1}_{\overline{E}}$$$
Lean4
/-- As the thickening radius δ tends to 0, the δ-thickened indicator of a set E (in α) tends
pointwise to the indicator function of the closure of E.
Note: This version is for the bundled bounded continuous functions, but the topology is not
the topology on `α →ᵇ ℝ≥0`. Coercions to functions `α → ℝ≥0` are done first, so the topology
instance is the product topology (the topology of pointwise convergence). -/
theorem thickenedIndicator_tendsto_indicator_closure {δseq : ℕ → ℝ} (δseq_pos : ∀ n, 0 < δseq n)
(δseq_lim : Tendsto δseq atTop (𝓝 0)) (E : Set α) :
Tendsto (fun n : ℕ => ((↑) : (α →ᵇ ℝ≥0) → α → ℝ≥0) (thickenedIndicator (δseq_pos n) E)) atTop
(𝓝 (indicator (closure E) fun _ => (1 : ℝ≥0))) :=
by
have key := thickenedIndicatorAux_tendsto_indicator_closure δseq_lim E
rw [tendsto_pi_nhds] at *
intro x
rw [show indicator (closure E) (fun _ => (1 : ℝ≥0)) x = (indicator (closure E) (fun _ => (1 : ℝ≥0∞)) x).toNNReal by
refine (congr_fun (comp_indicator_const 1 ENNReal.toNNReal toNNReal_zero) x).symm]
refine Tendsto.comp (tendsto_toNNReal ?_) (key x)
by_cases x_mem : x ∈ closure E <;> simp [x_mem]
