English
If c with 1<||c||, and x ∈ A f L1 r ε and x ∈ A f L2 r ε, then ||L1−L2|| ≤ 4||c|| ε.
Русский
При c с 1<||c||, если x∈A f L1 r ε и x∈A f L2 r ε, то ||L1−L2|| ≤ 4||c|| ε.
LaTeX
$$$$\|L_1 - L_2\| \le 4 \|c\| \varepsilon,$$ при условиях $$1<\|c\|, \; x\in A(f,L_1,r,\varepsilon) \;\text{и}\; x\in A(f,L_2,r,\varepsilon).$$$$
Lean4
theorem mem_A_of_differentiable {ε : ℝ} (hε : 0 < ε) {x : E} (hx : DifferentiableAt 𝕜 f x) :
∃ R > 0, ∀ r ∈ Ioo (0 : ℝ) R, x ∈ A f (fderiv 𝕜 f x) r ε :=
by
let δ := (ε / 2) / 2
obtain ⟨R, R_pos, hR⟩ : ∃ R > 0, ∀ y ∈ ball x R, ‖f y - f x - fderiv 𝕜 f x (y - x)‖ ≤ δ * ‖y - x‖ :=
eventually_nhds_iff_ball.1 <| hx.hasFDerivAt.isLittleO.bound <| by positivity
refine ⟨R, R_pos, fun r hr => ?_⟩
have : r ∈ Ioc (r / 2) r := right_mem_Ioc.2 <| half_lt_self hr.1
refine ⟨r, this, fun y hy z hz => ?_⟩
calc
‖f z - f y - (fderiv 𝕜 f x) (z - y)‖ =
‖f z - f x - (fderiv 𝕜 f x) (z - x) - (f y - f x - (fderiv 𝕜 f x) (y - x))‖ :=
by simp only [map_sub]; abel_nf
_ ≤ ‖f z - f x - (fderiv 𝕜 f x) (z - x)‖ + ‖f y - f x - (fderiv 𝕜 f x) (y - x)‖ := (norm_sub_le _ _)
_ ≤ δ * ‖z - x‖ + δ * ‖y - x‖ :=
(add_le_add (hR _ (ball_subset_ball hr.2.le hz)) (hR _ (ball_subset_ball hr.2.le hy)))
_ ≤ δ * r + δ * r := by rw [mem_ball_iff_norm] at hz hy; gcongr
_ = (ε / 2) * r := by ring
_ < ε * r := by gcongr; exacts [hr.1, half_lt_self hε]
