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 holomorphic on a disk around c of radius r and ∀ n, iteratedDeriv n f c ≥ 0, then ∀ z ∈ {c + t : t ∈ [0,r)}, f(z) ∈ [0,∞).$$
Lean4
/-- A function that is holomorphic on the open disk around `c` with radius `r` and whose iterated
derivatives at `c` are all nonnegative real has nonnegative real values on `c + [0,r)`. -/
theorem nonneg_of_iteratedDeriv_nonneg {f : ℂ → ℂ} {c : ℂ} {r : ℝ} (hf : DifferentiableOn ℂ f (Metric.ball c r))
(h : ∀ n, 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz₁ : c ≤ z) (hz₂ : z ∈ Metric.ball c r) : 0 ≤ f z :=
by
have H := taylorSeries_eq_on_ball' hz₂ hf
rw [← sub_nonneg] at hz₁
have hz' := eq_re_of_ofReal_le hz₁
rw [hz'] at hz₁ H
refine H ▸ tsum_nonneg fun n ↦ ?_
rw [← ofReal_natCast, ← ofReal_pow, ← ofReal_inv, eq_re_of_ofReal_le (h n), ← ofReal_mul, ← ofReal_mul]
norm_cast at hz₁ ⊢
have := zero_re ▸ (Complex.le_def.mp (h n)).1
positivity
