# `MeasurableModification.lean` --- Informal Summary

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

## Overview

Constructs a measurable **projection** $P \colon (E \to \mathbb{R}) \to \mathrm{WeakDual}\;\mathbb{R}\;E$ that pushes forward the Kolmogorov extension measure $\nu$ (living on the product space $E \to \mathbb{R}$) to a probability measure on the topological dual. The key idea is to identify a full-measure set of "good paths" --- those $\omega$ that are $\mathbb{Q}$-linear and bounded on a countable dense subset --- and extend each good path to a continuous linear functional via the Bounded Linear Extension Theorem (BLT). The resulting projection is measurable (as a pointwise limit of measurable functions) and satisfies $P \circ \mathrm{embed} = \mathrm{id}$, enabling the factorization argument for uniqueness of the Minlos measure.

## Status

**Main results**: `measurable_measurableProjection` (the projection is measurable), `projection_ae_eq` ($P(\omega)(f) = \omega(f)$ $\nu$-a.e.), `uniqueness_via_projection` (uniqueness of the pushforward measure).
**Sorries**: 0.
**Length**: 1106 lines, 7 definition(s) + 24 theorem(s)/lemma(s).

---

### [`weakDualEmbed`](../../Minlos/MeasurableModification.lean#L59) --- Definition (L59)

**Lean signature**
```lean
def weakDualEmbed (E : Type*) [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] :
    WeakDual ℝ E → (E → ℝ)
```

The evaluation embedding sending a continuous linear functional $l \in E'$ to the function $f \mapsto l(f)$. This is injective and measurable but not a `MeasurableEmbedding` in general.

---

### [`weakDualEmbed_apply`](../../Minlos/MeasurableModification.lean#L64) --- Lemma (L64)

**Statement**: For $l \in \mathrm{WeakDual}\;\mathbb{R}\;E$ and $f \in E$, $\mathrm{weakDualEmbed}\;E\;l\;f = l\;f$.

**Proof**: `rfl`.

---

### [`weakDualEmbed_injective`](../../Minlos/MeasurableModification.lean#L67) --- Lemma (L67)

**Statement**: $\mathrm{weakDualEmbed}\;E$ is injective: if two continuous linear functionals agree pointwise, they are equal.

**Proof uses**: `ContinuousLinearMap.ext`.

---

### [`measurable_weakDualEmbed`](../../Minlos/MeasurableModification.lean#L74) --- Lemma (L74)

**Statement**: The embedding $\mathrm{weakDualEmbed}\;E$ is measurable with respect to the cylinder $\sigma$-algebra on $\mathrm{WeakDual}\;\mathbb{R}\;E$ and the product $\sigma$-algebra on $E \to \mathbb{R}$.

**Proof uses**: `measurable_pi_lambda`, `WeakDual.eval_measurable`.

---

### [`qLinearPaths`](../../Minlos/MeasurableModification.lean#L86) --- Definition (L86)

**Lean signature**
```lean
def qLinearPaths (d : ℕ → E) : Set (E → ℝ)
```

The set of paths $\omega \colon E \to \mathbb{R}$ that respect all finite $\mathbb{Q}$-linear combinations of the dense sequence $d$: for every $c \in \mathbb{N} \to_0 \mathbb{Q}$, $\omega\bigl(\sum_i c_i \cdot d(i)\bigr) = \sum_i c_i \cdot \omega(d(i))$. Defined as a countable intersection over $c \in \mathbb{N} \to_0 \mathbb{Q}$.

---

### [`qLinearPaths_measurableSet`](../../Minlos/MeasurableModification.lean#L92) --- Lemma (L92)

**Statement**: $\mathrm{qLinearPaths}\;d$ is a measurable set (countable intersection of measurable sets).

**Proof uses**: `MeasurableSet.iInter`, `measurableSet_eq_fun`, coordinate measurability.

---

### [`boundedPaths`](../../Minlos/MeasurableModification.lean#L112) --- Definition (L112)

**Lean signature**
```lean
def boundedPaths (d : ℕ → E) (p : ℕ → Seminorm ℝ E) : Set (E → ℝ)
```

The set of paths $\omega$ bounded on all finite $\mathbb{Q}$-linear combinations: $\exists\;s\;\text{(finset)},\;C \in \mathbb{N},\;\forall\;c \in \mathbb{N} \to_0 \mathbb{Q}$, $\lvert \omega(\sum c_i \cdot d(i)) \rvert \le C \cdot (s.\sup\;p)(\sum c_i \cdot d(i))$. Combined with $\mathbb{Q}$-linearity this gives uniform continuity on the $\mathbb{Q}$-span.

---

### [`boundedPaths_measurableSet`](../../Minlos/MeasurableModification.lean#L118) --- Lemma (L118)

**Statement**: $\mathrm{boundedPaths}\;d\;p$ is a measurable set (countable union/intersection of measurable sets).

**Proof uses**: `MeasurableSet.iUnion`, `MeasurableSet.iInter`, `measurableSet_le`.

---

### [`goodPaths`](../../Minlos/MeasurableModification.lean#L128) --- Definition (L128)

**Lean signature**
```lean
def goodPaths (d : ℕ → E) (p : ℕ → Seminorm ℝ E) : Set (E → ℝ)
```

The intersection $\mathrm{qLinearPaths}\;d \cap \mathrm{boundedPaths}\;d\;p$. Paths that are both $\mathbb{Q}$-linear and bounded on the dense sequence.

---

### [`goodPaths_measurableSet`](../../Minlos/MeasurableModification.lean#L132) --- Lemma (L132)

**Statement**: $\mathrm{goodPaths}\;d\;p$ is measurable.

**Proof uses**: [`qLinearPaths_measurableSet`](../../Minlos/MeasurableModification.lean#L92), [`boundedPaths_measurableSet`](../../Minlos/MeasurableModification.lean#L118).

---

### [`extensionFun`](../../Minlos/MeasurableModification.lean#L151) --- Definition (L151)

**Lean signature**
```lean
noncomputable def extensionFun [SeparableSpace E] [IsHilbertNuclear E] [Nonempty E]
    (d : ℕ → E) (hd : DenseRange d)
    (p : ℕ → Seminorm ℝ E) (ω : E → ℝ) (hω : ω ∈ goodPaths d p) : E → ℝ
```

The continuous extension of a good path $\omega$ from $\mathrm{range}(d)$ to all of $E$, via `extendFrom`. On good paths, $\omega$ restricted to the dense range is uniformly continuous with respect to a seminorm, so `extendFrom` yields a continuous function agreeing with $\omega$ on $\mathrm{range}(d)$.

---

### [`extensionFun_eq`](../../Minlos/MeasurableModification.lean#L157) --- Private Lemma (L157)

**Statement**: $\mathrm{extensionFun}\;d\;hd\;p\;\omega\;h\omega\;(d\;n) = \omega(d\;n)$ for all $n$.

**Proof**: Shows `ContinuousWithinAt` of $\omega$ at $d(n)$ using the boundedness hypothesis with key bound $\lvert \omega(d\;m) - \omega(d\;n) \rvert \le C \cdot (s.\sup\;p)(d\;m - d\;n)$ via $\mathbb{Q}$-linearity with the Finsupp $\mathrm{single}\;m\;1 + \mathrm{single}\;n\;(-1)$, then applies `extendFrom_eq`.

---

### [`extensionFun_continuous`](../../Minlos/MeasurableModification.lean#L213) --- Private Lemma (L213)

**Statement**: $\mathrm{extensionFun}\;d\;hd\;p\;\omega\;h\omega$ is continuous.

**Proof**: Applies `continuous_extendFrom` with density of $\mathrm{range}(d)$. Shows that the image filter under $\omega$ is Cauchy in $\mathbb{R}$ using the uniform bound from boundedness, then invokes `CompleteSpace.complete`.

---

### [`extensionFun_map_add`](../../Minlos/MeasurableModification.lean#L287) --- Private Lemma (L287)

**Statement**: $\mathrm{extensionFun}$ is additive: $g(x + y) = g(x) + g(y)$ for all $x, y \in E$.

**Proof**: First shows $g(d\;m + d\;n) = g(d\;m) + g(d\;n)$ via $\mathbb{Q}$-linearity and `extendFrom_eq`. Then applies `Continuous.ext_on` twice (fix $y$ in the dense set, then vary $y$) to extend from the dense set to all of $E$.

**Proof uses**: [`extensionFun_eq`](../../Minlos/MeasurableModification.lean#L157), [`extensionFun_continuous`](../../Minlos/MeasurableModification.lean#L213).

---

### [`extensionFun_map_smul`](../../Minlos/MeasurableModification.lean#L386) --- Private Lemma (L386)

**Statement**: $\mathrm{extensionFun}$ respects scalar multiplication: $g(r \cdot x) = r \cdot g(x)$ for all $r \in \mathbb{R}$, $x \in E$.

**Proof**: Three-step density argument. (1) Show $g(q \cdot d\;n) = q \cdot g(d\;n)$ for $q \in \mathbb{Q}$ via $\mathbb{Q}$-linearity. (2) Fix $x = d\;n$ and extend from $\mathbb{Q}$ to $\mathbb{R}$ via `Continuous.ext_on` with `Rat.denseRange_cast`. (3) Fix $r$ and extend from $\mathrm{range}(d)$ to all of $E$ via `Continuous.ext_on`.

**Proof uses**: [`extensionFun_eq`](../../Minlos/MeasurableModification.lean#L157), [`extensionFun_continuous`](../../Minlos/MeasurableModification.lean#L213).

---

### [`extensionCLM`](../../Minlos/MeasurableModification.lean#L481) --- Definition (L481)

**Lean signature**
```lean
noncomputable def extensionCLM [SeparableSpace E] [IsHilbertNuclear E] [Nonempty E]
    (d : ℕ → E) (hd : DenseRange d)
    (p : ℕ → Seminorm ℝ E) (hp_top : WithSeminorms (fun n => p n))
    (ω : E → ℝ) (hω : ω ∈ goodPaths d p) : WeakDual ℝ E
```

Packages `extensionFun` into a `WeakDual ℝ E` (i.e., a continuous linear map $E \to_L \mathbb{R}$) using the additivity, scalar-multiplication, and continuity lemmas.

**Proof uses**: [`extensionFun`](../../Minlos/MeasurableModification.lean#L151), [`extensionFun_map_add`](../../Minlos/MeasurableModification.lean#L287), [`extensionFun_map_smul`](../../Minlos/MeasurableModification.lean#L386), [`extensionFun_continuous`](../../Minlos/MeasurableModification.lean#L213).

---

### [`extensionCLM_eq_on_dense`](../../Minlos/MeasurableModification.lean#L496) --- Theorem (L496)

**Statement**: The extension agrees with $\omega$ on the dense sequence: $\mathrm{extensionCLM}(\omega)(d\;n) = \omega(d\;n)$.

**Proof uses**: [`extensionFun_eq`](../../Minlos/MeasurableModification.lean#L157).

---

### [`embed_mem_goodPaths`](../../Minlos/MeasurableModification.lean#L506) --- Lemma (L506)

**Statement**: For any continuous linear functional $l \in \mathrm{WeakDual}\;\mathbb{R}\;E$, $\mathrm{weakDualEmbed}\;E\;l \in \mathrm{goodPaths}\;d\;p$.

**Proof**: $\mathbb{Q}$-linearity follows from $\mathbb{R}$-linearity of $l$ (`map_sum`, `map_smul`). Boundedness follows from continuity of $l$ via `Seminorm.bound_of_continuous`.

---

### [`extensionCLM_embed`](../../Minlos/MeasurableModification.lean#L541) --- Lemma (L541)

**Statement**: $\mathrm{extensionCLM}(\mathrm{embed}(l)) = l$ for all $l \in \mathrm{WeakDual}\;\mathbb{R}\;E$.

**Proof**: Both sides are continuous linear maps agreeing on the dense set $\mathrm{range}(d)$ (via [`extensionCLM_eq_on_dense`](../../Minlos/MeasurableModification.lean#L496)), hence equal by `Continuous.ext_on` (T2 target).

**Proof uses**: [`embed_mem_goodPaths`](../../Minlos/MeasurableModification.lean#L506), [`extensionCLM_eq_on_dense`](../../Minlos/MeasurableModification.lean#L496).

---

### [`measurableProjectionAux`](../../Minlos/MeasurableModification.lean#L567) --- Definition (L567)

**Lean signature**
```lean
def measurableProjectionAux [SeparableSpace E] [IsHilbertNuclear E] [Nonempty E]
    (d : ℕ → E) (hd : DenseRange d)
    (p : ℕ → Seminorm ℝ E) (hp_top : WithSeminorms (fun n => p n)) :
    (E → ℝ) → WeakDual ℝ E
```

Auxiliary projection given explicit dense sequence and seminorms. On good paths, applies `extensionCLM`; on bad paths, returns $0$.

---

### [`measurableProjection`](../../Minlos/MeasurableModification.lean#L580) --- Definition (L580)

**Lean signature**
```lean
def measurableProjection [SeparableSpace E] [IsHilbertNuclear E] [Nonempty E] :
    (E → ℝ) → WeakDual ℝ E
```

The canonical measurable projection, instantiating `measurableProjectionAux` with the canonical dense sequence (`denseSeq E`) and the Hilbert-nuclear seminorms from `IsHilbertNuclear E`.

---

### [`measurable_eval_comp_projection`](../../Minlos/MeasurableModification.lean#L589) --- Private Lemma (L589)

**Statement**: For each $f \in E$, the map $\omega \mapsto P(\omega)(f)$ is measurable as a function $(E \to \mathbb{R}) \to \mathbb{R}$.

**Proof**: Defines approximating functions $F_k(\omega) = \omega(d(\varphi(k)))$ on good paths (0 on bad paths), where $d(\varphi(k)) \to f$. Each $F_k$ is measurable. Shows $F_k \to g$ pointwise (on good paths via continuity of the extension; on bad paths both are 0). Concludes by `measurable_of_tendsto_metrizable`.

**Proof uses**: [`goodPaths_measurableSet`](../../Minlos/MeasurableModification.lean#L132), [`extensionFun_eq`](../../Minlos/MeasurableModification.lean#L157), [`extensionFun_continuous`](../../Minlos/MeasurableModification.lean#L213).

---

### [`measurable_measurableProjection`](../../Minlos/MeasurableModification.lean#L652) --- Theorem (L652)

**Statement**: $\mathrm{measurableProjection} \colon (E \to \mathbb{R}) \to \mathrm{WeakDual}\;\mathbb{R}\;E$ is measurable.

**Proof**: The measurable space on $\mathrm{WeakDual}$ is the cylinder $\sigma$-algebra $\bigvee_f \mathrm{comap}(\mathrm{eval}_f, \mathrm{borel}\;\mathbb{R})$. By `MeasurableSpace.comap_iSup`, measurability reduces to showing each $\mathrm{eval}_f \circ P$ is measurable, which is [`measurable_eval_comp_projection`](../../Minlos/MeasurableModification.lean#L589).

**Proof uses**: [`measurable_eval_comp_projection`](../../Minlos/MeasurableModification.lean#L589).

---

### [`projection_embed_eq`](../../Minlos/MeasurableModification.lean#L669) --- Lemma (L669)

**Statement**: $\mathrm{measurableProjection} \circ \mathrm{weakDualEmbed}\;E = \mathrm{id}$: the projection is a left inverse of the embedding.

**Proof**: For any $l$, $\mathrm{embed}(l) \in \mathrm{goodPaths}$ by [`embed_mem_goodPaths`](../../Minlos/MeasurableModification.lean#L506), so the `dif_pos` branch fires, and [`extensionCLM_embed`](../../Minlos/MeasurableModification.lean#L541) gives the result.

**Proof uses**: [`embed_mem_goodPaths`](../../Minlos/MeasurableModification.lean#L506), [`extensionCLM_embed`](../../Minlos/MeasurableModification.lean#L541).

---

### [`qLinearPaths_ae`](../../Minlos/MeasurableModification.lean#L710) --- Theorem (L710)

**Statement**: $\mathbb{Q}$-linearity holds $\nu$-a.e.: $\forall^{\mathrm{ae}}\;\omega,\;\omega \in \mathrm{qLinearPaths}(\mathrm{denseSeq}\;E)$.

**Proof**: For fixed $c \in \mathbb{N} \to_0 \mathbb{Q}$, define $X(\omega) = \omega(\sum c_i \cdot d_i) - \sum c_i \cdot \omega(d_i)$. Using `h_cf_joint` with cleverly chosen test vectors $\{y, d_{i_1}, \ldots, d_{i_k}\}$ and scalars $\{t, -tc_1, \ldots, -tc_k\}$, one shows $\sum s_j \cdot x_j = 0$, so the CF of $X$ equals $\Phi(0) = 1$ for all $t$. Then `ae_eq_zero_of_charfun_eq_one` gives $X = 0$ a.s. Countable intersection over $c$ via `ae_all_iff`.

**Proof uses**: `ae_eq_zero_of_charfun_eq_one` (from `MinlosConcentration`), `h_cf_joint` hypothesis.

---

### [`boundedPaths_tail_bound`](../../Minlos/MeasurableModification.lean#L788) --- Private Lemma (L788)

**Statement**: For any $\varepsilon > 0$, there exist a finset $s$ and $C \in \mathbb{N}$ such that $\nu\{\omega \mid \exists\;c,\;\lvert \omega(\sum c_i \cdot d_i) \rvert > C \cdot (s.\sup\;p)(\sum c_i \cdot d_i)\} < \varepsilon$.

**Proof**: Applies `minlos_concentration` to get a bound in terms of the Hilbert-nuclear seminorms $p'_m$, then converts to the given seminorms $p$ via `Seminorm.bound_of_continuous`.

**Proof uses**: `minlos_concentration` (from `MinlosConcentration`).

---

### [`boundedPaths_ae`](../../Minlos/MeasurableModification.lean#L842) --- Theorem (L842)

**Statement**: Boundedness holds $\nu$-a.e.: $\forall^{\mathrm{ae}}\;\omega,\;\omega \in \mathrm{boundedPaths}(\mathrm{denseSeq}\;E, p)$.

**Proof**: Proof by contradiction. If the bad set has positive measure $\varepsilon_0$, then [`boundedPaths_tail_bound`](../../Minlos/MeasurableModification.lean#L788) provides a finset $s$ and constant $C$ bounding the bad-set measure below $\varepsilon_0$, contradicting the assumption.

**Proof uses**: [`boundedPaths_tail_bound`](../../Minlos/MeasurableModification.lean#L788).

---

### [`goodPaths_ae`](../../Minlos/MeasurableModification.lean#L877) --- Lemma (L877)

**Statement**: $\forall^{\mathrm{ae}}\;\omega,\;\omega \in \mathrm{goodPaths}(\mathrm{denseSeq}\;E, p)$.

**Proof**: Combines [`qLinearPaths_ae`](../../Minlos/MeasurableModification.lean#L710) and [`boundedPaths_ae`](../../Minlos/MeasurableModification.lean#L842) via `filter_upwards`.

**Proof uses**: [`qLinearPaths_ae`](../../Minlos/MeasurableModification.lean#L710), [`boundedPaths_ae`](../../Minlos/MeasurableModification.lean#L842).

---

### [`projection_ae_eq`](../../Minlos/MeasurableModification.lean#L901) --- Theorem (L901)

**Statement**: For each $f \in E$, $P(\omega)(f) = \omega(f)$ for $\nu$-a.e. $\omega$.

**Proof**: Define $Z(\omega) = P(\omega)(f) - \omega(f)$ and $Y_k(\omega) = \omega(d(\varphi(k))) - \omega(f)$ where $d(\varphi(k)) \to f$. Using `h_cf_joint` with $n = 2$, scalars $(t, -t)$, and vectors $(d(\varphi(k)), f)$, the CF of $Y_k$ equals $\Phi(t \cdot (d(\varphi(k)) - f))$. On good paths (full measure), $Y_k(\omega) \to Z(\omega)$. By dominated convergence, $\int e^{itZ}\,d\nu = \lim \int e^{itY_k}\,d\nu = \lim \Phi(t(d(\varphi(k)) - f)) = \Phi(0) = 1$. Then `ae_eq_zero_of_charfun_eq_one` gives $Z = 0$ a.s.

**Proof uses**: [`goodPaths_ae`](../../Minlos/MeasurableModification.lean#L877), [`extensionCLM_eq_on_dense`](../../Minlos/MeasurableModification.lean#L496), [`measurable_measurableProjection`](../../Minlos/MeasurableModification.lean#L652), `ae_eq_zero_of_charfun_eq_one`, `tendsto_integral_of_dominated_convergence`.

---

### [`isProbabilityMeasure_map_projection`](../../Minlos/MeasurableModification.lean#L1013) --- Lemma (L1013)

**Statement**: The pushforward $\nu.\mathrm{map}\;P$ is a probability measure.

**Proof uses**: [`measurable_measurableProjection`](../../Minlos/MeasurableModification.lean#L652), `Measure.isProbabilityMeasure_map`.

---

### [`charFunctional_map_projection`](../../Minlos/MeasurableModification.lean#L1019) --- Lemma (L1019)

**Statement**: The characteristic functional of $\nu.\mathrm{map}\;P$ equals $\Phi$: for all $f \in E$, $\int_l e^{i\,l(f)}\,d(\nu.\mathrm{map}\;P)(l) = \Phi(f)$.

**Proof**: Rewrites via `integral_map`, then uses [`projection_ae_eq`](../../Minlos/MeasurableModification.lean#L901) to replace $P(\omega)(f)$ by $\omega(f)$ a.e., reducing to the single-variable CF hypothesis (derived from `h_cf_joint` with $n = 1$).

**Proof uses**: [`measurable_measurableProjection`](../../Minlos/MeasurableModification.lean#L652), [`projection_ae_eq`](../../Minlos/MeasurableModification.lean#L901).

---

### [`uniqueness_via_projection`](../../Minlos/MeasurableModification.lean#L1046) --- Lemma (L1046)

**Statement**: If $\mu'$ is a probability measure on $\mathrm{WeakDual}\;\mathbb{R}\;E$ with characteristic functional $\Phi$, then $\mu' = \nu.\mathrm{map}\;P$.

**Proof**: (1) Shows $\mu'.\mathrm{map}(\mathrm{embed})$ is a projective limit of the marginal family by verifying the finite-dimensional CF condition via `Measure.ext_of_charFun`. (2) By uniqueness of the projective limit (`marginalProjectiveLimit_unique`), $\mu'.\mathrm{map}(\mathrm{embed}) = \nu$. (3) Then $\mu' = \mu'.\mathrm{map}(\mathrm{embed}).\mathrm{map}(P) = \nu.\mathrm{map}(P)$ using [`projection_embed_eq`](../../Minlos/MeasurableModification.lean#L669) ($P \circ \mathrm{embed} = \mathrm{id}$).

**Proof uses**: [`projection_embed_eq`](../../Minlos/MeasurableModification.lean#L669), [`measurable_measurableProjection`](../../Minlos/MeasurableModification.lean#L652), [`measurable_weakDualEmbed`](../../Minlos/MeasurableModification.lean#L74), `marginalProjectiveLimit_unique`, `Measure.ext_of_charFun`, `marginalMeasure_charFun`.

---

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