English
The uniform product convergence condition HasProdUniformlyOn f g 𝔖 is equivalent to requiring that, for every s in 𝔖, the family of partial products ∏ i∈I f(i,·) converges uniformly to g on s as I grows; i.e., TendstoUniformlyOn holds for all s ∈ 𝔖.
Русский
Условие равномерной асимптотической сдачи произведения HasProdUniformlyOn f g 𝔖 эквивалентно требованию, чтобы для каждого s ∈ 𝔖 множество частичных произведений ∏ i∈I f(i,·) сходилось равномерно к g на s при росте I; т.е. выполняется TendstoUniformlyOn для всех s ∈ 𝔖.
LaTeX
$$$ HasProdUniformlyOn\ f\ g\ 𝔖 \iff \forall s\in 𝔖,\ TendstoUniformlyOn\ (\lambda I\ b. \prod_{i\in I} f(i,b))\ g\ atTop\ s $$$
Lean4
@[to_additive]
theorem hasProdUniformlyOn_iff_tendstoUniformlyOn :
HasProdUniformlyOn f g 𝔖 ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (fun I b ↦ ∏ i ∈ I, f i b) g atTop s := by
simpa [HasProdUniformlyOn, HasProd, ← UniformOnFun.ofFun_prod, Finset.prod_fn] using
UniformOnFun.tendsto_iff_tendstoUniformlyOn
