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

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
⊢ f 0 ≤ f z
Tactic:
let F : ℂ → ℂ := fun z ↦ f (-z)
State after:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 ≤ f z

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 ≤ f z
Tactic:
convert at_zero_le_of_iteratedDeriv_nonneg (f := F) (hf.comp <| differentiable_neg)
  (fun n hn ↦ ?_) (neg_nonneg.mpr hz) using 1
State after:
case h.e'_3
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 = F 0

case h.e'_4
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f z = F (-z)

f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n F 0

State before:
case h.e'_3
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f 0 = F 0
Tactic:
simp only [F, neg_zero]
State after:
no goals

State before:
case h.e'_4
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
⊢ f z = F (-z)
Tactic:
simp only [F, neg_neg]
State after:
no goals

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f 0
z : ℂ
hz : z ≤ 0
F : ℂ → ℂ := fun z => f (-z)
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n F 0
Tactic:
simpa only [F, iteratedDeriv_comp_neg, neg_zero] using h n hn
State after:
no goals