Finite two-block entropy repair

A point-mass bound on a joint source gives a nearby block source by replacing small rows with uniform rows of the same mass. This preserves the first marginal exactly. Conditional caps are stated without division by the row mass, so they apply to zero-mass rows as well. Row averaging retains the original joint point-mass cap, allowing the repair to feed later splitting steps at the same input threshold.

The power-of-two corollary is a finite marginal-preserving version of Chattopadhyay--Goodman--Liao, Lemma 5.3 of Affine Extractors for Almost Logarithmic Entropy, https://eccc.weizmann.ac.il/report/2021/075/, which attributes the splitting lemma to Goldreich--Wigderson (1997). The explicit repair and the sharper bound by the mass of the replaced rows are proved here. This module concerns probability weights; a recursive extractor and its seed-reuse argument require further results.

theorem Algebraic.Cutwidth.Extractor.twoBlockRepair_capped {α : Type u_1} {β : Type u_2} [Fintype β] (p : α × β → ℝ) (N K : ℕ) (μ : ℝ) (cap : CappedWeight p N) : CappedWeight (twoBlockRepair p K μ) N

Row averaging preserves any original joint cap, without probability, nonnegativity, or nonempty-alphabet assumptions.

theorem Algebraic.Cutwidth.Extractor.twoBlockRepair_firstWeight {α : Type u_1} {β : Type u_2} [Fintype β] [Nonempty β] (p : α × β → ℝ) (K : ℕ) (μ : ℝ) : firstWeight (twoBlockRepair p K μ) = firstWeight p

Uniformizing small rows preserves every first-coordinate mass exactly.

theorem Algebraic.Cutwidth.Extractor.twoBlockRepair_probability {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty β] (p : α × β → ℝ) (probability : IsProbabilityWeight p) (K : ℕ) (μ : ℝ) : IsProbabilityWeight (twoBlockRepair p K μ)

The repaired weights remain a probability distribution.

theorem Algebraic.Cutwidth.Extractor.twoBlockRepair_conditional_cap {α : Type u_1} {β : Type u_2} [Fintype β] [Nonempty β] (p : α × β → ℝ) (nonnegative : ∀ (x : α × β), 0 ≤ p x) {K : ℕ} {μ : ℝ} (size : K ≤ Fintype.card β) (cap : ∀ (x : α × β), p x ≤ μ) (a : α) (b : β) : ↑K * twoBlockRepair p K μ (a, b) ≤ firstWeight (twoBlockRepair p K μ) a

Every repaired row satisfies the conditional cap, including rows of mass zero.

theorem Algebraic.Cutwidth.Extractor.twoBlockRepair_first_cap {α : Type u_1} {β : Type u_2} [Fintype β] [Nonempty β] (p : α × β → ℝ) {K : ℕ} {μ : ℝ} (cap : ∀ (x : α × β), p x ≤ μ) (budget : ↑K * ↑(Fintype.card β) * μ ≤ 1) : CappedWeight (firstWeight (twoBlockRepair p K μ)) K

The original joint point cap also controls the unchanged first marginal.

theorem Algebraic.Cutwidth.Extractor.twoBlockRepair_dist_le_low_mass {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty β] (p : α × β → ℝ) (nonnegative : ∀ (x : α × β), 0 ≤ p x) (K : ℕ) (μ : ℝ) : weightDist p (twoBlockRepair p K μ) ≤ ∑ a : α, if firstWeight p a < ↑K * μ then firstWeight p a else 0

The repair costs at most the total mass of the rows it replaces.

theorem Algebraic.Cutwidth.Extractor.twoBlockRepair_dist_le {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] [Nonempty β] (p : α × β → ℝ) (probability : IsProbabilityWeight p) {K : ℕ} {μ : ℝ} (cap : ∀ (x : α × β), p x ≤ μ) : weightDist p (twoBlockRepair p K μ) ≤ ↑(Fintype.card α) * ↑K * μ

Each replaced row has mass less than K*μ, giving a cardinality bound.

theorem Algebraic.Cutwidth.Extractor.exists_twoBlock_repair {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : α × β → ℝ) (probability : IsProbabilityWeight p) {K : ℕ} {μ : ℝ} (positive : 0 < K) (size : K ≤ Fintype.card β) (cap : ∀ (x : α × β), p x ≤ μ) (budget : ↑K * ↑(Fintype.card β) * μ ≤ 1) : ∃ (q : α × β → ℝ), IsProbabilityWeight q ∧ firstWeight q = firstWeight p ∧ CappedWeight (firstWeight q) K ∧ (∀ (a : α) (b : β), ↑K * q (a, b) ≤ firstWeight q a) ∧ weightDist p q ≤ ↑(Fintype.card α) * ↑K * μ

Repair a joint source into a two-block source with threshold K, preserving its first marginal and paying at most card α*K*μ in distance.

theorem Algebraic.Cutwidth.Extractor.exists_twoBlock_repair_pow_two {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (p : α × β → ℝ) (probability : IsProbabilityWeight p) {m t k e : ℕ} (card_first : Fintype.card α = 2 ^ m) (card_second : Fintype.card β = 2 ^ m) (cap : CappedWeight p (2 ^ k)) (width : t ≤ m) (entropy : m + t + e ≤ k) : ∃ (q : α × β → ℝ), IsProbabilityWeight q ∧ firstWeight q = firstWeight p ∧ CappedWeight (firstWeight q) (2 ^ t) ∧ (∀ (a : α) (b : β), ↑(2 ^ t) * q (a, b) ≤ firstWeight q a) ∧ weightDist p q ≤ (2 ^ e)⁻¹

For equal m-bit alphabets, joint entropy at least m+t+e can be repaired to two blocks of entropy at least t with error at most 2^(-e).

theorem Algebraic.Cutwidth.Extractor.exists_twoBlock_repair_pow_two_capped {α : Type u_1} [Fintype α] (p : α × α → ℝ) (probability : IsProbabilityWeight p) {m s k e : ℕ} (card : Fintype.card α = 2 ^ m) (cap : CappedWeight p (2 ^ k)) (width : s ≤ m) (entropy : m + s + e ≤ k) : ∃ (q : α × α → ℝ), IsProbabilityWeight q ∧ CappedWeight q (2 ^ k) ∧ IsBlockSource (fun (x : Fin 2 → α) => q (x 0, x 1)) (2 ^ s) ∧ firstWeight q = firstWeight p ∧ weightDist p q ≤ (2 ^ e)⁻¹

The explicit power-of-two repair also retains the original joint cap, while producing two blocks at the smaller threshold and preserving their first marginal.