English
If f1 → f2 and g1 → g2 are asymptotically equivalent, then IsBigOWith c l f1 g1 is equivalent to IsBigOWith c l f2 g2.
Русский
Если f1 ≈ f2 и g1 ≈ g2 с точки зрения асимптотики, то IsBigOWith c l f1 g1 эквивалентно IsBigOWith c l f2 g2.
LaTeX
$$$ IsBigOWith\ c\ l\ f1\ g1 \rightarrow f1 \sim f2 \land g1 \sim g2 \Rightarrow IsBigOWith c l f2 g2 $$$
Lean4
theorem isLittleO_iff_nat_mul_le_aux (h₀ : (∀ x, 0 ≤ ‖f x‖) ∨ ∀ x, 0 ≤ ‖g x‖) :
f =o[l] g ↔ ∀ n : ℕ, ∀ᶠ x in l, ↑n * ‖f x‖ ≤ ‖g x‖ :=
by
constructor
· rintro H (_ | n)
· refine (H.def one_pos).mono fun x h₀' => ?_
rw [Nat.cast_zero, zero_mul]
refine h₀.elim (fun hf => (hf x).trans ?_) fun hg => hg x
rwa [one_mul] at h₀'
· have : (0 : ℝ) < n.succ := Nat.cast_pos.2 n.succ_pos
exact (isBigOWith_inv this).1 (H.def' <| inv_pos.2 this)
· refine fun H => isLittleO_iff.2 fun ε ε0 => ?_
rcases exists_nat_gt ε⁻¹ with ⟨n, hn⟩
have hn₀ : (0 : ℝ) < n := (inv_pos.2 ε0).trans hn
refine ((isBigOWith_inv hn₀).2 (H n)).bound.mono fun x hfg => ?_
refine hfg.trans (mul_le_mul_of_nonneg_right (inv_le_of_inv_le₀ ε0 hn.le) ?_)
refine h₀.elim (fun hf => nonneg_of_mul_nonneg_right ((hf x).trans hfg) ?_) fun h => h x
exact inv_pos.2 hn₀
