# `BernsteinMeasures.lean` — Informal Summary

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

## Overview

Constructs the approximating measures for Bernstein's theorem and proves the key analytic ingredients: the CM density $\rho_n$, its nonnegativity, integration-by-parts recursion for total mass bounds, the Bernstein kernel $\varphi_n$ and its pointwise convergence to $e^{-xp}$, rescaled pushforward measures, and the final packaging step assembling $\mu = \mu_0 + L \cdot \delta_0$. Split from `Bernstein.lean` to isolate the measure-construction layer.

## Status

**Main result**: All lemmas fully proven

None --- file is sorry-free.

**Length**: 498 lines, 4 definitions + 15 theorems/lemmas

---

## Key declarations

### [`cm_density`](../../HilleYosida/BernsteinMeasures.lean#L25) --- Definition
The density $\rho_n(t) = \frac{(-1)^n}{(n-1)!}\, t^{n-1}\, f^{(n)}(t)$ for $n \geq 1$ (zero for $n=0$). This is the Radon--Nikodym derivative of the $n$-th approximating measure in the Chafai approach to Bernstein's theorem.

### [`cm_measure`](../../HilleYosida/BernsteinMeasures.lean#L32) --- Definition
The $n$-th approximating measure $\sigma_n$, defined as $\mathrm{vol}\lvert_{(0,\infty)}$ weighted by $\rho_n$: `(volume.restrict (Ioi 0)).withDensity (ofReal (cm_density f n))`.

### [`cm_density_nonneg`](../../HilleYosida/BernsteinMeasures.lean#L37) --- Lemma
For a completely monotone $f$, the density $\rho_n(t) \geq 0$ for all $t > 0$: the sign $(-1)^n f^{(n)}(t) \geq 0$ from the CM condition combines with $t^{n-1}/(n-1)! \geq 0$.

### [`cm_density_one`](../../HilleYosida/BernsteinMeasures.lean#L54) --- Lemma
For $n = 1$ the density simplifies to $\rho_1(t) = -f'(t)$.

### [`IsCompletelyMonotone.integral_neg_deriv_Ici`](../../HilleYosida/BernsteinMeasures.lean#L60) --- Lemma
The interval integral of $-f'$ computed with the $T$-dependent set $[0,T]$ equals the integral computed with the fixed set $[0,\infty)$, by agreement of `iteratedDerivWithin` at interior points.

### [`IsCompletelyMonotone.tendsto_total_mass`](../../HilleYosida/BernsteinMeasures.lean#L78) --- Lemma
$\int_0^T (-f')\,dt \to f(0) - L$ as $T \to \infty$, where $L = \lim_{t\to\infty} f(t)$. Key uniform bound for tightness.

### [`IsCompletelyMonotone.neg_deriv_integrableOn`](../../HilleYosida/BernsteinMeasures.lean#L94) --- Lemma
$-f'$ is integrable on $(0,\infty)$ for CM functions, proved via `integrableOn_Ioi_of_intervalIntegral_norm_tendsto` using the total-mass bound.

### [`IsCompletelyMonotone.integral_Ioi_neg_deriv`](../../HilleYosida/BernsteinMeasures.lean#L126) --- Lemma
The improper integral $\int_0^\infty (-f')\,dt = f(0) - L$.

### [`bernstein_packaging`](../../HilleYosida/BernsteinMeasures.lean#L146) --- Lemma
**Packaging step**: given $f(x) = L + \int e^{-xp}\,d\mu_0$ with $\mu_0$ supported on $[0,\infty)$, produces $\mu = \mu_0 + L \cdot \delta_0$ so that $f(x) = \int e^{-xp}\,d\mu$ with $\mu$ finite and supported on $[0,\infty)$.

### [`bernstein_kernel`](../../HilleYosida/BernsteinMeasures.lean#L203) --- Definition
The Bernstein kernel $\varphi_n(x,p) = \max\!\bigl(1 - xp/(n{-}1),\, 0\bigr)^{n-1}$ for $n \geq 2$ (zero for $n \leq 1$). After the change of variable $p = (n{-}1)/t$, the Taylor integral kernel becomes $\varphi_n$.

### [`bernstein_kernel_tendsto`](../../HilleYosida/BernsteinMeasures.lean#L213) --- Lemma
**Pointwise convergence**: $\varphi_n(x,p) \to e^{-xp}$ as $n \to \infty$ for $x, p \geq 0$, via the classical $(1 + t/n)^n \to e^t$ limit (`Real.tendsto_one_add_div_pow_exp`).

### [`cm_rescaled`](../../HilleYosida/BernsteinMeasures.lean#L242) --- Definition
The rescaled measure $\tilde\sigma_n$: pushforward of $\sigma_n$ under $t \mapsto (n{-}1)/t$. After this change of variable the Taylor kernel becomes $\varphi_n(x,p)$.

### [`cm_rescaling_measurable`](../../HilleYosida/BernsteinMeasures.lean#L246) --- Lemma
The rescaling map $t \mapsto (n{-}1)/t$ is measurable.

### [`cm_measure_compl_Ioi`](../../HilleYosida/BernsteinMeasures.lean#L251) --- Lemma
$\sigma_n$ is supported on $(0,\infty)$: $\sigma_n\bigl((0,\infty)^c\bigr) = 0$.

### [`cm_rescaled_Iio_zero`](../../HilleYosida/BernsteinMeasures.lean#L263) --- Lemma
$\tilde\sigma_n$ is supported on $[0,\infty)$ for $n \geq 2$: $\tilde\sigma_n\bigl((-\infty,0)\bigr) = 0$.

### [`cm_rescaled_mass_eq`](../../HilleYosida/BernsteinMeasures.lean#L282) --- Lemma
Pushforward preserves total mass: $\tilde\sigma_n(\mathbb{R}) = \sigma_n(\mathbb{R})$.

### [`cm_density_ibp_step`](../../HilleYosida/BernsteinMeasures.lean#L375) --- Lemma
**IBP step**: $\int_0^T \rho_k\,dt \leq \int_0^T \rho_{k-1}\,dt$ for $k \geq 2$. The boundary term $B_k(T) = (-1)^k T^{k-1}/(k{-}1)!\cdot f^{(k-1)}(T) \leq 0$ by the CM sign condition.

### [`cm_measure_finite_mass`](../../HilleYosida/BernsteinMeasures.lean#L405) --- Lemma
**Total mass bound**: $\sigma_n$ is a finite measure with $\sigma_n(\mathbb{R}) \leq f(0) - L$. By IBP recursion $\int_0^T \rho_n \leq \int_0^T \rho_1 = f(0) - f(T) \leq f(0) - L$, then integrability on $(0,\infty)$ follows from `integrableOn_Ioi_of_intervalIntegral_norm_bounded`.

---

*This file has **4** definitions and **15** theorems/lemmas (0 with sorry).*