Helper Lemmas for Martingale-based de Finetti Proof

This file contains technical helper lemmas extracted from ViaMartingale.lean. These are general-purpose utilities for:

• Comap (pullback σ-algebra) operations
• Sequence shifting and manipulation
• Finset ordering and monotonicity
• Indicator algebra
• Re-exports from PathSpace.CylinderHelpers for backward compatibility

All lemmas are complete (no sorries) and have been validated for code quality.

Main sections

• ComapTools: Comap σ-algebra utilities
• SequenceShift: Sequence shifting operations
• FinsetOrder: Finset ordering and strict monotonicity lemmas
• IndicatorAlgebra: Helper lemmas for indicator functions
• Re-exports from PathSpace.CylinderHelpers for compatibility

theorem Exchangeability.DeFinetti.MartingaleHelpers.comap_comp_le {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [MeasurableSpace X] [MeasurableSpace Y] [MeasurableSpace Z] (f : X → Y) (g : Y → Z) (hg : Measurable g) : MeasurableSpace.comap (g ∘ f) inferInstance ≤ MeasurableSpace.comap f inferInstance

If g is measurable, then comap (g ∘ f) ≤ comap f.

def Exchangeability.DeFinetti.MartingaleHelpers.shiftSeq {β : Type u_1} (d : ℕ) (f : ℕ → β) : ℕ → β

Shift a sequence by dropping the first d entries.

Equations

• Exchangeability.DeFinetti.MartingaleHelpers.shiftSeq d f n = f (n + d)

@[simp]

theorem Exchangeability.DeFinetti.MartingaleHelpers.shiftSeq_apply {β : Type u_1} {d : ℕ} (f : ℕ → β) (n : ℕ) : shiftSeq d f n = f (n + d)

theorem Exchangeability.DeFinetti.MartingaleHelpers.measurable_shiftSeq {β : Type u_1} [MeasurableSpace β] {d : ℕ} : Measurable (shiftSeq d)

theorem Exchangeability.DeFinetti.MartingaleHelpers.forall_mem_erase {γ : Type u_2} [DecidableEq γ] {s : Finset γ} {a : γ} {P : γ → Prop} (ha : a ∈ s) : (∀ x ∈ s, P x) ↔ P a ∧ ∀ x ∈ s.erase a, P x

theorem Exchangeability.DeFinetti.MartingaleHelpers.orderEmbOfFin_strictMono {s : Finset ℕ} : StrictMono fun (i : Fin s.card) => (s.orderEmbOfFin ⋯) i

theorem Exchangeability.DeFinetti.MartingaleHelpers.orderEmbOfFin_mem {s : Finset ℕ} {i : Fin s.card} : (s.orderEmbOfFin ⋯) i ∈ s

theorem Exchangeability.DeFinetti.MartingaleHelpers.orderEmbOfFin_surj {s : Finset ℕ} {x : ℕ} (hx : x ∈ s) : ∃ (i : Fin s.card), (s.orderEmbOfFin ⋯) i = x

theorem Exchangeability.DeFinetti.MartingaleHelpers.strictMono_fin_cases {n : ℕ} {f : Fin n → ℕ} (hf : StrictMono f) {a : ℕ} (ha : ∀ (i : Fin n), a < f i) : StrictMono fun (i : Fin (n + 1)) => Fin.cases a (fun (i : Fin n) => f i) i

If f : Fin n → ℕ is strictly monotone and a < f i for all i, then Fin.cases a f : Fin (n+1) → ℕ is strictly monotone.

theorem Exchangeability.DeFinetti.MartingaleHelpers.indicator_mul_indicator_eq_indicator_inter {Ω : Type u_1} [MeasurableSpace Ω] (A B : Set Ω) (c d : ℝ) : ((A.indicator fun (x : Ω) => c) * B.indicator fun (x : Ω) => d) = (A ∩ B).indicator fun (x : Ω) => c * d

The product of two indicator functions equals the indicator of their intersection.

theorem Exchangeability.DeFinetti.MartingaleHelpers.indicator_comp_preimage {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (f : Ω → α) (B : Set α) (c : ℝ) : (B.indicator fun (x : α) => c) ∘ f = (f ⁻¹' B).indicator fun (x : Ω) => c

Indicator function composed with preimage.

theorem Exchangeability.DeFinetti.MartingaleHelpers.indicator_binary {Ω : Type u_1} [MeasurableSpace Ω] (A : Set Ω) (ω : Ω) : A.indicator (fun (x : Ω) => 1) ω = 0 ∨ A.indicator (fun (x : Ω) => 1) ω = 1

Binary indicator takes values in {0, 1}.

theorem Exchangeability.DeFinetti.MartingaleHelpers.indicator_le_const {Ω : Type u_1} [MeasurableSpace Ω] (A : Set Ω) (c : ℝ) (hc : 0 ≤ c) (ω : Ω) : A.indicator (fun (x : Ω) => c) ω ≤ c

Indicator is bounded by its constant.

theorem Exchangeability.DeFinetti.MartingaleHelpers.indicator_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (A : Set Ω) (c : ℝ) (hc : 0 ≤ c) (ω : Ω) : 0 ≤ A.indicator (fun (x : Ω) => c) ω

Indicator is nonnegative when constant is nonnegative.