theorem coe_default_Iic_zero : ↑default = 0

theorem ProbabilityTheory.Kernel.traj_zero_map_eval_zero {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] : ((traj κ 0).map fun (h : (n : ℕ) → X n) => h ↑default) = deterministic ⇑(MeasurableEquiv.piUnique fun (i : ↥(Finset.Iic 0)) => X ↑i) ⋯

def MeasurableEquiv.IicSuccProd (X : ℕ → Type u_3) [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) : ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ ((i : ↥(Finset.Iic n)) → X ↑i) × X (n + 1)

Measurable equivalence between a product up to n + 1 and the pair of the product up to n and the space at n + 1.

Equations

• MeasurableEquiv.IicSuccProd X n = (MeasurableEquiv.IicProdIoc ⋯).symm.trans ((MeasurableEquiv.refl ((i : ↥(Finset.Iic n)) → X ↑i)).prodCongr (MeasurableEquiv.piSingleton n).symm)

theorem ProbabilityTheory.Kernel.symm_IicSuccProd {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) : (MeasurableEquiv.IicSuccProd X n).symm = ((MeasurableEquiv.refl ((i : ↥(Finset.Iic n)) → X ↑i)).prodCongr (MeasurableEquiv.piSingleton n)).trans (MeasurableEquiv.IicProdIoc ⋯)

@[simp]

theorem ProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_apply {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) (h : (i : ↥(Finset.Iic (n + 1))) → X ↑i) : (MeasurableEquiv.IicSuccProd X n) h = (fun (i : ↥(Finset.Iic n)) => h ⟨↑i, ⋯⟩, h ⟨n + 1, ⋯⟩)

theorem ProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (e₁ : α ≃ᵐ β) (e₂ : γ ≃ᵐ δ) : ⇑(e₁.prodCongr e₂) = Prod.map ⇑e₁ ⇑e₂

theorem ProbabilityTheory.Kernel.MeasurableEquiv.coe_refl {α : Type u_3} {mα : MeasurableSpace α} : ⇑(MeasurableEquiv.refl α) = id

theorem ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} [MeasureTheory.IsProbabilityMeasure μ₀] [∀ (n : ℕ), StandardBorelSpace (X n)] [∀ (n : ℕ), Nonempty (X n)] {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) (h_condDistrib : ∀ (n : ℕ), HasCondDistrib (Y (n + 1)) (fun (ω : Ω) (i : ↥(Finset.Iic n)) => Y (↑i) ω) (κ n) P) (n : ℕ) : HasLaw (fun (ω : Ω) (i : ↥(Finset.Iic n)) => Y (↑i) ω) ((MeasureTheory.Measure.map (⇑(MeasurableEquiv.piUnique fun (i : ↥(Finset.Iic 0)) => X ↑i).symm) μ₀).bind ⇑(partialTraj κ 0 n)) P

theorem ProbabilityTheory.Kernel.trajMeasure_map_frestrictLe {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} (n : ℕ) : MeasureTheory.Measure.map (Preorder.frestrictLe n) (trajMeasure μ₀ κ) = (MeasureTheory.Measure.map (⇑(MeasurableEquiv.piUnique fun (i : ↥(Finset.Iic 0)) => X ↑i).symm) μ₀).bind ⇑(partialTraj κ 0 n)

theorem ProbabilityTheory.Kernel.eq_trajMeasure {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure P] {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} [MeasureTheory.IsProbabilityMeasure μ₀] [∀ (n : ℕ), StandardBorelSpace (X n)] [∀ (n : ℕ), Nonempty (X n)] {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ (n : ℕ), Measurable (Y n)) (h0 : HasLaw (Y 0) μ₀ P) (h_condDistrib : ∀ (n : ℕ), HasCondDistrib (Y (n + 1)) (fun (ω : Ω) (i : ↥(Finset.Iic n)) => Y (↑i) ω) (κ n) P) : MeasureTheory.Measure.map (fun (ω : Ω) (n : ℕ) => Y n ω) P = trajMeasure μ₀ κ

Uniqueness of trajMeasure.