Dini's Theorem

This file proves Dini's theorem, which states that if F n is a monotone increasing sequence of continuous real-valued functions on a compact set s converging pointwise to a continuous function f, then F n converges uniformly to f.

We generalize the codomain from ℝ to a normed lattice additive commutative group G. This theorem is true in a different generality as well: when G is a linearly ordered topological group with the order topology. This weakens the norm assumption, in exchange for strengthening to a linear order. This separate generality is not included in this file, but that generality was included in initial drafts of the original PR #19068 and can be recovered if necessary.

The key idea of the proof is to use a particular basis of 𝓝 0 which consists of open sets that are somehow monotone in the sense that if s is in the basis, and 0 ≤ x ≤ y, then y ∈ s → x ∈ s, and so the proof would work on any topological ordered group possessing such a basis. In the case of a linearly ordered topological group with the order topology, this basis is nhds_basis_Ioo. In the case of a normed lattice additive commutative group, this basis is nhds_basis_ball, and the fact that this basis satisfies the monotonicity criterion corresponds to HasSolidNorm.

theorem Monotone.tendstoLocallyUniformly_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} (hF_cont : ∀ (i : ι), Continuous (F i)) (hF_mono : Monotone F) (hf : Continuous f) (h_tendsto : ∀ (x : α), Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoLocallyUniformly F f Filter.atTop

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 Monotone.tendstoLocallyUniformlyOn_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} {s : Set α} (hF_cont : ∀ (i : ι), ContinuousOn (F i) s) (hF_mono : ∀ x ∈ s, Monotone fun (x_1 : ι) => F x_1 x) (hf : ContinuousOn f s) (h_tendsto : ∀ x ∈ s, Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoLocallyUniformlyOn F f Filter.atTop s

Dini's theorem: if F n is a monotone increasing collection of continuous functions on a set s converging pointwise to a continuous function f, then F n converges locally uniformly to f.

theorem Monotone.tendstoUniformly_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} [CompactSpace α] (hF_cont : ∀ (i : ι), Continuous (F i)) (hF_mono : Monotone F) (hf : Continuous f) (h_tendsto : ∀ (x : α), Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoUniformly F f Filter.atTop

Dini's theorem: if F n is a monotone increasing collection of continuous functions on a compact space converging pointwise to a continuous function f, then F n converges uniformly to f.

theorem Monotone.tendstoUniformlyOn_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} {s : Set α} (hs : IsCompact s) (hF_cont : ∀ (i : ι), ContinuousOn (F i) s) (hF_mono : ∀ x ∈ s, Monotone fun (x_1 : ι) => F x_1 x) (hf : ContinuousOn f s) (h_tendsto : ∀ x ∈ s, Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoUniformlyOn F f Filter.atTop s

Dini's theorem: if F n is a monotone increasing collection of continuous functions on a compact set s converging pointwise to a continuous function f, then F n converges uniformly to f.

theorem Antitone.tendstoLocallyUniformly_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} (hF_cont : ∀ (i : ι), Continuous (F i)) (hF_anti : Antitone F) (hf : Continuous f) (h_tendsto : ∀ (x : α), Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoLocallyUniformly F f Filter.atTop

Dini's theorem: if F n is a monotone decreasing collection of continuous functions on a converging pointwise to a continuous function f, then F n converges locally uniformly to f.

theorem Antitone.tendstoLocallyUniformlyOn_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} {s : Set α} (hF_cont : ∀ (i : ι), ContinuousOn (F i) s) (hF_anti : ∀ x ∈ s, Antitone fun (x_1 : ι) => F x_1 x) (hf : ContinuousOn f s) (h_tendsto : ∀ x ∈ s, Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoLocallyUniformlyOn F f Filter.atTop s

Dini's theorem: if F n is a monotone decreasing collection of continuous functions on a set s converging pointwise to a continuous function f, then F n converges locally uniformly to f.

theorem Antitone.tendstoUniformly_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} [CompactSpace α] (hF_cont : ∀ (i : ι), Continuous (F i)) (hF_anti : Antitone F) (hf : Continuous f) (h_tendsto : ∀ (x : α), Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoUniformly F f Filter.atTop

Dini's theorem: if F n is a monotone decreasing collection of continuous functions on a compact space converging pointwise to a continuous function f, then F n converges uniformly to f.

theorem Antitone.tendstoUniformlyOn_of_forall_tendsto {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → α → G} {f : α → G} {s : Set α} (hs : IsCompact s) (hF_cont : ∀ (i : ι), ContinuousOn (F i) s) (hF_anti : ∀ x ∈ s, Antitone fun (x_1 : ι) => F x_1 x) (hf : ContinuousOn f s) (h_tendsto : ∀ x ∈ s, Filter.Tendsto (fun (x_1 : ι) => F x_1 x) Filter.atTop (nhds (f x))) : TendstoUniformlyOn F f Filter.atTop s

Dini's theorem: if F n is a monotone decreasing collection of continuous functions on a compact set s converging pointwise to a continuous f, then F n converges uniformly to f.

theorem ContinuousMap.tendsto_of_monotone_of_pointwise {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → C(α, G)} {f : C(α, G)} (hF_mono : Monotone F) (h_tendsto : ∀ (x : α), Filter.Tendsto (fun (x_1 : ι) => (F x_1) x) Filter.atTop (nhds (f x))) : Filter.Tendsto F Filter.atTop (nhds f)

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 to f in the compact-open topology.

theorem ContinuousMap.tendsto_of_antitone_of_pointwise {ι : Type u_1} {α : Type u_2} {G : Type u_3} [Preorder ι] [TopologicalSpace α] [NormedAddCommGroup G] [Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → C(α, G)} {f : C(α, G)} (hF_anti : Antitone F) (h_tendsto : ∀ (x : α), Filter.Tendsto (fun (x_1 : ι) => (F x_1) x) Filter.atTop (nhds (f x))) : Filter.Tendsto F Filter.atTop (nhds f)

Dini's theorem: if F n is a monotone decreasing collection of continuous functions converging pointwise to a continuous function f, then F n converges to f in the compact-open topology.