English
If for every i in a multiset s we have f(i) =O_l(g(i)), then the product over s of f(i) is O_l the product over s of g(i).
Русский
Если для каждого элемента i в мультисете s выполняется f(i) =O_l(g(i)), то произведение по i∈s f(i) есть порядок O_l произведения по i∈s g(i).
LaTeX
$$$ (\\forall i \\in s,\\; f i =O[l] g i) \\Rightarrow (\\lambda x. (s.map (f \\cdot x)).prod) =O[l] (\\lambda x. (s.map (g \\cdot x)).prod) $$$
Lean4
theorem multisetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜] {s : Multiset ι} {f : ι → α → R}
{g : ι → α → 𝕜} (hf : ∀ i ∈ s, f i =O[l] g i) :
(fun x ↦ (s.map (f · x)).prod) =O[l] (fun x ↦ (s.map (g · x)).prod) :=
by
obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
exact mod_cast IsBigO.listProd hf
