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

Main sections

• ComapTools: Comap σ-algebra utilities
• SequenceShift: Sequence shifting operations
• FinsetOrder: Finset ordering and strict monotonicity lemmas
• IndicatorAlgebra: Helper lemmas for indicator functions

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)

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

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

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_nonneg {Ω : Type u_1} [MeasurableSpace Ω] (A : Set Ω) (c : ℝ) (hc : 0 ≤ c) (ω : Ω) : 0 ≤ A.indicator (fun (x : Ω) => c) ω

Indicator is nonnegative when constant is nonnegative.