Read-back: Erdos142.erdos_142_variants_lower

The statement

The declaration takes one explicit natural-number argument $k$ and one hypothesis $1 < k$, and asserts a little-o relation between two functions $\mathbb{N} \to \mathbb{R}$, taken along the filter $\text{atTop}$ on $\mathbb{N}$ (i.e. "as the natural number $N$ tends to infinity"):

$$N \longmapsto r_k(N) \quad \text{is } o\!\left( N \longmapsto \frac{N}{\log N} \right) \qquad (N \to \infty),$$

where $r_k(N)$ is the natural number defined below, injected into $\mathbb{R}$, and $\frac{N}{\log N}$ means the real number $\frac{(N : \mathbb{R})}{\log (N : \mathbb{R})}$ with $\log$ the natural logarithm on $\mathbb{R}$.

Unfolded, the little-o relation is exactly the following quantifier structure:

$$\forall\, c \in \mathbb{R},\ c > 0 \ \Longrightarrow\ \exists\, N_0 \in \mathbb{N},\ \forall\, N \ge N_0 : \quad \bigl\| r_k(N) \bigr\| \ \le\ c \cdot \left\| \frac{N}{\log N} \right\|.$$

Note the order of quantifiers: the threshold $N_0$ is chosen after $c$, and the bound is non-strict ($\le$), with $c$ ranging over all strictly positive reals. Both sides are absolute values (norms) of reals; the left side equals $r_k(N)$ since it is a natural number, and the right side equals $\left|\frac{N}{\log N}\right|$.

The hypothesis $1 < k$ is the only constraint on $k$; $k$ is otherwise arbitrary, and the claim is asserted for each such fixed $k$ separately (there is no uniformity in $k$).

What $r_k(N)$ means (expanded from the bundle)

For natural numbers $k$ and $N$,

$$r_k(N) \ :=\ \sup\ \bigl\{\, |S| \ :\ S \text{ a finite subset of } \mathbb{N},\ S \subseteq \{1, 2, \dots, N\},\ \text{$S$ is "AP-of-length-$k$-free"} \,\bigr\},$$

where the supremum is the supremum of a set of natural numbers, and $\{1,\dots,N\}$ is the integer interval $[1, N]$ (empty when $N = 0$).

Junk-value convention for this supremum: the supremum is taken in $\mathbb{N}$, where by convention the supremum of an empty set, or of a set unbounded above, is $0$. Here neither degenerate case arises: the empty set $S = \emptyset$ always qualifies (it is AP-free, and $\emptyset \subseteq \{1,\dots,N\}$), so the set of admissible cardinalities contains $0$ and is nonempty; and every admissible $|S|$ is at most $N$. So $r_k(N)$ is an attained maximum, and $r_k(0) = 0$.

"AP-of-length-$l$-free" (IsAPOfLengthFree)

For a set $s$ in an additive commutative monoid $\alpha$ and $l \in \mathbb{N} \cup \{\infty\}$ (the type $\mathbb{N}^\infty$), the predicate reads literally:

$$\forall\, t \subseteq s : \quad \bigl(\text{$t$ is an arithmetic progression of length $l$}\bigr) \ \Longrightarrow\ l \le 1 .$$

The conclusion $l \le 1$ does not mention $t$; it is a statement about the fixed parameter $l$ only. So the predicate is logically equivalent to

$$\bigl(\exists\, t \subseteq s \text{ that is an arithmetic progression of length } l\bigr) \ \Longrightarrow\ l \le 1 .$$

In the theorem, $l$ is the natural number $k$ coerced into $\mathbb{N}^\infty$, and the hypothesis $1 < k$ makes the conclusion $k \le 1$ false; hence for the values of $k$ covered by the theorem the predicate says: no subset $t \subseteq s$ is an arithmetic progression of length $k$. (For $k \le 1$ the predicate would hold vacuously-by-conclusion for every $s$, but those $k$ are excluded by the hypothesis.)

"Arithmetic progression of length $l$" (IsAPOfLength / IsAPOfLengthWith)

A set $t \subseteq \alpha$ is an arithmetic progression of length $l \in \mathbb{N}^\infty$ if there exist $a, d \in \alpha$ such that both:

1. the cardinality of $t$, computed in $\mathbb{N}^\infty$ (a genuine natural number if $t$ is finite, and $\infty$ if $t$ is infinite), equals $l$:

$$\#\,t \ =\ l \quad \text{in } \mathbb{N} \cup \{\infty\};$$

2. $t$ is exactly the image set

$$t \ =\ \{\, a + n\cdot d \ :\ n \in \mathbb{N},\ n < l \,\},$$

where $n < l$ compares the natural number $n$ with $l$ inside $\mathbb{N}^\infty$, and $n \cdot d$ is the $n$-fold monoid multiple of $d$.

Both conditions are required simultaneously. In particular condition 1 is what rules out degenerate progressions: with $l = k$ and $k > 1$, the choice $d = 0$ would make the set in condition 2 equal to the singleton $\{a\}$, whose cardinality is $1 \ne k$; so $d = 0$ is automatically excluded, and more generally the $k$ listed terms $a, a+d, \dots, a+(k-1)d$ must be pairwise distinct. There is no separate hypothesis "$d > 0$" in the definition — non-degeneracy is carried entirely by the cardinality equation in $\mathbb{N}^\infty$.

In the application inside $r_k(N)$, the ambient monoid is $\alpha = \mathbb{N}$, so $a$ and $d$ are natural numbers and $n \cdot d = nd$; the set $s$ is the finite set $S$ viewed as a set of naturals, and $t$ ranges over arbitrary subsets of $\mathbb{N}$ contained in $S$.

Putting it together, for $k > 1$: $r_k(N)$ is the largest cardinality of a subset $S \subseteq \{1,\dots,N\}$ such that there are no $a, d \in \mathbb{N}$ for which $\{a, a+d, \dots, a+(k-1)d\}$ has exactly $k$ elements and is contained in $S$.

Junk values in the comparison function

The comparison function is $N \mapsto \dfrac{(N:\mathbb{R})}{\log (N:\mathbb{R})}$, using real division, which is total: division by $0$ yields $0$.

• At $N = 0$: $\log 0 = 0$ by the real-logarithm convention, so the value is $0/0 = 0$.
• At $N = 1$: $\log 1 = 0$, so the value is $1/0 = 0$.
• For $N \ge 2$: $\log N > 0$ and the value is the usual positive quantity $N/\log N$.

Because the little-o relation is taken along $\text{atTop}$, the bound is only required for all sufficiently large $N$, so the two degenerate points $N = 0, 1$ (where the right-hand side is $0$ while $r_k(1) = 1$) place no constraint on the statement.

Items defined in the bundle but not used by this statement

The bundle also defines the elementary predicates

$$\mathrm{HasAP}(k, A) \ :\Longleftrightarrow\ \exists\, a, d \in \mathbb{N},\ d > 0 \ \wedge\ \forall\, i < k,\ a + i d \in A, \qquad \mathrm{APFree}(k, A) \ :\Longleftrightarrow\ \neg\,\mathrm{HasAP}(k, A),$$

for a finite set $A \subseteq \mathbb{N}$, and proves three auxiliary facts: that the empty set is AP-of-length-$k$-free for every $k$; that every AP-free $S \subseteq \{1,\dots,N\}$ satisfies $|S| \le r_k(N)$; and that $r_k(N) \le N$. Neither $\mathrm{HasAP}$ nor $\mathrm{APFree}$ appears in the definition of $r_k(N)$ or in the theorem statement; the theorem's notion of progression-freeness is the $\mathbb{N}^\infty$-cardinality one described above.

Summary of the literal claim

For every natural number $k$ with $k \ge 2$: for every real $c > 0$ there exists a threshold $N_0$ such that for every natural number $N \ge N_0$, the maximum size of a subset of $\{1,\dots,N\}$ containing no $k$-element arithmetic progression is at most $c \cdot \dfrac{N}{\log N}$. Equivalently, $r_k(N)\big/\bigl(N/\log N\bigr) \to 0$ as $N \to \infty$.