English
Let s be a convex subset of R, x0 in s, and f: R → E be such that f is differentiable along s with derivative f′(x) at each x ∈ s. If f′ = o_{𝓝[s] x0} (x − x0)^n for some n ∈ N, then f(x) − f(x0) = o_{𝓝[s] x0} (x − x0)^(n+1); in particular, the increment is of strictly higher order than the (n+1)th power of the distance to x0.
Русский
Пусть s ⊆ R выпукло; x0 ∈ s; f: R → E столь, что f дифференцируема по s и производная в точке x ∈ s равна f′(x). Если f′ = o_{𝓝[s] x0} (x − x0)^n для некоторого n ∈ N, то f(x) − f(x0) = o_{𝓝[s] x0} (x − x0)^(n+1); т.е. при этом прирост функции имеет более высокий порядок по отношению к (x − x0)^(n+1).
LaTeX
$$$$ (f(x) - f(x_0)) = o_{\mathcal{N}_{s}(x_0)}\big((x - x_0)^{n+1}\big). $$$$
Lean4
theorem isLittleO_pow_succ_real {f f' : ℝ → E} {x₀ : ℝ} {n : ℕ} {s : Set ℝ} (hs : Convex ℝ s) (hx₀s : x₀ ∈ s)
(hff' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf' : f' =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ n) :
(fun x ↦ f x - f x₀) =o[𝓝[s] x₀] fun x ↦ (x - x₀) ^ (n + 1) :=
by
have h := hs.isLittleO_pow_succ hx₀s hff' ?_ (n := n)
· rw [Asymptotics.isLittleO_iff] at h ⊢
simpa using h
· rw [Asymptotics.isLittleO_iff] at hf' ⊢
convert hf' using 4 with c hc x
simp
