hasProdUniformlyOn_nat_one_add — Mathlib

English

The natural-index version of HasProdUniformlyOn_one_add: with f_n : α → R indexed by n ∈ ℕ, the product ∏' i (1+f_i(x)) converges uniformly on K under the same hypotheses.

Русский

Натуральный вариант HasProdUniformlyOn_one_add: для f_n : α → R, произведение ∏' i (1+f_i(x)) сходится равномерно на K.

LaTeX

$$$HasProdUniformlyOn\\ (\\lambda n x, 1+f_n(x))\\ (\\lambda x, ∏' i, (1+f_i(x)))\\ {K}$$$

Lean4

/-- This is a version of `hasProdUniformlyOn_one_add` for sequences indexed by `ℕ`. -/
theorem 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

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