Core Infrastructure for ViaKoopman Proof

This file contains foundational infrastructure for the Koopman-based de Finetti proof:

• Reusable micro-lemmas
• Lp coercion lemmas
• Two-sided natural extension infrastructure (Ωℤ, shiftℤ)
• NaturalExtensionData structure
• Helper lemmas for shift operations
• Instance-locking shims for conditional expectation

All lemmas in this file are proved (no sorries).

Extracted from: Infrastructure.lean (Part 1/3) Status: Complete (no sorries in proofs)

API compatibility aliases

Lp coercion lemmas for measure spaces

theorem coeFn_finset_sum {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {p : ENNReal} {ι : Type u_3} (s : Finset ι) (F : ι → ↥(MeasureTheory.Lp E p μ)) : ↑↑(s.sum F) =ᵐ[μ] fun (ω : Ω) => ∑ i ∈ s, ↑↑(F i) ω

Coercion of finite sums in Lp is almost everywhere equal to pointwise sums. This is the measure-space analogue of lp.coeFn_sum (which is for sequence spaces).

Two-sided natural extension infrastructure

@[reducible, inline]

abbrev Exchangeability.DeFinetti.ViaKoopman.Ωℤ (α : Type u_2) : Type u_2

Bi-infinite path space indexed by ℤ.

Equations

• Ωℤ[α] = (ℤ → α)

def Exchangeability.DeFinetti.ViaKoopman.«termΩℤ[_]» : Lean.ParserDescr

Notation for bi-infinite path space ℤ → α.

Equations

• One or more equations did not get rendered due to their size.

def Exchangeability.DeFinetti.ViaKoopman.shiftℤ {α : Type u_1} (ω : Ωℤ[α]) : Ωℤ[α]

The two-sided shift on bi-infinite sequences.

Equations

• Exchangeability.DeFinetti.ViaKoopman.shiftℤ ω n = ω (n + 1)

def Exchangeability.DeFinetti.ViaKoopman.shiftℤInv {α : Type u_1} (ω : Ωℤ[α]) : Ωℤ[α]

The inverse shift on bi-infinite sequences.

Equations

• Exchangeability.DeFinetti.ViaKoopman.shiftℤInv ω n = ω (n - 1)

def Exchangeability.DeFinetti.ViaKoopman.restrictNonneg {α : Type u_1} (ω : Ωℤ[α]) : Ω[α]

Restrict a bi-infinite path to its nonnegative coordinates.

Equations

• Exchangeability.DeFinetti.ViaKoopman.restrictNonneg ω n = ω (Int.ofNat n)

def Exchangeability.DeFinetti.ViaKoopman.extendByZero {α : Type u_1} (ω : Ω[α]) : Ωℤ[α]

Extend a one-sided path to the bi-infinite path space by duplicating the zeroth coordinate on the negative side. This is a convenient placeholder when we only need the right-infinite coordinates.

Equations

• Exchangeability.DeFinetti.ViaKoopman.extendByZero ω (Int.ofNat n) = ω n
• Exchangeability.DeFinetti.ViaKoopman.extendByZero ω (Int.negSucc a) = ω 0

theorem Exchangeability.DeFinetti.ViaKoopman.measurable_shiftℤ {α : Type u_1} [MeasurableSpace α] : Measurable shiftℤ

def Exchangeability.DeFinetti.ViaKoopman.IsShiftInvariantℤ {α : Type u_1} [MeasurableSpace α] (S : Set Ωℤ[α]) : Prop

Two-sided shift-invariant sets. A set is shift-invariant if it is measurable and equals its preimage under the shift.

Equations

• Exchangeability.DeFinetti.ViaKoopman.IsShiftInvariantℤ S = (MeasurableSet S ∧ Exchangeability.DeFinetti.ViaKoopman.shiftℤ ⁻¹' S = S)

theorem Exchangeability.DeFinetti.ViaKoopman.isShiftInvariantℤ_iff {α : Type u_1} [MeasurableSpace α] (S : Set Ωℤ[α]) : IsShiftInvariantℤ S ↔ MeasurableSet S ∧ ∀ (ω : Ωℤ[α]), shiftℤ ω ∈ S ↔ ω ∈ S

@[reducible]

def Exchangeability.DeFinetti.ViaKoopman.shiftInvariantSigmaℤ {α : Type u_1} [MeasurableSpace α] : MeasurableSpace Ωℤ[α]

Shift-invariant σ-algebra on the two-sided path space.

This is defined directly as the sub-σ-algebra of measurable shift-invariant sets.

Equations

• One or more equations did not get rendered due to their size.

theorem Exchangeability.DeFinetti.ViaKoopman.shiftInvariantSigmaℤ_le {α : Type u_1} [MeasurableSpace α] : shiftInvariantSigmaℤ ≤ inferInstance

The shift-invariant σ-algebra is a sub-σ-algebra of the product σ-algebra.

structure Exchangeability.DeFinetti.ViaKoopman.NaturalExtensionData {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure Ω[α]) : Type u_1

Data describing the natural two-sided extension of a one-sided stationary process.

• μhat : MeasureTheory.Measure Ωℤ[α]

  The two-sided extension measure on bi-infinite path space.

• μhat_isProb : MeasureTheory.IsProbabilityMeasure self.μhat
• shift_preserving : MeasureTheory.MeasurePreserving shiftℤ self.μhat self.μhat
• shiftInv_preserving : MeasureTheory.MeasurePreserving shiftℤInv self.μhat self.μhat
• restrict_pushforward : MeasureTheory.Measure.map restrictNonneg self.μhat = μ

General infrastructure lemmas for factor maps and invariance

theorem Exchangeability.DeFinetti.ViaKoopman.integrable_comp_of_pushforward {Ω : Type u_2} {Ω' : Type u_3} [mΩ : MeasurableSpace Ω] [mΩ' : MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} {g : Ω' → Ω} {H : Ω → ℝ} (hg : Measurable g) (hpush : MeasureTheory.Measure.map g μ' = μ) (hH : MeasureTheory.Integrable H μ) : MeasureTheory.Integrable (H ∘ g) μ'

Transport integrability across a pushforward equality and then pull back by composition. This avoids instance gymnastics by rewriting the measure explicitly, then using comp_measurable.

Instance-locking shims for conditional expectation

These wrappers lock the ambient measurable space instance to prevent Lean from synthesizing the sub-σ-algebra as the ambient instance in type class arguments.

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.setIntegral_condExp' {Ω : Type u_2} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (m : MeasurableSpace Ω) (hm : m ≤ mΩ) [MeasureTheory.SigmaFinite (μ.trim hm)] {s : Set Ω} (hs : MeasurableSet s) {f : Ω → ℝ} (hf : MeasureTheory.Integrable f μ) : ∫ (x : Ω) in s, μ[f | m] x ∂μ = ∫ (x : Ω) in s, f x ∂μ

The defining property of conditional expectation on m-measurable sets, with ambient locked.

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.setIntegral_map_preimage {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} (g : Ω' → Ω) (hg : Measurable g) (hpush : MeasureTheory.Measure.map g μ' = μ) (f : Ω → ℝ) (s : Set Ω) (hs : MeasurableSet s) (hf : AEMeasurable f μ) : ∫ (x : Ω') in g ⁻¹' s, (f ∘ g) x ∂μ' = ∫ (x : Ω) in s, f x ∂μ

Set integral change of variables for pushforward measures.

If g : Ω' → Ω pushes forward μ' to μ, then integrating f ∘ g over g ⁻¹' s equals integrating f over s.

Note: we require AEMeasurable f μ and derive AEMeasurable f (Measure.map g μ') by rewriting with hpush.

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.integrable_of_ae_bound {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {f : Ω → ℝ} (hf : AEMeasurable f μ) (hbd : ∃ (C : ℝ), ∀ᵐ (x : Ω) ∂μ, |f x| ≤ C) : MeasureTheory.Integrable f μ

On a finite measure space, an a.e.-bounded, a.e.-measurable real function is integrable.