Mathlib.Probability.Kernel.FiniteSequence
This module bundles dependent finite transcript histories, sequential-kernel laws, their prefix and next-step identities, and exact singleton factorization.
Basic 7 core · 1 supporting This module provides dependent finite histories, their product measurable spaces, and the basic operations that restrict, extend, or split a transcript.
Finite dependent transcript histories
This module provides dependent finite histories, their product measurable spaces, and the basic operations that restrict, extend, or split a transcript.
def History reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given an output family, a history length, and evidence that the length does not exceed the horizon, a dependent history records one output at each earlier stage. It is given by the dependent function space indexed by the first k stages.
abbrev Transcript reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given an output family, a complete dependent transcript is given by a history spanning the whole horizon.
def take reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a prefix bound and a complete transcript, the requested prefix history is given by retaining exactly its first coordinates.
Definition (Lean source)
def nextIndex reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given evidence that stage k + 1 lies within the horizon, the next output index is the zero-based position k, which is the position of the (k + 1)-th output.
Definition (Lean source)
def snoc reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a valid successor bound, a preceding history, and its next output, the extended history is given by appending that output.
Definition (Lean source)
def init reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a valid successor bound and a nonempty history, its preceding history is given by removing the final coordinate.
Definition (Lean source)
parameters
def
given by
Fin.init u
def last reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a valid successor bound and a nonempty history, its final output is given by its last coordinate.
1 supporting declaration (lemmas, instances)
-
historyMeasurableSpaceinstance — Given measurable output spaces, a history length, and evidence that it lies within the output horizon, the measurable structure on the dependent history is given by the product σ-algebra of its coordinates.parametersinstancegiven by=> mZ _ infer_instance
Construction 3 core · 2 supporting This module recursively constructs laws of dependent finite output histories from kernels that may depend on the current input and all preceding private outputs. ★ isProbabilityMeasure_prefixLaw
Construction of finite sequential laws
This module recursively constructs laws of dependent finite output histories from kernels that may depend on the current input and all preceding private outputs.
abbrev KernelFamily reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given an input space and an output family, a sequential kernel family is given by one kernel at each stage from the current input and preceding private history to the current output.
Definition (Lean source)
parameters
def
def prefixLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a sequential kernel family, a fixed input vector, a prefix length, and evidence that the prefix lies within the horizon, the law of the first outputs is given by iterated composition from the unique empty history.
Definition (Lean source)
parameters
def
given by
Nat.rec (motive := fun j => (hj : j ≤ n) → Measure (History Z j hj)) (fun _ => Measure.dirac (fun j : Fin 0 => j.elim0)) (fun j prev hj => let hprev : j ≤ n := Nat.le_of_succ_le hj let idx : Fin n := nextIndex hj let K : Kernel (History Z j hprev) (Z idx) := (Q idx).comap (fun u => (x idx, u)) (by fun_prop) (prev hprev ⊗ₘ K).map (fun p => snoc hj p.1 p.2)) k hk
theorem isProbabilityMeasure_prefixLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a sequential kernel family, the condition that every stage kernel is Markov, a fixed input vector, a prefix length, and evidence that the prefix lies within the horizon, the prefix law has total mass one.
Formal statement
hypotheses
n :
ℕ
X :
Type u_1
Q :
KernelFamily X Z
hQ :
∀ i, IsMarkovKernel (Q i)
x :
Fin n → X
k :
ℕ
hk :
k ≤ n
conclusion
IsProbabilityMeasure (prefixLaw Q x k hk)
Proof (Lean source)
theorem isProbabilityMeasure_prefixLaw (Q : KernelFamily X Z)
(hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X) (k : ℕ) (hk : k ≤ n) :
IsProbabilityMeasure (prefixLaw Q x k hk) := by
induction k with
| zero =>
change IsProbabilityMeasure (Measure.dirac (fun j : Fin 0 => j.elim0))
exact ⟨by simp⟩
| succ j ih =>
let hprev : j ≤ n := Nat.le_of_succ_le hk
let idx : Fin n := nextIndex hk
let K : Kernel (History Z j hprev) (Z idx) :=
(Q idx).comap (fun u => (x idx, u)) (by fun_prop)
haveI : IsProbabilityMeasure (prefixLaw Q x j hprev) := ih hprev
haveI : IsMarkovKernel (Q idx) := hQ idx
haveI : IsMarkovKernel K := Kernel.IsMarkovKernel.comap _ (by fun_prop)
haveI : IsProbabilityMeasure (prefixLaw Q x j hprev ⊗ₘ K) :=
⟨by simp⟩
change IsProbabilityMeasure
((prefixLaw Q x j hprev ⊗ₘ K).map (fun p => snoc hk p.1 p.2))
exact Measure.isProbabilityMeasure_map (measurable_snoc hk).aemeasurable
2 supporting declarations (lemmas, instances)
-
measurable_snoctheorem — Given a successor bound, appending a next output to a preceding dependent history is measurable.hypothesesconclusionProof (Lean source)
theorem measurable_snoc {k : ℕ} (hk : k + 1 ≤ n) : Measurable (fun p : History Z k (le_of_succ_le hk) × Z (nextIndex hk) => snoc hk p.1 p.2) := by apply measurable_pi_iff.mpr intro j refine Fin.lastCases ?_ (fun i => ?_) j · have h : nextIndex hk = castLE hk (last k) := rfl have hm := (measurable_eq_mp Z h).comp (measurable_snd : Measurable (fun p : History Z k (le_of_succ_le hk) × Z (nextIndex hk) => p.2)) convert hm using 1 funext p simp [snoc, snoc] rfl · have h : castLE (le_of_succ_le hk) i = castLE hk i.castSucc := rfl have hm := (measurable_eq_mp Z h).comp ((measurable_pi_apply i).comp (measurable_fst : Measurable (fun p : History Z k (le_of_succ_le hk) × Z (nextIndex hk) => p.1))) convert hm using 1 funext p simp [snoc, snoc] rfl -
measurable_init_lasttheorem — Given a successor bound, splitting a nonempty dependent history into its preceding history and final output is measurable.hypothesesconclusionProof (Lean source)
theorem measurable_init_last {k : ℕ} (hk : k + 1 ≤ n) : Measurable (fun u : History Z (k + 1) hk => (init hk u, last hk u)) := by apply prodMk · apply measurable_pi_iff.mpr intro i exact measurable_pi_apply i.castSucc · exact measurable_pi_apply (last k)
Restriction 2 core · 3 supporting This module provides measurable maps which forget later coordinates of dependent finite histories and records their basic compatibility with transcript prefixes. ★ restrictHistory_succ
Restriction maps for finite dependent histories
This module provides measurable maps which forget later coordinates of dependent finite histories and records their basic compatibility with transcript prefixes.
def restrictHistory reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a target prefix bound, a source prefix bound, an ordering of the two lengths, and a source history, the restricted history is given by retaining its first coordinates.
theorem restrictHistory_succ reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a target prefix bound, a successor source bound, an ordering of the target and preceding source lengths, and a successor history, restricting it factors through removal of the final coordinate.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem restrictHistory_succ {k l : ℕ} (hk : k ≤ n) (hs : l + 1 ≤ n)
(hkl : k ≤ l) (u : History Z (l + 1) hs) :
restrictHistory hk hs (le_trans hkl (le_succ l)) u =
restrictHistory hk (le_of_succ_le hs) hkl (init hs u) := by
funext i
rfl
3 supporting declarations (lemmas, instances)
-
measurable_restrictHistorytheorem — Given a target prefix bound, a source prefix bound, and an ordering of the two lengths, the restriction map is measurable.hypothesesconclusionMeasurable (restrictHistory (Z := Z) hk hl hkl)Proof (Lean source)
theorem measurable_restrictHistory {k l : ℕ} (hk : k ≤ n) (hl : l ≤ n) (hkl : k ≤ l) : Measurable (restrictHistory (Z := Z) hk hl hkl) := by apply measurable_pi_iff.mpr intro i exact measurable_pi_apply (castLE hkl i) -
restrictHistory_selftheorem — Given a prefix bound and a history of that exact length, restricting it to the same length returns the original history.hypothesesconclusionrestrictHistory hk hk le_rfl u = uProof (Lean source)
theorem restrictHistory_self {k : ℕ} (hk : k ≤ n) (u : History Z k hk) : restrictHistory hk hk le_rfl u = u := by funext i rfl -
restrictHistory_transcripttheorem — Given a prefix bound and a complete transcript, restricting the transcript agrees with taking its prefix.hypothesesconclusionProof (Lean source)
theorem restrictHistory_transcript {k : ℕ} (hk : k ≤ n) (u : Transcript Z) : restrictHistory hk le_rfl hk u = take hk u := by funext i rfl
Law 2 core · 6 supporting This module identifies every finite prefix marginal and every prefix-plus-next-output law of the recursively constructed transcript measure. ★ transcriptLaw_map_take_next
Prefix and next-step identities for finite sequential laws
This module identifies every finite prefix marginal and every prefix-plus-next-output law of the recursively constructed transcript measure.
abbrev transcriptLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a sequential kernel family and a fixed input vector, the complete dependent transcript law is given by the final prefix law.
Definition (Lean source)
parameters
def
theorem transcriptLaw_map_take_next reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a sequential kernel family, the condition that every stage kernel is Markov, a fixed input vector, a prefix length, and a successor bound, under the complete transcript law, the joint law of the prefix of that length and the next output is the composition-product of the prefix law with the next-stage kernel evaluated at the next input coordinate.
Formal statement
hypotheses
n :
ℕ
X :
Type u_1
Q :
KernelFamily X Z
hQ :
∀ i, IsMarkovKernel (Q i)
x :
Fin n → X
k :
ℕ
hk :
k + 1 ≤ n
conclusion
= (prefixLaw Q x k (le_of_succ_le hk)) ⊗ₘ (Q (nextIndex hk)).comap (fun u => (x (nextIndex hk), u)) (by fun_prop)
Proof (Lean source)
theorem transcriptLaw_map_take_next (Q : KernelFamily X Z)
(hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X)
(k : ℕ) (hk : k + 1 ≤ n) :
(transcriptLaw Q x).map
(fun t => (take (le_of_succ_le hk) t, t (nextIndex hk))) =
(prefixLaw Q x k (le_of_succ_le hk)) ⊗ₘ
(Q (nextIndex hk)).comap (fun u => (x (nextIndex hk), u)) (by fun_prop) := by
have hmeas : Measurable (take hk : Transcript Z → History Z (k + 1) hk) := by
have hfun : (take hk : Transcript Z → History Z (k + 1) hk) =
restrictHistory hk le_rfl hk := by
funext u
exact (restrictHistory_transcript hk u).symm
rw [hfun]
exact measurable_restrictHistory hk le_rfl hk
have hfun : (fun t : Transcript Z =>
(take (le_of_succ_le hk) t, t (nextIndex hk))) =
(fun u : History Z (k + 1) hk => (init hk u, last hk u)) ∘ take hk := by
funext t
apply Prod.ext
· funext i
rfl
· rfl
rw [hfun, ← Measure.map_map (measurable_init_last hk) hmeas,
transcriptLaw_map_prefix Q hQ x (k + 1) hk,
prefixLaw_succ_map_init_last Q x k hk]
6 supporting declarations (lemmas, instances)
-
prefixLaw_succtheorem — Given a sequential kernel family, a fixed input vector, a prefix length, and a successor bound, the next prefix law is the composition-product of the preceding prefix and current kernel, pushed forward by appending.hypothesesProof (Lean source)
theorem prefixLaw_succ (Q : KernelFamily X Z) (x : Fin n → X) (k : ℕ) (hk : k + 1 ≤ n) : prefixLaw Q x (k + 1) hk = ((prefixLaw Q x k (le_of_succ_le hk)) ⊗ₘ (Q (nextIndex hk)).comap (fun u => (x (nextIndex hk), u)) (by fun_prop)).map (fun p => snoc hk p.1 p.2) := by rfl -
prefixLaw_succ_map_init_lasttheorem — Given a sequential kernel family, a fixed input vector, a prefix length, and a successor bound, splitting the next prefix into its preceding history and final output yields the composition-product law.hypothesesProof (Lean source)
theorem prefixLaw_succ_map_init_last (Q : KernelFamily X Z) (x : Fin n → X) (k : ℕ) (hk : k + 1 ≤ n) : (prefixLaw Q x (k + 1) hk).map (fun u => (init hk u, last hk u)) = (prefixLaw Q x k (le_of_succ_le hk)) ⊗ₘ (Q (nextIndex hk)).comap (fun u => (x (nextIndex hk), u)) (by fun_prop) := by rw [prefixLaw_succ, Measure.map_map (measurable_init_last hk) (measurable_snoc hk)] have h : (fun u : History Z (k + 1) hk => (init hk u, last hk u)) ∘ (fun p : History Z k (le_of_succ_le hk) × Z (nextIndex hk) => snoc hk p.1 p.2) = id := by funext p cases p with | mk a b => change (init hk (snoc hk a b), last hk (snoc hk a b)) = (a, b) apply Prod.ext · funext i exact congrFun (Fin.init_snoc (α := fun j : Fin (k + 1) => Z (castLE hk j)) (p := a) (x := b)) i · exact Fin.snoc_last (α := fun j : Fin (k + 1) => Z (castLE hk j)) (p := a) (x := b) rw [h, Measure.map_id] -
prefixLaw_succ_map_inittheorem — Given a sequential kernel family, the condition that every stage kernel is Markov, a fixed input vector, a prefix length, and a successor bound, forgetting the final output recovers the preceding prefix law.hypothesesn :sharedℕX :sharedType u_1Q :KernelFamily X ZhQ :∀ i, IsMarkovKernel (Q i)x :Fin n → Xk :ℕhk :k + 1 ≤ nconclusionProof (Lean source)
theorem prefixLaw_succ_map_init (Q : KernelFamily X Z) (hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X) (k : ℕ) (hk : k + 1 ≤ n) : (prefixLaw Q x (k + 1) hk).map (init hk) = prefixLaw Q x k (le_of_succ_le hk) := by let μ := prefixLaw Q x k (le_of_succ_le hk) let K := (Q (nextIndex hk)).comap (fun u => (x (nextIndex hk), u)) (by fun_prop) haveI : IsProbabilityMeasure μ := isProbabilityMeasure_prefixLaw Q hQ x k _ haveI : IsMarkovKernel (Q (nextIndex hk)) := hQ _ haveI : IsMarkovKernel K := Kernel.IsMarkovKernel.comap _ (by fun_prop) have h := congrArg (fun ν : Measure (History Z k (le_of_succ_le hk) × Z (nextIndex hk)) => ν.map fst) (prefixLaw_succ_map_init_last Q x k hk) rw [Measure.map_map measurable_fst (measurable_init_last hk)] at h have hfst : (μ ⊗ₘ K).fst = μ := by exact @Measure.fst_compProd _ _ _ _ μ (inferInstance) K (‹IsMarkovKernel K›) simpa only [Function.comp_def, μ, K, Measure.fst, fst] using h.trans hfst -
prefixLaw_map_restrictHistorytheorem — Given a sequential kernel family, the condition that every stage kernel is Markov, a fixed input vector, a target prefix bound, a source prefix bound, and an ordering of their lengths, restricting the longer prefix law recovers the shorter prefix law.hypothesesn :sharedℕX :sharedType u_1Q :KernelFamily X ZhQ :∀ i, IsMarkovKernel (Q i)x :Fin n → Xk l :ℕhk :k ≤ nhl :l ≤ nhkl :k ≤ lconclusionProof (Lean source)
theorem prefixLaw_map_restrictHistory (Q : KernelFamily X Z) (hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X) {k l : ℕ} (hk : k ≤ n) (hl : l ≤ n) (hkl : k ≤ l) : (prefixLaw Q x l hl).map (restrictHistory hk hl hkl) = prefixLaw Q x k hk := by induction l generalizing k with | zero => have h : k = 0 := Nat.eq_zero_of_le_zero hkl subst k have hp : hk = hl := Subsingleton.elim _ _ subst hk have hfun : restrictHistory (Z := Z) hl hl hkl = (id : History Z 0 hl → History Z 0 hl) := by funext u exact restrictHistory_self hl u rw [hfun, Measure.map_id] | succ l ih => rcases Nat.eq_or_lt_of_le hkl with heq | hlt · subst k have hp : hk = hl := Subsingleton.elim _ _ subst hk have hfun : restrictHistory (Z := Z) hl hl hkl = (id : History Z (l + 1) hl → History Z (l + 1) hl) := by funext u exact restrictHistory_self hl u rw [hfun, Measure.map_id] · have hkl' : k ≤ l := Nat.lt_succ_iff.mp hlt have hs : l + 1 ≤ n := hl have hinit := prefixLaw_succ_map_init Q hQ x l hs have hcomp : (restrictHistory (Z := Z) hk hl hkl) = (restrictHistory (Z := Z) hk (le_of_succ_le hs) hkl') ∘ init hs := by funext u exact restrictHistory_succ hk hs hkl' u rw [hcomp] have hmeas : Measurable (init hs : History Z (l + 1) hs → History Z l (le_of_succ_le hs)) := by apply measurable_pi_iff.mpr intro i exact measurable_pi_apply i.castSucc rw [← Measure.map_map (measurable_restrictHistory hk (le_of_succ_le hs) hkl') hmeas] rw [hinit] exact ih hk (le_of_succ_le hs) hkl' -
transcriptLaw_map_prefixtheorem — Given a sequential kernel family, the condition that every stage kernel is Markov, a fixed input vector, a prefix length, and evidence that the prefix lies within the horizon, the complete transcript law has the recursively constructed prefix law as its prefix marginal.hypothesesn :sharedℕX :sharedType u_1Q :KernelFamily X ZhQ :∀ i, IsMarkovKernel (Q i)x :Fin n → Xk :ℕhk :k ≤ nconclusionProof (Lean source)
theorem transcriptLaw_map_prefix (Q : KernelFamily X Z) (hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X) (k : ℕ) (hk : k ≤ n) : (transcriptLaw Q x).map (take hk) = prefixLaw Q x k hk := by have htake : (take hk : Transcript Z → History Z k hk) = restrictHistory hk le_rfl hk := by funext u exact (restrictHistory_transcript hk u).symm rw [htake] exact prefixLaw_map_restrictHistory Q hQ x hk le_rfl hk -
isProbabilityMeasure_transcriptLawtheorem — Given a sequential kernel family, the condition that every stage kernel is Markov, and a fixed input vector, the complete transcript law has total mass one.hypothesesconclusionProof (Lean source)
theorem isProbabilityMeasure_transcriptLaw (Q : KernelFamily X Z) (hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X) : IsProbabilityMeasure (transcriptLaw Q x) := by exact isProbabilityMeasure_prefixLaw Q hQ x n le_rfl
Factorization 1 core · 2 supporting This module evaluates atoms of dependent finite transcript laws as products of their stagewise conditional singleton probabilities. ★ transcriptLaw_singleton
Exact cylinder probabilities for finite sequential kernels
This module evaluates atoms of dependent finite transcript laws as products of their stagewise conditional singleton probabilities.
theorem transcriptLaw_singleton reviewed
⚑ flagged
Causalean.Mathlib.Probability.Kernel.FiniteSequence
Given a sequential kernel family, the condition that every stage kernel is Markov, a fixed input vector, and a complete transcript, the transcript atom probability is the finite product of its stagewise conditional singleton probabilities.
Formal statement
hypotheses
n :
ℕ
X :
Type u_1
Q :
KernelFamily X Z
hQ :
∀ i, IsMarkovKernel (Q i)
x :
Fin n → X
t :
conclusion
Proof (Lean source)
theorem transcriptLaw_singleton (Q : KernelFamily X Z)
(hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X)
(t : Transcript Z) :
transcriptLaw Q x {t} =
∏ i : Fin n,
(Q i) (x i, take (le_of_lt i.isLt) t) {t i} := by
have h (k : ℕ) (hk : k ≤ n) :
prefixLaw Q x k hk {take hk t} =
∏ i : Fin k,
(Q (castLE hk i))
(x (castLE hk i),
take (le_of_lt (castLE hk i).isLt) t)
{t (castLE hk i)} := by
induction k with
| zero =>
have he : ({take hk t} : Set (History Z 0 hk)) = univ := by
ext v
have hv : v = take hk t := by funext i; exact i.elim0
simp [hv]
change (Measure.dirac (fun j : Fin 0 => j.elim0))
({take hk t} : Set ((j : Fin 0) → Z (castLE hk j))) = _
have hm := congrArg
(fun s : Set (History Z 0 hk) =>
(Measure.dirac (fun j : Fin 0 => j.elim0)) s) he
change (Measure.dirac (fun j : Fin 0 => j.elim0))
({take hk t} : Set ((j : Fin 0) → Z (castLE hk j))) = 1
haveI : IsProbabilityMeasure (prefixLaw Q x 0 hk) :=
isProbabilityMeasure_prefixLaw Q hQ x 0 hk
exact hm.trans (by change (prefixLaw Q x 0 hk) univ = 1; exact measure_univ)
| succ j ih =>
let hj : j ≤ n := Nat.le_of_succ_le hk
have ht : take hk t = snoc hk (take hj t) (t (nextIndex hk)) := by
funext i
refine Fin.lastCases ?_ (fun a => ?_) i
· simp [take, snoc, nextIndex, snoc, castLE]
· simp [take, snoc, nextIndex, snoc, castLE]
rw [ht, prefixLaw_succ_singleton Q hQ x j hk]
rw [ih hj, Fin.prod_univ_castSucc]
rfl
have ht : take le_rfl t = t := by funext i; rfl
simpa only [transcriptLaw, ht, Fin.castLE_refl] using h n le_rfl
2 supporting declarations (lemmas, instances)
-
prefixLaw_succ_singletontheorem — Given a sequential kernel family, the condition that every stage kernel is Markov, a fixed input vector, a preceding-prefix length, a successor bound, a preceding history, and a next output, the atom of the extended history is the preceding atom mass times the conditional next-output mass.hypothesesn :sharedℕX :sharedType u_1Q :KernelFamily X ZhQ :∀ i, IsMarkovKernel (Q i)x :Fin n → Xk :ℕhk :k + 1 ≤ nu :History Z k (le_of_succ_le hk)z :Z (nextIndex hk)Proof (Lean source)
theorem prefixLaw_succ_singleton (Q : KernelFamily X Z) (hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin n → X) (k : ℕ) (hk : k + 1 ≤ n) (u : History Z k (le_of_succ_le hk)) (z : Z (nextIndex hk)) : prefixLaw Q x (k + 1) hk {snoc hk u z} = prefixLaw Q x k (le_of_succ_le hk) {u} * (Q (nextIndex hk)) (x (nextIndex hk), u) {z} := by let μ := prefixLaw Q x k (le_of_succ_le hk) let K := (Q (nextIndex hk)).comap (fun v => (x (nextIndex hk), v)) (by fun_prop) haveI : IsProbabilityMeasure μ := isProbabilityMeasure_prefixLaw Q hQ x k _ haveI : IsMarkovKernel (Q (nextIndex hk)) := hQ _ haveI : IsMarkovKernel K := Kernel.IsMarkovKernel.comap _ (by fun_prop) have hms (v : History Z (k + 1) hk) : MeasurableSet ({v} : Set (History Z (k + 1) hk)) := by change MeasurableSet ({v} : Set ((i : Fin (k + 1)) → Z (castLE hk i))) have h := MeasurableSet.univ_pi (fun i => measurableSet_singleton (v i)) exact (Set.univ_pi_singleton v) ▸ h have hmu (v : History Z k (le_of_succ_le hk)) : MeasurableSet ({v} : Set (History Z k (le_of_succ_le hk))) := by change MeasurableSet ({v} : Set ((i : Fin k) → Z (castLE (le_of_succ_le hk) i))) have h := MeasurableSet.univ_pi (fun i => measurableSet_singleton (v i)) exact (Set.univ_pi_singleton v) ▸ h letI : MeasurableSingletonClass (History Z k (le_of_succ_le hk)) := ⟨hmu⟩ have hs : (fun p : History Z k (le_of_succ_le hk) × Z (nextIndex hk) => snoc hk p.1 p.2) ⁻¹' {snoc hk u z} = {u} ×ˢ {z} := by ext p change (snoc hk p.1 p.2 = snoc hk u z) ↔ (p.1 = u ∧ p.2 = z) exact Fin.snoc_inj rw [prefixLaw_succ, Measure.map_apply (measurable_snoc hk) (hms _), hs] rw [Measure.compProd_apply_prod (hmu u) (measurableSet_singleton z)] rw [lintegral_singleton] simp only [Kernel.comap_apply] exact mul_comm _ _ -
transcriptLaw_zerotheorem — Given a zero-horizon output family, a sequential kernel family, the condition that every stage kernel is Markov, a zero-horizon input vector, and the sole empty transcript, that transcript has probability one.hypothesesconclusiontranscriptLaw Q x {t} = 1Proof (Lean source)
theorem transcriptLaw_zero (Z : Fin 0 → Type*) [∀ i, MeasurableSpace (Z i)] [∀ i, MeasurableSingletonClass (Z i)] (Q : KernelFamily X Z) (hQ : ∀ i, IsMarkovKernel (Q i)) (x : Fin 0 → X) (t : Transcript Z) : transcriptLaw Q x {t} = 1 := by simpa using transcriptLaw_singleton Q hQ x t