# `SemigroupGroupDefs.lean` — Informal Summary

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

## Overview

This short file defines the positive-definiteness condition for functions on the involutive semigroup $[0,\infty) \times \mathbb{R}^d$, where the involution is $(t, a)^* = (t, -a)$. This is the PD condition appearing in the BCR Theorem 4.1.13 and the semigroup-to-group extension.

## Status

**Main result**: Definition only (no theorems)
None --- file is sorry-free.
**Length**: 26 lines, 1 definition + 0 theorems/lemmas

---

## Key declarations

### `IsSemigroupGroupPD` (line 19) --- Definition
A function $F : \mathbb{R} \to (\operatorname{Fin}(d) \to \mathbb{R}) \to \mathbb{C}$ is positive-definite on $[0,\infty) \times \mathbb{R}^d$ if for all $n$, coefficients $c$, times $t_i \ge 0$, and spatial points $a_i$:
$$q = \sum_{i,j} \bar{c}_i\, c_j\, F(t_i + t_j,\; a_j - a_i)$$
satisfies $q.\mathrm{im} = 0$ and $0 \le q.\mathrm{re}$.

**Dependencies**: `Mathlib.MeasureTheory.Integral.Bochner.Basic`, `Mathlib.Analysis.InnerProductSpace.Basic`.

---

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