English
Same as the principal Big-O criterion; equivalence with a uniform bound on the norm of f relative to g over the set s.
Русский
То же самое: эквивалентность условия Big-O на множестве s через границу нормы.
LaTeX
$$$f =O[\mathcal{P}s] g \iff \exists c, \forall x \in s, \|f(x)\| \le c \|g(x)\|$$$
Lean4
@[simp]
theorem isLittleO_principal {s : Set α} : f'' =o[𝓟 s] g' ↔ ∀ x ∈ s, f'' x = 0 :=
by
refine ⟨fun h x hx ↦ norm_le_zero_iff.1 ?_, fun h ↦ ?_⟩
· simp only [isLittleO_iff] at h
have : Tendsto (fun c : ℝ => c * ‖g' x‖) (𝓝[>] 0) (𝓝 0) :=
((continuous_id.mul continuous_const).tendsto' _ _ (zero_mul _)).mono_left inf_le_left
apply le_of_tendsto_of_tendsto tendsto_const_nhds this
apply eventually_nhdsWithin_iff.2 (Eventually.of_forall (fun c hc ↦ ?_))
exact eventually_principal.1 (h hc) x hx
· apply (isLittleO_zero g' _).congr' ?_ EventuallyEq.rfl
exact fun x hx ↦ (h x hx).symm
