Rowwise finite entropy repair #
A uniform replacement preserves a row's total mass. Large rows satisfy the conditional cap by the original point bound, and small rows satisfy it by the second alphabet's cardinality. The variation distance is bounded by the total mass in replaced rows. Row averaging also preserves every original joint point-mass cap, independently of normalization or nonnegativity.
theorem
Algebraic.Cutwidth.Extractor.Internal.twoBlockRepair_capped
{α : Type u_1}
{β : Type u_2}
[Fintype β]
(p : α × β → ℝ)
(N K : ℕ)
(μ : ℝ)
(cap : CappedWeight p N)
:
CappedWeight (twoBlockRepair p K μ) N
theorem
Algebraic.Cutwidth.Extractor.Internal.twoBlockRepair_probability
{α : Type u_1}
{β : Type u_2}
[Fintype α]
[Fintype β]
[Nonempty β]
(p : α × β → ℝ)
(probability : IsProbabilityWeight p)
(K : ℕ)
(μ : ℝ)
:
IsProbabilityWeight (twoBlockRepair p K μ)
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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 * μ
theorem
Algebraic.Cutwidth.Extractor.Internal.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)⁻¹
theorem
Algebraic.Cutwidth.Extractor.Internal.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)⁻¹