Conditional-tail replacement after splitting a pair of heads #
Keeping a pair of head coordinates retains the mixture tag. Replacing its conditional tails therefore costs at most their weighted average distance. The component weights need not be normalized or nonnegative; only the mixing head coefficients must be nonnegative for the distance bound.
These finite identities supply the tail hybrid in the blockwise splitting argument of Chattopadhyay--Goodman--Liao, Corollary 5.4 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/.
theorem
Algebraic.Cutwidth.Extractor.Internal.splitBlock_pairPrepend_dist_le
{α : Type u_1}
[Fintype α]
{t : ℕ}
(w : α × α → ℝ)
(nonnegative : ∀ (ab : α × α), 0 ≤ w ab)
(p q : α × α → (Fin t → α) → ℝ)
:
weightDist
(mapWeight (fun (az : (α × α) × (Fin t → α)) => Fin.cons az.1.1 (Fin.cons az.1.2 az.2))
fun (az : (α × α) × (Fin t → α)) => w az.1 * p az.1 az.2)
(mapWeight (fun (az : (α × α) × (Fin t → α)) => Fin.cons az.1.1 (Fin.cons az.1.2 az.2))
fun (az : (α × α) × (Fin t → α)) => w az.1 * q az.1 az.2) ≤ ∑ ab : α × α, w ab * weightDist (p ab) (q ab)
theorem
Algebraic.Cutwidth.Extractor.Internal.splitBlock_pairPrepend_dist_le_of_le
{α : Type u_1}
[Fintype α]
{t : ℕ}
(w : α × α → ℝ)
(hw : IsProbabilityWeight w)
(p q : α × α → (Fin t → α) → ℝ)
{δ : ℝ}
(error : ∀ (ab : α × α), weightDist (p ab) (q ab) ≤ δ)
:
weightDist
(mapWeight (fun (az : (α × α) × (Fin t → α)) => Fin.cons az.1.1 (Fin.cons az.1.2 az.2))
fun (az : (α × α) × (Fin t → α)) => w az.1 * p az.1 az.2)
(mapWeight (fun (az : (α × α) × (Fin t → α)) => Fin.cons az.1.1 (Fin.cons az.1.2 az.2))
fun (az : (α × α) × (Fin t → α)) => w az.1 * q az.1 az.2) ≤ δ