multipliableUniformlyOn_one_add — Mathlib

English

If K is compact and u is summable and ∥f_i(x)∥ ≤ u_i on K eventually, then ∏' i (1+f_i(x)) converges uniformly on K.

Русский

Если K компактно и u суммируемо, а ∥f_i(x)∥ ≤ u_i почти повсюду на K, то произведение ∏' i (1+f_i(x)) сходится равномерно на K.

LaTeX

$$$IsCompact K\\Rightarrow\\Summable u\\Rightarrow\\Eventual (\\forall x∈K, \\|f_i(x)\\| ≤ u_i) \\Rightarrow HasProdUniformlyOn (\\lambda i x, 1+f_i(x)) (\\lambda x, ∏' i, (1+f_i(x))) {K}$$$

Lean4

theorem multipliableUniformlyOn_one_add (hK : IsCompact K) (hu : Summable u)
    (h : ∀ᶠ i in cofinite, ∀ x ∈ K, ‖f i x‖ ≤ u i) (hcts : ∀ i, ContinuousOn (f i) K) :
    MultipliableUniformlyOn (fun i x ↦ 1 + f i x) { K } :=
  ⟨_, hasProdUniformlyOn_one_add hK hu h hcts⟩

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