English
If for every i in a multiset s we have f i =O_l g i and there exists some i in s with 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 с 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) \\\\land (\\\\Exists 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 : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i) (h₂ : ∃ 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 IsLittleO.listProd h₁ h₂
