English
If for every i in a finite list L we have f(i) =O_l(g(i)), then the product over i in L of f(i) is O_l of the product over i in L of g(i).
Русский
Если для каждого элемента i из конечного списка L выполняется f(i) =O_l(g(i)), то произведение по i∈L f(i) имеет порядок O_l произведения по i∈L g(i).
LaTeX
$$$ \\forall i \\in L,\\; f(i) =O[l] g(i) \\Rightarrow \\left( x \\mapsto \\prod_{i \\in L} f(i)(x) \\right) =O[l] \\left( x \\mapsto \\prod_{i \\in L} g(i)(x) \\right) $$$
Lean4
theorem listProd {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ L, f i =O[l] g i) :
(fun x ↦ (L.map (f · x)).prod) =O[l] (fun x ↦ (L.map (g · x)).prod) := by
induction L with
| nil => simp [isBoundedUnder_const]
| cons i L ihL =>
simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢
exact hf.1.mul (ihL hf.2)
