Conditional independence after deterministic observations

A deterministic observation of one side extends the transcript and conditions that side's kernel. The opposite kernel stays unchanged, and the resulting factored law is exactly the pushforward of the original joint law. Every conditional kernel is normalized, including null observation rows. A second observation may depend on the first message.

This is the finite weighted deterministic-observation rule in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Lemma 3.25, printed p.15, repeatedly used in the proof of Theorem 6.1, pp.22--25: https://arxiv.org/abs/2110.12652. No positive-probability conditioning or additional independence hypothesis is hidden in a transcript update.

theorem Algebraic.Cutwidth.Extractor.factoredWeight_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (factoredWeight w l r)

Normalized transcript and side kernels define a normalized factored joint law.

theorem Algebraic.Cutwidth.Extractor.observedTranscriptWeight_probability {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype Z] [Fintype A] [Fintype U] (w : Z → ℝ) (p : Z → A → ℝ) (f : Z → A → U) (hw : IsProbabilityWeight w) (hp : ∀ (z : Z), IsProbabilityWeight (p z)) : IsProbabilityWeight (observedTranscriptWeight w p f)

A deterministic message extends the transcript to another probability law.

theorem Algebraic.Cutwidth.Extractor.observedTranscriptKernel_probability {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] [Fintype U] (p : Z → A → ℝ) (f : Z → A → U) (probability : ∀ (z : Z), IsProbabilityWeight (p z)) (zu : Z × U) : IsProbabilityWeight (observedTranscriptKernel p f zu)

Every updated conditional row is normalized, even for an impossible message.

theorem Algebraic.Cutwidth.Extractor.observedTranscriptKernel_eq_uniform {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (p : Z → A → ℝ) (f : Z → A → U) (zu : Z × U) (zero : mapWeight (f zu.1) (p zu.1) zu.2 = 0) : observedTranscriptKernel p f zu = uniformWeight A

A null observation row uses exactly the existing uniform completion.

theorem Algebraic.Cutwidth.Extractor.observedTranscriptWeight_mul_kernel {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (w : Z → ℝ) (p : Z → A → ℝ) (f : Z → A → U) (nonnegative : ∀ (z : Z) (a : A), 0 ≤ p z a) (zu : Z × U) (a : A) : observedTranscriptWeight w p f zu * observedTranscriptKernel p f zu a = if f zu.1 a = zu.2 then w zu.1 * p zu.1 a else 0

The new joint source masses are the original masses restricted to the message event.

theorem Algebraic.Cutwidth.Extractor.factoredWeight_observe_left {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → A → U) (nonnegative : ∀ (z : Z) (a : A), 0 ≤ l z a) : mapWeight (fun (p : (Z × B) × A) => (((p.1.1, f p.1.1 p.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight w l f) (observedTranscriptKernel l f) fun (zu : Z × U) => r zu.1

Observing the left side preserves the right kernel and the complete actual joint law.

theorem Algebraic.Cutwidth.Extractor.factoredWeight_observe_right {Z : Type u_1} {A : Type u_2} {B : Type u_3} {V : Type u_4} [Fintype Z] [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (g : Z → B → V) (nonnegative : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => (((p.1.1, g p.1.1 p.1.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight w r g) (fun (zv : Z × V) => l zv.1) (observedTranscriptKernel r g)

Observing the right side preserves the left kernel and the complete actual joint law.

theorem Algebraic.Cutwidth.Extractor.factoredWeight_observe_left_right {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {V : Type u_5} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → A → U) (g : Z × U → B → V) (left_nonnegative : ∀ (z : Z) (a : A), 0 ≤ l z a) (right_nonnegative : ∀ (z : Z) (b : B), 0 ≤ r z b) : mapWeight (fun (p : (Z × B) × A) => ((((p.1.1, f p.1.1 p.2), g (p.1.1, f p.1.1 p.2) p.1.2), p.1.2), p.2)) (factoredWeight w l r) = factoredWeight (observedTranscriptWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) g) (fun (zuv : (Z × U) × V) => observedTranscriptKernel l f zuv.1) (observedTranscriptKernel (fun (zu : Z × U) => r zu.1) g)

A left message followed by an adaptive right message has an exact factored representation.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_left_right_probability {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {V : Type u_5} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] [Fintype V] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (f : Z → A → U) (g : Z × U → B → V) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) : IsProbabilityWeight (observedTranscriptWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) g) ∧ (∀ (zuv : (Z × U) × V), IsProbabilityWeight (observedTranscriptKernel l f zuv.1)) ∧ ∀ (zuv : (Z × U) × V), IsProbabilityWeight (observedTranscriptKernel (fun (zu : Z × U) => r zu.1) g zuv)

Both conditional sides and the transcript remain normalized after two alternating messages.