listProd — Mathlib

English

If for every i in a finite set S we have f_i =Θ_l g_i, then the finite product over i∈S of f_i is Θ_l the product over i∈S of g_i.

Русский

Если для каждого i в конечном множестве S выполняется f_i =Θ_l g_i, то произведение по i∈S f_i эквивалентно Θ_l произведению по i∈S g_i.

LaTeX

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

Lean4

theorem listProd {ι : Type*} {L : List ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'} (h : ∀ i ∈ L, f i =Θ[l] g i) :
    (fun x ↦ (L.map (f · x)).prod) =Θ[l] (fun x ↦ (L.map (g · x)).prod) :=
  ⟨.listProd fun i hi ↦ (h i hi).isBigO, .listProd fun i hi ↦ (h i hi).symm.isBigO⟩

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