In the mathematics of coding theory, the Griesmer bound, named after James Hugo Griesmer, is a bound on the length of linear binary codes of dimension k and minimum distance d.
There is also a very similar version for non-binary codes.
Statement of the bound
For a binary linear code, the Griesmer bound is:

Proof
Let
denote the minimum length of a binary code of dimension k and distance d. Let C be such a code. We want to show that

Let G be a generator matrix of C. We can always suppose that the first row of G is of the form r = (1, ..., 1, 0, ..., 0) with weight d.

The matrix
generates a code
, which is called the residual code of
obviously has dimension
and length
has a distance
but we don't know it. Let
be such that
. There exists a vector
such that the concatenation
Then
On the other hand, also
since
and
is linear:
But

so this becomes
. By summing this with
we obtain
. But
so we get
As
is integral, we get
This implies

so that

By induction over k we will eventually get

Note that at any step the dimension decreases by 1 and the distance is halved, and we use the identity

for any integer a and positive integer k.
Bound for the general case
For a linear code over
, the Griesmer bound becomes:

The proof is similar to the binary case and so it is omitted.
See also
References
- J. H. Griesmer, "A bound for error-correcting codes," IBM Journal of Res. and Dev., vol. 4, no. 5, pp. 532-542, 1960.