The conditional-tail hybrid in block condensation #
Replacing every conditional tail by a close retained-seed law costs its weighted average error. Mapping the original head with the same seed preserves this bound, without discarding its correlations with the tail.
theorem
Algebraic.Cutwidth.Extractor.Internal.blockCondenser_map_prepend
{α : Type u_1}
{Ω : Type u_2}
[Fintype α]
[Fintype Ω]
{t : ℕ}
(w : α → ℝ)
(p : α → (Fin t → α) → ℝ)
(f : α → Ω)
:
(mapWeight (fun (x : Fin (t + 1) → α) (i : Fin (t + 1)) => f (x i)) fun (x : Fin (t + 1) → α) =>
w (x 0) * p (x 0) (Fin.tail x)) = mapWeight (fun (az : α × (Fin t → Ω)) => Fin.cons (f az.1) az.2) fun (az : α × (Fin t → Ω)) =>
w az.1 * mapWeight (fun (z : Fin t → α) (i : Fin t) => f (z i)) (p az.1) az.2
theorem
Algebraic.Cutwidth.Extractor.Internal.blockCondenser_tail_map_dist_le
{α : Type u_1}
{Ω : Type u_2}
[Fintype α]
[Fintype Ω]
{t : ℕ}
(w : α → ℝ)
(nonnegative : ∀ (a : α), 0 ≤ w a)
(p : α → (Fin t → α) → ℝ)
(q : α → (Fin t → Ω) → ℝ)
(f : α → Ω)
:
weightDist
(mapWeight (fun (x : Fin (t + 1) → α) (i : Fin (t + 1)) => f (x i)) fun (x : Fin (t + 1) → α) =>
w (x 0) * p (x 0) (Fin.tail x))
(mapWeight (fun (az : α × (Fin t → Ω)) => Fin.cons (f az.1) az.2) fun (az : α × (Fin t → Ω)) =>
w az.1 * q az.1 az.2) ≤ ∑ a : α, w a * weightDist (mapWeight (fun (x : Fin t → α) (i : Fin t) => f (x i)) (p a)) (q a)
theorem
Algebraic.Cutwidth.Extractor.Internal.blockCondenser_hybrid_le
{α : Type u_1}
{Seed : Type u_2}
{Ω : Type u_3}
[Fintype α]
[Fintype Seed]
[Fintype Ω]
{t : ℕ}
(C : α → Seed → Ω)
(w : α → ℝ)
(hw : IsProbabilityWeight w)
(p : α → (Fin t → α) → ℝ)
(q : α → Seed → (Fin t → Ω) → ℝ)
{δ : ℝ}
(error :
∀ (a : α),
weightDist (weightedSeededOutput (p a) fun (x : Fin t → α) (y : Seed) (i : Fin t) => C (x i) y)
(seedFamilyWeight (q a)) ≤ δ)
:
weightDist
(weightedSeededOutput (fun (x : Fin (t + 1) → α) => w (x 0) * p (x 0) (Fin.tail x))
fun (x : Fin (t + 1) → α) (y : Seed) (i : Fin (t + 1)) => C (x i) y)
(seedFamilyWeight fun (y : Seed) =>
mapWeight (fun (az : α × (Fin t → Ω)) => Fin.cons (C az.1 y) az.2) fun (az : α × (Fin t → Ω)) =>
w az.1 * q az.1 y az.2) ≤ δ