Absolutely monotone functions

A function f : ℝ → ℝ is absolutely monotone on a set s if its iterated derivatives are all nonnegative on s.

Main definitions

• AbsolutelyMonotoneOn — there exists a Taylor series for f on s with nonnegative terms at each point of s.

Main results

• AbsolutelyMonotoneOn.contDiffOn — the function is C^∞ on s.
• AbsolutelyMonotoneOn.of_contDiff — a globally C^∞ function with nonnegative iterated derivatives on s is absolutely monotone on s.
• AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg — under UniqueDiffOn, the definition is equivalent to f being C^∞ on s with every iterated derivative within s nonnegative.
• AbsolutelyMonotoneOn.add — closure under addition.
• AbsolutelyMonotoneOn.smul — closure under nonnegative scalar multiplication.

Implementation

The precise definition is phrased via the existence of a Taylor series with nonnegative terms (HasFTaylorSeriesUpToOn) rather than via iteratedDerivWithin. This avoids forcing a UniqueDiffOn s hypothesis on every result: without UniqueDiffOn, "the" iterated derivative within s is not canonical, but the existence of a Taylor series is intrinsic to f and s. When s does satisfy UniqueDiffOn, the condition reduces to f being C^∞ on s with every iterated derivative within s nonnegative.

References

• D. V. Widder, The Laplace Transform

def AbsolutelyMonotoneOn (f : ℝ → ℝ) (s : Set ℝ) : Prop

A function f : ℝ → ℝ is absolutely monotone on a set s if, heuristically, all iterated derivatives of f on s are nonnegative. For technical reasons related to unique differentiability, the precise definition is phrased as the existence of a Taylor series for f on s whose nth term, evaluated at the all-ones tuple, is nonnegative for every n and every x ∈ s. See AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg for the equivalence under UniqueDiffOn.

Equations

• AbsolutelyMonotoneOn f s = ∃ (p : ℝ → FormalMultilinearSeries ℝ ℝ ℝ), HasFTaylorSeriesUpToOn (↑⊤) f p s ∧ ∀ (n : ℕ) ⦃x : ℝ⦄, x ∈ s → 0 ≤ (p x n) fun (x : Fin n) => 1

theorem AbsolutelyMonotoneOn.contDiffOn {f : ℝ → ℝ} {s : Set ℝ} (hf : AbsolutelyMonotoneOn f s) : ContDiffOn ℝ (↑⊤) f s

An absolutely monotone function on s is C^∞ on s.

theorem AbsolutelyMonotoneOn.of_contDiff {f : ℝ → ℝ} {s : Set ℝ} (hf : ContDiff ℝ (↑⊤) f) (h : ∀ (n : ℕ), ∀ x ∈ s, 0 ≤ iteratedDeriv n f x) : AbsolutelyMonotoneOn f s

A globally C^∞ function whose iterated derivatives are nonnegative on s is absolutely monotone on s. The set s need not satisfy UniqueDiffOn.

theorem AbsolutelyMonotoneOn.iteratedDerivWithin_nonneg {f : ℝ → ℝ} {s : Set ℝ} (hf : AbsolutelyMonotoneOn f s) (hs : UniqueDiffOn ℝ s) (n : ℕ) {x : ℝ} (hx : x ∈ s) : 0 ≤ iteratedDerivWithin n f s x

Under UniqueDiffOn, a Taylor witness for an absolutely monotone function agrees with iteratedDerivWithin, so the latter is nonnegative on s.

theorem AbsolutelyMonotoneOn.iff_iteratedDerivWithin_nonneg {f : ℝ → ℝ} {s : Set ℝ} (hs : 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.

Closure properties

theorem AbsolutelyMonotoneOn.add {f g : ℝ → ℝ} {s : Set ℝ} (hf : AbsolutelyMonotoneOn f s) (hg : AbsolutelyMonotoneOn g s) : AbsolutelyMonotoneOn (f + g) s

The sum of two absolutely monotone functions is absolutely monotone.

theorem AbsolutelyMonotoneOn.smul {f : ℝ → ℝ} {s : Set ℝ} {c : ℝ} (hf : AbsolutelyMonotoneOn f s) (hc : 0 ≤ c) : AbsolutelyMonotoneOn (c • f) s

A nonnegative scalar multiple of an absolutely monotone function is absolutely monotone.