Theorem: Complex.realValued_of_iteratedDeriv_real_on_ball (EulerProducts/Auxiliary.lean)

State before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Tactic:
have Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), (x : ℂ) ∈ Metric.ball (c : ℂ) r := by
  intro x hx
  refine Metric.mem_ball.mpr ?_
  rw [dist_eq, ← ofReal_sub, abs_ofReal, abs_sub_lt_iff, sub_lt_iff_lt_add', sub_lt_comm]
  exact and_comm.mpr hx
State after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))

State before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Tactic:
have H ⦃z : ℂ⦄ (hz : z ∈ Metric.ball (c : ℂ) r) := taylorSeries_eq_on_ball' hz hf
State after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))

State before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, DifferentiableOn ℝ F (Set.Ioo (c - r) (c + r)) ∧ Set.EqOn (f ∘ ofReal') (ofReal' ∘ F) (Set.Ioo (c - r) (c + r))
Tactic:
refine ⟨fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ * (D n) * (x - c) ^ n, fun x hx ↦ ?_, fun x hx ↦ ?_⟩
State after:
case refine_1
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ DifferentiableWithinAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) (Set.Ioo (c - r) (c + r)) x

case refine_2
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ (f ∘ ofReal') x = (ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x

State before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
⊢ ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
Tactic:
intro x hx
State after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ↑x ∈ Metric.ball (↑c) r

State before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ↑x ∈ Metric.ball (↑c) r
Tactic:
refine Metric.mem_ball.mpr ?_
State after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ dist ↑x ↑c < r

State before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ dist ↑x ↑c < r
Tactic:
rw [dist_eq, ← ofReal_sub, abs_ofReal, abs_sub_lt_iff, sub_lt_iff_lt_add', sub_lt_comm]
State after:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ x < c + r ∧ c - r < x

State before:
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ x < c + r ∧ c - r < x
Tactic:
exact and_comm.mpr hx
State after:
no goals

State before:
case refine_1
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ DifferentiableWithinAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) (Set.Ioo (c - r) (c + r)) x
Tactic:
have Hx := Hz _ hx
State after:
case refine_1
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableWithinAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) (Set.Ioo (c - r) (c + r)) x

State before:
case refine_1
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableWithinAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) (Set.Ioo (c - r) (c + r)) x
Tactic:
refine DifferentiableAt.differentiableWithinAt ?_
State after:
case refine_1
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x

State before:
case refine_1
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
replace hf := ((hf x Hx).congr (fun _ hz ↦ H hz) (H Hx)).differentiableAt
  (Metric.isOpen_ball.mem_nhds Hx) |>.comp_ofReal
State after:
case refine_1
f : ℂ → ℂ
r c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (↑x - ↑c) ^ n) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x

State before:
case refine_1
f : ℂ → ℂ
r c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (↑x - ↑c) ^ n) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
simp_rw [hd, ← ofReal_sub, ← ofReal_natCast, ← ofReal_inv, ← ofReal_pow, ← ofReal_mul,
  ← ofReal_tsum] at hf
State after:
case refine_1
f : ℂ → ℂ
r c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x

State before:
case refine_1
f : ℂ → ℂ
r c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
Hx : ↑x ∈ Metric.ball (↑c) r
hf : DifferentiableAt ℝ (fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)) x
⊢ DifferentiableAt ℝ (fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
exact DifferentiableAt.ofReal_comp_iff.mp hf
State after:
no goals

State before:
case refine_2
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ (f ∘ ofReal') x = (ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
simp only [Function.comp_apply, ← H (Hz _ hx), hd, ofReal_tsum]
State after:
case refine_2
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)

State before:
case refine_2
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)
Tactic:
push_cast
State after:
case refine_2
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a

State before:
case refine_2
f : ℂ → ℂ
r c : ℝ
hf : DifferentiableOn ℂ f (Metric.ball (↑c) r)
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
Hz : ∀ x ∈ Set.Ioo (c - r) (c + r), ↑x ∈ Metric.ball (↑c) r
H : ∀ ⦃z : ℂ⦄, z ∈ Metric.ball (↑c) r → ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
x : ℝ
hx : x ∈ Set.Ioo (c - r) (c + r)
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a
Tactic:
rfl
State after:
no goals