Averaging seed error after an independent left observation

If the right seed and its right observation use only the actual prefix, retaining additional original left observations does not change their averaged distance from uniform. No individual transcript row is assumed close to uniform, and null rows contribute zero automatically.

theorem Algebraic.Cutwidth.Extractor.Internal.smooth_observedSeedWeight_dist_eq {Z : Type u_1} {B : Type u_2} {V : Type u_3} {Seed : Type u_4} [Fintype Z] [Fintype B] [Fintype V] [Fintype Seed] (w : Z → ℝ) (r : Z → B → ℝ) (v : Z → B → V) (y : Z → B → Seed) (nonnegative : ∀ (z : Z), 0 ≤ w z) : weightDist (observedSeedWeight w r v y) (uniformSecondWeight (observedSeedWeight w r v y)) = ∑ z : Z, w z * weightDist (mapWeight (fun (b : B) => (v z b, y z b)) (r z)) (uniformSecondWeight (mapWeight (fun (b : B) => (v z b, y z b)) (r z)))

theorem Algebraic.Cutwidth.Extractor.Internal.smoothPrefixSeedWeight_dist_eq {Z : Type u_1} {A : Type u_2} {B : Type u_3} {Q : Type u_4} {V : Type u_5} {Seed : Type u_6} [Fintype Z] [Fintype A] [Fintype B] [Fintype Q] [Fintype V] [Fintype Seed] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (q : Z → A → Q) (v : Z × Q → B → V) (y : Z × Q → B → Seed) (hw : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : weightDist (smoothPrefixSeedWeight w l r q v y) (uniformSecondWeight (smoothPrefixSeedWeight w l r q v y)) = ∑ z : Z, w z * ∑ a : A, l z a * weightDist (mapWeight (fun (b : B) => (v (z, q z a) b, y (z, q z a) b)) (r z)) (uniformSecondWeight (mapWeight (fun (b : B) => (v (z, q z a) b, y (z, q z a) b)) (r z)))

theorem Algebraic.Cutwidth.Extractor.Internal.smooth_observed_average {Z : Type u_1} {A : Type u_2} {U : Type u_3} [Fintype Z] [Fintype A] [Fintype U] (w : Z → ℝ) (l : Z → A → ℝ) (u : Z → A → U) (g : Z → A → ℝ) (hl : ∀ (z : Z) (a : A), 0 ≤ l z a) : ∑ zu : Z × U, observedTranscriptWeight w l u zu * ∑ a : A, observedTranscriptKernel l u zu a * g zu.1 a = ∑ z : Z, w z * ∑ a : A, l z a * g z a

theorem Algebraic.Cutwidth.Extractor.Internal.smoothMergingSeedWeight_prefix_dist {Z : Type u_1} {A : Type u_2} {B : Type u_3} {U : Type u_4} {Q : Type u_5} {V : Type u_6} {Seed : Type u_7} [Fintype Z] [Fintype A] [Fintype B] [Fintype U] [Fintype Q] [Fintype V] [Fintype Seed] (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (u : Z → A → U) (q : Z → A → Q) (v : Z × Q → B → V) (y : Z × Q → B → Seed) (hw : ∀ (z : Z), 0 ≤ w z) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) : weightDist (smoothMergingSeedWeight w l r u q (fun (h : SmoothMergingTranscript Z U Q) => v (h.1.1, h.2)) fun (h : SmoothMergingTranscript Z U Q) => y (h.1.1, h.2)) (uniformSecondWeight (smoothMergingSeedWeight w l r u q (fun (h : SmoothMergingTranscript Z U Q) => v (h.1.1, h.2)) fun (h : SmoothMergingTranscript Z U Q) => y (h.1.1, h.2))) = weightDist (observedSeedWeight (observedTranscriptWeight w l q) (fun (zq : Z × Q) => r zq.1) v y) (uniformSecondWeight (observedSeedWeight (observedTranscriptWeight w l q) (fun (zq : Z × Q) => r zq.1) v y))