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

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
h' : ∀ (n : ℕ), 0 ≤ iteratedDeriv n (fun x => f x - f 0) 0
⊢ f 0 ≤ f z
Tactic:
exact sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const (f 0)) h' hz
State after:
no goals

State before:
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv n (fun x => f x - f 0) 0
Tactic:
cases n with
| zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
| succ n =>
  specialize h n.succ <| succ_ne_zero n
  rw [iteratedDeriv_succ'] at h ⊢
  convert h using 2
  ext w
  exact deriv_sub_const (f 0)
State after:
no goals

State before:
case zero
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
⊢ 0 ≤ iteratedDeriv 0 (fun x => f x - f 0) 0
Tactic:
simp only [iteratedDeriv_zero, sub_self, le_refl]
State after:
no goals

State before:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f 0
z : ℂ
hz : 0 ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f 0) 0
Tactic:
specialize h n.succ <| succ_ne_zero n
State after:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n.succ f 0
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f 0) 0

State before:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n.succ f 0
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x => f x - f 0) 0
Tactic:
rw [iteratedDeriv_succ'] at h ⊢
State after:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ iteratedDeriv n (deriv fun x => f x - f 0) 0

State before:
case succ
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ 0 ≤ iteratedDeriv n (deriv fun x => f x - f 0) 0
Tactic:
convert h using 2
State after:
case h.e'_4.h.e'_7
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ (deriv fun x => f x - f 0) = deriv f

State before:
case h.e'_4.h.e'_7
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
⊢ (deriv fun x => f x - f 0) = deriv f
Tactic:
ext w
State after:
case h.e'_4.h.e'_7.h
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
w : ℂ
⊢ deriv (fun x => f x - f 0) w = deriv f w

State before:
case h.e'_4.h.e'_7.h
f : ℂ → ℂ
hf : Differentiable ℂ f
z : ℂ
hz : 0 ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (deriv f) 0
w : ℂ
⊢ deriv (fun x => f x - f 0) w = deriv f w
Tactic:
exact deriv_sub_const (f 0)
State after:
no goals