# `ProjectiveFamily.lean` — Informal Summary

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

## Overview

This file bridges finite-dimensional Bochner marginals (measures on $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\;n)$) to the `IsProjectiveMeasureFamily` API from Mathlib, enabling application of the Kolmogorov extension theorem. For a continuous positive-definite normalized function $\Phi : E \to \mathbb{C}$, it constructs a family of probability measures indexed by $\mathrm{Finset}\;E$ and proves the family is projective (consistent under coordinate restriction). Finally it applies Kolmogorov extension to obtain a unique probability measure on the full product space $E \to \mathbb{R}$.

## Status
**Main result**: `marginalFamily_isProjective` and `marginalProjectiveLimit` -- fully proven
**Length**: 271 lines, 6 definition(s) + 7 theorem(s)/lemma(s)

---

### Transport Equivalences

#### [`finsetReindexEquiv`](../../Minlos/ProjectiveFamily.lean#L30)

```lean
def finsetReindexEquiv (J : Finset E) :
    (↥J → ℝ) ≃ᵐ (Fin J.card → ℝ)
```

Measurable equivalence between $\prod_{j \in J} \mathbb{R}$ (indexed by the subtype $J$) and $\mathbb{R}^{\lvert J \rvert}$ (indexed by $\mathrm{Fin}\;\lvert J \rvert$), using the canonical enumeration `J.equivFin`.

#### [`finsetPiMeasEquiv`](../../Minlos/ProjectiveFamily.lean#L42)

```lean
def finsetPiMeasEquiv (J : Finset E) :
    (↥J → ℝ) ≃ᵐ EuclideanSpace ℝ (Fin J.card)
```

Measurable equivalence between $\prod_{j \in J} \mathbb{R}$ and $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\;\lvert J \rvert)$. Composition of [`finsetReindexEquiv`](../../Minlos/ProjectiveFamily.lean#L30) with the `WithLp` transport `MeasurableEquiv.toLp 2`.

---

### Marginal Family

#### [`finsetTestVectors`](../../Minlos/ProjectiveFamily.lean#L49)

```lean
def finsetTestVectors (J : Finset E) : Fin J.card → E
```

The test vectors for a finset $J$: the function $i \mapsto J.\mathrm{equivFin}^{-1}(i)$, selecting the $i$-th element of $J$ in its canonical enumeration.

#### [`marginalMeasure`](../../Minlos/ProjectiveFamily.lean#L53)

```lean
def marginalMeasure (Φ : E → ℂ) (hΦ_cont : Continuous Φ)
    (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) (J : Finset E) :
    ProbabilityMeasure (EuclideanSpace ℝ (Fin J.card))
```

The unique Bochner marginal probability measure on $\mathbb{R}^{\lvert J \rvert}$ for the test vectors extracted from finset $J$. Obtained by choosing the witness from [`marginal_measure_exists`](../../Minlos/FinDimMarginals.lean#L84).

#### [`marginalMeasure_charFun`](../../Minlos/ProjectiveFamily.lean#L58)

The characteristic function of `marginalMeasure` equals the marginal CF: for all $\xi$,
$$\mathrm{charFun}(\mu_J)(\xi) = \Phi\!\left(\sum_{i} \xi_i \cdot v_i\right)$$
where $v_i = \mathrm{finsetTestVectors}(J)(i)$.

**Proof depends on**: `marginal_measure_exists` (the `choose_spec`).

#### [`marginalFamily`](../../Minlos/ProjectiveFamily.lean#L67)

```lean
def marginalFamily (Φ : E → ℂ) (hΦ_cont : Continuous Φ)
    (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) :
    ∀ J : Finset E, Measure (∀ j : ↥J, ℝ)
```

The projective family of probability measures indexed by $\mathrm{Finset}\;E$. For each $J$, the Bochner marginal on $\mathrm{EuclideanSpace}\;\mathbb{R}\;(\mathrm{Fin}\;\lvert J \rvert)$ is transported to the Pi-type $\prod_{j \in J} \mathbb{R}$ via the inverse of [`finsetPiMeasEquiv`](../../Minlos/ProjectiveFamily.lean#L42).

#### [`marginalFamily_isFiniteMeasure`](../../Minlos/ProjectiveFamily.lean#L73)

**Instance**: Each measure in the marginal family is finite, via `Measure.isFiniteMeasure_map`.

#### [`marginalFamily_isProbabilityMeasure`](../../Minlos/ProjectiveFamily.lean#L79)

**Instance**: Each measure in the marginal family is a probability measure (total mass 1), via `Measure.isProbabilityMeasure_map` applied to the measurable equivalence.

---

### Projectivity

#### [`marginalFamily_isProjective`](../../Minlos/ProjectiveFamily.lean#L144)

For $J \subseteq I$, the pushforward of $P_I$ along the coordinate restriction $\pi_{I \to J}$ equals $P_J$:
$$(\mathrm{restrict}_J)_\# \, P_I = P_J.$$

**Proof strategy**: Characteristic function uniqueness (`Measure.ext_of_charFun`). The proof constructs:

1. An index injection $\sigma : \mathrm{Fin}\;\lvert J \rvert \hookrightarrow \mathrm{Fin}\;\lvert I \rvert$ (private `finsetIndexInj`).
2. A coordinate projection `euclideanProject` on EuclideanSpace that factors through the Pi-type restriction via [`finsetPiMeasEquiv`](../../Minlos/ProjectiveFamily.lean#L42).
3. A zero-extension $\xi_{\mathrm{ext}}$ of test frequencies from $J$-indices to $I$-indices.
4. An inner product identity $\langle \mathrm{euclideanProject}(y),\, \xi \rangle = \langle y,\, \xi_{\mathrm{ext}} \rangle$ reducing the pushforward CF to a sum identity.

**Proof depends on**: [`marginalMeasure_charFun`](../../Minlos/ProjectiveFamily.lean#L58), `Measure.ext_of_charFun`, `charFun_apply`, `integral_map`, private helpers `finsetIndexInj_injective`, `euclideanProject_measurable`, `euclideanProject_restrict₂`, `finsetTestVectors_comp_inj`.

---

### Kolmogorov Extension

#### [`marginalProjectiveLimit`](../../Minlos/ProjectiveFamily.lean#L240)

```lean
def marginalProjectiveLimit (Φ : E → ℂ) (hΦ_cont : Continuous Φ)
    (hΦ_pd : IsPositiveDefinite Φ) (hΦ_norm : Φ 0 = 1) [Nonempty E] :
    Measure (E → ℝ)
```

The Kolmogorov projective limit of the marginal family: a measure on the full product space $E \to \mathbb{R}$. Obtained by applying `projectiveLimit` from the `KolmogorovExtension4` library to [`marginalFamily`](../../Minlos/ProjectiveFamily.lean#L67) and [`marginalFamily_isProjective`](../../Minlos/ProjectiveFamily.lean#L144).

#### [`marginalProjectiveLimit_isProbability`](../../Minlos/ProjectiveFamily.lean#L247)

**Instance**: The projective limit is a probability measure.

**Proof depends on**: `isProbabilityMeasure_projectiveLimit`, [`marginalFamily_isProjective`](../../Minlos/ProjectiveFamily.lean#L144).

#### [`marginalProjectiveLimit_isProjectiveLimit`](../../Minlos/ProjectiveFamily.lean#L255)

The projective limit projects correctly onto each finite-dimensional marginal: for every $J \in \mathrm{Finset}\;E$, the pushforward of the limit measure along the $J$-coordinate projection equals $P_J$.

**Proof depends on**: `isProjectiveLimit_projectiveLimit`, [`marginalFamily_isProjective`](../../Minlos/ProjectiveFamily.lean#L144).

#### [`marginalProjectiveLimit_unique`](../../Minlos/ProjectiveFamily.lean#L263)

If any measure $\nu$ on $E \to \mathbb{R}$ satisfies the projective limit property with respect to the marginal family, then $\nu$ equals the Kolmogorov extension. That is, the projective limit is unique.

**Proof depends on**: `IsProjectiveLimit.unique`, [`marginalProjectiveLimit_isProjectiveLimit`](../../Minlos/ProjectiveFamily.lean#L255).

---

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