feat: TendstoUniformlyOn for tprod's (#13349)

Give conditions for prods to converge uniformly to a tprod.



Co-authored-by: David Loeffler <d.loeffler.01@cantab.net>

Author: CBirkbeck

Mathlib.lean

@@ -1723,6 +1723,7 @@ import Mathlib.Analysis.NormedSpace.Int
 import Mathlib.Analysis.NormedSpace.MStructure
 import Mathlib.Analysis.NormedSpace.Multilinear.Basic
 import Mathlib.Analysis.NormedSpace.Multilinear.Curry
+import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Asymptotics
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Basic
 import Mathlib.Analysis.NormedSpace.OperatorNorm.Bilinear
@@ -5916,6 +5917,7 @@ import Mathlib.Topology.Algebra.IntermediateField
 import Mathlib.Topology.Algebra.IsOpenUnits
 import Mathlib.Topology.Algebra.IsUniformGroup.Basic
 import Mathlib.Topology.Algebra.IsUniformGroup.Defs
+import Mathlib.Topology.Algebra.IsUniformGroup.Order
 import Mathlib.Topology.Algebra.LinearTopology
 import Mathlib.Topology.Algebra.Localization
 import Mathlib.Topology.Algebra.Module.Alternating.Basic

Mathlib/Analysis/NormedSpace/FunctionSeries.lean

@@ -13,6 +13,9 @@ We show that series of functions are continuous when each individual function in
 additionally suitable uniform summable bounds are satisfied, in `continuous_tsum`.
 
 For smoothness of series of functions, see the file `Analysis.Calculus.SmoothSeries`.
+
+TODO: update this to use `SummableUniformlyOn`.
+
 -/
 
 open Set Metric TopologicalSpace Function Filter

Mathlib/Analysis/NormedSpace/MultipliableUniformlyOn.lean

@@ -0,0 +1,158 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import Mathlib.Analysis.NormedSpace.FunctionSeries
+import Mathlib.Analysis.SpecialFunctions.Log.Summable
+import Mathlib.Topology.Algebra.InfiniteSum.UniformOn
+import Mathlib.Topology.Algebra.IsUniformGroup.Order
+
+/-!
+# Uniform convergence of products of functions
+
+We gather some results about the uniform convergence of infinite products, in particular those of
+the form `∏' i, (1 + f i x)` for a sequence `f` of complex valued functions.
+-/
+
+open Filter Function Complex Finset Topology
+
+variable {α ι : Type*} {𝔖 : Set (Set α)} {K : Set α} {u : ι → ℝ}
+
+section Complex
+
+variable {f : ι → α → ℂ}
+
+lemma TendstoUniformlyOn.comp_cexp {p : Filter ι} {g : α → ℂ}
+    (hf : TendstoUniformlyOn f g p K) (hg : BddAbove <| (fun x ↦ (g x).re) '' K) :
+    TendstoUniformlyOn (cexp ∘ f ·) (cexp ∘ g) p K := by
+  obtain ⟨v, hv⟩ : ∃ v, ∀ x ∈ K, (g x).re ≤ v := hg.imp <| by simp [mem_upperBounds]
+  have : ∀ᶠ i in p, ∀ x ∈ K, (f i x).re ≤ v + 1 := hf.re.eventually_forall_le (lt_add_one v) hv
+  refine (UniformContinuousOn.cexp _).comp_tendstoUniformlyOn_eventually (by simpa) ?_ hf
+  exact fun x hx ↦ (hv x hx).trans (lt_add_one v).le
+
+lemma Summable.hasSumUniformlyOn_log_one_add (hu : Summable u)
+    (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) :
+    HasSumUniformlyOn (fun i x ↦ log (1 + f i x)) (fun x ↦ ∑' i, log (1 + f i x)) {K} := by
+  simp only [hasSumUniformlyOn_iff_tendstoUniformlyOn, Set.mem_singleton_iff, forall_eq]
+  apply tendstoUniformlyOn_tsum_of_cofinite_eventually <| hu.mul_left (3 / 2)
+  filter_upwards [h, hu.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi hi' x hx
+    using (norm_log_one_add_half_le_self <| (hi x hx).trans hi').trans (by simpa using hi x hx)
+
+lemma Summable.tendstoUniformlyOn_tsum_nat_log_one_add {f : ℕ → α → ℂ} {u : ℕ → ℝ}
+    (hu : Summable u) (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) :
+    TendstoUniformlyOn (fun n x ↦ ∑ m ∈ Finset.range n, log (1 + f m x))
+    (fun x ↦ ∑' n, log (1 + f n x)) atTop K := by
+  rw [← Nat.cofinite_eq_atTop] at h
+  exact (hu.hasSumUniformlyOn_log_one_add h).tendstoUniformlyOn_finset_range rfl
+
+/-- If `x ↦ ∑' i, log (f i x)` is uniformly convergent on `𝔖`, its sum has bounded-above real part
+on each set in `𝔖`, and the functions `f i x` have no zeroes, then  `∏' i, f i x` is uniformly
+convergent on `𝔖`.
+
+Note that the non-vanishing assumption is really needed here: if this assumption is dropped then
+one obtains a counterexample if `ι = α = ℕ` and `f i x` is `0` if `i = x` and `1` otherwise. -/
+lemma hasProdUniformlyOn_of_clog (hf : SummableUniformlyOn (fun i x ↦ log (f i x)) 𝔖)
+    (hfn : ∀ K ∈ 𝔖, ∀ x ∈ K, ∀ i, f i x ≠ 0)
+    (hg : ∀ K ∈ 𝔖, BddAbove <| (fun x ↦ (∑' i, log (f i x)).re) '' K) :
+    HasProdUniformlyOn f (fun x ↦ ∏' i, f i x) 𝔖 := by
+  simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn]
+  obtain ⟨r, hr⟩ := hf.exists
+  intro K hK
+  suffices H : TendstoUniformlyOn (fun s x ↦ ∏ i ∈ s, f i x) (cexp ∘ r) atTop K by
+    refine H.congr_right ((hr.tsum_eqOn hK).comp_left.symm.trans ?_)
+    exact fun x hx ↦ (cexp_tsum_eq_tprod (hfn K hK x hx) (hf.summable hK hx))
+  have h1 := hr.tsum_eqOn hK
+  simp only [hasSumUniformlyOn_iff_tendstoUniformlyOn] at hr
+  refine ((hr K hK).comp_cexp ?_).congr ?_
+  · simp +contextual [← h1 _]
+    exact hg K hK
+  · filter_upwards with s i hi using by simp [exp_sum, fun y ↦ exp_log (hfn K hK i hi y)]
+
+lemma multipliableUniformlyOn_of_clog (hf : SummableUniformlyOn (fun i x ↦ log (f i x)) 𝔖)
+    (hfn : ∀ K ∈ 𝔖, ∀ x ∈ K, ∀ i, f i x ≠ 0)
+    (hg : ∀ K ∈ 𝔖, BddAbove <| (fun x ↦ (∑' i, log (f i x)).re) '' K) :
+    MultipliableUniformlyOn f 𝔖 :=
+  ⟨_, hasProdUniformlyOn_of_clog hf hfn hg⟩
+
+end Complex
+
+namespace Summable
+
+variable {R : Type*} [NormedCommRing R] [NormOneClass R] [CompleteSpace R] [TopologicalSpace α]
+  {f : ι → α → R}
+
+/-- If a sequence of continuous functions `f i x` on an open compact `K` have norms eventually
+bounded by a summable function, then `∏' i, (1 + f i x)` is uniformly convergent on `K`. -/
+lemma hasProdUniformlyOn_one_add (hK : IsCompact K) (hu : Summable u)
+    (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) (hcts : ∀ i, ContinuousOn (f i) K) :
+    HasProdUniformlyOn (fun i x ↦ 1 + f i x) (fun x ↦ ∏' i, (1 + f i x)) {K} := by
+  simp only [hasProdUniformlyOn_iff_tendstoUniformlyOn, Set.mem_singleton_iff,
+    tendstoUniformlyOn_iff_tendstoUniformly_comp_coe, forall_eq]
+  by_cases hKe : K = ∅
+  · simp [TendstoUniformly, hKe]
+  · haveI hCK : CompactSpace K := isCompact_iff_compactSpace.mp hK
+    haveI hne : Nonempty K := by rwa [Set.nonempty_coe_sort, Set.nonempty_iff_ne_empty]
+    let f' i : C(K, R) := ⟨_, continuousOn_iff_continuous_restrict.mp (hcts i)⟩
+    have hf'_bd : ∀ᶠ i in cofinite, ‖f' i‖ ≤ u i := by
+      simp only [ContinuousMap.norm_le_of_nonempty]
+      filter_upwards [h] with i hi using fun x ↦ hi x x.2
+    have hM : Multipliable fun i ↦ 1 + f' i := by
+      refine multipliable_one_add_of_summable (hu.of_norm_bounded_eventually _ ?_)
+      simpa using hf'_bd
+    convert ContinuousMap.tendsto_iff_tendstoUniformly.mp hM.hasProd
+    · simp [f']
+    · exact funext fun k ↦ ContinuousMap.tprod_apply hM k
+
+lemma multipliableUniformlyOn_one_add (hK : IsCompact K) (hu : Summable u)
+    (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) (hcts : ∀ i, ContinuousOn (f i) K) :
+    MultipliableUniformlyOn (fun i x ↦ 1 + f i x) {K} :=
+  ⟨_, hasProdUniformlyOn_one_add hK hu h hcts⟩
+
+/-- This is a version of `hasProdUniformlyOn_one_add` for sequences indexed by `ℕ`. -/
+lemma hasProdUniformlyOn_nat_one_add {f : ℕ → α → R} (hK : IsCompact K) {u : ℕ → ℝ}
+    (hu : Summable u) (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
+    (hcts : ∀ n, ContinuousOn (f n) K) :
+    HasProdUniformlyOn (fun n x ↦ 1 + f n x) (fun x ↦ ∏' i, (1 + f i x)) {K} :=
+  hasProdUniformlyOn_one_add hK hu (Nat.cofinite_eq_atTop ▸ h) hcts
+
+lemma multipliableUniformlyOn_nat_one_add {f : ℕ → α → R} (hK : IsCompact K)
+    {u : ℕ → ℝ} (hu : Summable u) (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
+    (hcts : ∀ n, ContinuousOn (f n) K) :
+    MultipliableUniformlyOn (fun n x ↦ 1 + f n x) {K} :=
+  ⟨_, hasProdUniformlyOn_nat_one_add hK hu h hcts⟩
+
+section LocallyCompactSpace
+
+variable [LocallyCompactSpace α]
+
+/-- If a sequence of continuous functions `f i x` on an open subset `K` have norms eventually
+bounded by a summable function, then `∏' i, (1 + f i x)` is locally uniformly convergent on `K`. -/
+lemma hasProdLocallyUniformlyOn_one_add (hK : IsOpen K) (hu : Summable u)
+    (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) (hcts : ∀ i, ContinuousOn (f i) K) :
+    HasProdLocallyUniformlyOn (fun i x ↦ 1 + f i x) (fun x ↦ ∏' i, (1 + f i x)) K := by
+  apply hasProdLocallyUniformlyOn_of_forall_compact hK
+  refine fun S hS hC ↦ hasProdUniformlyOn_one_add hC hu ?_ fun i ↦ (hcts i).mono hS
+  filter_upwards [h] with i hi a ha using hi a (hS ha)
+
+lemma multipliableLocallyUniformlyOn_one_add (hK : IsOpen K) (hu : Summable u)
+    (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) (hcts : ∀ i, ContinuousOn (f i) K) :
+    MultipliableLocallyUniformlyOn (fun i x ↦ 1 + f i x) K :=
+  ⟨_, hasProdLocallyUniformlyOn_one_add hK hu h hcts⟩
+
+/-- This is a version of `hasProdLocallyUniformlyOn_one_add` for sequences indexed by `ℕ`. -/
+lemma hasProdLocallyUniformlyOn_nat_one_add {f : ℕ → α → R} (hK : IsOpen K) {u : ℕ → ℝ}
+    (hu : Summable u) (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
+    (hcts : ∀ n, ContinuousOn (f n) K) :
+    HasProdLocallyUniformlyOn (fun n x ↦ 1 + f n x) (fun x ↦ ∏' i, (1 + f i x)) K :=
+  hasProdLocallyUniformlyOn_one_add hK hu (Nat.cofinite_eq_atTop ▸ h) hcts
+
+lemma multipliableLocallyUniformlyOn_nat_one_add  {f : ℕ → α → R} (hK : IsOpen K) {u : ℕ → ℝ}
+    (hu : Summable u) (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n)
+    (hcts : ∀ n, ContinuousOn (f n) K) :
+    MultipliableLocallyUniformlyOn (fun n x ↦ 1 + f n x) K :=
+  ⟨_, hasProdLocallyUniformlyOn_nat_one_add hK hu h hcts⟩
+
+end LocallyCompactSpace
+
+end Summable

Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

@@ -5,7 +5,6 @@ Authors: Chris Birkbeck
 -/
 
 import Mathlib.Analysis.SpecialFunctions.Complex.LogBounds
-import Mathlib.Analysis.NormedSpace.FunctionSeries
 
 /-!
 # Summability of logarithms
@@ -43,7 +42,8 @@ lemma summable_log_one_add_of_summable {f : ι → ℂ} (hf : Summable f) :
   filter_upwards [hf.norm.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi
     using norm_log_one_add_half_le_self hi
 
-lemma multipliable_one_add_of_summable (hf : Summable f) : Multipliable (fun i ↦ 1 + f i) :=
+protected lemma multipliable_one_add_of_summable (hf : Summable f) :
+    Multipliable (fun i ↦ 1 + f i) :=
   multipliable_of_summable_log (summable_log_one_add_of_summable hf)
 
 end Complex
@@ -94,21 +94,6 @@ lemma multipliable_one_add_of_summable (hf : Summable f) : Multipliable (fun i 
 
 end Real
 
-lemma Complex.tendstoUniformlyOn_tsum_nat_log_one_add {α : Type*} {f : ℕ → α → ℂ} (K : Set α)
-    {u : ℕ → ℝ} (hu : Summable u) (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) :
-    TendstoUniformlyOn (fun (n : ℕ) (a : α) => ∑ i ∈ Finset.range n,
-    (Complex.log (1 + f i a))) (fun a => ∑' i : ℕ, Complex.log (1 + f i a)) atTop K := by
-  apply tendstoUniformlyOn_tsum_nat_eventually (hu.mul_left (3/2))
-  obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp (Summable.tendsto_atTop_zero hu) (1/2) (one_half_pos)
-  simp only [eventually_atTop, ge_iff_le] at *
-  obtain ⟨N2, hN2⟩ := h
-  refine ⟨max N N2, fun n hn x hx => ?_⟩
-  apply le_trans (Complex.norm_log_one_add_half_le_self (z := (f n x)) ?_)
-  · simp only [Nat.ofNat_pos, div_pos_iff_of_pos_left, mul_le_mul_left]
-    exact hN2 n (le_of_max_le_right hn) x hx
-  · apply le_trans (le_trans (hN2 n (le_of_max_le_right hn) x hx)
-    (by simpa using Real.le_norm_self (u n))) (hN n (le_of_max_le_left hn)).le
-
 section NormedRing
 
 lemma Multipliable.eventually_bounded_finset_prod {v : ι → ℝ} (hv : Multipliable v) :

Mathlib/Topology/Algebra/InfiniteSum/UniformOn.lean

@@ -5,6 +5,7 @@ Authors: Chris Birkbeck, David Loeffler
 -/
 import Mathlib.Topology.Algebra.InfiniteSum.Defs
 import Mathlib.Topology.Algebra.UniformConvergence
+import Mathlib.Order.Filter.AtTopBot.Finset
 
 /-!
 # Infinite sum and products that converge uniformly on a set
@@ -63,6 +64,13 @@ lemma hasProdUniformlyOn_iff_tendstoUniformlyOn : HasProdUniformlyOn f g 𝔖 
   simpa [HasProdUniformlyOn, HasProd, ← UniformOnFun.ofFun_prod, Finset.prod_fn] using
     UniformOnFun.tendsto_iff_tendstoUniformlyOn
 
+@[to_additive]
+lemma HasProdUniformlyOn.tendstoUniformlyOn_finset_range
+    {f : ℕ → β → α} (h : HasProdUniformlyOn f g 𝔖) (hs : s ∈ 𝔖) :
+    TendstoUniformlyOn (fun N b ↦ ∏ i ∈ Finset.range N, f i b) g atTop s := by
+  rw [hasProdUniformlyOn_iff_tendstoUniformlyOn] at h
+  exact fun v hv => Filter.tendsto_finset_range.eventually (h s hs v hv)
+
 @[to_additive]
 theorem HasProdUniformlyOn.hasProd (h : HasProdUniformlyOn f g 𝔖) (hs : s ∈ 𝔖) (hx : x ∈ s) :
     HasProd (f · x) (g x) :=
@@ -142,6 +150,18 @@ lemma hasProdLocallyUniformlyOn_of_of_forall_exists_nhds
 @[deprecated (since := "2025-05-22")] alias hasSumLocallyUniformlyOn_of_of_forall_exists_nhd :=
   hasSumLocallyUniformlyOn_of_of_forall_exists_nhds
 
+@[to_additive]
+lemma HasProdUniformlyOn.hasProdLocallyUniformlyOn (h : HasProdUniformlyOn f g {s}) :
+  HasProdLocallyUniformlyOn f g s := by
+  simp [HasProdLocallyUniformlyOn, hasProdUniformlyOn_iff_tendstoUniformlyOn] at *
+  exact TendstoUniformlyOn.tendstoLocallyUniformlyOn h
+
+@[to_additive]
+lemma hasProdLocallyUniformlyOn_of_forall_compact (hs : IsOpen s) [LocallyCompactSpace β]
+    (h : ∀ K ⊆ s, IsCompact K → HasProdUniformlyOn f g {K}) : HasProdLocallyUniformlyOn f g s := by
+  rw [HasProdLocallyUniformlyOn, tendstoLocallyUniformlyOn_iff_forall_isCompact hs]
+  simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn] using h
+
 @[to_additive]
 theorem HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn
     (h : HasProdLocallyUniformlyOn f g s) : MultipliableLocallyUniformlyOn f s :=

Mathlib/Topology/Algebra/IsUniformGroup/Order.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import Mathlib.Topology.Algebra.IsUniformGroup.Defs
+import Mathlib.Topology.Order.Basic
+import Mathlib.Topology.UniformSpace.UniformConvergence
+
+/-!
+# TendstoUniformlyOn on ordered spaces
+
+We gather some results about `TendstoUniformlyOn f g K` on ordered spaces,
+in particular bounding the values of `f` in terms of bounds on the limit `g`.
+
+-/
+
+open Filter Function Finset Topology
+
+variable {α ι : Type*}
+
+section order
+
+variable {β : Type*} [UniformSpace β] [AddGroup β] [IsUniformAddGroup β] [PartialOrder β]
+  [OrderTopology β] [AddLeftMono β] [AddRightMono β]
+
+variable {f : ι → α → β} {g : α → β} {K : Set α} {p : Filter ι}
+
+/-- If a sequence of functions converges uniformly on a set to a function `g` which is bounded above
+by a value `u`, then the sequence is strictly bounded by any `v` such that `u < v`. -/
+lemma TendstoUniformlyOn.eventually_forall_lt {u v : β} (huv : u < v)
+    (hf : TendstoUniformlyOn f g p K) (hg : ∀ x ∈ K, g x ≤ u) :
+    ∀ᶠ i in p, ∀ x ∈ K, f i x < v := by
+  simp only [tendstoUniformlyOn_iff_tendsto, uniformity_eq_comap_neg_add_nhds_zero,
+    tendsto_iff_eventually, eventually_comap, Prod.forall] at *
+  conv at hf => enter [2]; rw [eventually_iff_exists_mem]
+  have hf2 := hf (fun x ↦ -x.1 + x.2 < -u + v) ⟨_, (isOpen_gt' (-u + v)).mem_nhds (by simp [huv]),
+    fun y hy a b hab ↦ (hab.symm ▸ hy :)⟩
+  filter_upwards [eventually_prod_principal_iff.mp hf2] with i hi x hx
+  simpa using add_lt_add_of_le_of_lt (hg x hx) (hi x hx)
+
+lemma TendstoUniformlyOn.eventually_forall_le {u v : β} (huv : u < v)
+    (hf : TendstoUniformlyOn f g p K) (hg : ∀ x ∈ K, g x ≤ u) :
+    ∀ᶠ i in p, ∀ x ∈ K, f i x ≤ v := by
+  filter_upwards [hf.eventually_forall_lt huv hg] with i hi x hx using (hi x hx).le
+
+end order

Mathlib/Topology/UniformSpace/UniformConvergence.lean

@@ -123,6 +123,10 @@ theorem tendstoUniformlyOn_iff_tendstoUniformly_comp_coe :
     TendstoUniformlyOn F f p s ↔ TendstoUniformly (fun i (x : s) => F i x) (f ∘ (↑)) p :=
   forall₂_congr fun u _ => by simp
 
+lemma tendstoUniformlyOn_iff_restrict {K : Set α} : TendstoUniformlyOn F f p K ↔
+    TendstoUniformly (fun n : ι => K.restrict (F n)) (K.restrict f) p :=
+  tendstoUniformlyOn_iff_tendstoUniformly_comp_coe
+
 /-- A sequence of functions `Fₙ` converges uniformly to a limiting function `f` w.r.t.
 filter `p` iff the function `(n, x) ↦ (f x, Fₙ x)` converges along `p ×ˢ ⊤` to the uniformity.
 In other words: one knows nothing about the behavior of `x` in this limit.

Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean

@@ -1117,38 +1117,46 @@ end UniformFun
 
 section UniformComposition
 
-variable {α β γ ι : Type*} [UniformSpace β] [UniformSpace γ] {p : Filter ι}
+variable {α β γ ι : Type*} [UniformSpace β] [UniformSpace γ] {p : Filter ι} {s : Set β}
+  {F : ι → α → β} {f : α → β} {g : β → γ}
 
 /-- Composing on the left by a uniformly continuous function preserves uniform convergence -/
-theorem UniformContinuousOn.comp_tendstoUniformly (s : Set β) (F : ι → α → β) (f : α → β)
-    (hF : ∀ i x, F i x ∈ s) (hf : ∀ x, f x ∈ s)
-    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
+theorem UniformContinuousOn.comp_tendstoUniformly
+    (hF : ∀ i x, F i x ∈ s) (hf : ∀ x, f x ∈ s) (hg : UniformContinuousOn g s)
+    (h : TendstoUniformly F f p) :
     TendstoUniformly (fun i x => g (F i x)) (fun x => g (f x)) p := by
   rw [uniformContinuousOn_iff_restrict] at hg
   lift F to ι → α → s using hF with F' hF'
   lift f to α → s using hf with f' hf'
   rw [tendstoUniformly_iff_tendsto] at h
-  have : Tendsto (fun q : ι × α ↦ (f' q.2, (F' q.1 q.2))) (p ×ˢ ⊤) (𝓤 s) :=
+  have : Tendsto (fun q ↦ (f' q.2, F' q.1 q.2)) (p ×ˢ ⊤) (𝓤 s) :=
     h.of_tendsto_comp isUniformEmbedding_subtype_val.comap_uniformity.le
   apply UniformContinuous.comp_tendstoUniformly hg ?_
   rwa [← tendstoUniformly_iff_tendsto] at this
 
-theorem UniformContinuousOn.comp_tendstoUniformly_eventually (s : Set β) (F : ι → α → β) (f : α → β)
-    (hF : ∀ᶠ i in p, ∀ x, F i x ∈ s) (hf : ∀ x, f x ∈ s)
-    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformly F f p) :
-    TendstoUniformly (fun i => fun x => g (F i x)) (fun x => g (f x)) p := by
+theorem UniformContinuousOn.comp_tendstoUniformly_eventually
+    (hF : ∀ᶠ i in p, ∀ x, F i x ∈ s) (hf : ∀ x, f x ∈ s) (hg : UniformContinuousOn g s)
+    (h : TendstoUniformly F f p) :
+    TendstoUniformly (fun i x ↦ g (F i x)) (fun x ↦ g (f x)) p := by
   classical
-  rw [eventually_iff_exists_mem] at hF
-  obtain ⟨s', hs', hs⟩ := hF
-  let F' : ι → α → β := fun (i : ι) x => if i ∈ s' then F i x else f x
+  obtain ⟨s', hs', hs⟩ := eventually_iff_exists_mem.mp hF
+  let F' : ι → α → β := fun i x => if i ∈ s' then F i x else f x
   have hF : F =ᶠ[p] F' :=  by
     rw [eventuallyEq_iff_exists_mem]
     refine ⟨s', hs', fun y hy => by aesop⟩
   have h' : TendstoUniformly F' f p := by
     rwa [tendstoUniformly_congr hF] at h
   apply (tendstoUniformly_congr _).mpr
-    (UniformContinuousOn.comp_tendstoUniformly s F' f (by aesop) hf hg h')
+    (UniformContinuousOn.comp_tendstoUniformly (by aesop) hf hg h')
   rw [eventuallyEq_iff_exists_mem]
   refine ⟨s', hs', fun i hi => by aesop⟩
 
+theorem UniformContinuousOn.comp_tendstoUniformlyOn_eventually {t : Set α}
+    (hF : ∀ᶠ i in p, ∀ x ∈ t, F i x ∈ s) (hf : ∀ x ∈ t, f x ∈ s)
+    {g : β → γ} (hg : UniformContinuousOn g s) (h : TendstoUniformlyOn F f p t) :
+    TendstoUniformlyOn (fun i x ↦ g (F i x)) (fun x => g (f x)) p t := by
+  rw [tendstoUniformlyOn_iff_restrict]
+  apply UniformContinuousOn.comp_tendstoUniformly_eventually (by simpa using hF )
+     (by simpa using hf) hg (tendstoUniformlyOn_iff_restrict.mp h)
+
 end UniformComposition