§8.4, p. 160 — the distance distribution sums to and is feasible for the Delsarte LP
ProvedMatousekLP.Codes.xtilde_feasiblecoding-theorylinear-programmingp2o-batch-b23bp2o-gran-per-chapterp2o-plan-bookp2o-v1
For every code , the quantities satisfy
and whenever is a nonempty code with distance , the vector is a feasible solution of the Delsarte linear program: , for , for , and for all .
This is the step that turns a code into a feasible solution of the linear program, from which the Delsarte bound follows.
Formalization Note The book's divides by and its claim presupposes ; the hypothesis C.Nonempty makes this explicit. The identity holds (trivially) for the empty code as well and is stated under the same hypothesis.
Preamble
import Mathlib import Definitions.Def_MatousekLP_Codes_Basic import Definitions.Def_MatousekLP_Codes_DelsarteLP open Finset
Formal statement
namespace MatousekLP.Codes
/-- §8.4, p. 160 ("Toward an explanation"): for every `C ⊆ {0,1}^n`,
`x̃_0(C) + ⋯ + x̃_n(C) = |C|`; and whenever `C` is a (nonempty) code with distance `d`, the
vector `(x̃_0(C), …, x̃_n(C))` is a feasible solution of the Delsarte linear program. -/
theorem xtilde_feasible {n d : ℕ} (C : Finset (Word n)) (hC : C.Nonempty)
(hd : HasDistance C d) :
delsarteObjective (fun i : Fin (n + 1) => xtilde C i) = (C.card : ℝ) ∧
IsDelsarteFeasible n d (fun i : Fin (n + 1) => xtilde C i) := by sorry
end MatousekLP.Codes
Source
Matoušek & Gärtner, Understanding and Using Linear Programming, Springer 2007, p. 160, §8.4 'Toward an explanation' (x̃_0 + ⋯ + x̃_n = |C|; the x̃_i are feasible for the LP of Theorem 8.4.3)
Human review
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.