Nonnegativity of values of holomorphic functions

We show that if f is holomorphic on an open disk B(c,r) and all iterated derivatives of f at c are nonnegative real, then f z ≥ 0 for all z ≥ c in the disk; see DifferentiableOn.nonneg_of_iteratedDeriv_nonneg. We also provide a variant Differentiable.nonneg_of_iteratedDeriv_nonneg for entire functions and versions showing f z ≥ f c when all iterated derivatives except f itseld are nonnegative.

theorem DifferentiableOn.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

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 Differentiable.nonneg_of_iteratedDeriv_nonneg {f : ℂ → ℂ} (hf : Differentiable ℂ f) {c : ℂ} (h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : c ≤ z) : 0 ≤ f z

An entire function whose iterated derivatives at c are all nonnegative real has nonnegative real values on c + ℝ≥0.

theorem Differentiable.apply_le_of_iteratedDeriv_nonneg {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : c ≤ z) : f c ≤ f z

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 Differentiable.apply_le_of_iteratedDeriv_alternating {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f) (h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : z ≤ c) : f c ≤ f z

An entire function whose iterated derivatives at c are all real with alternating signs (except possibly the value itself) has values of the form f c + nonneg. real along the set c - ℝ≥0.