Averaging multiblock splitting over retained seeds

Choose a repaired block source in every seed fiber. Splitting preserves the seed coordinate, and its joint distance is the average of the fiber distances. The empty seed type contributes zero total mass and zero distance.

theorem Algebraic.Cutwidth.Extractor.Internal.exists_split_pow_two_seedFamily {α : Type u_1} {Seed : Type u_2} [Fintype α] [Fintype Seed] {t m s k e : ℕ} (p : Seed → (Fin t → α × α) → ℝ) (source : ∀ (y : Seed), IsBlockSource (p y) (2 ^ k)) (card : Fintype.card α = 2 ^ m) (width : s ≤ m) (entropy : m + s + e ≤ k) : ∃ (q : Seed → (Fin (2 * t) → α) → ℝ), (∀ (y : Seed), IsBlockSource (q y) (2 ^ s)) ∧ weightDist (mapWeight (fun (yx : Seed × (Fin t → α × α)) => (yx.1, (splitBlockEquiv α t) yx.2)) (seedFamilyWeight p)) (seedFamilyWeight q) ≤ ↑t * (2 ^ e)⁻¹