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

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Tactic:
have H (z : ℂ) := taylorSeries_eq_of_entire' c z hf
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f ↑c * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Tactic:
simp_rw [hd] at H
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ ∃ F, Differentiable ℝ F ∧ f ∘ ofReal' = ofReal' ∘ F
Tactic:
refine ⟨fun x ↦ ∑' (n : ℕ), (↑n !)⁻¹ * (D n) * (x - c) ^ n, ?_, ?_⟩
State after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n

case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ f ∘ ofReal' = ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n

State before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
have := hf.comp_ofReal
State after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => f ↑x
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n

State before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => f ↑x
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
simp_rw [← H, ← ofReal_sub, ← ofReal_natCast, ← ofReal_inv, ← ofReal_pow, ← ofReal_mul,
  ← ofReal_tsum] at this
State after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n

State before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
this : Differentiable ℝ fun x => ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * (x - c) ^ a)
⊢ Differentiable ℝ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
exact Differentiable.ofReal_comp_iff.mp this
State after:
no goals

State before:
case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
⊢ f ∘ ofReal' = ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n
Tactic:
ext x
State after:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ (f ∘ ofReal') x = (ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x

State before:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ (f ∘ ofReal') x = (ofReal' ∘ fun x => ∑' (n : ℕ), (↑n !)⁻¹ * D n * (x - c) ^ n) x
Tactic:
simp only [Function.comp_apply, ofReal_eq_coe, ← H, ofReal_tsum]
State after:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)

State before:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (↑x - ↑c) ^ n = ∑' (a : ℕ), ↑((↑a !)⁻¹ * D a * (x - c) ^ a)
Tactic:
push_cast
State after:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a

State before:
case refine_2.h
f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℝ
D : ℕ → ℝ
hd : ∀ (n : ℕ), iteratedDeriv n f ↑c = ↑(D n)
H : ∀ (z : ℂ), ∑' (n : ℕ), (↑n !)⁻¹ * ↑(D n) * (z - ↑c) ^ n = f z
x : ℝ
⊢ ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a = ∑' (a : ℕ), (↑a !)⁻¹ * ↑(D a) * (↑x - ↑c) ^ a
Tactic:
rfl
State after:
no goals