# `BCR_General.lean` — Informal Summary

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

## Overview

Proves BCR Theorem 4.1.13 for general $d$: bounded continuous positive-definite functions on $[0,\infty) \times \mathbb{R}^d$ are Fourier-Laplace transforms. The proof decomposes into spatial Bochner (each time slice is PD on $\mathbb{R}^d$), temporal BCR d=0 (each Borel set gives a semigroup-PD function), and product measure assembly.

## Status

**Main result**: Fully proven

None — file is sorry-free.

**Length**: 2822 lines, ~15 definitions + ~20 theorems/lemmas

---

## Key declarations

### `spatial_slice_pd` — Lemma
For fixed $t \geq 0$, the spatial slice $a \mapsto F(t,a)$ is positive-definite on $(\mathbb{R}^d, +)$.

### `spatial_bochner_measures` — Lemma
Bochner's theorem gives spatial measures $\nu_t$ with $F(t,a) = \int e^{i\langle a,q\rangle}\, d\nu_t(q)$.

### `spatial_measures_pd` — Theorem
For each Borel set $B \subseteq \mathbb{R}^d$, $t \mapsto \nu_t(B)$ is semigroup-PD.

### `product_measure_assembly` — Theorem
The family $\{\sigma_B\}$ (Laplace measures for each Borel $B$) assembles into a product measure $\mu$ on $[0,\infty) \times \mathbb{R}^d$.

### [`semigroupGroupBochner_proof`](../../HilleYosida/BCR_General.lean#L2789) — Theorem
**Statement**: BCR 4.1.13: if $F$ is bounded, continuous, and PD on $[0,\infty) \times \mathbb{R}^d$, then
$$F(t,a) = \int e^{-tp} e^{i\langle a,q\rangle}\, d\mu(p,q)$$
for a finite positive measure $\mu$ supported on $[0,\infty) \times \mathbb{R}^d$.

**Proof uses**: [`semigroup_pd_laplace`](../../HilleYosida/BCR_d0.lean#L1270), `bochner_theorem` (external), `spatial_slice_pd`, `product_measure_assembly`

---

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