Composing uniformly convergent families with continuous maps

Mathlib composes a uniformly convergent family with a uniformly continuous map (UniformContinuous.comp_tendstoUniformlyOn). A map that is only continuous at the points of the set of values of the limit suffices, provided that set is compact: by the Heine–Cantor argument (IsCompact.uniformContinuousAt_of_continuousAt) the map is uniformly continuous at that compact set, so it sends points close to it close to their images.

This applies, for instance, to families of paths converging uniformly on a compact interval to a continuous limit, composed with a continuous integrand. To compose with a map that also depends on the point a itself, as a time-dependent integrand does, first pass to the graphs a ↦ (a, F i a), which converge uniformly to the graph of the limit (TendstoUniformlyOn.graph).

For coefficients P (x, y) that depend on both the point x and the value y, continuity on a compact product s ×ˢ t suffices when all the values lie in t (IsCompact.tendstoUniformlyOn_comp_prodMk): P is then uniformly continuous there. This is the form in which the coefficients J(z, u(z)) of a nonlinear equation converge along a sequence of maps u converging uniformly on a compact set.

The file also records that a constant family converges uniformly (TauCeti.tendstoUniformlyOn_const), and that two families converging uniformly along the same filter converge jointly (TendstoUniformlyOn.prodMk_same), which is the form needed to compose with maps of several variables.

theorem IsCompact.comp_tendstoUniformlyOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {F : ι → α → β} {f : α → β} {s : Set α} {g : β → γ} {p : Filter ι} (hf : IsCompact (f '' s)) (hg : ∀ y ∈ f '' s, ContinuousAt g y) (h : TendstoUniformlyOn F f p s) : TendstoUniformlyOn (fun (i : ι) (x : α) => g (F i x)) (fun (x : α) => g (f x)) p s

Composing a family converging uniformly on s with a map continuous at every value of the limit on s preserves uniform convergence on s, provided the values of the limit on s form a compact set.

theorem TauCeti.tendstoUniformlyOn_const {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] (f : α → β) (p : Filter ι) (s : Set α) : TendstoUniformlyOn (fun (x : ι) => f) f p s

A constant family converges uniformly to its value.

theorem TendstoUniformlyOn.prodMk_same {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} {F' : ι → α → γ} {f' : α → γ} (h : TendstoUniformlyOn F f p s) (h' : TendstoUniformlyOn F' f' p s) : TendstoUniformlyOn (fun (i : ι) (x : α) => (F i x, F' i x)) (fun (x : α) => (f x, f' x)) p s

Two families converging uniformly on s along the same filter converge jointly. Mathlib's TendstoUniformlyOn.prodMk gives the joint convergence along the product filter p ×ˢ p.

theorem TendstoUniformlyOn.graph {α : Type u_1} {β : Type u_2} {ι : Type u_4} [UniformSpace β] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [UniformSpace α] (h : TendstoUniformlyOn F f p s) : TendstoUniformlyOn (fun (i : ι) (a : α) => (a, F i a)) (fun (a : α) => (a, f a)) p s

The graphs a ↦ (a, F i a) of a family converging uniformly on s converge uniformly on s to the graph of the limit.

theorem IsCompact.tendstoUniformlyOn_comp_prodMk {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Type u_4} [UniformSpace β] [UniformSpace γ] {F : ι → α → β} {f : α → β} {s : Set α} {p : Filter ι} [UniformSpace α] {t : Set β} {P : α × β → γ} (hs : IsCompact s) (ht : IsCompact t) (hP : ContinuousOn P (s ×ˢ t)) (hF : ∀ᶠ (i : ι) in p, Set.MapsTo (F i) s t) (hf : Set.MapsTo f s t) (h : TendstoUniformlyOn F f p s) : TendstoUniformlyOn (fun (i : ι) (x : α) => P (x, F i x)) (fun (x : α) => P (x, f x)) p s

Let Fᵢ → f uniformly on a compact set s, with all values on s in a compact set t. Then P (x, Fᵢ x) → P (x, f x) uniformly on s, for every P continuous on s ×ˢ t.