LeanMachineLearning exposition

ProbabilityTheory.Kernel.eq_trajMeasure_map_frestrictLe🔗

Minimal Lean file

eq_trajMeasure_map_frestrictLe🔗

LemmaProbabilityTheory.Kernel.eq_trajMeasure_map_frestrictLe
Details

No docstring.

🔗theorem
ProbabilityTheory.Kernel.eq_trajMeasure_map_frestrictLe.{u_1, u_2}
  {Ω : 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 => Y (↑i) ω) (κ n) P) :
  MeasureTheory.Measure.map (fun ω n => Y (↑n) ω) P =
    MeasureTheory.Measure.map (Preorder.frestrictLe N)
      (trajMeasure μ₀ κ)
ProbabilityTheory.Kernel.eq_trajMeasure_map_frestrictLe.{u_1,
    u_2}
  {Ω : 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 => Y (↑i) ω) (κ n) P) :
  MeasureTheory.Measure.map
      (fun ω n => Y (↑n) ω) P =
    MeasureTheory.Measure.map
      (Preorder.frestrictLe N)
      (trajMeasure μ₀ κ)

Code

lemma eq_trajMeasure_map_frestrictLe {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N : ℕ}
    (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) :
    P.map (fun ω (n : Iic N) ↦ Y n ω) = (trajMeasure μ₀ κ).map (frestrictLe N)
Body uses (2)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [(hasLaw_Iic_of_forall_hasCondDistrib' h0 h_condDistrib le_rfl).map_eq,
    trajMeasure_map_frestrictLe]