case intro.intro
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
L : ℝ
hL1 : L < M
hL2 : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
⊢ ‖cderiv r f z‖ < M / r
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ‖cderiv r f z‖ < M / r
obtain ⟨L, hL1, hL2⟩ : ∃ L < M, ∀ w ∈ sphere z r, ‖f w‖ ≤ L := by
  have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
  have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
  obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_forall_ge e1 e2
  exact ⟨‖f x‖, hfM x hx, hx'⟩
no goals
case intro.intro
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
L : ℝ
hL1 : L < M
hL2 : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
⊢ ‖cderiv r f z‖ < M / r
exact (norm_cderiv_le hr hL2).trans_lt ((div_lt_div_right hr).mpr hL1)
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
case intro.intro
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : ∀ (y : ℂ), y ∈ sphere z r → ‖f y‖ ≤ ‖f x‖
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_forall_ge e1 e2
no goals
case intro.intro
E : Type u_1
ι : Type ?u.28951
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hfM : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ < M
hf : ContinuousOn f (sphere z r)
e1 : Set.Nonempty (sphere z r)
e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r)
x : ℂ
hx : x ∈ sphere z r
hx' : ∀ (y : ℂ), y ∈ sphere z r → ‖f y‖ ≤ ‖f x‖
⊢ ∃ L, L < M ∧ ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ L
exact ⟨‖f x‖, hfM x hx, hx'⟩