# `SemigroupGroupExtension.lean` — Informal Summary

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

## Overview

This file states and proves the **semigroup-to-group Bochner representation** (BCR Theorem 4.1.13) and derives the **group extension** for positive-definite functions on $[0,\infty) \times \mathbb{R}^d$. The Bochner theorem gives a Fourier-Laplace representation $F(t,a) = \int e^{-tp}\, e^{i\langle a,q\rangle}\, d\mu(p,q)$ for bounded continuous PD functions. The extension theorem constructs a Fourier function $G(t,a) = \int e^{itp}\, e^{i\langle a,q\rangle}\, d\mu(p,q)$ defined for all $t \in \mathbb{R}$, which is bounded, continuous, and positive-definite on the full group.

## Status

**Main result**: Fully proven (0 sorry's)
None --- file is sorry-free. The Bochner theorem delegates to `semigroupGroupBochner_proof` in `BCR_General.lean`. The extension and its PD property are proved directly via `pd_quadratic_form_of_measure`.
**Length**: 271 lines, 0 definitions + 3 theorems/lemmas

---

## Key declarations

### `semigroupGroupBochner` (line 59) --- Theorem
**BCR Theorem 4.1.13.** A bounded continuous PD function $F$ on $[0,\infty) \times \mathbb{R}^d$ is the Fourier-Laplace transform of a finite positive measure $\mu$ supported on $[0,\infty) \times \mathbb{R}^d$:
$$F(t, a) = \int e^{-tp}\, e^{i\langle a, q\rangle}\, d\mu(p, q), \quad t \ge 0.$$

**Proof**: Delegates to `semigroupGroupBochner_proof` from `BCR_General.lean`.

### `semigroupGroupBochnerExtension` (line 104) --- Theorem
**Group extension.** Given the hypotheses of `semigroupGroupBochner`, there exist $\mu$ and $G : \mathbb{R} \to (\operatorname{Fin}(d) \to \mathbb{R}) \to \mathbb{C}$ such that:
1. $F$ has the Laplace representation (for $t \ge 0$),
2. $G(t,a) = \int e^{itp}\, e^{i\langle a,q\rangle}\, d\mu$ for all $t \in \mathbb{R}$,
3. $G$ is bounded ($\lVert G(t,a) \rVert \le \mu(\text{univ})$),
4. $G$ is continuous on $\mathbb{R} \times \mathbb{R}^d$ (via `continuous_of_dominated`),
5. $G$ is PD on all of $\mathbb{R}$: $\sum_{i,j} \bar{c}_i c_j\, G(t_j - t_i, a_j - a_i) \ge 0$.

Note: $G$ is **not** a pointwise extension of $F$. They use different kernels ($e^{-tp}$ vs $e^{itp}$) and are related by analytic continuation $t \mapsto -it$.

The PD property is proved by factoring the quadratic form as $\int \lvert \sum_j c_j\, e^{it_j p + i\langle a_j, q\rangle} \rvert^2\, d\mu$ and applying `pd_quadratic_form_of_measure`.

**Dependencies**: `StronglyContinuousSemigroup.lean`, `FourierPD.lean`, `SemigroupGroupDefs.lean`, `BCR_General.lean`.

---

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