tendstoUniformlyOn_tsum_nat_log_one_add

English

If f and u satisfy summability and uniform bound hypotheses, then the sequence of partial sums ∑_{m<n} log(1+f(m,x)) converges uniformly on atTop to the full sum ∑_{n} log(1+f(n,x)) on K.

Русский

Если выполнены условия суммируемости и ограничений, частичные суммы ∑_{m<n} log(1+f(m,x)) сходятся равномерно к полной сумме ∑_{n} log(1+f(n,x)) на K.

LaTeX

$$$TendstoUniformlyOn\\ (\\lambda n x, \\sum_{m< n} \\log(1+f_m(x)))\\ (\\lambda x, \\sum_{n} \\log(1+f_n(x)))\\ atTop\\ K$$$

Lean4

theorem tendstoUniformlyOn_tsum_nat_log_one_add {f : ℕ → α → ℂ} {u : ℕ → ℝ} (hu : Summable u)
    (h : ∀ᶠ n in atTop, ∀ x ∈ K, ‖f n x‖ ≤ u n) :
    TendstoUniformlyOn (fun n x ↦ ∑ m ∈ Finset.range n, log (1 + f m x)) (fun x ↦ ∑' n, log (1 + f n x)) atTop K :=
  by
  rw [← Nat.cofinite_eq_atTop] at h
  exact (hu.hasSumUniformlyOn_log_one_add h).tendstoUniformlyOn_finsetRange rfl

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