Read-back: Erdos142.exists_density_limit

The statement

For every natural number $k$ satisfying $0 < k$, there exists a real number $c$ such that the sequence of real numbers

$$N \;\longmapsto\; \frac{r(k, N)}{N}, \qquad N \in \mathbb{N},$$

converges to $c$ as $N \to \infty$ (convergence along the "eventually large" filter on $\mathbb{N}$, towards the standard neighbourhood filter of $c$ in $\mathbb{R}$).

Here $k$ ranges over the natural numbers, $c$ is an unconstrained real number (no sign, size, or membership condition is imposed on it — in particular it is not required to lie in $[0,1]$), and $r(k,N)$ is the natural number defined in the accompanying bundle, coerced into $\mathbb{R}$, divided by the coercion of $N$ into $\mathbb{R}$. The assertion is purely the existence of a limit; no value, no formula, no rate, and no monotonicity for the sequence is claimed, and the existential is a plain $\exists$, not a uniqueness statement.

Expansion of the quantity $r(k,N)$

$r(k,N)$ is not a standard imported notion; it is defined in the bundle as a supremum of a set of natural numbers:

$$r(k,N) \;=\; \sup\;\bigl\{\, |S| \;\bigm|\; S \subseteq \{1,\dots,N\} \text{ a finite set of naturals, and } S \text{ is "AP-of-length-}k\text{ free"} \,\bigr\},$$

where:

• $S$ ranges over finite subsets of $\mathbb{N}$ with $S \subseteq \{1, 2, \dots, N\}$ (the integer interval from $1$ to $N$ inclusive, which is empty when $N = 0$), and $|S|$ is its cardinality;
• the length parameter is the natural number $k$ regarded as an element of $\mathbb{N} \cup \{\infty\}$;
• the supremum is the order-theoretic supremum inside $\mathbb{N}$. This is a total operation with a junk value: the supremum of the empty set, or of a set unbounded above, is $0$. (For this particular set neither degeneracy occurs: the empty set $S = \emptyset$ always qualifies, contributing the value $0$, and every candidate value is bounded by $N$; the bundle records this as $r(k,N) \le N$.)

Expansion of "AP-of-length-$k$ free"

The freeness predicate applied to $S$ (viewed as a set of naturals) unfolds, in the bundle, to:

for every subset $t \subseteq S$, if $t$ is an arithmetic progression of length $k$, then $k \le 1$.

Note the exact shape: the conclusion of the implication is a statement about the length parameter $k$ alone, not about $t$. Consequently, when $k \le 1$ the predicate is satisfied by every set $S$ vacuously (the conclusion $k \le 1$ is already true), and when $k \ge 2$ the predicate says exactly that no subset of $S$ is an arithmetic progression of length $k$. Since the theorem's hypothesis is $0 < k$, the case $k = 1$ is permitted and falls into the first, degenerate regime: there $r(1,N)$ is the supremum of $|S|$ over all $S \subseteq \{1,\dots,N\}$, i.e. $r(1,N) = N$.

"$t$ is an arithmetic progression of length $k$" itself unfolds to: there exist a first term $a \in \mathbb{N}$ and a common difference $d \in \mathbb{N}$ such that

$$\#t = k \quad\text{and}\quad t = \{\, a + n\cdot d \;\mid\; n \in \mathbb{N},\; n < k \,\},$$

where $\#t$ denotes the cardinality of $t$ as an element of $\mathbb{N} \cup \{\infty\}$, and $n \cdot d$ is the $n$-fold sum of $d$ (in $\mathbb{N}$, ordinary multiplication). Two things this literally requires: the set $t$ must be equal to the displayed set (not merely contain it), and its cardinality must be exactly $k$. The difference $d$ is allowed to be $0$ and no positivity is assumed of it; however, when $k \ge 2$ the value $d = 0$ makes the displayed set equal to $\{a\}$, of cardinality $1 \ne k$, so the cardinality clause rules it out. The subsets $t$ quantified over are arbitrary subsets of $S$ (all of them finite, since $S$ is).

The bundle also defines an elementary predicate — "there exist $a$ and $d > 0$ with $a + i\cdot d \in A$ for all $i < k$" — and its negation, but neither of these appears in the definition of $r$ nor anywhere in the theorem statement; they play no role in what is asserted here.

Degenerate and edge cases the statement silently includes

• $k = 0$ is excluded by the hypothesis $0 < k$; $k = 1$ is included, and in that case, as noted, the freeness condition is vacuous.
• Division by zero. The quotient is real division, which in this setting is a total function with $x/0 = 0$ by convention. The term at $N = 0$ is therefore $r(k,0)/0 = 0$, regardless of the numerator. (Here $\{1,\dots,0\}$ is empty, so $r(k,0) = 0$ as well.) Because the convergence is along the filter of large $N$, any finite set of initial terms — including this one — is irrelevant to the truth of the claim.
• Empty sets. $S = \emptyset$ is always an admissible competitor in the supremum defining $r$, and the bundle records that the empty set is free of arithmetic progressions of every length.
• The hypothesis $0 < k$ is satisfiable, so the statement is not vacuous on that account; it is a claim about every positive $k$.

Ambient conventions

The declaration lives in the namespace Erdos142. The definitions of arithmetic progressions in the bundle are stated for a general commutative additive monoid, but $r$, and hence this theorem, instantiate them at $\mathbb{N}$. The limit is taken in $\mathbb{R}$ with its usual topology; the index set is $\mathbb{N}$ with its order filter at infinity.