comp_summable — Mathlib

English

If f is Asymptotics.IsBigO w.r.t. id and g is summable, then f ∘ g is summable.

Русский

Если f =O (id) и g суммируема, то f ∘ g суммируема.

LaTeX

$$$\\text{Asymptotics.IsBigO} (\\\\nhds 0) f id \\\\Rightarrow Summable g \\\\Rightarrow Summable (f \\\\circ g)$$$

Lean4

theorem comp_summable {ι E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
    [NormedAddCommGroup F] [CompleteSpace F] {f : E → F} (hf : f =O[𝓝 0] id) {g : ι → E} (hg : Summable g) :
    Summable (f ∘ g) :=
  .of_norm <| hf.comp_summable_norm hg.norm

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