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

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
⊢ 0 ≤ f z
Tactic:
have H := taylorSeries_eq_of_entire' 0 z hf
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
⊢ 0 ≤ f z

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
⊢ 0 ≤ f z
Tactic:
have hz' := eq_re_of_ofReal_le hz
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
hz' : z = ↑z.re
⊢ 0 ≤ f z

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (z - 0) ^ n = f z
hz' : z = ↑z.re
⊢ 0 ≤ f z
Tactic:
rw [hz'] at hz H ⊢
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ 0 ≤ f ↑z.re

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ 0 ≤ f ↑z.re
Tactic:
obtain ⟨D, hD⟩ : ∃ D : ℕ → ℝ, ∀ n, 0 ≤ D n ∧ iteratedDeriv n f 0 = D n
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ ∃ D, ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)

case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ f ↑z.re

State before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ f ↑z.re
Tactic:
simp_rw [← H, hD, ← ofReal_natCast, sub_zero, ← ofReal_pow, ← ofReal_inv, ← ofReal_mul,
  ← ofReal_tsum]
State after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a)

State before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ↑(∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a)
Tactic:
norm_cast
State after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a

State before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
⊢ 0 ≤ ∑' (a : ℕ), (↑a !)⁻¹ * D a * z.re ^ a
Tactic:
refine tsum_nonneg fun n ↦ ?_
State after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n

State before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Tactic:
norm_cast at hz
State after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n

State before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Tactic:
have := (hD n).1
State after:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
this : 0 ≤ D n
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n

State before:
case intro
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
D : ℕ → ℝ
hD : ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
n : ℕ
hz : 0 ≤ z.re
this : 0 ≤ D n
⊢ 0 ≤ (↑n !)⁻¹ * D n * z.re ^ n
Tactic:
positivity
State after:
no goals

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
⊢ ∃ D, ∀ (n : ℕ), 0 ≤ D n ∧ iteratedDeriv n f 0 = ↑(D n)
Tactic:
refine ⟨fun n ↦ (iteratedDeriv n f 0).re, fun n ↦ ⟨?_, ?_⟩⟩
State after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n

case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ iteratedDeriv n f 0 = ↑((fun n => (iteratedDeriv n f 0).re) n)

State before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n
Tactic:
have := eq_re_of_ofReal_le (h n) ▸ h n
State after:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
this : 0 ≤ ↑(iteratedDeriv n f 0).re
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n

State before:
case refine_1
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
this : 0 ≤ ↑(iteratedDeriv n f 0).re
⊢ 0 ≤ (fun n => (iteratedDeriv n f 0).re) n
Tactic:
norm_cast at this
State after:
no goals

State before:
case refine_2
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ ↑z.re
H : ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f 0 * (↑z.re - 0) ^ n = f ↑z.re
hz' : z = ↑z.re
n : ℕ
⊢ iteratedDeriv n f 0 = ↑((fun n => (iteratedDeriv n f 0).re) n)
Tactic:
rw [eq_re_of_ofReal_le (h n)]
State after:
no goals