hasProdLocallyUniformlyOn_nat_one_add

English

Again a nat-indexed variant: with appropriate hypotheses, the product ∏' i (1+f_i x) converges uniformly on K.

Русский

Снова nat-инденекс: при заданных условиях произведение сходится равномерно на K.

LaTeX

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

Lean4

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

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