English
In the natural-number index setting, if u is summable and the norms of f_n(x) are bounded by u_n uniformly on K for n large, then the product ∏' i (1+f_i(x)) converges uniformly on K.
Русский
Для индексации по естественным числам: если u суммируемо и ||f_n(x)|| ≤ u_n для больших n на K, то произведение ∏' i (1+f_i(x)) сходится равномерно на K.
LaTeX
$$$IsCompact K\\Rightarrow\\Summable u\\Rightarrow\\Eventual (\\forall x∈K, \\|f_n(x)\\| ≤ u_n) \\Rightarrow HasProdUniformlyOn (\\lambda n x, 1+f_n(x)) (\\lambda x, ∏' i, (1+f_i(x))) {K}$$$
Lean4
/-- 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`. -/
theorem 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 :=
multipliable_one_add_of_summable (hu.of_norm_bounded_eventually (by simpa using hf'_bd))
convert ContinuousMap.tendsto_iff_tendstoUniformly.mp hM.hasProd
· simp [f']
· exact funext fun k ↦ ContinuousMap.tprod_apply hM k
