Symmetry notions under a coordinatewise almost-everywhere change of process

Every symmetry predicate of Layer 0 is a statement about the finite-dimensional laws of X, or — for FullyExchangeable — about its path law, so each sees the coordinates only modulo μ-a.e. equality. This file records that: replacing each X i by a coordinatewise a.e. equal Y i changes neither blockLaw, prefixLaw and pathLaw nor any of ExchangeableAt, Exchangeable, FullyExchangeable and Contractable.

Changing a random variable on a null set is routine — most often to replace an a.e. measurable coordinate by a measurable version — and without these lemmas a valid process becomes unusable at the interfaces that demand exact measurability. The representation predicates get the same treatment beside their own definitions, in MixedIID/Congr.lean and ConditionallyIID/Congr.lean.

Main results

• blockLaw_congr, prefixLaw_congr, pathLaw_congr — the finite-dimensional and path laws are unchanged.
• ExchangeableAt.congr, Exchangeable.congr, FullyExchangeable.congr, Contractable.congr — the symmetry predicates transport.

Implementation

Everything reduces to Measure.map_congr: a coordinate selection Fin m → ι is countable, so ae_all_iff turns the coordinatewise hypotheses into a single a.e. statement about the tuple map, and the same argument over ℕ handles the path map.

theorem TauCeti.Probability.blockLaw_congr {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ι → Ω → α} (h : ∀ (i : ι), X i =ᵐ[μ] Y i) {m : ℕ} (k : Fin m → ι) : blockLaw μ X k = blockLaw μ Y k

Coordinatewise a.e. equal families have the same finite-dimensional block laws.

theorem TauCeti.Probability.prefixLaw_congr {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ℕ → Ω → α} (h : ∀ (i : ℕ), X i =ᵐ[μ] Y i) (n : ℕ) : prefixLaw μ X n = prefixLaw μ Y n

Coordinatewise a.e. equal processes have the same prefix laws.

theorem TauCeti.Probability.pathLaw_congr {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ℕ → Ω → α} (h : ∀ (i : ℕ), X i =ᵐ[μ] Y i) : pathLaw μ X = pathLaw μ Y

Coordinatewise a.e. equal processes have the same path law.

theorem TauCeti.Probability.ExchangeableAt.congr {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ℕ → Ω → α} {n : ℕ} (hX : ExchangeableAt μ X n) (h : ∀ (i : ℕ), X i =ᵐ[μ] Y i) : ExchangeableAt μ Y n

Exchangeability at a fixed length transports along a coordinatewise a.e. change of process.

theorem TauCeti.Probability.Exchangeable.congr {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ℕ → Ω → α} (hX : Exchangeable μ X) (h : ∀ (i : ℕ), X i =ᵐ[μ] Y i) : Exchangeable μ Y

Exchangeability transports along a coordinatewise a.e. change of process.

theorem TauCeti.Probability.FullyExchangeable.congr {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ℕ → Ω → α} (hX : FullyExchangeable μ X) (h : ∀ (i : ℕ), X i =ᵐ[μ] Y i) : FullyExchangeable μ Y

Full exchangeability transports along a coordinatewise a.e. change of process.

theorem TauCeti.Probability.Contractable.congr {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ℕ → Ω → α} (hX : Contractable μ X) (h : ∀ (i : ℕ), X i =ᵐ[μ] Y i) : Contractable μ Y

Contractability transports along a coordinatewise a.e. change of process.