ForMathlib.Probability.Kernel.IonescuTulcea.Traj

`coe_default_Iic_zero`🔗

Lemmacoe_default_Iic_zero

Details

No docstring.

theorem

coe_default_Iic_zero : ↑default = 0
coe_default_Iic_zero : ↑default = 0

Code

lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0

Used by (1)

hasLaw_step_zero

Actions: Source · Open Issue

Proof

rfl

`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)

hasLaw_step_zero

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

`IicSuccProd`🔗

DefinitionMeasurableEquiv.IicSuccProd

Details

Measurable equivalence between a product up to n + 1 and the pair of the product up to n and the space at n + 1.

def

MeasurableEquiv.IicSuccProd.{u_3} (X : ℕ → Type u_3)
  [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) :
  ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ
    ((i : ↥(Finset.Iic n)) → X ↑i) × X (n + 1)
MeasurableEquiv.IicSuccProd.{u_3}
  (X : ℕ → Type u_3)
  [(n : ℕ) → MeasurableSpace (X n)]
  (n : ℕ) :
  ((i : ↥(Finset.Iic (n + 1))) → X ↑i) ≃ᵐ
    ((i : ↥(Finset.Iic n)) → X ↑i) ×
      X (n + 1)

Code

def _root_.MeasurableEquiv.IicSuccProd (X : ℕ → Type*) [∀ n, MeasurableSpace (X n)] (n : ℕ) :
    MeasurableEquiv (Π i : Iic (n + 1), X i) ((Π i : Iic n, X i) × X (n + 1)) :=
  (MeasurableEquiv.IicProdIoc (Nat.le_succ n)).symm.trans
    (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) (MeasurableEquiv.piSingleton n).symm)

Used by (11)

Actions: Source · Open Issue

`symm_IicSuccProd`🔗

LemmaProbabilityTheory.Kernel.symm_IicSuccProd

Details

No docstring.

theorem

ProbabilityTheory.Kernel.symm_IicSuccProd.{u_2} {X : ℕ → Type u_2}
  [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ) :
  MeasurableEquiv.symm (MeasurableEquiv.IicSuccProd X n) =
    MeasurableEquiv.trans
      (MeasurableEquiv.prodCongr
        (MeasurableEquiv.refl ((i : ↥(Finset.Iic n)) → X ↑i))
        (MeasurableEquiv.piSingleton n))
      (MeasurableEquiv.IicProdIoc ⋯)
ProbabilityTheory.Kernel.symm_IicSuccProd.{u_2}
  {X : ℕ → Type u_2}
  [(n : ℕ) → MeasurableSpace (X n)]
  (n : ℕ) :
  MeasurableEquiv.symm
      (MeasurableEquiv.IicSuccProd X n) =
    MeasurableEquiv.trans
      (MeasurableEquiv.prodCongr
        (MeasurableEquiv.refl
          ((i : ↥(Finset.Iic n)) → X ↑i))
        (MeasurableEquiv.piSingleton n))
      (MeasurableEquiv.IicProdIoc ⋯)

Code

lemma symm_IicSuccProd (n : ℕ) :
    (MeasurableEquiv.IicSuccProd X n).symm =
      (MeasurableEquiv.prodCongr (MeasurableEquiv.refl _) (MeasurableEquiv.piSingleton n)).trans
        (MeasurableEquiv.IicProdIoc (Nat.le_succ n))

Type uses (1)

IicSuccProd

Used by (1)

hasLaw_Iic_of_forall_hasCondDistrib'

Actions: Source · Open Issue

Proof

rfl

`IicSuccProd_apply`🔗

LemmaProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_apply

Details

No docstring.

theorem

ProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_apply.{u_2}
  {X : ℕ → Type u_2} [(n : ℕ) → MeasurableSpace (X n)] (n : ℕ)
  (h : (i : ↥(Finset.Iic (n + 1))) → X ↑i) :
  (MeasurableEquiv.IicSuccProd X n) h =
    (fun i => h ⟨↑i, ⋯⟩, h ⟨n + 1, ⋯⟩)
ProbabilityTheory.Kernel.MeasurableEquiv.IicSuccProd_apply.{u_2}
  {X : ℕ → Type u_2}
  [(n : ℕ) → MeasurableSpace (X n)]
  (n : ℕ)
  (h :
    (i : ↥(Finset.Iic (n + 1))) → X ↑i) :
  (MeasurableEquiv.IicSuccProd X n) h =
    (fun i => h ⟨↑i, ⋯⟩, h ⟨n + 1, ⋯⟩)

Code

lemma MeasurableEquiv.IicSuccProd_apply (n : ℕ) (h : Π i : Iic (n + 1), X i) :
    MeasurableEquiv.IicSuccProd X n h = (fun i : Iic n ↦ h ⟨i.1, by grind⟩, h ⟨n + 1, by simp⟩)

Type uses (1)

IicSuccProd

Actions: Source · Open Issue

Proof

rfl

`coe_prodCongr`🔗

LemmaProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr

Details

No docstring.

theorem

ProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr.{u_3, u_4, u_5,
    u_6}
  {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6}
  {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (e₁ : α ≃ᵐ β)
  (e₂ : γ ≃ᵐ δ) : ⇑(MeasurableEquiv.prodCongr e₁ e₂) = Prod.map ⇑e₁ ⇑e₂
ProbabilityTheory.Kernel.MeasurableEquiv.coe_prodCongr.{u_3,
    u_4, u_5, u_6}
  {α : Type u_3} {β : Type u_4}
  {γ : Type u_5} {δ : Type u_6}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ}
  {mδ : MeasurableSpace δ} (e₁ : α ≃ᵐ β)
  (e₂ : γ ≃ᵐ δ) :
  ⇑(MeasurableEquiv.prodCongr e₁ e₂) =
    Prod.map ⇑e₁ ⇑e₂

Code

lemma MeasurableEquiv.coe_prodCongr {α β γ δ : Type*}
    {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
    {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ}
    (e₁ : MeasurableEquiv α β) (e₂ : MeasurableEquiv γ δ) :
    (MeasurableEquiv.prodCongr e₁ e₂ : (α × γ) → (β × δ)) = Prod.map e₁ e₂

Used by (1)

hasLaw_Iic_of_forall_hasCondDistrib'

Actions: Source · Open Issue

Proof

rfl

`coe_refl`🔗

LemmaProbabilityTheory.Kernel.MeasurableEquiv.coe_refl

Details

No docstring.

theorem

ProbabilityTheory.Kernel.MeasurableEquiv.coe_refl.{u_3} {α : Type u_3}
  {mα : MeasurableSpace α} : ⇑(MeasurableEquiv.refl α) = id
ProbabilityTheory.Kernel.MeasurableEquiv.coe_refl.{u_3}
  {α : Type u_3}
  {mα : MeasurableSpace α} :
  ⇑(MeasurableEquiv.refl α) = id

Code

lemma MeasurableEquiv.coe_refl {α : Type*} {mα : MeasurableSpace α} :
    (MeasurableEquiv.refl α : α → α) = id

Actions: Source · Open Issue

Proof

rfl

`hasLaw_Iic_of_forall_hasCondDistrib'`🔗

LemmaProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib'

Details

No docstring.

theorem

ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib'.{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 n : ℕ}
  (h_condDistrib :
    ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω i => Y (↑i) ω) (κ n) P)
  (hn : n ≤ N) :
  HasLaw (fun ω i => Y (↑i) ω)
    (MeasureTheory.Measure.bind
      (MeasureTheory.Measure.map
        (⇑(MeasurableEquiv.symm
            (MeasurableEquiv.piUnique fun i => X ↑i)))
        μ₀)
      ⇑(partialTraj κ 0 n))
    P
ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib'.{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 n : ℕ}
  (h_condDistrib :
    ∀ n < N,
      HasCondDistrib (Y (n + 1))
        (fun ω i => Y (↑i) ω) (κ n) P)
  (hn : n ≤ N) :
  HasLaw (fun ω i => Y (↑i) ω)
    (MeasureTheory.Measure.bind
      (MeasureTheory.Measure.map
        (⇑(MeasurableEquiv.symm
            (MeasurableEquiv.piUnique
              fun i => X ↑i)))
        μ₀)
      ⇑(partialTraj κ 0 n))
    P

Code

lemma hasLaw_Iic_of_forall_hasCondDistrib'
    {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P) {N n : ℕ}
    (h_condDistrib : ∀ n < N, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P)
    (hn : n ≤ N) :
    HasLaw (fun ω (i : Iic n) ↦ Y i ω)
      ((partialTraj κ 0 n) ∘ₘ (μ₀.map (MeasurableEquiv.piUnique _).symm)) P

Body uses (4)

Used by (2)

Actions: Source · Open Issue

Proof

by
  revert hn
  induction n with
  | zero =>
    intro _
    simp only [piUnique_symm_apply, partialTraj_self, Measure.id_comp]
    rw [← h0.map_eq, AEMeasurable.map_map_of_aemeasurable (by fun_prop) (by fun_prop)]
    constructor
    · have h_meas := h0.aemeasurable
      have : (fun ω (i : Iic 0) ↦ Y i ω) = (MeasurableEquiv.piUnique _).symm ∘ (Y 0) := by
        ext ω i
        simp only [piUnique_symm_apply, Function.comp_apply]
        rw [Unique.eq_default i]
        simp [coe_default_Iic_zero]
      rw [this]
      exact AEMeasurable.comp_aemeasurable (by fun_prop) h_meas
    · congr
      ext ω i
      simp only [Function.comp_apply]
      rw [Unique.eq_default i]
      simp [coe_default_Iic_zero]
  | succ n hn =>
    intro hn_le
    specialize h_condDistrib n (by grind)
    specialize hn (by grind)
    have h_law := hn.prod_of_hasCondDistrib h_condDistrib
    have : (fun ω (i : Iic (n + 1)) ↦ Y i ω) =
        (MeasurableEquiv.IicSuccProd X n).symm ∘
          (fun ω ↦ (fun i : Iic n ↦ Y i ω, Y (n + 1) ω)) := by
      suffices (MeasurableEquiv.IicSuccProd X n) ∘ (fun ω (i : Iic (n + 1)) ↦ Y i ω) =
          (fun ω ↦ (fun i : Iic n ↦ Y i ω, Y (n + 1) ω)) by
        rw [← this, ← Function.comp_assoc, MeasurableEquiv.symm_comp_self]
        simp
      ext ω : 1
      simp
    rw [this]
    refine HasLaw.comp ⟨by fun_prop, ?_⟩ h_law
    rw [Measure.compProd_eq_comp_prod, partialTraj_succ_eq_comp (by simp), Measure.comp_assoc,
      ← Measure.deterministic_comp_eq_map (by fun_prop), Measure.comp_assoc]
    congr 1
    rw [← Kernel.comp_assoc]
    congr
    rw [Kernel.deterministic_comp_eq_map, partialTraj_succ_self, symm_IicSuccProd]
    rw [MeasurableEquiv.coe_trans, MeasurableEquiv.coe_prodCongr]
    rw [Kernel.map_comp_right _ (by fun_prop) (by fun_prop),
      ← Kernel.map_prod_map _ _ (by fun_prop) (by fun_prop)]
    congr
    simp [MeasurableEquiv.coe_refl]

`hasLaw_Iic_of_forall_hasCondDistrib`🔗

LemmaProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib

Details

No docstring.

theorem

ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib.{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)
  (h_condDistrib :
    ∀ (n : ℕ), HasCondDistrib (Y (n + 1)) (fun ω i => Y (↑i) ω) (κ n) P)
  (n : ℕ) :
  HasLaw (fun ω i => Y (↑i) ω)
    (MeasureTheory.Measure.bind
      (MeasureTheory.Measure.map
        (⇑(MeasurableEquiv.symm
            (MeasurableEquiv.piUnique fun i => X ↑i)))
        μ₀)
      ⇑(partialTraj κ 0 n))
    P
ProbabilityTheory.Kernel.hasLaw_Iic_of_forall_hasCondDistrib.{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)
  (h_condDistrib :
    ∀ (n : ℕ),
      HasCondDistrib (Y (n + 1))
        (fun ω i => Y (↑i) ω) (κ n) P)
  (n : ℕ) :
  HasLaw (fun ω i => Y (↑i) ω)
    (MeasureTheory.Measure.bind
      (MeasureTheory.Measure.map
        (⇑(MeasurableEquiv.symm
            (MeasurableEquiv.piUnique
              fun i => X ↑i)))
        μ₀)
      ⇑(partialTraj κ 0 n))
    P

Code

lemma hasLaw_Iic_of_forall_hasCondDistrib {Y : (n : ℕ) → Ω → X n} (h0 : HasLaw (Y 0) μ₀ P)
    (h_condDistrib : ∀ n, HasCondDistrib (Y (n + 1)) (fun ω ↦ fun i : Iic n ↦ Y i ω) (κ n) P)
    (n : ℕ) :
    HasLaw (fun ω (i : Iic n) ↦ Y i ω)
      ((partialTraj κ 0 n) ∘ₘ (μ₀.map (MeasurableEquiv.piUnique _).symm)) P

Body uses (1)

hasLaw_Iic_of_forall_hasCondDistrib'

Used by (1)

hasLaw_trajMeasure

Actions: Source · Open Issue

Proof

by
  exact hasLaw_Iic_of_forall_hasCondDistrib' (N := n) h0 (fun n _ ↦ h_condDistrib n) le_rfl

`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]

`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)

eq_trajMeasure_map_frestrictLe_of_isAlgEnvSeqUntil

Actions: Source · Open Issue

Proof

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

`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)

map_trajectory

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]

LeanMachineLearning exposition

1.17. ForMathlib.Probability.Kernel.IonescuTulcea.Traj🔗

`coe_default_Iic_zero`🔗

`traj_zero_map_eval_zero`🔗

`IicSuccProd`🔗

`symm_IicSuccProd`🔗

`IicSuccProd_apply`🔗

`coe_prodCongr`🔗

`coe_refl`🔗

`hasLaw_Iic_of_forall_hasCondDistrib'`🔗

`hasLaw_Iic_of_forall_hasCondDistrib`🔗

`trajMeasure_map_frestrictLe`🔗

`eq_trajMeasure_map_frestrictLe`🔗

`hasLaw_trajMeasure`🔗

1.17. ForMathlib.Probability.Kernel.IonescuTulcea.Traj🔗

coe_default_Iic_zero🔗

traj_zero_map_eval_zero🔗

IicSuccProd🔗

symm_IicSuccProd🔗

IicSuccProd_apply🔗

coe_prodCongr🔗

coe_refl🔗

hasLaw_Iic_of_forall_hasCondDistrib'🔗

hasLaw_Iic_of_forall_hasCondDistrib🔗

trajMeasure_map_frestrictLe🔗

eq_trajMeasure_map_frestrictLe🔗

hasLaw_trajMeasure🔗

`coe_default_Iic_zero`🔗

`traj_zero_map_eval_zero`🔗

`IicSuccProd`🔗

`symm_IicSuccProd`🔗

`IicSuccProd_apply`🔗

`coe_prodCongr`🔗

`coe_refl`🔗

`hasLaw_Iic_of_forall_hasCondDistrib'`🔗

`hasLaw_Iic_of_forall_hasCondDistrib`🔗

`trajMeasure_map_frestrictLe`🔗

`eq_trajMeasure_map_frestrictLe`🔗

`hasLaw_trajMeasure`🔗