instance instUniqueSubtypeMemFinsetIicOfNat_leanBandits : Unique ↥(Finset.Iic 0)

Equations

• instUniqueSubtypeMemFinsetIicOfNat_leanBandits = instUniqueSubtypeMemFinsetIicOfNat_leanBandits._proof_1.mpr (Unique.subtypeEq 0)

theorem coe_default_Iic_zero : ↑default = 0

def MeasurableEquiv.piIicZero (X : ℕ → Type u_2) [(n : ℕ) → MeasurableSpace (X n)] : ((i : ↥(Finset.Iic 0)) → X ↑i) ≃ᵐ X 0

Measurable equivalence between Iic 0 → X i and X 0.

Equations

• MeasurableEquiv.piIicZero X = (MeasurableEquiv.piUnique fun (i : ↥(Finset.Iic 0)) => X ↑i).trans (MeasurableEquiv.piIicZero._proof_1 ▸ MeasurableEquiv.refl (X 0))

noncomputable def ProbabilityTheory.Kernel.trajMeasure {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (μ₀ : MeasureTheory.Measure (X 0)) (κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) [∀ (n : ℕ), IsMarkovKernel (κ n)] : MeasureTheory.Measure ((n : ℕ) → X n)

Distribution of the infinite trajectory given the distribution of X 0.

Equations

• ProbabilityTheory.Kernel.trajMeasure μ₀ κ = (MeasureTheory.Measure.map (⇑(MeasurableEquiv.piIicZero X).symm) μ₀).bind ⇑(ProbabilityTheory.Kernel.traj κ 0)

instance ProbabilityTheory.Kernel.instIsProbabilityMeasureForallTrajMeasure {X : ℕ → Type u_1} [(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.IsProbabilityMeasure (trajMeasure μ₀ κ)

theorem ProbabilityTheory.Kernel.traj_map_eq_kernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {a : ℕ} : ((traj κ a).map fun (x : (n : ℕ) → X n) => x (a + 1)) = κ a

theorem ProbabilityTheory.Kernel.partialTraj_compProd_kernel_eq_traj_map {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {a : ℕ} {x₀ : (n : ↥(Finset.Iic 0)) → X ↑n} : ((partialTraj κ 0 a) x₀).compProd (κ a) = MeasureTheory.Measure.map (fun (x : (i : ℕ) → X i) => (Preorder.frestrictLe a x, x (a + 1))) ((traj κ 0) x₀)

theorem ProbabilityTheory.Kernel.trajMeasure_map_frestrictLe_compProd_kernel_eq_trajMeasure_map {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} [MeasureTheory.IsProbabilityMeasure μ₀] {a : ℕ} : (MeasureTheory.Measure.map (Preorder.frestrictLe a) (trajMeasure μ₀ κ)).compProd (κ a) = MeasureTheory.Measure.map (fun (x : (i : ℕ) → X i) => (Preorder.frestrictLe a x, x (a + 1))) (trajMeasure μ₀ κ)

theorem ProbabilityTheory.Kernel.condDistrib_trajMeasure_ae_eq_kernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] {κ : (n : ℕ) → Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {μ₀ : MeasureTheory.Measure (X 0)} [MeasureTheory.IsProbabilityMeasure μ₀] {a : ℕ} [StandardBorelSpace (X (a + 1))] [Nonempty (X (a + 1))] : ⇑𝓛[fun (x : (i : ℕ) → X i) => x (a + 1) | Preorder.frestrictLe a; trajMeasure μ₀ κ] =ᵐ[MeasureTheory.Measure.map (Preorder.frestrictLe a) (trajMeasure μ₀ κ)] ⇑(κ a)

theorem ProbabilityTheory.Kernel.traj_zero_map_eval_zero {X : ℕ → Type u_1} [(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 0) = deterministic ⇑(MeasurableEquiv.piIicZero X) ⋯