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

Reusable micro-lemmas for Steps 4b–4c

theorem ae_ball_range_mpr {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {n : ℕ} {P : ℕ → Ω → Prop} (h : ∀ k ∈ Finset.range n, ∀ᵐ (ω : Ω) ∂μ, P k ω) : ∀ᵐ (ω : Ω) ∂μ, ∀ k ∈ Finset.range n, P k ω

ae_ball_iff in the direction we need on a finite index set (Finset.range n).

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)

@[simp]

theorem Exchangeability.DeFinetti.ViaKoopman.shiftℤ_apply {α : Type u_1} (ω : Ωℤ[α]) (n : ℤ) : 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)

@[simp]

theorem Exchangeability.DeFinetti.ViaKoopman.shiftℤInv_apply {α : Type u_1} (ω : Ωℤ[α]) (n : ℤ) : shiftℤInv ω n = ω (n - 1)

@[simp]

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

@[simp]

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

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)

@[simp]

theorem Exchangeability.DeFinetti.ViaKoopman.restrictNonneg_apply {α : Type u_1} (ω : Ωℤ[α]) (n : ℕ) : 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

@[simp]

theorem Exchangeability.DeFinetti.ViaKoopman.restrictNonneg_extendByZero {α : Type u_1} (ω : Ω[α]) : restrictNonneg (extendByZero ω) = ω

@[simp]

theorem Exchangeability.DeFinetti.ViaKoopman.extendByZero_apply_nat {α : Type u_1} (ω : Ω[α]) (n : ℕ) : extendByZero ω ↑n = ω n

theorem Exchangeability.DeFinetti.ViaKoopman.restrictNonneg_shiftℤ {α : Type u_1} (ω : Ωℤ[α]) : restrictNonneg (shiftℤ ω) = PathSpace.shift (restrictNonneg ω)

theorem Exchangeability.DeFinetti.ViaKoopman.restrictNonneg_shiftℤInv {α : Type u_1} (ω : Ωℤ[α]) : restrictNonneg (shiftℤInv ω) = fun (n : ℕ) => ω (Int.ofNat n - 1)

theorem Exchangeability.DeFinetti.ViaKoopman.measurable_restrictNonneg {α : Type u_1} [MeasurableSpace α] : Measurable restrictNonneg

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

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

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

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.ae_comp_of_pushforward {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} {g : Ω' → Ω} (hg : Measurable g) (hpush : MeasureTheory.Measure.map g μ' = μ) {P : Ω → Prop} : (∀ᵐ (x : Ω) ∂μ, P x) → ∀ᵐ (x' : Ω') ∂μ', P (g x')

Push AE along a factor map using only null sets and a measurable null superset.

theorem Exchangeability.DeFinetti.ViaKoopman.indicator_preimage_comp {Ω : Type u_2} {Ω' : Type u_3} {g : Ω' → Ω} {B : Set Ω} (K : Ω → ℝ) : (g ⁻¹' B).indicator (K ∘ g) = fun (x' : Ω') => B.indicator K (g x')

Indicator pulls through a preimage under composition.

Infrastructure Lemmas for Conditional Expectation Pullback

This section contains infrastructure lemmas needed for the Koopman approach to de Finetti's theorem. These lemmas handle the interaction between conditional expectation, factor maps, and measure-preserving transformations.

Key Technical Details

The Indicator Trick:

• Converts set integrals ∫ x in s, f x ∂μ to whole-space integrals ∫ x, (indicator s f) x ∂μ
• Avoids measure composition Measure.restrict which has type class defeq issues
• Uses MeasureTheory.integral_indicator for the conversion

Type Class Management (CRITICAL):

• m : MeasurableSpace Ω is a plain parameter, NEVER installed as an instance
• Ambient instance explicitly named: [inst : MeasurableSpace Ω]
• Binder order matters: m must come AFTER all instance parameters
• Measurability lift: have hBm' : @MeasurableSet Ω inst B := hm B hBm

theorem Exchangeability.DeFinetti.ViaKoopman.ae_pullback_iff {Ω : Type u_2} {Ω' : Type u_3} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} (g : Ω' → Ω) (hg : Measurable g) (hpush : MeasureTheory.Measure.map g μ' = μ) {F G : Ω → ℝ} (hF : AEMeasurable F μ) (hG : AEMeasurable G μ) : F =ᵐ[μ] G ↔ F ∘ g =ᵐ[μ'] G ∘ g

AE-pullback along a factor map: Almost-everywhere equalities transport along pushforward.

If g : Ω̂ → Ω is a factor map (i.e., map g μ̂ = μ), then two functions are a.e.-equal on Ω iff their pullbacks are a.e.-equal on Ω̂.

Note: For our use case with restrictNonneg : Ωℤ[α] → Ω[α], the forward direction (which is what we primarily need) works and the map is essentially surjective onto a set of full measure.

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.aestronglyMeasurable_condExp' {Ω : Type u_2} {β : Type u_3} [mΩ : MeasurableSpace Ω] [NormedAddCommGroup β] [NormedSpace ℝ β] [CompleteSpace β] {μ : MeasureTheory.Measure Ω} (m : MeasurableSpace Ω) (_hm : m ≤ mΩ) (f : Ω → β) : MeasureTheory.AEStronglyMeasurable μ[f|m] μ

CE is a.e.-strongly measurable w.r.t. the sub σ-algebra, with ambient locked.

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.

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.abs_indicator_le_abs_self {Ω : Type u_2} (s : Set Ω) (f : Ω → ℝ) (x : Ω) : |s.indicator f x| ≤ |f x|

Norm/abs bound for indicators (ℝ and general normed targets).

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.norm_indicator_le_norm_self {Ω : Type u_2} {E : Type u_3} [SeminormedAddCommGroup E] (s : Set Ω) (f : Ω → E) (x : Ω) : ‖s.indicator f x‖ ≤ ‖f x‖

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.indicator_as_mul_one {Ω : Type u_2} (s : Set Ω) (f : Ω → ℝ) : s.indicator f = fun (x : Ω) => f x * s.indicator (fun (x : Ω) => 1) x

Indicator ↔ product with a 0/1 mask (for ℝ).

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.integral_indicator_as_mul {Ω : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (s : Set Ω) (f : Ω → ℝ) : ∫ (x : Ω), s.indicator f x ∂μ = ∫ (x : Ω), f x * s.indicator (fun (x : Ω) => 1) x ∂μ

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.measurableSet_of_sub {Ω : Type u_2} [mΩ : MeasurableSpace Ω] (m : MeasurableSpace Ω) (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) : MeasurableSet s

"Lift" a measurable-in-sub-σ-algebra set to ambient measurability.

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.aemeasurable_indicator_of_sub {Ω : Type u_2} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (m : MeasurableSpace Ω) (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) {f : Ω → ℝ} (hf : AEMeasurable f μ) : AEMeasurable (s.indicator f) μ

AEMeasurable indicator under ambient from sub-σ-algebra measurability.

theorem Exchangeability.DeFinetti.ViaKoopman.MeasureTheory.condExp_idempotent' {Ω : Type u_2} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (m : MeasurableSpace Ω) (hm : m ≤ mΩ) [MeasureTheory.SigmaFinite (μ.trim hm)] {f : Ω → ℝ} (hf_m : MeasureTheory.AEStronglyMeasurable f μ) (hf_int : MeasureTheory.Integrable f μ) : μ[f|m] =ᵐ[μ] f

Idempotence of conditional expectation for m-measurable integrable functions.

Note: Mathlib API candidates for this standard result:

• condExp_of_stronglyMeasurable (needs StronglyMeasurable, not AEStronglyMeasurable)
• Some version of condexp_of_aestronglyMeasurable (not found in current snapshot)
• Direct proof via uniqueness characterization

The statement is correct and will be used in rectangle-case proofs.