LeanMachineLearning exposition

ProbabilityTheory.Kernel.traj_zero_map_eval_zero🔗

Minimal Lean file

traj_zero_map_eval_zero🔗

LemmaProbabilityTheory.Kernel.traj_zero_map_eval_zero
Details

No docstring.

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

Code

lemma traj_zero_map_eval_zero :
    (Kernel.traj κ 0).map (fun h ↦ h (default : Iic 0))
      = Kernel.deterministic (MeasurableEquiv.piUnique (fun i : Iic 0 ↦ X i))
        (MeasurableEquiv.piUnique _).measurable
Used by (1)

Actions: Source · Open Issue

Proof
by
  suffices (Kernel.traj κ 0).map (fun h ↦ h (default : Iic 0))
      = (Kernel.partialTraj κ 0 0).map (MeasurableEquiv.piUnique (fun i : Iic 0 ↦ X i)) by
    rwa [Kernel.partialTraj_zero, Kernel.deterministic_map] at this
    fun_prop
  rw [← Kernel.traj_map_frestrictLe, ← Kernel.map_comp_right _ (by fun_prop) (by fun_prop)]
  rfl