# `BCR_d0.lean` — Informal Summary

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

## Overview

Proves BCR Theorem 4.1.13 for $d=0$: bounded continuous semigroup-PD functions on $[0,\infty)$ are Laplace transforms of finite positive measures. The proof goes through: (1) PD → alternating forward differences via Vandermonde convolution, (2) iterated integral bridge connecting differences to derivatives, (3) mollifier smoothing to get `IsCompletelyMonotone`, (4) `bernstein_theorem` for each mollified function, (5) Prokhorov extraction of a weak limit, (6) verification of the Laplace representation.

## Status

**Main result**: Fully proven

None — file is sorry-free.

**Length**: 1503 lines, 6 definitions + 18 theorems/lemmas

---

## Key declarations

### `IsSemigroupPD` — Definition
A function $f : \mathbb{R} \to \mathbb{R}$ is semigroup-PD if $\sum_{i,j} c_i c_j f(t_i + t_j) \geq 0$ for all choices of coefficients and times $t_i \geq 0$.

### `IsSemigroupPD.alternating_forwardDiff` — Lemma
Semigroup-PD implies $(-1)^n \Delta_h^n f(t) \geq 0$ for all $n, h > 0, t \geq 0$ (alternating forward differences are nonneg).

### `iterOp_fd_eq_intOp_deriv` — Lemma
The $n$-th iterated forward difference equals the $n$-th iterated integral of the $n$-th derivative (bridge from discrete to smooth).

### `smooth_discrete_cm_implies_cm` — Lemma
A smooth function with nonneg alternating differences is completely monotone.

### `mollify_isCompletelyMonotone` — Lemma
Mollified semigroup-PD functions are completely monotone.

### [`semigroup_pd_laplace`](../../HilleYosida/BCR_d0.lean#L1270) — Theorem
**Statement**: If $f$ is bounded, continuous, and semigroup-PD on $[0,\infty)$, then there exists a finite positive measure $\mu$ on $[0,\infty)$ such that $f(t) = \int_0^\infty e^{-tp}\, d\mu(p)$ for all $t \geq 0$.

**Proof uses**: [`bernstein_theorem`](../../HilleYosida/Bernstein.lean#L2429), `mollify_isCompletelyMonotone`, `mollify_tendsto`, Prokhorov extraction

---

*This file has **6** definitions and **18** theorems/lemmas (0 with sorry).*