finsetProd — Mathlib

English

As with finsetProd, if each f_i =Θ_l g_i for i in a finite set S, then the finite product over i in S of f_i is Θ_l the product over i in S of g_i.

Русский

Аналогично для конечного множества: если для каждого i∈S выполняется f_i =Θ_l g_i, то произведение по i∈S сохраняет Θ-equivalence.

LaTeX

$$$ (\forall i ∈ S, f(i) =Θ[l] g(i)) \Rightarrow (\prod_{i ∈ S} f(i)) =Θ[l] (\prod_{i ∈ S} g(i)). $$$

Lean4

theorem finsetProd {ι : Type*} {s : Finset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'} (h : ∀ i ∈ s, f i =Θ[l] g i) :
    (∏ i ∈ s, f i ·) =Θ[l] (∏ i ∈ s, g i ·) :=
  ⟨.finsetProd fun i hi ↦ (h i hi).isBigO, .finsetProd fun i hi ↦ (h i hi).symm.isBigO⟩

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