English
A variant of the previous result for an altered argument; the same monotonicity conclusion holds under a reflected setup.
Русский
Вариант предыдущего вывода для отражённого аргумента; заключение о монотонности сохраняется.
LaTeX
$$Same as previous with a reflected function: f ≤ g under the transformed conditions.$$
Lean4
/-- 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`. -/
theorem apply_le_of_iteratedDeriv_alternating {f : ℂ → ℂ} {c : ℂ} (hf : Differentiable ℂ f)
(h : ∀ n ≠ 0, 0 ≤ (-1) ^ n * iteratedDeriv n f c) ⦃z : ℂ⦄ (hz : z ≤ c) : f c ≤ f z :=
by
convert
apply_le_of_iteratedDeriv_nonneg (f := fun z ↦ f (-z)) (hf.comp <| differentiable_neg) (fun n hn ↦ ?_)
(neg_le_neg_iff.mpr hz) using
1
· simp only [neg_neg]
· simp only [neg_neg]
· simpa only [iteratedDeriv_comp_neg, neg_neg, smul_eq_mul] using h n hn
