theorem measurable_cast {X : Type u} {Y : Type u} [mX : MeasurableSpace X] [mY : MeasurableSpace Y] (h : X = Y) (hm : HEq mX mY) : Measurable (cast h)

theorem update_updateFinset_eq {X : ℕ → Type u_1} (x : (n : ℕ) → X n) (z : (n : ℕ) → X n) {m : ℕ} : Function.update (Function.updateFinset x (Finset.Iic m) (Preorder.frestrictLe m z)) (m + 1) (z (m + 1)) = Function.updateFinset x (Finset.Iic (m + 1)) (Preorder.frestrictLe (m + 1) z)

def e {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (n : ℕ) : X (n + 1) ≃ᵐ ((i : { x : ℕ // x ∈ Finset.Ioc n (n + 1) }) → X ↑i)

Identifying {n + 1} with Ioc n (n+1), as a measurable equiv on dependent functions.

Equations

• One or more equations did not get rendered due to their size.

def el {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (m : ℕ) (n : ℕ) (hmn : m ≤ n) : ((i : { x : ℕ // x ∈ Finset.Iic m }) → X ↑i) × ((i : { x : ℕ // x ∈ Finset.Ioc m n }) → X ↑i) ≃ᵐ ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i)

Gluing Iic m and Ioc m n into Iic n, as a measurable equiv of dependent functions.

Equations

• One or more equations did not get rendered due to their size.

def el' {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (n : ℕ) : ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) × ((i : ↑(Set.Ioi n)) → X ↑i) ≃ᵐ ((n : ℕ) → X n)

The union of Iic n and Ioi n is the whole ℕ, version as a measurable equivalence on dependent functions.

Equations

• One or more equations did not get rendered due to their size.

def er {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (i : ℕ) (j : ℕ) (k : ℕ) (hij : i < j) (hjk : j ≤ k) : ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l) × ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l) ≃ᵐ ((l : { x : ℕ // x ∈ Finset.Ioc i k }) → X ↑l)

Gluing Ioc i j and Ioc j k into Ioc i k, as a measurable equiv of dependent functions.

Equations

• One or more equations did not get rendered due to their size.

theorem restrict₂_er {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (i : ℕ) (j : ℕ) (k : ℕ) (hij : i < j) (hjk : j ≤ k) (y : (n : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑n) (z : (n : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑n) : Finset.restrict₂ ⋯ ((er i j k hij hjk) (y, z)) = y

theorem el_assoc {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (hij : i < j) (hjk : j ≤ k) (a : (x : { x : ℕ // x ∈ Finset.Iic i }) → X ↑x) (b : (l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l) (c : (l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l) : (el j k hjk) ((el i j ⋯) (a, b), c) = (el i k ⋯) (a, (er i j k hij hjk) (b, c))

theorem er_assoc {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} {l : ℕ} (hij : i < j) (hjk : j < k) (hkl : k ≤ l) (b : (l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l) (c : (l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l) (d : (m : { x : ℕ // x ∈ Finset.Ioc k l }) → X ↑m) : (er i j l hij ⋯) (b, (er j k l hjk hkl) (c, d)) = (er i k l ⋯ hkl) ((er i j k hij ⋯) (b, c), d)

def e_path_eq {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (h : j = k) : ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l) ≃ᵐ ((l : { x : ℕ // x ∈ Finset.Ioc i k }) → X ↑l)

When j = k, then Ioc i j = Ioc i k, as a measurable equiv of dependent functions.

Equations

• e_path_eq h = MeasurableEquiv.cast ⋯ ⋯

def split {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (i : ℕ) (j : ℕ) (k : ℕ) (hij : i < j) (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) : ProbabilityTheory.Kernel (((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) × ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)

Given a kernel from variables in Iic j, split Iic j into the union of Iic i and Ioc i j and construct the resulting kernel. TODO: the target space could be anything, generalize.

Equations

• split i j k hij κ = κ.comap ⇑(el i j ⋯) ⋯

theorem split_eq_comap {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (i : ℕ) (j : ℕ) (k : ℕ) (hij : i < j) (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) : split i j k hij κ = κ.comap ⇑(el i j ⋯) ⋯

instance instIsSFiniteKernelProdForallValNatMemFinsetIicForallIocSplit {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (hij : i < j) (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (split i j k hij κ)

Equations

• ⋯ = ⋯

instance instIsFiniteKernelProdForallValNatMemFinsetIicForallIocSplit {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (hij : i < j) (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (split i j k hij κ)

Equations

• ⋯ = ⋯

@[simp]

theorem split_zero {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (i : ℕ) (j : ℕ) (k : ℕ) (hij : i < j) : split i j k hij 0 = 0

def ProbabilityTheory.Kernel.compProdNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i k }) → X ↑l)

Given a kernel from variables in Ici i to Ioc i j, and another one from variables in Iic j to Ioc j k, compose them to get a kernel from Ici i to Ioc i k. This makes sense only when i < j and j < k. Otherwise, use 0 as junk value.

Equations

• (κ ⊗ₖ' η) = if h : i < j ∧ j < k then (κ.compProd (split i j k ⋯ η)).map ⇑(er i j k ⋯ ⋯) else 0

theorem ProbabilityTheory.Kernel.compProdNat_eq {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) (hij : i < j) (hjk : j < k) : (κ ⊗ₖ' η) = (κ.compProd (split i j k hij η)).map ⇑(er i j k hij ⋯)

instance ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicForallIocCompProdNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) : ProbabilityTheory.IsSFiniteKernel (κ ⊗ₖ' η)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsFiniteKernelForallValNatMemFinsetIicForallIocCompProdNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) [ProbabilityTheory.IsFiniteKernel κ] (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) [ProbabilityTheory.IsFiniteKernel η] : ProbabilityTheory.IsFiniteKernel (κ ⊗ₖ' η)

Equations

• ⋯ = ⋯

def ProbabilityTheory.Kernel.«term_⊗ₖ'_» : Lean.TrailingParserDescr

Given a kernel from variables in Ici i to Ioc i j, and another one from variables in Iic j to Ioc j k, compose them to get a kernel from Ici i to Ioc i k. This makes sense only when i < j and j < k. Otherwise, use 0 as junk value.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Kernel.compProdNat_apply' {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η] (hij : i < j) (hjk : j < k) (a : (l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) {s : Set ((l : { x : ℕ // x ∈ Finset.Ioc i k }) → X ↑l)} (hs : MeasurableSet s) : ((κ ⊗ₖ' η) a) s = ∫⁻ (b : (l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l), (η ((el i j ⋯) (a, b))) {c : (l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l | (b, c) ∈ ⇑(er i j k hij ⋯) ⁻¹' s} ∂κ a

@[simp]

theorem ProbabilityTheory.Kernel.compProdNat_zero_right {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (k : ℕ) : (κ ⊗ₖ' 0) = 0

@[simp]

theorem ProbabilityTheory.Kernel.compProdNat_zero_left {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {j : ℕ} {k : ℕ} (i : ℕ) (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) : (0 ⊗ₖ' κ) = 0

theorem ProbabilityTheory.Kernel.compProdNat_undef_left {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) (hij : i < j) (hjk : j < k) (h : ¬ProbabilityTheory.IsSFiniteKernel κ) : (κ ⊗ₖ' η) = 0

theorem ProbabilityTheory.Kernel.compProdNat_assoc {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} {l : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) (ξ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) ((m : { x : ℕ // x ∈ Finset.Ioc k l }) → X ↑m)) [ProbabilityTheory.IsSFiniteKernel η] [ProbabilityTheory.IsSFiniteKernel ξ] (hij : i < j) (hjk : j < k) (hkl : k < l) : (κ ⊗ₖ' η ⊗ₖ' ξ) = (κ ⊗ₖ' η) ⊗ₖ' ξ

def ProbabilityTheory.Kernel.castPath {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (h : j = k) : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i k }) → X ↑l)

Given a kernel taking values in Ioc i j, convert it to a kernel taking values in Ioc i k when j = k.

Equations

• κ.castPath h = κ.map ⇑(e_path_eq h)

theorem ProbabilityTheory.Kernel.castPath_self {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) : κ.castPath ⋯ = κ

theorem ProbabilityTheory.Kernel.castPath_apply {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (h : j = k) (a : (l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) (s : Set ((l : { x : ℕ // x ∈ Finset.Ioc i k }) → X ↑l)) (hs : MeasurableSet s) : ((κ.castPath h) a) s = (κ a) (⇑(e_path_eq h) ⁻¹' s)

instance ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicForallIocCastPath {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (h : j = k) [ProbabilityTheory.IsSFiniteKernel κ] : ProbabilityTheory.IsSFiniteKernel (κ.castPath h)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsFiniteKernelForallValNatMemFinsetIicForallIocCastPath {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (h : j = k) [ProbabilityTheory.IsFiniteKernel κ] : ProbabilityTheory.IsFiniteKernel (κ.castPath h)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicForallIocCastPath {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) [ProbabilityTheory.IsMarkovKernel κ] (hjk : j = k) : ProbabilityTheory.IsMarkovKernel (κ.castPath hjk)

Equations

• ⋯ = ⋯

def ProbabilityTheory.Kernel.kerNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) (i : ℕ) (j : ℕ) : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Kernel.kerNat_zero {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) (i : ℕ) : ProbabilityTheory.Kernel.kerNat κ i 0 = 0

theorem ProbabilityTheory.Kernel.kerNat_succ {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) (i : ℕ) (j : ℕ) : ProbabilityTheory.Kernel.kerNat κ i (j + 1) = if h : i = j then ((κ i).map ⇑(e i)).castPath ⋯ else ProbabilityTheory.Kernel.kerNat κ i j ⊗ₖ' (κ j).map ⇑(e j)

theorem ProbabilityTheory.Kernel.kerNat_succ_self {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) (i : ℕ) : ProbabilityTheory.Kernel.kerNat κ i (i + 1) = (κ i).map ⇑(e i)

theorem ProbabilityTheory.Kernel.kerNat_succ_of_ne {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) (h : i ≠ j) : ProbabilityTheory.Kernel.kerNat κ i (j + 1) = ProbabilityTheory.Kernel.kerNat κ i j ⊗ₖ' (κ j).map ⇑(e j)

theorem ProbabilityTheory.Kernel.kerNat_succ_right {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) (i : ℕ) (j : ℕ) (hij : i < j) : ProbabilityTheory.Kernel.kerNat κ i (j + 1) = ProbabilityTheory.Kernel.kerNat κ i j ⊗ₖ' ProbabilityTheory.Kernel.kerNat κ j (j + 1)

theorem ProbabilityTheory.Kernel.kerNat_of_ge {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) (h : j ≤ i) : ProbabilityTheory.Kernel.kerNat κ i j = 0

instance ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicForallIocKerNatOfHAddOfNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) [∀ (i : ℕ), ProbabilityTheory.IsSFiniteKernel (κ i)] : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.kerNat κ i j)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsFiniteKernelForallValNatMemFinsetIicForallIocKerNatOfHAddOfNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) [∀ (i : ℕ), ProbabilityTheory.IsFiniteKernel (κ i)] : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.kerNat κ i j)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.Kernel.kerNat_succ_left {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) [∀ (i : ℕ), ProbabilityTheory.IsSFiniteKernel (κ i)] (i : ℕ) (j : ℕ) (hij : i + 1 < j) : ProbabilityTheory.Kernel.kerNat κ i j = ProbabilityTheory.Kernel.kerNat κ i (i + 1) ⊗ₖ' ProbabilityTheory.Kernel.kerNat κ (i + 1) j

theorem ProbabilityTheory.Kernel.compProdNat_kerNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) [∀ (i : ℕ), ProbabilityTheory.IsSFiniteKernel (κ i)] (hij : i < j) (hjk : j < k) : (ProbabilityTheory.Kernel.kerNat κ i j ⊗ₖ' ProbabilityTheory.Kernel.kerNat κ j k) = ProbabilityTheory.Kernel.kerNat κ i k

theorem ProbabilityTheory.Kernel.isMarkovKernel_compProdNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} {k : ℕ} (κ : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic i }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc i j }) → X ↑l)) (η : ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic j }) → X ↑l) ((l : { x : ℕ // x ∈ Finset.Ioc j k }) → X ↑l)) [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η] (hij : i < j) (hjk : j < k) : ProbabilityTheory.IsMarkovKernel (κ ⊗ₖ' η)

theorem ProbabilityTheory.Kernel.isMarkovKernel_kerNat {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] {i : ℕ} {j : ℕ} (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) [∀ (k : ℕ), ProbabilityTheory.IsMarkovKernel (κ k)] (hij : i < j) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.kerNat κ i j)

theorem ProbabilityTheory.Kernel.kerNat_proj {X : ℕ → Type u_1} [(i : ℕ) → MeasurableSpace (X i)] (κ : (k : ℕ) → ProbabilityTheory.Kernel ((l : { x : ℕ // x ∈ Finset.Iic k }) → X ↑l) (X (k + 1))) [∀ (i : ℕ), ProbabilityTheory.IsMarkovKernel (κ i)] {a : ℕ} {b : ℕ} {c : ℕ} (hab : a < b) (hbc : b ≤ c) : (ProbabilityTheory.Kernel.kerNat κ a c).map (Finset.restrict₂ ⋯) = ProbabilityTheory.Kernel.kerNat κ a b

noncomputable def ProbabilityTheory.Kernel.partialKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) (a : ℕ) (b : ℕ) : ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic a }) → X ↑i) ((i : { x : ℕ // x ∈ Finset.Iic b }) → X ↑i)

Given a family of kernels κ : (n : ℕ) → Kernel ((i : Iic n) → X i) (X (n + 1)), we can compose them: if a < b, then (κ a) ⊗ₖ ... ⊗ₖ (κ (b - 1)) is a kernel from (i : Iic a) → X i to (i : Ioc a b) → X i. This composition is called kerNat κ a b.

In order to make manipulations easier, we define partialKernel κ a b : Kernel ((i : Iic a) → X i) ((i : Iic b) → X i). Given the trajectory up to time a, partialKernel κ a b gives the distribution of the trajectory up to time b. It is the product of a Dirac mass along the trajectory, up to a, with kerNat κ a b.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Kernel.partialKernel_lt {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) {a : ℕ} {b : ℕ} (hab : a < b) : ProbabilityTheory.Kernel.partialKernel κ a b = ((ProbabilityTheory.Kernel.deterministic id ⋯).prod (ProbabilityTheory.Kernel.kerNat κ a b)).map ⇑(el a b ⋯)

theorem ProbabilityTheory.Kernel.partialKernel_le {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) {a : ℕ} {b : ℕ} (hab : b ≤ a) : ProbabilityTheory.Kernel.partialKernel κ a b = ProbabilityTheory.Kernel.deterministic (Preorder.frestrictLe₂ hab) ⋯

instance ProbabilityTheory.Kernel.instIsSFiniteKernelForallValNatMemFinsetIicPartialKernelOfHAddOfNat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsSFiniteKernel (κ n)] (a : ℕ) (b : ℕ) : ProbabilityTheory.IsSFiniteKernel (ProbabilityTheory.Kernel.partialKernel κ a b)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsFiniteKernelForallValNatMemFinsetIicPartialKernelOfHAddOfNat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κ n)] (a : ℕ) (b : ℕ) : ProbabilityTheory.IsFiniteKernel (ProbabilityTheory.Kernel.partialKernel κ a b)

Equations

• ⋯ = ⋯

instance ProbabilityTheory.Kernel.instIsMarkovKernelForallValNatMemFinsetIicPartialKernelOfHAddOfNat {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) (b : ℕ) : ProbabilityTheory.IsMarkovKernel (ProbabilityTheory.Kernel.partialKernel κ a b)

Equations

• ⋯ = ⋯

theorem ProbabilityTheory.Kernel.partialKernel_proj {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) {b : ℕ} {c : ℕ} (hbc : b ≤ c) : (ProbabilityTheory.Kernel.partialKernel κ a c).map (Preorder.frestrictLe₂ hbc) = ProbabilityTheory.Kernel.partialKernel κ a b

If b ≤ c, then projecting the trajectory up to time c on first coordinates gives the trajectory up to time b.

theorem ProbabilityTheory.Kernel.partialKernel_proj_apply {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {n : ℕ} (x : (i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (a : ℕ) (b : ℕ) (hab : a ≤ b) : MeasureTheory.Measure.map (Preorder.frestrictLe₂ hab) ((ProbabilityTheory.Kernel.partialKernel κ n b) x) = (ProbabilityTheory.Kernel.partialKernel κ n a) x

theorem ProbabilityTheory.Kernel.partialKernel_comp {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (c : ℕ) {a : ℕ} {b : ℕ} (h : a ≤ b) : (ProbabilityTheory.Kernel.partialKernel κ b c).comp (ProbabilityTheory.Kernel.partialKernel κ a b) = ProbabilityTheory.Kernel.partialKernel κ a c

Given the trajectory up to time a, first computing the distribution up to time b and then the distribution up to time c is the same as directly computing the distribution up to time c.

theorem ProbabilityTheory.Kernel.partialKernel_comp' {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) {b : ℕ} {c : ℕ} (h : c ≤ b) : (ProbabilityTheory.Kernel.partialKernel κ b c).comp (ProbabilityTheory.Kernel.partialKernel κ a b) = ProbabilityTheory.Kernel.partialKernel κ a c

Given the trajectory up to time a, first computing the distribution up to time b and then the distribution up to time c is the same as directly computing the distribution up to time c.

noncomputable def ProbabilityTheory.Kernel.lmarginalPartialKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) (a : ℕ) (b : ℕ) (f : ((n : ℕ) → X n) → ENNReal) (x : (n : ℕ) → X n) : ENNReal

This function computes the integral of a function f against partialKernel, and allows to view it as a function depending on all the variables.

Equations

• One or more equations did not get rendered due to their size.

theorem ProbabilityTheory.Kernel.lmarginalPartialKernel_le {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) {a : ℕ} {b : ℕ} (hba : b ≤ a) {f : ((n : ℕ) → X n) → ENNReal} (mf : Measurable f) : ProbabilityTheory.Kernel.lmarginalPartialKernel κ a b f = f

If b ≤ a, then integrating f against the partialKernel κ a b does nothing.

theorem ProbabilityTheory.Kernel.lmarginalPartialKernel_mono {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) (a : ℕ) (b : ℕ) {f : ((n : ℕ) → X n) → ENNReal} {g : ((n : ℕ) → X n) → ENNReal} (hfg : f ≤ g) (x : (n : ℕ) → X n) : ProbabilityTheory.Kernel.lmarginalPartialKernel κ a b f x ≤ ProbabilityTheory.Kernel.lmarginalPartialKernel κ a b g x

theorem ProbabilityTheory.Kernel.lmarginalPartialKernel_lt {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κ n)] {a : ℕ} {b : ℕ} (hab : a < b) {f : ((n : ℕ) → X n) → ENNReal} (mf : Measurable f) (x : (n : ℕ) → X n) : ProbabilityTheory.Kernel.lmarginalPartialKernel κ a b f x = ∫⁻ (y : (i : { x : ℕ // x ∈ Finset.Ioc a b }) → X ↑i), f (Function.updateFinset x (Finset.Ioc a b) y) ∂(ProbabilityTheory.Kernel.kerNat κ a b) (Preorder.frestrictLe a x)

If a < b, then integrating f against the partialKernel κ a b is the same as integrating against kerNat a b.

theorem ProbabilityTheory.Kernel.measurable_lmarginalPartialKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsSFiniteKernel (κ n)] (a : ℕ) (b : ℕ) {f : ((n : ℕ) → X n) → ENNReal} (hf : Measurable f) : Measurable (ProbabilityTheory.Kernel.lmarginalPartialKernel κ a b f)

theorem ProbabilityTheory.Kernel.lmarginalPartialKernel_self {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsFiniteKernel (κ n)] {a : ℕ} {b : ℕ} {c : ℕ} (hab : a ≤ b) (hbc : b ≤ c) {f : ((n : ℕ) → X n) → ENNReal} (hf : Measurable f) : ProbabilityTheory.Kernel.lmarginalPartialKernel κ a b (ProbabilityTheory.Kernel.lmarginalPartialKernel κ b c f) = ProbabilityTheory.Kernel.lmarginalPartialKernel κ a c f

theorem DependsOn.lmarginalPartialKernel_eq {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {a : ℕ} {b : ℕ} (c : ℕ) {f : ((n : ℕ) → X n) → ENNReal} (mf : Measurable f) (hf : DependsOn f ↑(Finset.Iic a)) (hab : a ≤ b) : ProbabilityTheory.Kernel.lmarginalPartialKernel κ b c f = f

theorem DependsOn.lmarginalPartialKernel_right {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] {f : ((i : ℕ) → X i) → ENNReal} {a : ℕ} (b : ℕ) {c : ℕ} {d : ℕ} (mf : Measurable f) (hf : DependsOn f ↑(Finset.Iic a)) (hac : a ≤ c) (had : a ≤ d) : ProbabilityTheory.Kernel.lmarginalPartialKernel κ b c f = ProbabilityTheory.Kernel.lmarginalPartialKernel κ b d f

theorem DependsOn.dependsOn_lmarginalPartialKernel {X : ℕ → Type u_1} [(n : ℕ) → MeasurableSpace (X n)] (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : { x : ℕ // x ∈ Finset.Iic n }) → X ↑i) (X (n + 1))) [∀ (n : ℕ), ProbabilityTheory.IsMarkovKernel (κ n)] (a : ℕ) {b : ℕ} {f : ((n : ℕ) → X n) → ENNReal} (hf : DependsOn f ↑(Finset.Iic b)) (mf : Measurable f) : DependsOn (ProbabilityTheory.Kernel.lmarginalPartialKernel κ a b f) ↑(Finset.Iic a)