Head and tail conditioning for finite block sources

A nonempty block source splits into a normalized capped head distribution and a normalized block-source tail for every head value. Positive rows use their conditional distribution. Zero rows can copy a positive row because their coefficient in the joint distribution is zero.

Conversely, a capped head and block-source tails form a block source. The more general coefficient criterion combines tails with nonnegative weights whose row totals form the prescribed capped head distribution; it needs no positive-row assumptions or conditional division.

These are finite structural steps for the block-source argument in Chattopadhyay--Goodman--Liao, Lemma 5.5 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/. Block.Condenser uses these laws to prove shared-seed condensation.

theorem Algebraic.Cutwidth.Extractor.blockPrefix_cons {α : Type u_1} {i t : ℕ} (h : i ≤ t) (a : α) (z : Fin t → α) : blockPrefix ⋯ (Fin.cons a z) = Fin.cons a (blockPrefix h z)

A nonempty prefix retains the head and restricts only the tail.

theorem Algebraic.Cutwidth.Extractor.blockPrefixWeight_cons {α : Type u_1} [Fintype α] {i t : ℕ} (p : (Fin (t + 1) → α) → ℝ) (h : i ≤ t) (a : α) (u : Fin i → α) : blockPrefixWeight p ⋯ (Fin.cons a u) = blockPrefixWeight (fun (z : Fin t → α) => p (Fin.cons a z)) h u

Fixing a nonempty prefix is the corresponding prefix event in its head row.

theorem Algebraic.Cutwidth.Extractor.mapWeight_blockHead_apply {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin (t + 1) → α) → ℝ) (a : α) : mapWeight (fun (x : Fin (t + 1) → α) => x 0) p a = ∑ z : Fin t → α, p (Fin.cons a z)

The head marginal counts every tail in the corresponding row.

theorem Algebraic.Cutwidth.Extractor.IsBlockSource.head_capped {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin (t + 1) → α) → ℝ} (source : IsBlockSource p K) : CappedWeight (mapWeight (fun (x : Fin (t + 1) → α) => x 0) p) K

The head inherits the block-source threshold.

theorem Algebraic.Cutwidth.Extractor.IsBlockSource.exists_head_tail {α : Type u_1} [Fintype α] {t K : ℕ} {p : (Fin (t + 1) → α) → ℝ} (source : IsBlockSource p K) : ∃ (w : α → ℝ) (q : α → (Fin t → α) → ℝ), IsProbabilityWeight w ∧ CappedWeight w K ∧ (∀ (a : α), IsBlockSource (q a) K) ∧ ∀ (a : α) (z : Fin t → α), p (Fin.cons a z) = w a * q a z

Disintegrate a nonempty tuple source into a capped head and normalized block-source tails, completing zero-mass head rows without extra assumptions.

theorem Algebraic.Cutwidth.Extractor.isBlockSource_prepend {α : Type u_1} [Fintype α] {t K : ℕ} (w : α → ℝ) (tail : α → (Fin t → α) → ℝ) (head_prob : IsProbabilityWeight w) (head_cap : CappedWeight w K) (tail_source : ∀ (a : α), IsBlockSource (tail a) K) : IsBlockSource (fun (x : Fin (t + 1) → α) => w (x 0) * tail (x 0) (Fin.tail x)) K

Prepend a normalized capped head to a block-source tail for every head value.

theorem Algebraic.Cutwidth.Extractor.isBlockSource_of_prepend_mixture {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] {t K : ℕ} (r : (Fin (t + 1) → α) → ℝ) (target : α → ℝ) (tail : ι → (Fin t → α) → ℝ) (c : α → ι → ℝ) (target_prob : IsProbabilityWeight target) (target_cap : CappedWeight target K) (tail_source : ∀ (a : ι), IsBlockSource (tail a) K) (coeff_nonneg : ∀ (h : α) (a : ι), 0 ≤ c h a) (rows : ∀ (h : α), ∑ a : ι, c h a = target h) (factor : ∀ (h : α) (z : Fin t → α), r (Fin.cons h z) = ∑ a : ι, c h a * tail a z) : IsBlockSource r K

Nonnegative mixtures in each head row preserve all tail caps when the row totals form a normalized capped head distribution.