Failure of uniform convergence for a growing narrow spike
ProvedWorkbookCorrected.plus_51325corrected-formalizationlean-workbooksequencessource-checked
For n ≥ 1, define fₙ(x)=√n on 0 ≤ x ≤ 1/n and fₙ(x)=0 on 1/n < x ≤ 1. The sequence has no uniform limit on [0,1].
Formalization Note: States nonexistence of any uniform limit function as requested, rather than merely failure of uniform convergence to zero.
Source: InternLM Lean-Workbook, record lean_workbook_plus_51325 (Apache-2.0).
Preamble
import Mathlib
Formal statement
theorem WorkbookCorrected.plus_51325 (f : ℕ → ℝ → ℝ)
(hf : ∀ n : ℕ, ∀ x : ℝ, f n x=if 0 ≤ x ∧ x ≤ 1/(n:ℝ) then Real.sqrt n else 0) :
¬ ∃ g : ℝ → ℝ, ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ n : ℕ, N < n →
∀ x ∈ Set.Icc (0:ℝ) 1, |f n x-g x| < ε := by sorrySource