no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ HasDerivAtFilter f f' x L ↔ Tendsto (fun y => slope f x y - (y - x)⁻¹ • (y - x) • f') L (𝓝 0)
simp only [hasDerivAtFilter_iff_tendsto, ← norm_inv, ← norm_smul,
  ← tendsto_zero_iff_norm_tendsto_zero, slope_def_module, smul_sub]
no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ ∀ (x_1 : 𝕜), ¬x_1 ∈ {x}ᶜ → slope f x x_1 - (x_1 - x)⁻¹ • (x_1 - x) • f' = 0
simp
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
y : 𝕜
hy : y ∈ {x}ᶜ
⊢ slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ (fun y => slope f x y - (y - x)⁻¹ • (y - x) • f') =ᶠ[L ⊓ 𝓟 ({x}ᶜ)] fun y => slope f x y - f'
refine (EqOn.eventuallyEq fun y hy ↦ ?_).filter_mono inf_le_right
no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
y : 𝕜
hy : y ∈ {x}ᶜ
⊢ slope f x y - (y - x)⁻¹ • (y - x) • f' = slope f x y - f'
rw [inv_smul_smul₀ (sub_ne_zero.2 hy) f']
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0) ↔
    Tendsto ((fun x => x - f') ∘ slope f x) (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0)
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0) ↔ Tendsto (slope f x) (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 f')
rw [← nhds_translation_sub f', tendsto_comap_iff]
no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x✝ : 𝕜
s t : Set 𝕜
L✝ L₁ L₂ : Filter 𝕜
x : 𝕜
L : Filter 𝕜
⊢ Tendsto (fun y => slope f x y - f') (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0) ↔
    Tendsto ((fun x => x - f') ∘ slope f x) (L ⊓ 𝓟 ({x}ᶜ)) (𝓝 0)
rfl