Original-source envelopes under the common look-ahead transcript

The left source pays for the four left outputs, while its envelope is scaled by the right-pair probability. The right source pays for the two right inputs; the subsequent left observation preserves its total envelope.

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBaseLeftEnvelope_nonnegative {Z : Type u_1} {B : Type u_2} {Q : Type u_3} {Mid : Type u_4} [Fintype B] (μ : Z → ℝ) (r : Z → B → ℝ) (q q' : Z → B → Q) (hμ : ∀ (z : Z), 0 ≤ μ z) (hr : ∀ (z : Z) (b : B), 0 ≤ r z b) (t : LookAheadBaseTranscript Z Q Mid) : 0 ≤ lookAheadBaseLeftEnvelope μ r q q' t

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBaseRightEnvelope_nonnegative {Z : Type u_1} {A : Type u_2} {X : Type u_3} {Q : Type u_4} {Seed : Type u_5} {Mid : Type u_6} [Fintype A] (ν : Z → ℝ) (l : Z → A → ℝ) (x x' : Z → A → X) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (hν : ∀ (z : Z), 0 ≤ ν z) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) (t : LookAheadBaseTranscript Z Q Mid) : 0 ≤ lookAheadBaseRightEnvelope ν l x x' initialSeed W QExt t

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBase_left_envelope {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → X) (q q' : Z → B → Q) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (μ : 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) (t : LookAheadBaseTranscript Z Q Mid) (x₀ : X) : lookAheadBaseWeight w l r x x' q q' initialSeed W QExt t * mapWeight (x t.1.1) (lookAheadBaseLeft l x x' initialSeed W QExt t) x₀ ≤ lookAheadBaseLeftEnvelope μ r q q' t

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBase_right_envelope {Z : Type u_1} {A : Type u_2} {B : Type u_3} {X : Type u_4} {Q : Type u_5} {Seed : Type u_6} {Mid : Type u_7} {Y : Type u_8} [Fintype A] [Fintype B] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x x' : Z → A → X) (q q' : Z → B → Q) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (y : Z → B → Y) (ν : 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) (y₀ : Y), w z * mapWeight (y z) (r z) y₀ ≤ ν z) (t : LookAheadBaseTranscript Z Q Mid) (y₀ : Y) : lookAheadBaseWeight w l r x x' q q' initialSeed W QExt t * mapWeight (y t.1.1) (lookAheadBaseRight r q q' t) y₀ ≤ lookAheadBaseRightEnvelope ν l x x' initialSeed W QExt t

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBaseLeftEnvelope_sum {Z : Type u_1} {B : Type u_2} {Q : Type u_3} {Mid : Type u_4} [Fintype Z] [Fintype B] [Fintype Q] [Fintype Mid] (μ : Z → ℝ) (r : Z → B → ℝ) (q q' : Z → B → Q) (mass : ∀ (z : Z), ∑ b : B, r z b = 1) : ∑ t : LookAheadBaseTranscript Z Q Mid, lookAheadBaseLeftEnvelope μ r q q' t = ↑(Fintype.card ((Mid × Mid) × Mid × Mid)) * ∑ z : Z, μ z

theorem Algebraic.Cutwidth.Extractor.Internal.lookAheadBaseRightEnvelope_sum {Z : Type u_1} {A : Type u_2} {X : Type u_3} {Q : Type u_4} {Seed : Type u_5} {Mid : Type u_6} [Fintype Z] [Fintype A] [Fintype Q] [Fintype Mid] (ν : Z → ℝ) (l : Z → A → ℝ) (x x' : Z → A → X) (initialSeed : Q → Seed) (W : X → Seed → Mid) (QExt : Q → Mid → Seed) (mass : ∀ (z : Z), ∑ a : A, l z a = 1) : ∑ t : LookAheadBaseTranscript Z Q Mid, lookAheadBaseRightEnvelope ν l x x' initialSeed W QExt t = ↑(Fintype.card (Q × Q)) * ∑ z : Z, ν z