LeanMachineLearning exposition

ProbabilityTheory.Kernel.trajMeasure_map_frestrictLe🔗

Minimal Lean file

trajMeasure_map_frestrictLe🔗

LemmaProbabilityTheory.Kernel.trajMeasure_map_frestrictLe
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.trajMeasure_map_frestrictLe.{u_2}
  {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.bind
      (MeasureTheory.Measure.map
        (⇑(MeasurableEquiv.symm
            (MeasurableEquiv.piUnique fun i => X ↑i)))
        μ₀)
      ⇑(partialTraj κ 0 n)
ProbabilityTheory.Kernel.trajMeasure_map_frestrictLe.{u_2}
  {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.bind
      (MeasureTheory.Measure.map
        (⇑(MeasurableEquiv.symm
            (MeasurableEquiv.piUnique
              fun i => X ↑i)))
        μ₀)
      ⇑(partialTraj κ 0 n)

Code

lemma trajMeasure_map_frestrictLe (n : ℕ) :
    (trajMeasure μ₀ κ).map (frestrictLe n) =
      (partialTraj κ 0 n) ∘ₘ (μ₀.map (MeasurableEquiv.piUnique _).symm)
Used by (2)

Actions: Source · Open Issue

Proof
by
  rw [trajMeasure, ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc,
    Kernel.deterministic_comp_eq_map, traj_map_frestrictLe]