+# Updating finite transcripts by deterministic observations

An observation extends a transcript by a deterministic function of one side's variable. Its new transcript mass counts all preimages, and its conditional kernel keeps the original variable. Null observation rows use the existing uniform completion of conditionalWeight. The other side's kernel will remain unchanged in the factorization theorems.

These definitions give the finite weighted form of the deterministic observation rule in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Lemma 3.25, printed p.15, used in the proof of Theorem 6.1: https://arxiv.org/abs/2110.12652.

noncomputable def Algebraic.Cutwidth.Extractor.observedTranscriptWeight {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (w : Z → ℝ) (p : Z → A → ℝ) (f : Z → A → U) (zu : Z × U) : ℝ

Extend a transcript by an observation of its conditional source.

Equations

• Algebraic.Cutwidth.Extractor.observedTranscriptWeight w p f zu = w zu.1 * Algebraic.Cutwidth.Extractor.mapWeight (f zu.1) (p zu.1) zu.2

noncomputable def Algebraic.Cutwidth.Extractor.observedTranscriptKernel {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (p : Z → A → ℝ) (f : Z → A → U) (zu : Z × U) : A → ℝ

Condition the observed side on its message, with normalized null-row completion.

Equations

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