LeanMachineLearning exposition

ProbabilityTheory.Kernel.hasLaw_trajMeasure🔗

Minimal Lean file

hasLaw_trajMeasure🔗

LemmaProbabilityTheory.Kernel.hasLaw_trajMeasure
Details

Uniqueness of trajMeasure.

🔗theorem
ProbabilityTheory.Kernel.hasLaw_trajMeasure.{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 μ₀]
  [MeasureTheory.IsFiniteMeasure P] {Y : (n : ℕ) → Ω → X n}
  (hY_meas : ∀ (n : ℕ), Measurable (Y n)) (h0 : HasLaw (Y 0) μ₀ P)
  (h_condDistrib :
    ∀ (n : ℕ),
      HasCondDistrib (Y (n + 1)) (fun ω i => Y (↑i) ω) (κ n) P) :
  HasLaw (fun ω n => Y n ω) (trajMeasure μ₀ κ) P
ProbabilityTheory.Kernel.hasLaw_trajMeasure.{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 μ₀]
  [MeasureTheory.IsFiniteMeasure P]
  {Y : (n : ℕ) → Ω → X n}
  (hY_meas : ∀ (n : ℕ), Measurable (Y n))
  (h0 : HasLaw (Y 0) μ₀ P)
  (h_condDistrib :
    ∀ (n : ℕ),
      HasCondDistrib (Y (n + 1))
        (fun ω i => Y (↑i) ω) (κ n) P) :
  HasLaw (fun ω n => Y n ω)
    (trajMeasure μ₀ κ) P

Code

lemma hasLaw_trajMeasure [IsFiniteMeasure P]
    {Y : (n : ℕ) → Ω → X n} (hY_meas : ∀ n, Measurable (Y n))
    (h0 : HasLaw (Y 0) μ₀ P)
    (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P) :
    HasLaw (fun ω n ↦ Y n ω) (trajMeasure μ₀ κ) P where
  aemeasurable
Body uses (2)
Used by (1)

Actions: Source · Open Issue

Proof
by fun_prop
  map_eq := by
    refine IsProjectiveLimit.unique (P := fun (J : Finset ℕ) ↦ P.map (fun ω (i : J) ↦ Y i ω)) ?_ ?_
    · exact isProjectiveLimit_map (by fun_prop)
    rw [isProjectiveLimit_nat_iff]
    swap; · exact isProjectiveMeasureFamily_map_restrict (by fun_prop)
    intro n
    rw [(hasLaw_Iic_of_forall_hasCondDistrib h0 h_condDistrib n).map_eq,
      trajMeasure_map_frestrictLe]