instance instUniqueSubtypeMemFinsetIicOfNat_leanBandits : Unique { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))} [∀ (n : ℕ), IsMarkovKernel (κ n)] {a : ℕ} {x₀ : (n : { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ 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 : { x : ℕ // x ∈ 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))] : ⇑(condDistrib (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 : { x : ℕ // x ∈ 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) ⋯