English
If F i are continuous, F is monotone increasing, f is continuous and F x → f x pointwise, then F converges locally uniformly to f.
Русский
Если F i непрерывны, F монотонно возрастает, f непрерывна и F x → f x точечно, то F сходится локально равномерно к f.
LaTeX
$$"Dini's theorem" : (∀ i, Continuous (F i)) → Monotone F → Continuous f → (∀ x, Tendsto (F · x) atTop (𝓝 (f x))) → TendstoLocallyUniformly F f atTop$$
Lean4
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions
converging pointwise to a continuous function `f`, then `F n` converges locally uniformly to `f`. -/
theorem tendstoLocallyUniformly_of_forall_tendsto (hF_cont : ∀ i, Continuous (F i)) (hF_mono : Monotone F)
(hf : Continuous f) (h_tendsto : ∀ x, Tendsto (F · x) atTop (𝓝 (f x))) : TendstoLocallyUniformly F f atTop :=
by
refine (atTop : Filter ι).eq_or_neBot.elim (fun h ↦ ?eq_bot) (fun _ ↦ ?_)
case eq_bot => simp [h, tendstoLocallyUniformly_iff_forall_tendsto]
have F_le_f (x : α) (n : ι) : F n x ≤ f x :=
by
refine ge_of_tendsto (h_tendsto x) ?_
filter_upwards [Ici_mem_atTop n] with m hnm
exact hF_mono hnm x
simp_rw [Metric.tendstoLocallyUniformly_iff, dist_eq_norm']
intro ε ε_pos x
simp_rw +singlePass [tendsto_iff_norm_sub_tendsto_zero] at h_tendsto
obtain ⟨n, hn⟩ := (h_tendsto x).eventually (eventually_lt_nhds ε_pos) |>.exists
refine ⟨{y | ‖F n y - f y‖ < ε}, ⟨isOpen_lt (by fun_prop) continuous_const |>.mem_nhds hn, ?_⟩⟩
filter_upwards [eventually_ge_atTop n] with m hnm z hz
refine norm_le_norm_of_abs_le_abs ?_ |>.trans_lt hz
simp only [abs_of_nonpos (sub_nonpos_of_le (F_le_f _ _)), neg_sub, sub_le_sub_iff_left]
exact hF_mono hnm z
