Theorems · Theorem · complex analysis
Differentiable.apply_le_of_iteratedDeriv_nonneg
∀ {f : ℂ → ℂ} {c : ℂ}, Differentiable ℂ f → (∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c) → ∀ ⦃z : ℂ⦄, c ≤ z → f c ≤ f zAn 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.
- Defined in
- Mathlib.Analysis.Complex.Positivity
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 290 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- sub_selfproof · cited by 996
- Differentiablestatement and proof · cited by 298
- iteratedDerivstatement and proof · cited by 188
- sub_nonnegproof · cited by 167
- Complex.partialOrderstatement · cited by 64
- iteratedDeriv_zeroproof · cited by 34
- Differentiable.sub_constproof · cited by 5
- iteratedDeriv_succ'proof · cited by 5
- deriv_sub_constproof · cited by 3
- Differentiable.nonneg_of_iteratedDeriv_nonnegproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Differentiable.apply_le_of_iteratedDeriv_alternatingproof · cited by 1