E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖deriv f c‖ ≤ C / R
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R
set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ ≤ C / R
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖deriv f c‖ ≤ C / R
have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
  e.hasFDerivAt.comp_hasDerivAt c
    (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt
no goals
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ ≤ C / R
calc
  ‖deriv f c‖ = ‖deriv (e ∘ f) c‖ := by
    rw [this.deriv]
    exact (UniformSpace.Completion.norm_coe _).symm
  _ ≤ C / R :=
    norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
      (UniformSpace.Completion.norm_coe _).trans_le (hC z hz)
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖↑e (deriv f c)‖
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖deriv (↑e ∘ f) c‖
rw [this.deriv]
no goals
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ (z : ℂ), z ∈ sphere c R → ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (↑e ∘ f) (↑e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖↑e (deriv f c)‖
exact (UniformSpace.Completion.norm_coe _).symm