Maps of conditionally i.i.d. families

Two ways of moving ConditionallyIID along a map. Applying a measurable map to the values of every coordinate gives another conditionally i.i.d. family, whose directing measure is the pushforward of the original one; and a family that is conditionally i.i.d. under a pushforward μ.map φ pulls back along φ, in particular from the canonical process on path space to the original process.

Main results

• ConditionallyIIDWith.map_values — the coordinatewise value pushforward, at a named directing measure, together with its existential corollary ConditionallyIID.map_values.
• ConditionallyIIDWith.of_map — pulling the predicate back along a map φ from a pushforward μ.map φ, with directing measure ν ∘ φ.
• ConditionallyIIDWith.of_pathLaw — the transfer at a named directing measure, identifying the transferred witness as ν ∘ (ω ↦ fun i => X i ω).
• conditionallyIID_of_conditionallyIID_pathLaw — its existential corollary.

Implementation

These are the conditional counterparts of MixedIIDWith.map_values and mixedIID_of_mixedIID_pathLaw; the roadmap refers to the second as conditionallyIID_transfer, and asks for the first as the closure of each symmetry class under a coordinatewise pushforward (TauCetiRoadmap/Exchangeability/README.md, Layer 0). Where the mixture predicate needs only the block identity to move, the conditional predicate carries the directing measure along as a coordinate of a joint law, so map_values transports the whole disintegration identity along (Q, x) ↦ (Q.map f, f ∘ x). That map splits as a product, which is what lets Measure.map_prod_map reduce the mixture side to Measure.map_dirac' on the tag and Measure.pi_map_pi on the sampled block.

The path-law transfer is the pullback along the path map φ ω = fun i => X i ω, under which the directing measure transfers as ν ∘ φ. Its purpose is to remove [StandardBorelSpace Ω] from statements proved on path space, which is standard Borel whenever the state space is.

theorem TauCeti.Probability.ConditionallyIIDWith.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {f : α → β} (hf : Measurable f) : ConditionallyIIDWith μ (fun (i : ι) (ω : Ω) => f (X i ω)) fun (ω : Ω) => (ν ω).map f

Conditional i.i.d.-ness is preserved by a coordinatewise measurable map of the value space, at a named directing measure: if X is conditionally i.i.d. with directing measure ν, then fun i ω => f (X i ω) is conditionally i.i.d. with directing measure the pushforward fun ω => (ν ω).map f.

Unlike its mixture counterpart MixedIIDWith.map_values, this moves the joint law of the directing measure and a block, so the transported map acts on the tag as well: it is (Q, x) ↦ (Q.map f, f ∘ x).

theorem TauCeti.Probability.ConditionallyIID.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : ConditionallyIID μ X) {f : α → β} (hf : Measurable f) : ConditionallyIID μ fun (i : ι) (ω : Ω) => f (X i ω)

Conditional i.i.d.-ness is preserved by a coordinatewise measurable map of the value space.

theorem TauCeti.Probability.ConditionallyIIDWith.of_map {Ω : Type u_1} {α : Type u_2} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] {Ω' : Type u_5} [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {φ : Ω → Ω'} (hφ : Measurable φ) {X : ι → Ω' → α} {ν : Ω' → MeasureTheory.ProbabilityMeasure α} (hν : ConditionallyIIDWith (MeasureTheory.Measure.map φ μ) X ν) : ConditionallyIIDWith μ (fun (i : ι) (ω : Ω) => X i (φ ω)) fun (ω : Ω) => ν (φ ω)

Pulling conditional i.i.d.-ness back along a map. If a process X is conditionally i.i.d. with directing measure ν under the pushforward μ.map φ, then its composite with φ is conditionally i.i.d. under μ with directing measure ν ∘ φ.

Both sides of the disintegration identity move along φ: the joint law by Measure.map_map, the mixture by bind_map.

theorem TauCeti.Probability.ConditionallyIIDWith.of_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) {ν : (ℕ → α) → MeasureTheory.ProbabilityMeasure α} (hν : ConditionallyIIDWith (pathLaw μ X) (fun (n : ℕ) (p : ℕ → α) => p n) ν) : ConditionallyIIDWith μ X fun (ω : Ω) => ν fun (i : ℕ) => X i ω

Path-law transfer, at a named directing measure. If the coordinate process is conditionally i.i.d. under the path law of X with directing measure ν, then X is conditionally i.i.d. with directing measure ν ∘ (ω ↦ fun i => X i ω). This is ConditionallyIIDWith.of_map along the path map.

theorem TauCeti.Probability.conditionallyIID_of_conditionallyIID_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (h : ConditionallyIID (pathLaw μ X) fun (n : ℕ) (p : ℕ → α) => p n) : ConditionallyIID μ X

Path-law transfer for the conditional predicate, existential form. The roadmap names this conditionallyIID_transfer; the name here matches its mixture counterpart mixedIID_of_mixedIID_pathLaw.