The de Finetti directing measure

For a process X : ℕ → Ω → α valued in a standard Borel space α, directingMeasure μ X ω is the conditional law of the initial coordinate X 0 given the process tail σ-algebra tailProcess X, realised as Mathlib's regular conditional distribution condDistrib of X 0, conditioning on tailProcess X via the identity map:

directingMeasure μ X ω = condDistrib (X 0) (id) μ ω    (conditioning on tailProcess X).

Because it lives over the value space α, it needs only [StandardBorelSpace α] (and [Nonempty α]); the sample space Ω is an arbitrary measurable space.

This is the tail-conditioned directing measure: the object the martingale route proves to be a ConditionallyIIDWith witness, and the one any route conditioning on tailProcess X will use. A route conditioning on a different σ-algebra builds its own conditional law — see DeFinetti.ViaKoopman.InvariantConditionalLaw for the shift-invariant one, which ContractableLaw.conditionallyIIDWith_invariantConditionalProbabilityMeasure proves is a witness in its own right — and whether two such objects agree a.e. is a theorem about them, not a property of this file.

This file records the basic theory: it is a probability measure (isProbabilityMeasure_directingMeasure), its set evaluations are tailProcess X-measurable (measurable_tailProcess_directingMeasure_coe, with the ambient corollary measurable_directingMeasure_coe), and it is the conditional law of X 0 given the tail (directingMeasure_ae_eq_condExp). It is also bundled as the ProbabilityMeasure-valued directingProbabilityMeasure, measurable at the tailProcess X level (measurable_tailProcess_directingProbabilityMeasure, with the ambient corollary measurable_directingProbabilityMeasure) — the form MixedIIDWith consumes as its witness ν. The block-product factorisation (conditional independence across a whole block) is a separate concern and lives with the routes that establish it.

Adapted from cameronfreer/exchangeability (DeFinetti/ViaMartingale/DirectingMeasure.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22); that version conditions over Ω (needing [StandardBorelSpace Ω]), here strengthened to the value-space formulation over Mathlib's condDistrib and the Tau Ceti tailProcess API.

noncomputable def TauCeti.Probability.directingMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X : ℕ → Ω → α) (ω : Ω) : MeasureTheory.Measure α

The de Finetti directing measure: the conditional law of the initial coordinate X 0 given the process tail σ-algebra tailProcess X, as the regular conditional distribution of X 0 given that σ-algebra (Mathlib's condDistrib, conditioning on tailProcess X via the identity map). It lives over the value space α, so it needs α standard Borel, not Ω.

Equations

• TauCeti.Probability.directingMeasure μ X ω = (ProbabilityTheory.condDistrib (X 0) id μ) ω

instance TauCeti.Probability.isProbabilityMeasure_directingMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {ω : Ω} : MeasureTheory.IsProbabilityMeasure (directingMeasure μ X ω)

The directing measure is a probability measure: the regular conditional distribution is a Markov kernel.

theorem TauCeti.Probability.measurable_tailProcess_directingMeasure_coe {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} {B : Set α} (hB : MeasurableSet B) : Measurable fun (ω : Ω) => (directingMeasure μ X ω) B

The characteristic measurability of the directing measure: each set-evaluation ω ↦ directingMeasure μ X ω B is tailProcess X-measurable (it is a coordinate of the conditional-distribution kernel conditioning on tailProcess X).

theorem TauCeti.Probability.measurable_directingMeasure_coe {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hTail : tailProcess X ≤ inferInstance) {B : Set α} (hB : MeasurableSet B) : Measurable fun (ω : Ω) => (directingMeasure μ X ω) B

Ambient-measurability of the set-evaluation, a corollary of the tailProcess-measurable form via hTail : tailProcess X ≤ ‹MeasurableSpace Ω›.

theorem TauCeti.Probability.directingMeasure_ae_eq_condExp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hTail : tailProcess X ≤ inferInstance) (hX0 : Measurable (X 0)) {B : Set α} (hB : MeasurableSet B) : (fun (ω : Ω) => (directingMeasure μ X ω).real B) =ᵐ[μ] μ[(B.indicator fun (x : α) => 1) ∘ X 0 | tailProcess X]

The directing measure is the conditional law of the initial coordinate X 0 given the tail σ-algebra: for measurable B, the real evaluation ω ↦ directingMeasure μ X ω B is a version of the conditional expectation of 𝟙_B ∘ X 0 given tailProcess X.

noncomputable def TauCeti.Probability.directingProbabilityMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] (X : ℕ → Ω → α) (ω : Ω) : MeasureTheory.ProbabilityMeasure α

The directing measure bundled as a ProbabilityMeasure-valued map — the form that MixedIIDWith consumes as its witness ν.

Equations

• TauCeti.Probability.directingProbabilityMeasure μ X ω = TauCeti.Probability.Kernel.probabilityMeasure (ProbabilityTheory.condDistrib (X 0) id μ) ω

@[simp]

theorem TauCeti.Probability.directingProbabilityMeasure_toMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (ω : Ω) : ↑(directingProbabilityMeasure μ X ω) = directingMeasure μ X ω

The underlying measure of the bundled directing measure is directingMeasure μ X ω.

theorem TauCeti.Probability.measurable_tailProcess_directingProbabilityMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} : Measurable (directingProbabilityMeasure μ X)

The bundled directing measure is tailProcess X-measurable into ProbabilityMeasure α.

theorem TauCeti.Probability.measurable_directingProbabilityMeasure {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hTail : tailProcess X ≤ inferInstance) : Measurable (directingProbabilityMeasure μ X)

The bundled directing measure is measurable into ProbabilityMeasure α — the ambient corollary of the tailProcess X-measurable form, the measurability that MixedIIDWith requires.