English
An entire function whose iterated derivatives at c are real with alternating signs has nonnegative values on c - ℝ≥0.
Русский
Целая функция, чьи итеративные производные при c имеют чередующиеся знаки, принимает неотрицательные значения на c - ℝ≥0.
LaTeX
$$If ∀ n ≠ 0, 0 ≤ (-1)^n · iteratedDeriv n f c, then ∀ z with z ≤ c along the real axis, f(c) ≤ f(z).$$
Lean4
/-- An entire function whose iterated derivatives at `c` are all nonnegative real (except
possibly the value itself) has values of the form `f c + nonneg. real` on the set `c + ℝ≥0`. -/
theorem apply_le_of_iteratedDeriv_nonneg {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f)
(h : ∀ n ≠ 0, 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : c ≤ z) : f c ≤ f z :=
by
have h' (n : ℕ) : 0 ≤ iteratedDeriv n (f · - f c) c := by
cases n with
| zero => simp only [iteratedDeriv_zero, sub_self, le_refl]
| succ n =>
specialize h (n + 1) n.succ_ne_zero
rw [iteratedDeriv_succ'] at h ⊢
rwa [funext fun x ↦ deriv_sub_const (f := f) (x := x) (f c)]
exact sub_nonneg.mp <| nonneg_of_iteratedDeriv_nonneg (hf.sub_const _) h' hz
