Theorems · Theorem · complex analysis
Differentiable.apply_le_of_iteratedDeriv_alternating
∀ {f : ℂ → ℂ} {c : ℂ},
Differentiable ℂ f → (∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c) → ∀ ⦃z : ℂ⦄, z ≤ c → f c ≤ f zAn 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.
- Defined in
- Mathlib.Analysis.Complex.Positivity
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 291 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites10
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Complexstatement and proof · cited by 5,565
- neg_negproof · cited by 960
- Differentiablestatement and proof · cited by 298
- iteratedDerivstatement and proof · cited by 188
- Complex.partialOrderstatement · cited by 64
- neg_le_neg_iffproof · cited by 57
- Differentiable.compproof · cited by 17
- differentiable_negproof · cited by 5
- iteratedDeriv_comp_negproof · cited by 2
- Differentiable.apply_le_of_iteratedDeriv_nonnegproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- LSeries.positive_of_differentiable_of_eqOnproof · cited by 1