Conditional i.i.d.-ness under almost-everywhere changes

ConditionallyIIDWith μ X ν constrains the joint law of (ν, block), a Measure.map of μ compared against a Measure.bind over μ. Both sides see X and ν only modulo μ-a.e. equality, so the predicate transports along a coordinatewise a.e. change of the process and along an a.e. change of the directing measure.

The directing-measure congruence is the one that matters in practice. A directing measure is only ever determined a.e. — that is exactly what conditionallyIID_ae_unique says — so any construction of one is free to be modified on a null set, and without this lemma a mathematically valid witness becomes unusable at the interfaces that name it. Measurability is not an a.e. notion and is part of the predicate, so it must be supplied afresh for the new witness.

The mixture-side analogues are in MixedIID/Congr.lean and the symmetry predicates are handled in Exchangeability/Congr.lean.

Main results

• ConditionallyIIDWith.congr_process, ConditionallyIID.congr_process — coordinatewise a.e. equal processes.
• ConditionallyIIDWith.congr_directing — an a.e. equal, measurable directing measure. A merely a.e. measurable replacement ν' is handled by applying it at hν'.mk ν', with hν'.measurable_mk and hνν'.trans hν'.ae_eq_mk.

theorem TauCeti.Probability.ConditionallyIIDWith.congr_process {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) (hXY : ∀ (i : ι), X i =ᵐ[μ] Y i) : ConditionallyIIDWith μ Y ν

Changing the process on a null set. A directing measure for X is one for any coordinatewise a.e. equal Y: the joint law of (ν, block) is unchanged.

theorem TauCeti.Probability.ConditionallyIID.congr_process {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X Y : ι → Ω → α} (h : ConditionallyIID μ X) (hXY : ∀ (i : ι), X i =ᵐ[μ] Y i) : ConditionallyIID μ Y

Changing the process on a null set, existential form.

theorem TauCeti.Probability.ConditionallyIIDWith.congr_directing {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν ν' : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) (hν' : Measurable ν') (hνν' : ν =ᵐ[μ] ν') : ConditionallyIIDWith μ X ν'

Changing the directing measure on a null set. An a.e. equal random probability measure is again a directing measure, provided it is measurable. Both sides of the defining identity move together: the joint law changes only in its first coordinate, and the disintegration is a Measure.bind over μ.