multisetProd — Mathlib

English

Same as multisetProd, but with a different indexing set; if f_i =Θ_l g_i for all i in s, then the multiset product across i∈s preserves Θ_l equivalence.

Русский

То же самое для мульти-множества: если для всех i в s выполнено f_i =Θ_l g_i, произведение по i∈s сохраняет эквивалентность Θ_l.

LaTeX

$$$ (\forall i ∈ s, f(i) =Θ[l] g(i)) \Rightarrow (\prod i ∈ s, f(i)) =Θ[l] (\prod i ∈ s, g(i)). $$$

Lean4

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

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