Source envelopes after finite transcript updates

The exact conditional-row factorization restricts the old source mass to the observed message. Refinement bounds then charge a left message by its alphabet size. A right message scales the envelope by its own probability and preserves the total envelope when the right kernel has total mass one.

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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₀)

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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