Finite-dimensional marginal uniqueness

A finite measure on path space ℕ → α is determined by its finite prefix marginals: any measure agreeing with it on every prefix projection (prefixProj α n, the projection to the first n coordinates) is equal to it. This is a thin ℕ-prefix wrapper over Mathlib's projective-limit machinery (IsProjectiveLimit.unique), not new measure theory.

The public API:

• measure_eq_of_prefixProj_map_eq — the map-equality form;
• measure_eq_of_fin_marginals_eq — the setwise form;
• prefixProjPair, measurable_prefixProjPair, prefixProjPair_comp — the same prefix projection, carrying an extra factor along;
• measure_eq_of_prefixProjPair_map_eq — paired finite-marginal uniqueness on T × (ℕ → α).

The paired form reduces to the unpaired one rather than reproving it. Mathlib's IsProjectiveLimit is stated for dependent products ∀ i, α i, and T × (ℕ → α) is not of that shape — but replicating the first factor at every coordinate, (t, x) ↦ fun n => (t, x n), embeds it in ℕ → T × α, which is. That map has an explicit measurable left inverse, so it is injective on measures, and each of its prefix marginals is read off the paired prefix marginal one step longer.

Both apply directly to probability measures, since IsProbabilityMeasure provides IsFiniteMeasure, so no separate probability-measure theorem is needed.

theorem TauCeti.Probability.measure_eq_of_prefixProj_map_eq {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (n : ℕ), MeasureTheory.Measure.map (prefixProj α n) μ = MeasureTheory.Measure.map (prefixProj α n) ν) : μ = ν

Finite-marginal uniqueness. Two measures on ℕ → α, with μ finite, that have the same law under every finite prefix projection prefixProj α n are equal. (Finiteness of ν is not needed: projective-limit uniqueness only requires the prefix-marginal family, supplied by μ, to be finite.)

theorem TauCeti.Probability.measure_eq_of_fin_marginals_eq {α : Type u_1} [MeasurableSpace α] {μ ν : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (n : ℕ) (S : Set (Fin n → α)), MeasurableSet S → (MeasureTheory.Measure.map (prefixProj α n) μ) S = (MeasureTheory.Measure.map (prefixProj α n) ν) S) : μ = ν

Finite-marginal uniqueness, setwise form: two measures on ℕ → α, with μ finite, agreeing on every measurable prefix-cylinder are equal. It assumes only μ is finite; ν's finiteness is forced by the conclusion.

def TauCeti.Probability.prefixProjPair (T : Type u_2) (α : Type u_3) (n : ℕ) : T × (ℕ → α) → T × (Fin n → α)

The prefix map onto the first n path coordinates, keeping the first factor.

Equations

• TauCeti.Probability.prefixProjPair T α n q = (q.1, fun (i : Fin n) => q.2 ↑i)

@[simp]

theorem TauCeti.Probability.prefixProjPair_apply {T : Type u_2} {α : Type u_3} (n : ℕ) (q : T × (ℕ → α)) : prefixProjPair T α n q = (q.1, fun (i : Fin n) => q.2 ↑i)

Applying the paired prefix map.

theorem TauCeti.Probability.measurable_prefixProjPair (T : Type u_2) (α : Type u_3) [MeasurableSpace T] [MeasurableSpace α] (n : ℕ) : Measurable (prefixProjPair T α n)

The paired prefix projection is measurable: it keeps the first factor and reads finitely many path coordinates.

Paired prefix marginals

theorem TauCeti.Probability.prefixProjPair_comp {T : Type u_2} {α : Type u_3} {m n : ℕ} (hmn : m ≤ n) : prefixProjPair T α m = (fun (r : T × (Fin n → α)) => (r.1, fun (i : Fin m) => r.2 (Fin.castLE hmn i))) ∘ prefixProjPair T α n

Longer prefixes refine shorter ones.

theorem TauCeti.Probability.measure_eq_of_prefixProjPair_map_eq {α : Type u_1} [MeasurableSpace α] {T : Type u_2} [MeasurableSpace T] {μ ν : MeasureTheory.Measure (T × (ℕ → α))} [MeasureTheory.IsFiniteMeasure μ] (h : ∀ (n : ℕ), MeasureTheory.Measure.map (prefixProjPair T α n) μ = MeasureTheory.Measure.map (prefixProjPair T α n) ν) : μ = ν

Paired finite-marginal uniqueness. Two measures on T × (ℕ → α) that agree under every prefix projection — keeping the T coordinate — are equal.

As with measure_eq_of_prefixProj_map_eq, only one of the two measures need be assumed finite: the n = 0 projection already forces the total masses to agree, since prefixProjPair retains the first factor even at the empty prefix.