The invariant conditional law

On path space, the conditional law of the initial coordinate given the shift-invariant σ-algebra MeasurableSpace.invariants (shift α), bundled as a random probability measure.

It is named a conditional law, not a directing measure: this file does not prove that it directs the process, and Tau Ceti reserves "directing measure" for a witness of ConditionallyIIDWith. That name belongs with the theorem, not here. It is deliberately a separate object from directingProbabilityMeasure, which conditions on the process tail: the two σ-algebras are not interchangeable — invariants_shift_le_pathTail is one-sided, and invariants_shift_lt_pathTail shows the inclusion is strict over Bool — so sharing the underlying construction asserts nothing about the witnesses being equal. Whether they agree a.e. is a separate question, not settled here.

Main results

• invariantConditionalProbabilityMeasure — the witness;
• invariantConditionalProbabilityMeasure_toMeasure — its underlying measure, the abstraction boundary that lets measure-level operations cross without unfolding the definition;
• measurable_invariants_invariantConditionalProbabilityMeasure — measurability relative to the invariant σ-algebra;
• measurable_invariantConditionalProbabilityMeasure — the ambient corollary;
• invariantConditionalProbabilityMeasure_ae_eq_condExp — the characteristic property: evaluated on a measurable set, it is a version of the conditional expectation of that set's indicator at coordinate 0, given the invariant σ-algebra.

Nothing here proves that this witness directs the process; that is the Koopman block factorization, which is not part of this file.

Adapted from DeFinetti/DirectingMeasure/Basic.lean, which carries the attribution to cameronfreer/exchangeability (DeFinetti/ViaMartingale/DirectingMeasure.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22). The specialization here is the conditioning σ-algebra: that file conditions on tailProcess X, this one on MeasurableSpace.invariants (shift α), with the shared bundling factored through Kernel.probabilityMeasure.

noncomputable def TauCeti.Probability.invariantConditionalProbabilityMeasure {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] (ρ : MeasureTheory.Measure (ℕ → α)) [MeasureTheory.IsFiniteMeasure ρ] : (ℕ → α) → MeasureTheory.ProbabilityMeasure α

The invariant conditional law: the conditional law of the initial coordinate x 0 given the shift-invariant σ-algebra, bundled as a ProbabilityMeasure.

The invariant σ-algebra is a non-ambient MeasurableSpace on ℕ → α, so it must be pinned at every layer — both on the bundling wrapper and on the condDistrib whose fibres it bundles.

Equations

• TauCeti.Probability.invariantConditionalProbabilityMeasure ρ = TauCeti.Probability.Kernel.probabilityMeasure (ProbabilityTheory.condDistrib (fun (x : ℕ → α) => x 0) id ρ)

@[simp]

theorem TauCeti.Probability.invariantConditionalProbabilityMeasure_toMeasure {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] (x : ℕ → α) : ↑(invariantConditionalProbabilityMeasure ρ x) = (ProbabilityTheory.condDistrib (fun (x : ℕ → α) => x 0) id ρ) x

The underlying measure is the invariant-indexed condDistrib fibre.

This is the abstraction boundary: downstream measure-level reasoning goes through this lemma rather than unfolding the definition.

theorem TauCeti.Probability.measurable_invariants_invariantConditionalProbabilityMeasure {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] : Measurable (invariantConditionalProbabilityMeasure ρ)

The invariant conditional law is measurable with respect to the invariant σ-algebra.

theorem TauCeti.Probability.measurable_invariantConditionalProbabilityMeasure {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] : Measurable (invariantConditionalProbabilityMeasure ρ)

The ambient corollary, by monotonicity along MeasurableSpace.invariants_le.

theorem TauCeti.Probability.invariantConditionalProbabilityMeasure_ae_eq_condExp {α : Type u_1} [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α] {ρ : MeasureTheory.Measure (ℕ → α)} [MeasureTheory.IsFiniteMeasure ρ] {B : Set α} (hB : MeasurableSet B) : (fun (x : ℕ → α) => (↑(invariantConditionalProbabilityMeasure ρ x)).real B) =ᵐ[ρ] ρ[(B.indicator fun (x : α) => 1) ∘ fun (x : ℕ → α) => x 0 | MeasurableSpace.invariants (shift α)]

Characteristic property. Evaluated on a measurable set B, the invariant conditional law is a version of the conditional expectation of 𝟙_B ∘ (· 0) given the shift-invariant σ-algebra.

This is what identifies the witness: everything the Koopman route needs to know about it is that its evaluations are these conditional expectations.