English
For HasFPowerSeriesWithinOnBall hf, the isBigO statement for the Substitution y1,y2 yields a principal filter bound around (x,x) showing asymptotic control of differences by norms.
Русский
Для HasFPowerSeriesWithinOnBall hf неравенство isBigO для пары y1,y2 задаёт предел в главной филтере около (x,x) и управляет разностями по нормам.
LaTeX
$$$\text{IsBigO}\; (\mathcal{P} (\text{EMetric.ball} (x,x) r'))\; (f(y_1) - f(y_2) - p(1)(y_1-y_2)) \; (y) \text{bounded by } C \cdot \|y_1 - x\| \|y_2 - x\| \cdot \|y_1 - y_2\|$$$
Lean4
/-- If `f` has formal power series `∑ n, pₙ` within a set, on a ball of radius `r`, then for `y, z`
in any smaller ball, the norm of the difference `f y - f z - p 1 (fun _ ↦ y - z)` is bounded above
by `C * (max ‖y - x‖ ‖z - x‖) * ‖y - z‖`. -/
theorem image_sub_sub_deriv_le (hf : HasFPowerSeriesWithinOnBall f p s x r) (hr : r' < r) :
∃ C,
∀ᵉ (y ∈ insert x s ∩ EMetric.ball x r') (z ∈ insert x s ∩ EMetric.ball x r'),
‖f y - f z - p 1 fun _ => y - z‖ ≤ C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖ :=
by
have := hf.isBigO_image_sub_image_sub_deriv_principal hr
simp only [isBigO_principal, mem_inter_iff, EMetric.mem_ball, Prod.edist_eq, max_lt_iff, mem_prod, norm_mul,
Real.norm_eq_abs, abs_norm, and_imp, Prod.forall, mul_assoc] at this ⊢
rcases this with ⟨C, hC⟩
exact ⟨C, fun y ys hy z zs hz ↦ hC y z hy hz ys zs⟩
