comp_summable_norm — Mathlib

English

If f: E → F is o near 0 with respect to id (i.e., f = O_{𝓝0} id) and g: ι → E has summable norm, then the norm of f composed with g, i.e., ∥f(g(n))∥, is summable over n.

Русский

Пусть f: E→F удовлетворяет f = O_{𝓝0} id, и g: ι → E имеет суммируемую норму. Тогда ∥f(g(n))∥ суммируема по n.

LaTeX

$$$ (f =O_{𝓝 0} \\mathrm{id}) \\wedge (Summable \\ ‖g·‖) \\Rightarrow Summable (\\|f \\circ g\\|) $$$

Lean4

theorem comp_summable_norm {ι E F : Type*} [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] {f : E → F} {g : ι → E}
    (hf : f =O[𝓝 0] id) (hg : Summable (‖g ·‖)) : Summable (‖f <| g ·‖) :=
  summable_of_isBigO hg <| hf.norm_norm.comp_tendsto <| tendsto_zero_iff_norm_tendsto_zero.2 hg.tendsto_cofinite_zero

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