# `PositiveDefinite.lean` — Informal Summary

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

## Overview

This file defines positive-definite functions on additive groups and proves their fundamental properties. A function $\varphi : \alpha \to \mathbb{C}$ is positive definite if it satisfies Hermitian symmetry ($\varphi(-x) = \overline{\varphi(x)}$) and the matrix condition that $\sum_{i,j} \overline{c_i}\, c_j\, \varphi(x_i - x_j) \geq 0$ for all finite point sets and coefficient vectors. The file establishes basic consequences (boundedness, value at zero) and proves that the pointwise product of two positive-definite functions is positive definite (Schur product theorem), which is a key ingredient for Gaussian regularization in Bochner's theorem.

## Status
**Main result**: Fully proven
**Gaps**: None --- file is sorry-free.
**Length**: 201 lines, 1 definition(s) + 8 theorem(s)/lemma(s)

---

## Positive Definite Functions

### [`IsPositiveDefinite`](../../Bochner/PositiveDefinite.lean#L63) --- Definition

**Lean signature**
```lean
structure IsPositiveDefinite {α : Type*} [AddGroup α] (φ : α → ℂ) : Prop
```
**Informal**: A function $\varphi : \alpha \to \mathbb{C}$ on an additive group is positive definite if $\varphi(-x) = \overline{\varphi(x)}$ for all $x$ (Hermitian symmetry) and $\mathrm{Re}\bigl(\sum_{i,j} \overline{c_i}\, c_j\, \varphi(x_i - x_j)\bigr) \geq 0$ for every finite collection of points and coefficients (positive semidefiniteness of the kernel matrix).

---

### [`isPositiveDefinite_precomp_linear`](../../Bochner/PositiveDefinite.lean#L70) --- Lemma

**Statement**: If $\psi : H \to \mathbb{C}$ is positive definite and $T : E \to_{\mathbb{R}} H$ is a linear map, then $\psi \circ T$ is positive definite on $E$.

**Proof uses**: `IsPositiveDefinite.hermitian`, `IsPositiveDefinite.nonneg`, `LinearMap.map_neg`

---

### [`IsPositiveDefinite.kernelMatrix_posSemidef`](../../Bochner/PositiveDefinite.lean#L82) --- Lemma (private)

**Statement**: If $\varphi$ is positive definite, then the kernel matrix $[\varphi(x_i - x_j)]_{i,j}$ is positive semidefinite.

**Proof uses**: `IsPositiveDefinite.hermitian`, `IsPositiveDefinite.nonneg`, `Matrix.IsHermitian`, `Matrix.posSemidef_iff_dotProduct_mulVec`, `Complex.nonneg_iff`

---

### [`IsPositiveDefinite.conj_symm`](../../Bochner/PositiveDefinite.lean#L102) --- Lemma

**Statement**: If $\varphi$ is positive definite, then $\varphi(-x) = \overline{\varphi(x)}$.

**Proof uses**: `IsPositiveDefinite.hermitian`

---

### [`IsPositiveDefinite.eval_zero_nonneg`](../../Bochner/PositiveDefinite.lean#L106) --- Lemma

**Statement**: If $\varphi$ is positive definite, then $\mathrm{Re}(\varphi(0)) \geq 0$.

**Proof uses**: `IsPositiveDefinite.nonneg` (with $m = 1$, $x_1 = 0$, $c_1 = 1$)

---

### [`IsPositiveDefinite.eval_zero_real`](../../Bochner/PositiveDefinite.lean#L112) --- Lemma

**Statement**: If $\varphi$ is positive definite, then $\mathrm{Im}(\varphi(0)) = 0$, i.e., $\varphi(0) \in \mathbb{R}$.

**Proof uses**: `IsPositiveDefinite.hermitian` (at $x = 0$, giving $\varphi(0) = \overline{\varphi(0)}$)

---

### [`IsPositiveDefinite.pd_two`](../../Bochner/PositiveDefinite.lean#L122) --- Lemma (private)

**Statement**: For any two points $a, b$ and coefficients $c_0, c_1$, the $2 \times 2$ positive-definiteness inequality holds: $0 \leq \mathrm{Re}\bigl(\overline{c_0}\, c_0\, \varphi(0) + \overline{c_0}\, c_1\, \varphi(a - b) + \overline{c_1}\, c_0\, \varphi(b - a) + \overline{c_1}\, c_1\, \varphi(0)\bigr)$.

**Proof uses**: `IsPositiveDefinite.nonneg` (with $m = 2$)

---

### [`IsPositiveDefinite.bounded_by_zero`](../../Bochner/PositiveDefinite.lean#L130) --- Lemma

**Statement**: If $\varphi$ is positive definite, then $\lVert \varphi(x) \rVert \leq \mathrm{Re}(\varphi(0))$ for all $x$.

**Proof uses**: [`IsPositiveDefinite.pd_two`](../../Bochner/PositiveDefinite.lean#L122), [`IsPositiveDefinite.eval_zero_nonneg`](../../Bochner/PositiveDefinite.lean#L106), [`IsPositiveDefinite.eval_zero_real`](../../Bochner/PositiveDefinite.lean#L112), [`IsPositiveDefinite.hermitian`](../../Bochner/PositiveDefinite.lean#L64), `Complex.mul_conj`, `Complex.normSq_eq_norm_sq`

---

### [`IsPositiveDefinite.mul`](../../Bochner/PositiveDefinite.lean#L180) --- Lemma

**Statement**: If $\varphi$ and $\psi$ are both positive definite, then their pointwise product $x \mapsto \varphi(x)\,\psi(x)$ is positive definite (Schur product theorem for functions).

**Proof uses**: [`IsPositiveDefinite.kernelMatrix_posSemidef`](../../Bochner/PositiveDefinite.lean#L82), `Matrix.PosSemidef.kronecker`, `Matrix.PosSemidef.submatrix`, `Matrix.PosSemidef.dotProduct_mulVec_nonneg`

---

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