E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
set F : ℂ → E := fun z => (z - c) • f z
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
suffices DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c by
  rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc,
    dslope_sub_smul] at this
  have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
    continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
  rwa [hc.limUnder_eq]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousAt F c
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
refine' ⟨(differentiableOn_id.sub_const _).smul hd, _⟩
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousWithinAt F ({c}ᶜ) c
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousAt F c
rw [← continuousWithinAt_compl_self]
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[{c}ᶜ] c) (𝓝 0)
⊢ ContinuousWithinAt F ({c}ᶜ) c
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
⊢ ContinuousWithinAt F ({c}ᶜ) c
have H := ho.tendsto_inv_smul_nhds_zero
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[{c}ᶜ] c) (𝓝 0)
H' : Tendsto (fun z => (z - c) • f c) (𝓝[{c}ᶜ] c) (𝓝 (F c))
⊢ ContinuousWithinAt F ({c}ᶜ) c
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[{c}ᶜ] c) (𝓝 0)
⊢ ContinuousWithinAt F ({c}ᶜ) c
have H' : Tendsto (fun z => (z - c) • f c) (𝓝[≠] c) (𝓝 (F c)) :=
  (continuousWithinAt_id.tendsto.sub tendsto_const_nhds).smul tendsto_const_nhds
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
H : Tendsto (fun x => (x - c)⁻¹⁻¹ • (f x - f c)) (𝓝[{c}ᶜ] c) (𝓝 0)
H' : Tendsto (fun z => (z - c) • f c) (𝓝[{c}ᶜ] c) (𝓝 (F c))
⊢ ContinuousWithinAt F ({c}ᶜ) c
simpa [← smul_add, ContinuousWithinAt] using H.add H'
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this✝ : DifferentiableOn ℂ (dslope F c) s
this : DifferentiableOn ℂ (update (fun z => f z) c (deriv (fun x => (x - c) • f x) c)) s
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this : DifferentiableOn ℂ F (s \ {c}) ∧ ContinuousAt F c
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
rw [differentiableOn_compl_singleton_and_continuousAt_iff hc, ← differentiableOn_dslope hc,
  dslope_sub_smul] at this
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc✝ : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this✝ : DifferentiableOn ℂ (dslope F c) s
this : DifferentiableOn ℂ (update (fun z => f z) c (deriv (fun x => (x - c) • f x) c)) s
hc : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (deriv F c))
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this✝ : DifferentiableOn ℂ (dslope F c) s
this : DifferentiableOn ℂ (update (fun z => f z) c (deriv (fun x => (x - c) • f x) c)) s
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
have hc : Tendsto f (𝓝[≠] c) (𝓝 (deriv F c)) :=
  continuousAt_update_same.mp (this.continuousOn.continuousAt hc)
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
c : ℂ
hc✝ : s ∈ 𝓝 c
hd : DifferentiableOn ℂ f (s \ {c})
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
F : ℂ → E := fun z => (z - c) • f z
this✝ : DifferentiableOn ℂ (dslope F c) s
this : DifferentiableOn ℂ (update (fun z => f z) c (deriv (fun x => (x - c) • f x) c)) s
hc : Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (deriv F c))
⊢ DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) s
rwa [hc.limUnder_eq]