The joint law of a directing measure and a path

For a process X : ℕ → Ω → α carried along by a candidate directing measure ν : Ω → ProbabilityMeasure α, jointPathLaw μ X ν is the law of the pair (ν ω, fun i => X i ω) on ProbabilityMeasure α × (ℕ → α).

Main declarations

• jointPathLaw — the definition, with jointPathLaw_def its unfolding;
• map_fst_jointPathLaw, map_snd_jointPathLaw — the two marginals, μ.map ν and pathLaw μ X;
• map_prefixProjPair_jointPathLaw — the pushforward along the paired prefix projection.

Nothing here mentions conditional independence: these are facts about the law of a pair, and hold for an arbitrary ν. The conditional statements that consume them — in particular the full-path disintegration identifying this law with a mixture — live in Exchangeability/ConditionallyIID/PathDisintegration.lean.

noncomputable def TauCeti.Probability.jointPathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (ν : Ω → MeasureTheory.ProbabilityMeasure α) : MeasureTheory.Measure (MeasureTheory.ProbabilityMeasure α × (ℕ → α))

The joint path law: the law of the directing measure together with the whole path.

Equations

• TauCeti.Probability.jointPathLaw μ X ν = MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : ℕ) => X i ω)) μ

@[simp]

theorem TauCeti.Probability.jointPathLaw_def {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] (μ : MeasureTheory.Measure Ω) (X : ℕ → Ω → α) (ν : Ω → MeasureTheory.ProbabilityMeasure α) : jointPathLaw μ X ν = MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : ℕ) => X i ω)) μ

The definitional expansion of jointPathLaw: the pushforward of μ along ω ↦ (ν ω, fun i => X i ω).

theorem TauCeti.Probability.map_fst_jointPathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (hν : AEMeasurable ν μ) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : MeasureTheory.Measure.map Prod.fst (jointPathLaw μ X ν) = MeasureTheory.Measure.map ν μ

The first marginal of the joint path law is the law of the directing measure.

theorem TauCeti.Probability.map_snd_jointPathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (hν : AEMeasurable ν μ) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : MeasureTheory.Measure.map Prod.snd (jointPathLaw μ X ν) = pathLaw μ X

The second marginal of the joint path law is the law of the path.

theorem TauCeti.Probability.map_prefixProjPair_jointPathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) (hν : AEMeasurable ν μ) (n : ℕ) : MeasureTheory.Measure.map (prefixProjPair (MeasureTheory.ProbabilityMeasure α) α n) (jointPathLaw μ X ν) = MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin n) => X (↑i) ω)) μ

The prefix pushforward of the joint path law is the joint block law of the first n coordinates.