# `BernsteinChafai.lean` — Informal Summary

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

## Overview

This file proves the **Chafai identity** and the **Prokhorov extraction** step for Bernstein's theorem. The Chafai identity expresses $f(x) - L = \int \varphi_n(x,p)\,d\tilde\sigma_n(p)$ where $\varphi_n$ is the Bernstein kernel and $\tilde\sigma_n$ is the rescaled approximating measure. The proof combines a change-of-variables (`chafai_kernel_density_eq`) with repeated integration by parts and boundary decay (`chafai_repeated_ibp`). The Prokhorov extraction provides a subsequential weak limit of finite measures on $[0,\infty)$ with uniformly bounded mass, and the limit identification shows $f(x) - L = \int e^{-xp}\,d\mu_0(p)$ via diagonal convergence of kernel integrals.

Split from `Bernstein.lean`.

## Status

**Main results**: Fully proven (0 `sorry`'s in proof terms)

None --- file is sorry-free.

**Length**: 1660 lines, 1 definition + 19 theorems/lemmas

---

## Key declarations

### [`cm_rescaled_isFiniteMeasure`](../../HilleYosida/BernsteinChafai.lean#L26) --- Lemma

The rescaled measure `cm_rescaled f n` is a finite measure when the underlying `cm_measure f n` is finite.

### `chafai_kernel_density_eq` (private, [line 55](../../HilleYosida/BernsteinChafai.lean#L55)) --- Lemma

**Change of variables**: for a CM function $f$, $n \ge 2$, $x \ge 0$:
$$\int_0^\infty \varphi_n\!\bigl(x,\, \tfrac{n-1}{t}\bigr)\, \rho_n(t)\,dt \;=\; \int_x^\infty \frac{(-1)^n}{(n{-}1)!}\,(t-x)^{n-1}\, f^{(n)}(t)\,dt$$
where $\varphi_n$ is `bernstein_kernel` and $\rho_n$ is `cm_density`. Sorry-free; proved by restricting the LHS to $\mathrm{Ioi}\,x$ (the kernel vanishes on the complement) and simplifying the integrand via `field_simp`. Requires `maxHeartbeats 3200000`.

### `boundary_term_decay` (private, [line 193](../../HilleYosida/BernsteinChafai.lean#L193)) --- Lemma

For a CM function with $f(t) \to L$:
$$\frac{(-1)^{k+1}}{k!}\,(T-x)^k\, f^{(k)}(T) \;\to\; 0 \quad\text{as } T \to \infty$$
Proved by a squeeze argument: the boundary term is bounded by a constant times $\int_{\mathrm{Ioi}(T/2)} \rho_k(t)\,dt$, which tends to zero by integrability of `cm_density`. Uses antitone-on structure of $(-1)^k f^{(k)}$ on $[0,\infty)$.

### `chafai_repeated_ibp` (private, [line 495](../../HilleYosida/BernsteinChafai.lean#L495)) --- Lemma

**Repeated integration by parts**: for CM $f$ with $f(t) \to L$, $n \ge 1$, $x \ge 0$:
$$\int_x^\infty \frac{(-1)^n}{(n{-}1)!}\,(t-x)^{n-1}\, f^{(n)}(t)\,dt \;=\; f(x) - L$$
Induction on $n$: base case $n=1$ uses $\int_x^\infty (-f')\,dt = f(x) - L$; inductive step applies `ibp_finite_interval` on $[x,T]$, sends $T \to \infty$ using `boundary_term_decay`, and matches the limit via `ibp_kernel_integrableOn`.

### [`chafai_identity`](../../HilleYosida/BernsteinChafai.lean#L575) --- Lemma

**Statement**: For a CM function $f$ with $f(t) \to L$, $n \ge 2$, $x \ge 0$:
$$f(x) - L \;=\; \int \varphi_n(x,p)\,d\tilde\sigma_n(p)$$
where $\tilde\sigma_n = \mathtt{cm\_rescaled}\; f\; n$.

**Proof**: Four steps: (1) push forward through `cm_rescaling` to get $\int \varphi_n(x, (n{-}1)/t)\,d\sigma_n(t)$; (2) unfold `cm_measure` as `withDensity` to get $\int \varphi_n(x,(n{-}1)/t)\,\rho_n(t)\,dt$; (3) apply `chafai_kernel_density_eq` for the change of variables; (4) apply `chafai_repeated_ibp` to evaluate the resulting integral as $f(x) - L$.

### [`finite_measure_subseq_limit`](../../HilleYosida/BernsteinChafai.lean#L673) --- Lemma

**Statement**: Given a sequence $(\sigma_n)$ of finite measures on $\mathbb{R}$ with uniformly bounded mass ($\sigma_n(\mathbb{R}) \le C$) and supported on $[0,\infty)$, there exist a finite measure $\mu_0$ and a strictly monotone $\varphi : \mathbb{N} \to \mathbb{N}$ such that:
- $\mu_0$ is finite and supported on $[0,\infty)$,
- $\mu_0(\mathbb{R}) \le C$,
- $\int g\,d\sigma_{\varphi(k)} \to \int g\,d\mu_0$ for every bounded continuous $g$.

**Proof** (~500 lines): Adds a Dirac mass at $-1$ to each $\sigma_n$ to create $\nu_n$ with mass $\ge 1$; normalizes to get probability measures $\pi_n$; shows tightness from the support condition + mass bound; applies `isCompact_closure_of_isTightMeasureSet` + sequential compactness to extract a convergent subsequence of $\pi_n$ (and a convergent subsequence of masses); reconstructs $\mu_0 = M \cdot \pi_0$ scaled by the limiting mass; proves the limit is supported on $[0,\infty)$ using bump functions `f_cut` and `h_cut` that detect mass on $(-1,0)$ and $(-\infty,-1)$; recovers weak convergence for $\sigma$ from weak convergence for $\nu$ using the cutoff function $\chi$.

### [`tendsto_exp_integral`](../../HilleYosida/BernsteinChafai.lean#L1169) --- Lemma

Weak convergence of $\int e^{-xp}\,d\sigma_{\varphi(k)}$ to $\int e^{-xp}\,d\mu_0$ for measures supported on $[0,\infty)$, by replacing $e^{-xp}$ with the bounded continuous surrogate `exp_bcf` (which agrees with $e^{-xp}$ on $[0,\infty)$).

### [`prokhorov_limit_identification`](../../HilleYosida/BernsteinChafai.lean#L1447) --- Lemma

**Statement**: Given a CM function $f$ with $f(t) \to L \ge 0$, the Chafai identity, and the mass/support/finiteness conditions on `cm_rescaled f n`, there exists a finite measure $\mu_0$ supported on $[0,\infty)$ with
$$f(t) = L + \int_0^\infty e^{-tp}\,d\mu_0(p) \quad \text{for all } t \ge 0.$$

**Proof**: Shifts indices to $\sigma(n) = \mathtt{cm\_rescaled}\; f\; (n+2)$; proves tightness from the CM structure (continuity at 0 gives $f(0) - f(x_0) < \varepsilon/2$, kernel lower bound on $\mathrm{Ioi}\,K$ gives $(1 - e^{-x_0 K})\cdot\sigma_n(\mathrm{Ioi}\,K) \le f(0) - f(x_0)$); applies `finite_measure_subseq_limit` for Prokhorov extraction; verifies the Laplace identity via `diagonal_convergence`, which decomposes $\int \varphi_{n_k+2}\,d\sigma_{n_k}$ into a kernel approximation error (tending to 0 by `kernel_approx_error_tendsto` via uniform convergence of $\varphi_n \to e^{-xp}$) plus $\int e^{-xp}\,d\sigma_{n_k}$ (tending to $\int e^{-xp}\,d\mu_0$ by `tendsto_exp_integral`).

---

### Notable private helpers

| Declaration | Line | Role |
|---|---|---|
| [`ibp_finite_interval`](../../HilleYosida/BernsteinChafai.lean#L101) | 101 | IBP on $[x,T]$: $(k{+}1)$-th Taylor kernel $\to$ boundary term + $k$-th kernel |
| [`tail_setIntegral_tendsto_zero`](../../HilleYosida/BernsteinChafai.lean#L165) | 165 | $\int_{\mathrm{Ioi}\,T} g \to 0$ for integrable $g$ on $(a,\infty)$ |
| [`ibp_kernel_integrableOn`](../../HilleYosida/BernsteinChafai.lean#L396) | 396 | Integrability of the $k$-th Taylor kernel on $(\,x,\infty)$, dominated by `cm_density` |
| [`kernel_uniform_conv`](../../HilleYosida/BernsteinChafai.lean#L1193) | 1193 | $\lVert\varphi_n(x,\cdot) - e^{-x\,\cdot}\rVert_\infty \to 0$ for fixed $x > 0$ via $\lvert(1{-}u/m)^m - e^{-u}\rvert \le u^2/(m{-}u)$ |
| [`kernel_approx_error_tendsto`](../../HilleYosida/BernsteinChafai.lean#L1316) | 1316 | $\int (\varphi_{n+2} - e^{-xp})\,d\sigma_n \to 0$ from uniform convergence + mass bound |
| [`integral_bernstein_kernel_tendsto`](../../HilleYosida/BernsteinChafai.lean#L1368) | 1368 | $\int \varphi_{\varphi(k)+2}\,d\sigma_{\varphi(k)} \to \int e^{-xp}\,d\mu_0$: error + weak convergence |
| [`diagonal_convergence`](../../HilleYosida/BernsteinChafai.lean#L1424) | 1424 | Constant sequence $f(x)-L = \int \varphi\,d\sigma$ converging to $\int e^{-xp}\,d\mu_0$ gives equality |

---

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