English
Dually to the right fiberwise statement, if IsBigO on the product with l ×ˢ l' holds, then almost surely the slices over β satisfy a corresponding bound with l and l'.
Русский
Аналогично по левому компоненту: если существует.bound на произведение по l ×ˢ l', то соответствующие секции по β удовлетворяют аналогичному ограничению.
LaTeX
$$$\text{fiberwise_left} : \text{IsBigO} (\text{Filter.instSProd.sprod } l l')\, f\, g \Rightarrow \forall^\infty b \in l', \; f(\cdot, b) =O_l (g(\cdot, b))$$$
Lean4
protected theorem comp_fst : f =o[l] g → (f ∘ Prod.fst) =o[l ×ˢ l'] (g ∘ Prod.fst) :=
by
simp only [isLittleO_iff, eventually_prod_iff]
exact fun h _ hc ↦ ⟨_, h hc, fun _ ↦ True, eventually_true l', fun {_} h {_} _ ↦ h⟩
