Joint source envelopes under deterministic transcript messages

A left message restricts each original source event, so copying the old envelope to every message bounds the updated joint masses. Its total grows by the message alphabet's size. A right message scales each envelope by the message probability, preserving the total for a normalized right kernel. The same laws compose when the right message depends on the left message.

These are finite mass bounds underlying the conditional-entropy accounting in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), proof of Theorem 6.1, printed pp.22--25, using the deterministic observation rule of Lemma 3.25: https://arxiv.org/abs/2110.12652. The bounds apply to the actual updated kernels, including null observation rows; they impose no individual conditional entropy requirement.

theorem Algebraic.Cutwidth.Extractor.observedTranscriptWeight_nonnegative {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype A] (w : Z → ℝ) (p : Z → A → ℝ) (f : Z → A → U) (hw : ∀ (z : Z), 0 ≤ w z) (hp : ∀ (z : Z) (a : A), 0 ≤ p z a) (zu : Z × U) : 0 ≤ observedTranscriptWeight w p f zu

Updating a nonnegative transcript envelope by nonnegative message weights preserves its sign.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_left_source_eq {Z : Type u_1} {A : Type u_2} {X : Type u_3} {U : Type u_4} [Fintype A] (w : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → X) (f : Z → A → U) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (zu : Z × U) (x₀ : X) : observedTranscriptWeight w l f zu * mapWeight (x zu.1) (observedTranscriptKernel l f zu) x₀ = w zu.1 * mapWeight (fun (a : A) => (f zu.1 a, x zu.1 a)) (l zu.1) (zu.2, x₀)

Observed source masses are exactly the original joint message-and-source masses.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_left_envelope {Z : Type u_1} {A : Type u_2} {X : Type u_3} {U : Type u_4} [Fintype A] (w : Z → ℝ) (l : Z → A → ℝ) (x : Z → A → X) (f : Z → A → U) (μ : Z → ℝ) (hw : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (zu : Z × U) (x₀ : X) : observedTranscriptWeight w l f zu * mapWeight (x zu.1) (observedTranscriptKernel l f zu) x₀ ≤ μ zu.1

Copying the old envelope to each left message bounds the updated joint source law.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_left_envelope_sum {Z : Type u_1} {U : Type u_2} [Fintype Z] [Fintype U] (μ : Z → ℝ) : ∑ zu : Z × U, μ zu.1 = ↑(Fintype.card U) * ∑ z : Z, μ z

Copying an envelope over a finite message alphabet multiplies its total by that size.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_right_envelope {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {V : Type u_5} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (g : Z → B → V) (μ : Z → ℝ) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) (cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (zv : Z × V) (x₀ : X) : observedTranscriptWeight w r g zv * mapWeight (x zv.1) (l zv.1) x₀ ≤ observedTranscriptWeight μ r g zv

A right message scales the source envelope by its own probability, leaving the source intact.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_right_envelope_sum {Z : Type u_1} {B : Type u_2} {V : Type u_3} [Fintype Z] [Fintype B] [Fintype V] (μ : Z → ℝ) (r : Z → B → ℝ) (g : Z → B → V) (mass : ∀ (z : Z), ∑ b : B, r z b = 1) : ∑ zv : Z × V, observedTranscriptWeight μ r g zv = ∑ z : Z, μ z

A right kernel of total mass one preserves the total source envelope exactly.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_left_right_envelope {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {U : Type u_5} {V : Type u_6} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → X) (f : Z → A → U) (g : Z × U → B → V) (μ : Z → ℝ) (hw : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) (cap : ∀ (z : Z) (x₀ : X), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (zuv : (Z × U) × V) (x₀ : X) : observedTranscriptWeight (observedTranscriptWeight w l f) (fun (zu : Z × U) => r zu.1) g zuv * mapWeight (x zuv.1.1) (observedTranscriptKernel l f zuv.1) x₀ ≤ observedTranscriptWeight (fun (zu : Z × U) => μ zu.1) (fun (zu : Z × U) => r zu.1) g zuv

A left message followed by an adaptive right message has the composed joint envelope.

theorem Algebraic.Cutwidth.Extractor.observedTranscript_left_right_envelope_sum {Z : Type u_1} {B : Type u_2} {U : Type u_3} {V : Type u_4} [Fintype Z] [Fintype B] [Fintype U] [Fintype V] (μ : Z → ℝ) (r : Z → B → ℝ) (g : Z × U → B → V) (mass : ∀ (z : Z), ∑ b : B, r z b = 1) : ∑ zuv : (Z × U) × V, observedTranscriptWeight (fun (zu : Z × U) => μ zu.1) (fun (zu : Z × U) => r zu.1) g zuv = ↑(Fintype.card U) * ∑ z : Z, μ z

The adaptive two-message envelope pays only for the left message alphabet.