English
A protected result asserting that continuous-within holds on the insert point when a power-series within-ball holds.
Русский
Защищённая лемма: непрерывность внутри сохраняется на вставке x, если существует разложение в шаре.
LaTeX
$$$\\text{continuousWithinAtInsert}\\; (hf) : \\text{ContinuousWithinAt}(f,(\\mathrm{insert}\\ x\\ s),x)$$$
Lean4
/-- If `f` has formal power series `∑ n, pₙ` at `x` within a set `s`, then
`f y - f z - p 1 (fun _ ↦ y - z) = O(‖(y, z) - (x, x)‖ * ‖y - z‖)` as `(y, z) → (x, x)`
within `s × s`. -/
theorem isBigO_image_sub_norm_mul_norm_sub (hf : HasFPowerSeriesWithinAt f p s x) :
(fun y : E × E => f y.1 - f y.2 - p 1 fun _ => y.1 - y.2) =O[𝓝[(insert x s) ×ˢ (insert x s)] (x, x)] fun y =>
‖y - (x, x)‖ * ‖y.1 - y.2‖ :=
by
rcases hf with ⟨r, hf⟩
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩
refine (hf.isBigO_image_sub_image_sub_deriv_principal h).mono ?_
rw [inter_comm]
exact le_principal_iff.2 (inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ r'0))
