tendstoUniformlyOn_finsetRange — Mathlib

English

If HasProdUniformlyOn f g 𝔖 holds and hs ∈ 𝔖, then the sequence of finite range products ∏ i∈range N f i b converges uniformly to g on s as N→∞.

Русский

Если HasProdUniformlyOn f g 𝔖 выполняется и hs ∈ 𝔖, то последовательность конечных диапазонных произведений ∏ i∈range N f i b сходится равномерно к g на s при N→∞.

LaTeX

$$$ HasProdUniformlyOn\ f\ g\ 𝔖 \to hs∈𝔖 \Rightarrow TendstoUniformlyOn(\lambda N,b. \prod_{i∈Finset.range N} f i b)\ g\ atTop\ s $$$

Lean4

@[to_additive]
theorem tendstoUniformlyOn_finsetRange {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)

Похожие утверждения