Theorems · Theorem · real analysis
AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg
∀ {f : ℝ → ℝ} {s : Set ℝ},
UniqueDiffOn ℝ s →
(AbsolutelyMonotoneOn f s ↔ ContDiffOn ℝ (↑⊤) f s ∧ ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDerivWithin n f s x)Under UniqueDiffOn, a function is absolutely monotone on s iff it is C^∞ on s with
every iterated derivative within s nonnegative.
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 185 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- Realstatement and proof · cited by 25,697
- Top.topstatement and proof · cited by 9,680
- ENatstatement · cited by 4,985
- WithTop.somestatement and proof · cited by 1,128
- ContDiffOnstatement and proof · cited by 294
- UniqueDiffOnstatement and proof · cited by 215
- iteratedDerivWithinstatement and proof · cited by 122
- ftaylorSeriesWithinproof · cited by 17
- ContDiffOn.ftaylorSeriesWithinproof · cited by 11
- AbsolutelyMonotoneOnstatement and proof · cited by 6
- iteratedDerivWithin_eq_iteratedFDerivWithinproof · cited by 5
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.