English
Coordinatewise composition: the pi construction respects the Big-O relation componentwise.
Русский
Координатная композиция сохраняет отношение Big-O по компонентам.
LaTeX
$$$\forall i,\ f_i =O_{𝕜;l} g \Rightarrow (\lambda x, f_i x) =O_{𝕜;l} g.$$$
Lean4
protected theorem pi {ι : Type*} {E : ι → Type*} [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
[∀ i, TopologicalSpace (E i)] [∀ i, ContinuousSMul 𝕜 (E i)] {f : ∀ i, α → E i} (h : ∀ i, f i =O[𝕜; l] g) :
(fun x i ↦ f i x) =O[𝕜; l] g :=
by
have := hasBasis_pi fun i ↦ nhds_basis_balanced 𝕜 (E i)
rw [← nhds_pi, ← Pi.zero_def] at this
simp only [this.isBigOTVS_iff (basis_sets _), forall_and, Prod.forall, id]
rintro I U ⟨hIf, hU, Ub⟩
have := fun i hi ↦ (h i).eventually_smallSets (U i) (hU i hi)
rcases (hIf.eventually_all.mpr this).exists_mem_of_smallSets with ⟨V, hV₀, hV⟩
use V, hV₀
refine (hIf.eventually_all.mpr hV).mono fun x hx ↦ ?_
simpa only [id, egauge_pi hIf Ub, iSup₂_le_iff]
