Finite block sources

A source on t blocks is a probability weighting on Fin t → α. For positive K, each one-block extension of a prefix has mass at most the previous prefix's mass divided by K. The definition multiplies by K instead of dividing by the previous mass, so it includes prefixes of mass zero and does not need a positivity convention for conditioning. The threshold K = 0 is allowed and imposes no additional restriction.

def Algebraic.Cutwidth.Extractor.blockPrefix {α : Type u_1} {i t : ℕ} (h : i ≤ t) (x : Fin t → α) : Fin i → α

Restrict a block tuple to its first i coordinates.

Equations

• Algebraic.Cutwidth.Extractor.blockPrefix h x j = x (Fin.castLE h j)

noncomputable def Algebraic.Cutwidth.Extractor.blockPrefixWeight {α : Type u_1} [Fintype α] {i t : ℕ} (p : (Fin t → α) → ℝ) (h : i ≤ t) : (Fin i → α) → ℝ

The probability mass of each prefix, counting all of its extensions.

Equations

• Algebraic.Cutwidth.Extractor.blockPrefixWeight p h = Algebraic.Cutwidth.Extractor.mapWeight (Algebraic.Cutwidth.Extractor.blockPrefix h) p

def Algebraic.Cutwidth.Extractor.IsBlockSource {α : Type u_1} [Fintype α] {t : ℕ} (p : (Fin t → α) → ℝ) (K : ℕ) : Prop

A probability source satisfying the threshold-K mass inequality for every block and earlier prefix, without conditional division.

Equations

• One or more equations did not get rendered due to their size.