# `BernsteinBasic.lean` --- Informal Summary

> **Source**: [`HilleYosida/BernsteinBasic.lean`](../../HilleYosida/BernsteinBasic.lean)
> **Generated**: 2026-03-27
> **Note**: Auto-generated by `/lean-summarize`. Re-run to refresh.

## Overview

This file defines completely monotone (CM) functions on $[0,\infty)$ and develops their basic properties: nonnegativity, boundedness by $f(0)$, non-increasing first derivative, the alternating-sign condition for higher derivatives, and convergence at infinity. It also proves the Taylor integral remainder formula on closed intervals and connects it to the CM sign condition via a set-transfer lemma (`iteratedDerivWithin` on $[x,T]$ agrees with that on $[0,\infty)$ at interior points). The file closes with two integration lemmas expressing $f(x) - f(T)$ as $\int_x^T (-f')\,dt$.

## Status

**Main result**: Fully proven (0 sorry's)
None --- file is sorry-free.
**Length**: 236 lines, 1 definition + 13 theorems/lemmas

---

## Key declarations

### [`IsCompletelyMonotone`](../../HilleYosida/BernsteinBasic.lean#L36) --- Definition
A function $f : \mathbb{R} \to \mathbb{R}$ is completely monotone on $[0,\infty)$ when it is $C^\infty$ on $[0,\infty)$ and $(-1)^n f^{(n)}(t) \ge 0$ for every $n \in \mathbb{N}$ and $t \ge 0$. This is Widder's smooth-derivative definition.

### [`coe_top_ne_zero`](../../HilleYosida/BernsteinBasic.lean#L43) --- Lemma
$\uparrow(\top : \mathbb{N}_\infty) \ne 0$ in $\mathrm{WithTop}\;\mathbb{N}_\infty$. Helper for smoothness-index coercions.

### [`nat_le_coe_top`](../../HilleYosida/BernsteinBasic.lean#L46) --- Lemma
$\uparrow n \le \uparrow(\top : \mathbb{N}_\infty)$ for every $n : \mathbb{N}$.

### [`nat_lt_coe_top`](../../HilleYosida/BernsteinBasic.lean#L49) --- Lemma
$\uparrow n < \uparrow(\top : \mathbb{N}_\infty)$ for every $n : \mathbb{N}$.

### [`IsCompletelyMonotone.nonneg`](../../HilleYosida/BernsteinBasic.lean#L55) --- Lemma
A CM function satisfies $f(t) \ge 0$ for all $t \ge 0$ (the $n = 0$ case of the sign condition).

### [`IsCompletelyMonotone.deriv_nonpos`](../../HilleYosida/BernsteinBasic.lean#L60) --- Lemma
A CM function satisfies $f'(t) \le 0$ for all $t \ge 0$ (the $n = 1$ case), so $f$ is non-increasing.

### [`IsCompletelyMonotone.bounded`](../../HilleYosida/BernsteinBasic.lean#L67) --- Lemma
A CM function satisfies $f(t) \le f(0)$ for all $t \ge 0$. Uses `antitoneOn_of_deriv_nonpos` on $[0,\infty)$.

### [`IsCompletelyMonotone.deriv_cm_sign`](../../HilleYosida/BernsteinBasic.lean#L83) --- Lemma
The sign condition for $-f'$ being CM: $(-1)^n D^n(-f')(t) = (-1)^{n+1} f^{(n+1)}(t) \ge 0$. The smoothness half (`ContDiffOn`) is omitted because it is not used downstream.

### [`taylor_integral_remainder`](../../HilleYosida/BernsteinBasic.lean#L101) --- Theorem
**Taylor integral remainder** (sorry-free). For $a < b$ and $f \in C^{n+1}([a,b])$:
$$f(b) - P_n(a,b) = \int_a^b \frac{(b-t)^n}{n!}\, f^{(n+1)}(t)\, dt$$
where $P_n$ is the $n$-th Taylor polynomial centered at $a$. Proved via FTC applied to `taylorWithinEval`.

### [`IsCompletelyMonotone.tendsto_atTop`](../../HilleYosida/BernsteinBasic.lean#L137) --- Lemma
A CM function converges at infinity: there exists $L \ge 0$ with $f(t) \to L$ as $t \to \infty$. Uses antitonicity plus the lower bound $f \ge 0$ to invoke `tendsto_atTop_ciInf`.

### [`iteratedDerivWithin_Icc_eq_Ici`](../../HilleYosida/BernsteinBasic.lean#L162) --- Lemma
Set transfer: `iteratedDerivWithin n f (Icc x T) t = iteratedDerivWithin n f (Ici 0) t` for $t \in (x, T)$ with $0 \le x$, since both equal `iteratedDeriv n f t` at interior points where $f$ is $C^n$.

### [`IsCompletelyMonotone.taylor_nonneg_remainder`](../../HilleYosida/BernsteinBasic.lean#L182) --- Lemma
**CM sign condition for Taylor remainder.** For a CM function with $0 \le x < T$:
$$(-1)^n \int_x^T \frac{(T-t)^{n-1}}{(n-1)!}\, f^{(n)}(t)\, dt \ge 0$$
Combines `taylor_integral_remainder` with `iteratedDerivWithin_Icc_eq_Ici` and the a.e.\ equality $\mathrm{Ioo} =_{\mathrm{ae}} \mathrm{Icc}$.

### [`IsCompletelyMonotone.integral_neg_deriv`](../../HilleYosida/BernsteinBasic.lean#L210) --- Lemma
For a CM function with $0 \le x < T$:
$$f(x) - f(T) = \int_x^T (-f'(t))\, dt$$
Specializes `taylor_integral_remainder` at $n = 0$, where $P_0(x, T) = f(x)$.

### [`IsCompletelyMonotone.integral_mass`](../../HilleYosida/BernsteinBasic.lean#L230) --- Lemma
The integral of $-f'$ on $[0, T]$ equals $f(0) - f(T)$. Immediate from `integral_neg_deriv` at $x = 0$.

---

*This file has **1** definition and **13** theorems/lemmas (0 with sorry).*