The dimension of the high-rate line code

The high-rate line code on K ^ ℓ is spanned by the monomials whose exponent matrices, with m columns of A possible values each, have a zero column. There are retainedDimension A m = A ^ m - (A - 1) ^ m of them (card_exists_eq_retainedDimension). By Bernoulli's inequality this is at least a P / (P + 1) fraction of all A ^ m matrices once m ≥ P * (A - 1) (retainedDimension_rate), so the rate of the code tends to one.

Main definitions

• Cslib.LineCode.HighRate.retainedDimension: the number A ^ m - (A - 1) ^ m.

Main results

• Cslib.LineCode.HighRate.card_exists_eq_retainedDimension: retainedDimension (card α) m words of length m over α contain a given letter.
• Cslib.LineCode.HighRate.retainedDimension_pos: the dimension is positive.
• Cslib.LineCode.HighRate.retainedDimension_rate: the denominator-free rate bound.

References

• Adapted from MassProduction/HighRate/Rate.lean and MassProduction/HighRate/DigitMonomials.lean in S. Schlesinger, Boolean circuit mass production formalization.

def Cslib.LineCode.HighRate.retainedDimension (A m : ℕ) : ℕ

The number A ^ m - (A - 1) ^ m of words of length m over an alphabet of A letters that contain a given letter.

theorem Cslib.LineCode.HighRate.card_exists_eq_retainedDimension (α : Type u_1) [Fintype α] [DecidableEq α] (a : α) (m : ℕ) : Fintype.card { w : Fin m → α // ∃ (j : Fin m), w j = a } = retainedDimension (Fintype.card α) m

Exactly retainedDimension (Fintype.card α) m words w : Fin m → α contain the letter a.

theorem Cslib.LineCode.HighRate.retainedDimension_pos {A m : ℕ} (hA : 0 < A) (hm : 0 < m) : 0 < retainedDimension A m

The dimension retainedDimension A m is positive when 0 < A and 0 < m.

theorem Cslib.LineCode.HighRate.retainedDimension_rate (A m P : ℕ) (hm : 0 < m) (hmP : P * (A - 1) ≤ m) : P * A ^ m ≤ (P + 1) * retainedDimension A m

Rate bound. If 0 < m and P * (A - 1) ≤ m, then retainedDimension A m is at least a P / (P + 1) fraction of A ^ m: P * A ^ m ≤ (P + 1) * retainedDimension A m.