English
If ε > 0 and x is differentiable within Ici x, there exists a radius R > 0 such that for all r ∈ (0,R), x ∈ A(f, derivWithin f (Ici x) x, r, ε).
Русский
Если ε>0 и x дифференцируем в Ici x, существует R>0 такое, что для всех r в (0,R) выполняется x ∈ A(f, derivWithin f (Ici x) x, r, ε).
LaTeX
$$$\\exists R>0, \\forall r \\in (0,R),\, x \\in A f (derivWithin f (Ici x) x) r ε$$$
Lean4
theorem mem_A_of_differentiable {ε : ℝ} (hε : 0 < ε) {x : ℝ} (hx : DifferentiableWithinAt ℝ f (Ici x) x) :
∃ R > 0, ∀ r ∈ Ioo (0 : ℝ) R, x ∈ A f (derivWithin f (Ici x) x) r ε :=
by
have := hx.hasDerivWithinAt
simp_rw [hasDerivWithinAt_iff_isLittleO, isLittleO_iff] at this
rcases mem_nhdsGE_iff_exists_Ico_subset.1 (this (half_pos hε)) with ⟨m, xm, hm⟩
refine ⟨m - x, by linarith [show x < m from xm], fun r hr => ?_⟩
have : r ∈ Ioc (r / 2) r := ⟨half_lt_self hr.1, le_rfl⟩
refine ⟨r, this, fun y hy z hz => ?_⟩
calc
‖f z - f y - (z - y) • derivWithin f (Ici x) x‖ =
‖f z - f x - (z - x) • derivWithin f (Ici x) x - (f y - f x - (y - x) • derivWithin f (Ici x) x)‖ :=
by congr 1; simp only [sub_smul]; abel
_ ≤ ‖f z - f x - (z - x) • derivWithin f (Ici x) x‖ + ‖f y - f x - (y - x) • derivWithin f (Ici x) x‖ :=
(norm_sub_le _ _)
_ ≤ ε / 2 * ‖z - x‖ + ε / 2 * ‖y - x‖ :=
(add_le_add (hm ⟨hz.1, hz.2.trans_lt (by linarith [hr.2])⟩) (hm ⟨hy.1, hy.2.trans_lt (by linarith [hr.2])⟩))
_ ≤ ε / 2 * r + ε / 2 * r := by
gcongr
· rw [Real.norm_of_nonneg] <;> linarith [hz.1, hz.2]
· rw [Real.norm_of_nonneg] <;> linarith [hy.1, hy.2]
_ = ε * r := by ring
