English
An entire function whose iterated derivatives at c are all nonnegative real has nonnegative real values on c + ℝ≥0.
Русский
Целая функция с неотрицательными производными в c имеет неотрицательные значения на c + ℝ≥0.
LaTeX
$$If f is entire and ∀ n, 0 ≤ iteratedDeriv n f c, then ∀ z = c + t with t ≥ 0, f(z) ∈ [0,∞).$$
Lean4
/-- An entire function whose iterated derivatives at `c` are all nonnegative real has nonnegative
real values on `c + ℝ≥0`. -/
theorem nonneg_of_iteratedDeriv_nonneg {f : ℂ → ℂ} (hf : Differentiable ℂ f) {c : ℂ} (h : ∀ n, 0 ≤ iteratedDeriv n f c)
⦃z : ℂ⦄ (hz : c ≤ z) : 0 ≤ f z :=
by
refine hf.differentiableOn.nonneg_of_iteratedDeriv_nonneg (r := (z - c).re + 1) h hz ?_
rw [← sub_nonneg] at hz
rw [Metric.mem_ball, dist_eq, eq_re_of_ofReal_le hz]
simpa only [Complex.norm_of_nonneg (nonneg_iff.mp hz).1] using lt_add_one _
