[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
have hM : 0 ≤ M := by
  obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
  exact (norm_nonneg _).trans (hf w hw)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
⊢ 0 ≤ M
[PROOFSTEP]
obtain ⟨w, hw⟩ : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
[GOAL]
case intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ 0 ≤ M
[PROOFSTEP]
exact (norm_nonneg _).trans (hf w hw)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
have h1 : ∀ w ∈ sphere z r, ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2 :=
  by
  intro w hw
  simp only [mem_sphere_iff_norm, norm_eq_abs] at hw 
  simp only [norm_smul, inv_mul_eq_div, hw, norm_eq_abs, map_inv₀, Complex.abs_pow]
  exact div_le_div hM (hf w hw) (sq_pos_of_pos hr) le_rfl
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
⊢ ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
[PROOFSTEP]
intro w hw
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : w ∈ sphere z r
⊢ ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
[PROOFSTEP]
simp only [mem_sphere_iff_norm, norm_eq_abs] at hw 
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : ↑abs (w - z) = r
⊢ ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
[PROOFSTEP]
simp only [norm_smul, inv_mul_eq_div, hw, norm_eq_abs, map_inv₀, Complex.abs_pow]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
w : ℂ
hw : ↑abs (w - z) = r
⊢ ‖f w‖ / r ^ 2 ≤ M / r ^ 2
[PROOFSTEP]
exact div_le_div hM (hf w hw) (sq_pos_of_pos hr) le_rfl
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
have h2 := circleIntegral.norm_integral_le_of_norm_le_const hr.le h1
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ ‖cderiv r f z‖ ≤ M / r
[PROOFSTEP]
simp only [cderiv, norm_smul]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ ‖(2 * ↑π * I)⁻¹‖ * ‖∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r
[PROOFSTEP]
refine' (mul_le_mul le_rfl h2 (norm_nonneg _) (norm_nonneg _)).trans (le_of_eq _)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ ‖(2 * ↑π * I)⁻¹‖ * (2 * π * r * (M / r ^ 2)) = M / r
[PROOFSTEP]
field_simp [_root_.abs_of_nonneg Real.pi_pos.le, Real.pi_pos.ne.symm, hr.ne.symm]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ∀ (w : ℂ), w ∈ sphere z r → ‖f w‖ ≤ M
hM : 0 ≤ M
h1 : ∀ (w : ℂ), w ∈ sphere z r → ‖((w - z) ^ 2)⁻¹ • f w‖ ≤ M / r ^ 2
h2 : ‖∮ (z_1 : ℂ) in C(z, r), ((z_1 - z) ^ 2)⁻¹ • f z_1‖ ≤ 2 * π * r * (M / r ^ 2)
⊢ 2 * π * r * M * r = M * (2 * π * r ^ 2)
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
[PROOFSTEP]
have h1 : ContinuousOn (fun w : ℂ => ((w - z) ^ 2)⁻¹) (sphere z r) :=
  by
  refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne _
  rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw 
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
⊢ ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
[PROOFSTEP]
refine' ((continuous_id'.sub continuous_const).pow 2).continuousOn.inv₀ fun w hw h => hr.ne _
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
w : ℂ
hw : w ∈ sphere z r
h : (w - z) ^ 2 = 0
⊢ 0 = r
[PROOFSTEP]
rwa [mem_sphere_iff_norm, sq_eq_zero_iff.mp h, norm_zero] at hw 
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ cderiv r (f - g) z = cderiv r f z - cderiv r g z
[PROOFSTEP]
simp_rw [cderiv, ← smul_sub]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ ((2 * ↑π * I)⁻¹ • ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (2 * ↑π * I)⁻¹ • ((∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hr : 0 < r
hf : ContinuousOn f (sphere z r)
hg : ContinuousOn g (sphere z r)
h1 : ContinuousOn (fun w => ((w - z) ^ 2)⁻¹) (sphere z r)
⊢ (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • (f - g) w) =
    (∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • f w) - ∮ (w : ℂ) in C(z, r), ((w - z) ^ 2)⁻¹ • g w
[PROOFSTEP]
simpa only [Pi.sub_apply, smul_sub] using
  circleIntegral.integral_sub ((h1.smul hf).circleIntegrable hr.le) ((h1.smul hg).circleIntegrable hr.le)
[GOAL]
E : Type u_1
ι : Type u_2
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
[PROOFSTEP]
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'⟩
[GOAL]
E : Type u_1
ι : Type u_2
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
[PROOFSTEP]
have e1 : (sphere z r).Nonempty := NormedSpace.sphere_nonempty.mpr hr.le
[GOAL]
E : Type u_1
ι : Type u_2
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
[PROOFSTEP]
have e2 : ContinuousOn (fun w => ‖f w‖) (sphere z r) := continuous_norm.comp_continuousOn hf
[GOAL]
E : Type u_1
ι : Type u_2
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
[PROOFSTEP]
obtain ⟨x, hx, hx'⟩ := (isCompact_sphere z r).exists_forall_ge e1 e2
[GOAL]
case intro.intro
E : Type u_1
ι : Type u_2
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
[PROOFSTEP]
exact ⟨‖f x‖, hfM x hx, hx'⟩
[GOAL]
case intro.intro
E : Type u_1
ι : Type u_2
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
[PROOFSTEP]
exact (norm_cderiv_le hr hL2).trans_lt ((div_lt_div_right hr).mpr hL1)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
[PROOFSTEP]
rcases φ.eq_or_neBot with rfl | hne
[GOAL]
case inl
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
F : ι → ℂ → E
f g : ℂ → E
hδ : 0 < δ
hF : TendstoUniformlyOn F f ⊥ (cthickening δ K)
hFn : ∀ᶠ (n : ι) in ⊥, ContinuousOn (F n) (cthickening δ K)
⊢ TendstoUniformlyOn (cderiv δ ∘ F) (cderiv δ f) ⊥ K
[PROOFSTEP]
simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
[PROOFSTEP]
have e1 : ContinuousOn f (cthickening δ K) := TendstoUniformlyOn.continuousOn hF hFn
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : TendstoUniformlyOn F f φ (cthickening δ K)
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
⊢ TendstoUniformlyOn (Complex.cderiv δ ∘ F) (Complex.cderiv δ f) φ K
[PROOFSTEP]
rw [tendstoUniformlyOn_iff] at hF ⊢
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
⊢ ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ K → dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
[PROOFSTEP]
rintro ε hε
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
⊢ ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ K → dist (Complex.cderiv δ f x) ((Complex.cderiv δ ∘ F) n x) < ε
[PROOFSTEP]
filter_upwards [hF (ε * δ) (mul_pos hε hδ), hFn] with n h h' z hz
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h : ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε * δ
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
⊢ dist (Complex.cderiv δ f z) ((Complex.cderiv δ ∘ F) n z) < ε
[PROOFSTEP]
simp_rw [dist_eq_norm] at h ⊢
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
have e2 : ∀ w ∈ sphere z δ, ‖f w - F n w‖ < ε * δ := fun w hw1 =>
  h w (closedBall_subset_cthickening hz δ (sphere_subset_closedBall hw1))
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
e2 : ∀ (w : ℂ), w ∈ sphere z δ → ‖f w - F n w‖ < ε * δ
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
have e3 := sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ)
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
e2 : ∀ (w : ℂ), w ∈ sphere z δ → ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
have hf : ContinuousOn f (sphere z δ) := e1.mono (sphere_subset_closedBall.trans (closedBall_subset_cthickening hz δ))
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hF : ∀ (ε : ℝ), ε > 0 → ∀ᶠ (n : ι) in φ, ∀ (x : ℂ), x ∈ cthickening δ K → dist (f x) (F n x) < ε
hδ : 0 < δ
hFn : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
hne : NeBot φ
e1 : ContinuousOn f (cthickening δ K)
ε : ℝ
hε : ε > 0
n : ι
h' : ContinuousOn (F n) (cthickening δ K)
z : ℂ
hz : z ∈ K
h : ∀ (x : ℂ), x ∈ cthickening δ K → ‖f x - F n x‖ < ε * δ
e2 : ∀ (w : ℂ), w ∈ sphere z δ → ‖f w - F n w‖ < ε * δ
e3 : sphere z δ ⊆ cthickening δ K
hf : ContinuousOn f (sphere z δ)
⊢ ‖Complex.cderiv δ f z - (Complex.cderiv δ ∘ F) n z‖ < ε
[PROOFSTEP]
simpa only [mul_div_cancel _ hδ.ne.symm] using norm_cderiv_sub_lt hδ e2 hf (h'.mono e3)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
have h1 : ∀ᶠ n in φ, ContinuousOn (F n) (cthickening δ K) := by
  filter_upwards [hF] with n h using h.continuousOn.mono hKU
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
⊢ ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
[PROOFSTEP]
filter_upwards [hF] with n h using h.continuousOn.mono hKU
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
have h2 : IsCompact (cthickening δ K) := isCompact_of_isClosed_bounded isClosed_cthickening hK.bounded.cthickening
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
have h3 : TendstoUniformlyOn F f φ (cthickening δ K) :=
  (tendstoLocallyUniformlyOn_iff_forall_isCompact hU).mp hf (cthickening δ K) hKU h2
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
⊢ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
apply (h3.cderiv hδ h1).congr
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
⊢ ∀ᶠ (n : ι) in φ, EqOn ((cderiv δ ∘ F) n) ((deriv ∘ F) n) K
[PROOFSTEP]
filter_upwards [hF] with n h z hz
[GOAL]
case h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z✝ : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
δ : ℝ
hδ : 0 < δ
hK : IsCompact K
hU : IsOpen U
hKU : cthickening δ K ⊆ U
h1 : ∀ᶠ (n : ι) in φ, ContinuousOn (F n) (cthickening δ K)
h2 : IsCompact (cthickening δ K)
h3 : TendstoUniformlyOn F f φ (cthickening δ K)
n : ι
h : DifferentiableOn ℂ (F n) U
z : ℂ
hz : z ∈ K
⊢ (cderiv δ ∘ F) n z = (deriv ∘ F) n z
[PROOFSTEP]
exact cderiv_eq_deriv hU h hδ ((closedBall_subset_cthickening hz δ).trans hKU)
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
⊢ ∃ δ, δ > 0 ∧ cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
obtain ⟨δ, hδ, hKδ⟩ := hK.exists_cthickening_subset_open hU hKU
[GOAL]
case intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hK : IsCompact K
hU : IsOpen U
hKU : K ⊆ U
δ : ℝ
hδ : 0 < δ
hKδ : cthickening δ K ⊆ U
⊢ ∃ δ, δ > 0 ∧ cthickening δ K ⊆ U ∧ TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
[PROOFSTEP]
exact ⟨δ, hδ, hKδ, tendstoUniformlyOn_deriv_of_cthickening_subset hf hF hδ hK hU hKδ⟩
[GOAL]
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ DifferentiableOn ℂ f U
[PROOFSTEP]
rintro x hx
[GOAL]
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
obtain ⟨K, ⟨hKx, hK⟩, hKU⟩ := (compact_basis_nhds x).mem_iff.mp (hU.mem_nhds hx)
[GOAL]
case intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
obtain ⟨δ, _, _, h1⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h2 : interior K ⊆ U := interior_subset.trans hKU
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h3 : ∀ᶠ n in φ, DifferentiableOn ℂ (F n) (interior K)
[GOAL]
case h3
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
⊢ ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
filter_upwards [hF] with n h using h.mono h2
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h4 : TendstoLocallyUniformlyOn F f φ (interior K) := hf.mono h2
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K) :=
  h1.tendstoLocallyUniformlyOn.mono interior_subset
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h6 : ∀ x ∈ interior K, HasDerivAt f (cderiv δ f x) x := fun x h =>
  hasDerivAt_of_tendsto_locally_uniformly_on' isOpen_interior h5 h3 (fun _ => h4.tendsto_at) h
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
h6 : ∀ (x : ℂ), x ∈ interior K → HasDerivAt f (cderiv δ f x) x
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
have h7 : DifferentiableOn ℂ f (interior K) := fun x hx => (h6 x hx).differentiableAt.differentiableWithinAt
[GOAL]
case intro.intro.intro.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
inst✝¹ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
inst✝ : NeBot φ
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
x : ℂ
hx : x ∈ U
K : Set ℂ
hKU : K ⊆ U
hKx : K ∈ 𝓝 x
hK : IsCompact K
δ : ℝ
left✝¹ : δ > 0
left✝ : cthickening δ K ⊆ U
h1 : TendstoUniformlyOn (deriv ∘ F) (cderiv δ f) φ K
h2 : interior K ⊆ U
h3 : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) (interior K)
h4 : TendstoLocallyUniformlyOn F f φ (interior K)
h5 : TendstoLocallyUniformlyOn (deriv ∘ F) (cderiv δ f) φ (interior K)
h6 : ∀ (x : ℂ), x ∈ interior K → HasDerivAt f (cderiv δ f x) x
h7 : DifferentiableOn ℂ f (interior K)
⊢ DifferentiableWithinAt ℂ f U x
[PROOFSTEP]
exact (h7.differentiableAt (interior_mem_nhds.mpr hKx)).differentiableWithinAt
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ TendstoLocallyUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ U
[PROOFSTEP]
rw [tendstoLocallyUniformlyOn_iff_forall_isCompact hU]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
⊢ ∀ (K : Set ℂ), K ⊆ U → IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
rcases φ.eq_or_neBot with rfl | hne
[GOAL]
case inl
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
F : ι → ℂ → E
f g : ℂ → E
hU : IsOpen U
hf : TendstoLocallyUniformlyOn F f ⊥ U
hF : ∀ᶠ (n : ι) in ⊥, DifferentiableOn ℂ (F n) U
⊢ ∀ (K : Set ℂ), K ⊆ U → IsCompact K → TendstoUniformlyOn (deriv ∘ F) (deriv f) ⊥ K
[PROOFSTEP]
simp only [TendstoUniformlyOn, eventually_bot, imp_true_iff]
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
⊢ ∀ (K : Set ℂ), K ⊆ U → IsCompact K → TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
rintro K hKU hK
[GOAL]
case inr
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
obtain ⟨δ, hδ, hK4, h⟩ := exists_cthickening_tendstoUniformlyOn hf hF hK hU hKU
[GOAL]
case inr.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K✝ : Set ℂ
z : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K
⊢ TendstoUniformlyOn (_root_.deriv ∘ F) (_root_.deriv f) φ K
[PROOFSTEP]
refine' h.congr_right fun z hz => cderiv_eq_deriv hU (hf.differentiableOn hF hU) hδ _
[GOAL]
case inr.intro.intro.intro
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K✝ : Set ℂ
z✝ : ℂ
M r δ✝ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
hf : TendstoLocallyUniformlyOn F f φ U
hF : ∀ᶠ (n : ι) in φ, DifferentiableOn ℂ (F n) U
hU : IsOpen U
hne : NeBot φ
K : Set ℂ
hKU : K ⊆ U
hK : IsCompact K
δ : ℝ
hδ : δ > 0
hK4 : cthickening δ K ⊆ U
h : TendstoUniformlyOn (_root_.deriv ∘ F) (cderiv δ f) φ K
z : ℂ
hz : z ∈ K
⊢ closedBall z δ ⊆ U
[PROOFSTEP]
exact (closedBall_subset_cthickening hz δ).trans hK4
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
[PROOFSTEP]
classical
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
refine' hc.differentiableOn (eventually_of_forall fun s => _) hU
exact DifferentiableOn.sum fun i _ => hf i
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
[PROOFSTEP]
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
[PROOFSTEP]
refine' hc.differentiableOn (eventually_of_forall fun s => _) hU
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn ℂ (fun x => Finset.sum s fun n => F n x) U
[PROOFSTEP]
exact DifferentiableOn.sum fun i _ => hf i
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
⊢ HasSum (fun i => deriv (F i) z) (deriv (fun w => ∑' (i : ι), F i w) z)
[PROOFSTEP]
rw [HasSum]
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
⊢ Tendsto (fun s => Finset.sum s fun b => deriv (F b) z) atTop (𝓝 (deriv (fun w => ∑' (i : ι), F i w) z))
[PROOFSTEP]
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
[GOAL]
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ Tendsto (fun s => Finset.sum s fun b => deriv (F b) z) atTop (𝓝 (deriv (fun w => ∑' (i : ι), F i w) z))
[PROOFSTEP]
convert (hc.deriv (eventually_of_forall fun s => DifferentiableOn.sum fun i _ => hf i) hU).tendsto_at hz using 1
[GOAL]
case h.e'_3
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ (fun s => Finset.sum s fun b => deriv (F b) z) = fun i => (deriv ∘ fun t x => Finset.sum t fun n => F n x) i z
[PROOFSTEP]
ext1 s
[GOAL]
case h.e'_3.h
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
U K : Set ℂ
z : ℂ
M r δ : ℝ
φ : Filter ι
F : ι → ℂ → E
f g : ℂ → E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i
hz : z ∈ U
hc : TendstoLocallyUniformlyOn (fun t x => Finset.sum t fun n => F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ (Finset.sum s fun b => deriv (F b) z) = (deriv ∘ fun t x => Finset.sum t fun n => F n x) s z
[PROOFSTEP]
exact (deriv_sum fun i _ => (hf i).differentiableAt (hU.mem_nhds hz)).symm
