Olson's Lemma 3.1: some translate $B+a_v$ meets $\bar B$ in $\ge \min\{\frac12(k+1),\frac14(w+2)\}$ points

Let $G$ be an abelian group and let $B\subseteq G$ be non-empty and proper, with either $B$ or its complement $\bar B$ finite. Put

Let $a_1,\dots,a_w$ be $w$ distinct non-zero elements of $G$ and suppose the subgroup $H=\langle a_1,\dots,a_w\rangle$ they generate has $|H|\ge 2k$. Then

for at least one index $1\le v\le w$.

This is the averaging step of Olson's paper: it says that among $w$ prescribed non-zero elements, some translate of $B$ must stick out of $B$ by a definite amount. It is what makes the induction of Theorem 3.1 gain roughly $s/4$ new subset sums at each step, and it is proved in the paper's §4 from Theorem 2.2 by subadditivity of $\lambda(g)=|(B+g)\cap\bar B|$.

Formalisation notes.

$B$ is a Set G rather than a Finset G because Olson explicitly allows $B$ to be infinite with finite complement. The number $k$ is pinned down by (k : ℕ∞) = min B.encard Bᶜ.encard; working in ℕ∞ is what makes $\min\{|B|,|\bar B|\}$ mean what Olson means, since an infinite side is $\top$ and the minimum is then the finite side.

The hypothesis hfin : B.Finite ∨ Bᶜ.Finite is the source's "either $B$ or $\bar B$ is finite". It is logically redundant — if both sides were infinite the minimum would be $\top$, which is not the image of any natural number, so hk would already be unsatisfiable — but it is kept because the source states it.

The size condition on $H$ is also compared in ℕ∞, so the Remark that follows the lemma in the paper ("the subgroup $H$ may be infinite, in which case the condition $|H|\ge2k$ is satisfied") is covered with no case split.

The elements $a_1,\dots,a_w$ are carried by a Finset G, which supplies their distinctness for free; $w$ is T.card and hT0 is the non-zeroness. The translate $B+a_v$ is written as the image of $x\mapsto x+v$, and $|(B+a_v)\cap\bar B|$ as Set.ncard — the intersection is finite whichever of $B,\bar B$ is, so ncard is the honest count.

Olson states the lemma for an arbitrary (possibly non-abelian) group. This card is the abelian case, which is the one this mission consumes; in the abelian case left and right translates agree, so nothing else changes.