English
If a function f is Big-O with respect to a product filter l ×ˢ l' of f and g, then for almost every a in l, the section x ↦ f{ fst := a, snd := x } is Big-O with respect to l' of the corresponding section g{ fst := a, snd := x }.
Русский
Если функция f ограничена по произведению фильтров l ×ˢ l', то практически для почти всех a в l секция x ↦ f{ fst := a, snd := x } ограничена относительно соответствующей секции g{ fst := a, snd := x } по l'.
LaTeX
$$$\text{If } \text{IsBigO} (\text{Filter.instSProd.sprod } l\, l')\, f\, g \Rightarrow \forall^\infty a\in l,\; f\langle a, \cdot \rangle =O_{l'} (g\langle a, \cdot \rangle)$.$$
Lean4
protected theorem fiberwise_right : f =O[l ×ˢ l'] g → ∀ᶠ a in l, (f ⟨a, ·⟩) =O[l'] (g ⟨a, ·⟩) :=
by
simp only [isBigO_iff, eventually_iff, mem_prod_iff]
rintro ⟨c, t₁, ht₁, t₂, ht₂, ht⟩
exact mem_of_superset ht₁ fun _ ha ↦ ⟨c, mem_of_superset ht₂ fun _ hb ↦ ht ⟨ha, hb⟩⟩
