# `FejerPD.lean` — Informal Summary

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

## Overview

This file proves that the Fourier transform of a continuous, integrable, positive-definite function on a finite-dimensional real inner product space has nonnegative real part. The proof proceeds by Fejer averaging: the double integral $\frac{1}{\mu(B_R)} \iint_{B_R \times B_R} \psi(x-y)\,dx\,dy$ has $\Re \geq 0$ (Step A via Riemann-sum approximation), converges to $\int \psi$ by Fubini and dominated convergence (Step B), and the limit inequality follows by `ge_of_tendsto'` (Step C).

## Status

**Main result**: Fully proven
**Length**: 612 lines, 2 definition(s) + 15 theorem(s)/lemma(s)

---

## Fourier transform of L1 positive-definite functions is nonneg

### [`isPositiveDefinite_exp_inner`](../../Bochner/FejerPD.lean#L55) — Lemma

**Statement**: The exponential character $x \mapsto e^{2\pi i \langle x, \xi \rangle}$ is positive definite; the PD sum equals $\lvert \sum_k c_k e^{2\pi i \langle x_k, \xi \rangle} \rvert^2$.

**Proof uses**: `Complex.exp_conj`, `Complex.normSq_eq_conj_mul_self`, `Complex.normSq_nonneg`

---

## Haar measure neg-invariance

### [`volume_isNegInvariant`](../../Bochner/FejerPD.lean#L92) — Instance

**Lean signature**
```lean
instance volume_isNegInvariant : (volume : Measure V).IsNegInvariant
```
**Informal**: Volume on a finite-dimensional inner product space is negation-invariant, since negation is a linear isometry equivalence.

### [`integral_sub_left_eq`](../../Bochner/FejerPD.lean#L96) — Lemma

**Statement**: Haar translation invariance: $\int f(a - x)\,dx = \int f(x)\,dx$ for any $f : V \to \mathbb{C}$ and $a \in V$.

**Proof uses**: `integral_neg_eq_self`, `integral_add_left_eq_self`

---

## Step A: The PD double integral has nonneg real part

### [`integral_simpleFunc_comp`](../../Bochner/FejerPD.lean#L109) — Lemma

**Statement**: For a simple function $s_n : V \to V$ and any $g : V \to \mathbb{C}$, the integral $\int g(s_n(x))\,d\mu$ equals $\sum_{u \in \mathrm{range}(s_n)} \mu(s_n^{-1}\{u\}) \cdot g(u)$.

**Proof uses**: `Finset.sum_ite_eq'`, `integral_finset_sum`, `integral_indicator`, `setIntegral_const`

### [`pd_double_integral_re_nonneg`](../../Bochner/FejerPD.lean#L130) — Lemma

**Statement**: For a continuous positive-definite function $\psi$ and a bounded measurable set $S$, the double integral $\iint_{S \times S} \psi(x - y)\,dx\,dy$ has nonnegative real part.

**Proof uses**: [`IsPositiveDefinite.nonneg`](../../Bochner/PositiveDefinite.lean#L63), [`IsPositiveDefinite.bounded_by_zero`](../../Bochner/PositiveDefinite.lean#L130), `StronglyMeasurable.approx`, `tendsto_integral_of_dominated_convergence`, `ge_of_tendsto'`, `Complex.continuous_re`

---

## Integral of PD function has nonneg real part

### [`overlapRatio`](../../Bochner/FejerPD.lean#L270) — Definition

**Lean signature**
```lean
private def overlapRatio (R : ℝ) (v : V) : ℝ
```
**Informal**: The overlap ratio $\mu(B_R(0) \cap B_R(v)) / \mu(B_R(0))$, defined to be $0$ when $\mu(B_R(0)) = 0$.

### [`overlapRatio_le_one`](../../Bochner/FejerPD.lean#L276) — Lemma

**Statement**: The overlap ratio satisfies $\mathrm{overlapRatio}(R, v) \leq 1$ for all $R$ and $v$.

**Proof uses**: `div_le_one_of_le₀`, `ENNReal.toReal_mono`, `measure_mono`

### [`overlapRatio_nonneg`](../../Bochner/FejerPD.lean#L285) — Lemma

**Statement**: The overlap ratio satisfies $0 \leq \mathrm{overlapRatio}(R, v)$ for all $R$ and $v$.

**Proof uses**: `div_nonneg`, `ENNReal.toReal_nonneg`

### [`measurable_overlapRatio`](../../Bochner/FejerPD.lean#L291) — Lemma

**Statement**: The function $v \mapsto \mathrm{overlapRatio}(R, v)$ is measurable.

**Proof uses**: `measurable_measure_prodMk_left`, `Measurable.div_const`

### [`closedBall_sub_norm_subset`](../../Bochner/FejerPD.lean#L310) — Lemma

**Statement**: Ball containment: $\overline{B}(0, R - \lVert v \rVert) \subseteq \overline{B}(0, R) \cap \overline{B}(v, R)$.

**Proof uses**: `dist_triangle`

### [`overlapRatio_tendsto_one`](../../Bochner/FejerPD.lean#L325) — Lemma

**Statement**: For fixed $v$, the overlap ratio converges to $1$ as $n \to \infty$: $\mathrm{overlapRatio}(n, v) \to 1$.

**Proof uses**: `Filter.Tendsto.squeeze'`, `Measure.addHaar_closedBall`, `ENNReal.toReal_mul`, `tendsto_natCast_atTop_atTop`, [`closedBall_sub_norm_subset`](../../Bochner/FejerPD.lean#L310), [`overlapRatio_le_one`](../../Bochner/FejerPD.lean#L276)

### [`inner_integral_sub`](../../Bochner/FejerPD.lean#L387) — Lemma

**Statement**: Haar substitution: $\int_{\overline{B}(0,R)} \psi(x - y)\,dy = \int_{\overline{B}(x,R)} \psi(v)\,dv$.

**Proof uses**: `integral_indicator`, `integral_neg_eq_self`, `integral_add_left_eq_self`

### [`indicator_closedBall_inter`](../../Bochner/FejerPD.lean#L410) — Lemma

**Statement**: The nested indicator $\mathbf{1}_{\overline{B}(0,R)}(x) \cdot \mathbf{1}_{\overline{B}(x,R)}(v)$ equals $\mathbf{1}_{\overline{B}(0,R) \cap \overline{B}(v,R)}(x)$, using $\mathrm{dist}(v,x) = \mathrm{dist}(x,v)$.

**Proof uses**: `dist_comm`

### [`integrable_indicator_prod`](../../Bochner/FejerPD.lean#L421) — Lemma

**Statement**: The function $(x, v) \mapsto \mathbf{1}_{\overline{B}(0,R) \cap \overline{B}(v,R)}(x) \cdot \psi(v)$ is integrable on $V \times V$ with respect to the product measure.

**Proof uses**: `Metric.isCompact_of_isClosed_isBounded`, `ContinuousOn.integrableOn_compact`, `Integrable.integrable_indicator`

### [`fejer_avg_eq_integral`](../../Bochner/FejerPD.lean#L463) — Lemma

**Statement**: The Fejer-averaged double integral equals the weighted integral: $\frac{1}{\mu(B_R)} \int_{B_R} \int_{B_R} \psi(x-y)\,dx\,dy = \int_V \mathrm{overlapRatio}(R, v) \cdot \psi(v)\,dv$.

**Proof uses**: [`inner_integral_sub`](../../Bochner/FejerPD.lean#L387), [`indicator_closedBall_inter`](../../Bochner/FejerPD.lean#L410), [`integrable_indicator_prod`](../../Bochner/FejerPD.lean#L421), `integral_integral_swap`, `integral_indicator`, `setIntegral_const`, `setIntegral_congr_fun`

### [`pd_integral_re_nonneg`](../../Bochner/FejerPD.lean#L519) — Lemma

**Statement**: For a continuous, integrable, positive-definite function $\psi : V \to \mathbb{C}$, the integral has nonnegative real part: $0 \leq \Re\!\bigl(\int \psi\bigr)$.

**Proof uses**: [`pd_double_integral_re_nonneg`](../../Bochner/FejerPD.lean#L130), [`fejer_avg_eq_integral`](../../Bochner/FejerPD.lean#L463), [`overlapRatio_tendsto_one`](../../Bochner/FejerPD.lean#L325), [`overlapRatio_nonneg`](../../Bochner/FejerPD.lean#L285), [`overlapRatio_le_one`](../../Bochner/FejerPD.lean#L276), [`measurable_overlapRatio`](../../Bochner/FejerPD.lean#L291), [`IsPositiveDefinite.eval_zero_nonneg`](../../Bochner/PositiveDefinite.lean#L106), `tendsto_integral_of_dominated_convergence`, `ge_of_tendsto'`, `Complex.continuous_re`

---

## Step B + C: The main theorem

### [`pd_l1_fourier_re_nonneg_theorem`](../../Bochner/FejerPD.lean#L576) — Theorem

**Statement**: For a continuous, integrable, positive-definite function $\varphi : V \to \mathbb{C}$ on a finite-dimensional real inner product space, the Fourier transform has nonnegative real part at every point: $0 \leq \Re(\mathcal{F}\varphi(\xi))$ for all $\xi \in V$.

**Proof uses**: [`isPositiveDefinite_exp_inner`](../../Bochner/FejerPD.lean#L55), [`IsPositiveDefinite.mul`](../../Bochner/PositiveDefinite.lean#L180), [`pd_integral_re_nonneg`](../../Bochner/FejerPD.lean#L519), `Real.fourierChar_apply`, `norm_exp_ofReal_mul_I`, `Integrable.mono`

---

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