English
If every i in a finite list L satisfies f i =O_l g i and there exists at least one index with f i = o_l g i, then the product over i in L of f i is o_l the product over i in L of g i.
Русский
Если для каждого элемента i в списке L имеет f i =O_l g i и существует минимум один индекс с 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) \\land (\\exists i \\in L,\\; f i =o[l] g i) \\Rightarrow (\\\\lambda x. (L.map (f \\cdot x)).prod) =o[l] (\\\\lambda x. (L.map (g \\cdot x)).prod) $$$
Lean4
theorem listProd {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ L, f i =O[l] g i)
(h₂ : ∃ 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 at h₂
| cons i L
ihL =>
simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff] at h₁ h₂ ⊢
cases h₂ with
| inl hi => exact hi.mul_isBigO <| .listProd h₁.2
| inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL
