Lemmas about traj and trajMeasure

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) ⋯

theorem ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib' {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {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 μ₀] {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N n : ℕ} (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun (ω : Ω) (i : ↥(Finset.Iic n)) => Y (↑i) ω) (κ n) P) (hn : n ≤ 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.hasLaw_Iic_of_forall_hasCondDistrib {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {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 μ₀] {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_map_frestrictLe {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {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 μ₀] {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ} (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun (ω : Ω) (i : ↥(Finset.Iic n)) => Y (↑i) ω) (κ n) P) : MeasureTheory.Measure.map (fun (ω : Ω) (n : ↥(Finset.Iic N)) => Y (↑n) ω) P = MeasureTheory.Measure.map (Preorder.frestrictLe N) (trajMeasure μ₀ κ)

theorem ProbabilityTheory.Kernel.hasLaw_trajMeasure {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {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 μ₀] [MeasureTheory.IsFiniteMeasure P] {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) : HasLaw (fun (ω : Ω) (n : ℕ) => Y n ω) (trajMeasure μ₀ κ) P

Uniqueness of trajMeasure.

noncomputable def ProbabilityTheory.Kernel.iicOfFin {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] (κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)) (n : ℕ) : Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))

Kernels indexed by Iic n (as needed for Kernel.traj), obtained from kernels indexed by Fin n: the kernel κ' (n + 1) on Π i : Fin (n + 1), X i is seen as a kernel on Π i : Iic n, X i.

Equations

• ProbabilityTheory.Kernel.iicOfFin κ' n = (κ' (n + 1)).comap ⇑(MeasurableEquiv.finSuccPiIic X n).symm ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicHAddOfNatIicOfFin {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)} [∀ (n : ℕ), IsMarkovKernel (κ' n)] (n : ℕ) : IsMarkovKernel (iicOfFin κ' n)

noncomputable def ProbabilityTheory.Kernel.trajMeasureFin {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] (κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)) [∀ (n : ℕ), IsMarkovKernel (κ' n)] : MeasureTheory.Measure ((n : ℕ) → X n)

Measure on trajectories Π n, X n built from kernels κ' n : Kernel (Π i : Fin n, X i) (X n) describing the law of the coordinate n given the n previous coordinates. The initial measure is κ' 0 default.

Equations

• ProbabilityTheory.Kernel.trajMeasureFin κ' = ProbabilityTheory.Kernel.trajMeasure ((κ' 0) default) (ProbabilityTheory.Kernel.iicOfFin κ')

instance ProbabilityTheory.Kernel.instIsProbabilityMeasureForallTrajMeasureFin {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)) [∀ (n : ℕ), IsMarkovKernel (κ' n)] : MeasureTheory.IsProbabilityMeasure (trajMeasureFin κ')

theorem ProbabilityTheory.Kernel.trajMeasureFin_def {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)} [∀ (n : ℕ), IsMarkovKernel (κ' n)] : trajMeasureFin κ' = trajMeasure ((κ' 0) default) (iicOfFin κ')

theorem ProbabilityTheory.Kernel.hasLaw_eval_zero_trajMeasure {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)} : HasLaw (fun (x : (n : ℕ) → X n) => x 0) μ₀ (trajMeasure μ₀ κ)

theorem ProbabilityTheory.Kernel.hasLaw_eval_zero_trajMeasureFin {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)} [∀ (n : ℕ), IsMarkovKernel (κ' n)] : HasLaw (fun (x : (n : ℕ) → X n) => x 0) ((κ' 0) default) (trajMeasureFin κ')

theorem ProbabilityTheory.Kernel.hasCondDistrib_trajMeasureFin {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)} [∀ (n : ℕ), IsMarkovKernel (κ' n)] (n : ℕ) : HasCondDistrib (fun (x : (n : ℕ) → X n) => x n) (fun (x : (n : ℕ) → X n) (i : Fin n) => x ↑i) (κ' n) (trajMeasureFin κ')

theorem ProbabilityTheory.Kernel.hasLaw_trajMeasureFin {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)} [∀ (n : ℕ), IsMarkovKernel (κ' n)] [MeasureTheory.IsProbabilityMeasure P] {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ (n : ℕ), Measurable (Y n)) (h_condDistrib : ∀ (n : ℕ), HasCondDistrib (Y n) (fun (ω : Ω) (i : Fin n) => Y (↑i) ω) (κ' n) P) : HasLaw (fun (ω : Ω) (n : ℕ) => Y n ω) (trajMeasureFin κ') P

Uniqueness of trajMeasureFin.

theorem ProbabilityTheory.Kernel.eq_trajMeasureFin_map {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] {κ' : (n : ℕ) → Kernel ((i : Fin n) → X ↑i) (X n)} [∀ (n : ℕ), IsMarkovKernel (κ' n)] [MeasureTheory.IsProbabilityMeasure P] {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ (n : ℕ), Measurable (Y n)) {N : ℕ} (h_condDistrib : ∀ n < N, HasCondDistrib (Y n) (fun (ω : Ω) (i : Fin n) => Y (↑i) ω) (κ' n) P) : MeasureTheory.Measure.map (fun (ω : Ω) (i : Fin N) => Y (↑i) ω) P = MeasureTheory.Measure.map (fun (x : (n : ℕ) → X n) (i : Fin N) => x ↑i) (trajMeasureFin κ')