# `FourierPD.lean` — Informal Summary

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

## Overview

This file proves the "easy direction" of Bochner's theorem: the Fourier transform of a finite positive measure is positive-definite. Concretely, for a finite measure $\mu$ and functions $\chi_j$, the quadratic form $q = \sum_{i,j} \bar{c}_i c_j \int \overline{\chi_i}\, \chi_j\, d\mu$ satisfies $\operatorname{Im}(q) = 0$ and $\operatorname{Re}(q) \ge 0$. The proof swaps sum and integral to write $q = \int \lvert \sum_j c_j \chi_j \rvert^2\, d\mu$ and applies `integral_nonneg`.

## Status

**Main result**: Fully proven (0 sorry's)
None --- file is sorry-free.
**Length**: 72 lines, 0 definitions + 1 theorem

---

## Key declarations

### `pd_quadratic_form_of_measure` (line 34) --- Theorem
For a finite measure $\mu$ on $\alpha$, coefficients $c : \operatorname{Fin}(n) \to \mathbb{C}$, and functions $\chi : \operatorname{Fin}(n) \to \alpha \to \mathbb{C}$ with pairwise products integrable:
$$q = \sum_{i,j} \bar{c}_i\, c_j \int \overline{\chi_i(\xi)}\, \chi_j(\xi)\, d\mu(\xi)$$
satisfies $q.\mathrm{im} = 0$ and $0 \le q.\mathrm{re}$.

**Proof strategy**: Factor the double sum as $\int \lVert \sum_j c_j \chi_j \rVert^2\, d\mu$ via `Complex.normSq_eq_conj_mul_self`, then apply `integral_ofReal` and `integral_nonneg`.

**Dependencies**: `Mathlib.MeasureTheory.Integral.Bochner.Basic`, `Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap`.

---

*This file has **0** definitions and **1** theorem (0 with sorry).*