theorem binom_eq {n k : ℕ} (hk : 1 ≤ k) : n.choose k * k = (n - 1).choose (k - 1) * n

$$\binom\{n\}\{k\} \cdot k = \binom\{n-1\}\{k-1\} \cdot n$$.

theorem binom_eq_2 {n k : ℕ} (hk : 2 ≤ k) : n.choose k * k * (k - 1) = (n - 2).choose (k - 2) * (n - 1) * n

$$\binom\{n\}\{k\} \cdot k \cdot (k-1) = \binom\{n-2\}\{k-2\} \cdot (n-1) \cdot n$$.

theorem lemma_1 {n k p a b : ℕ} (hk : 1 ≤ k) (hp : Nat.Prime p) (h1 : p ^ (a + b + 1) ∣ n) : p ^ (a + 1) ∣ n.choose k ∨ p ^ (b + 1) ∣ k

If $$p^\{a+b+1\} \mid n$$, then $$p^\{a+1\} \mid \binom\{n\}\{k\}$$ or $$p^\{b+1\} \mid k$$.

theorem lemma_2 {n k p r : ℕ} (hk : 2 ≤ k) (hn : k ≤ n) (hp : Nat.Prime p) (h1 : p ^ r ∣ n - 1) (hr : 0 < r) (h2 : ¬p ∣ k) (h3 : ¬p ∣ n - k) : p ^ r ∣ n.choose k

If $$p^r \mid n-1$$ and $$k,n-k$$ are not divisible by $$p$$, then $$p^r \mid \binom\{n\}\{k\}$$.

theorem key_prop {k n p r R : ℕ} (hn : n = 2 ^ (p ^ R).totient) (hk : 1 ≤ k) (hkn : k < n) (hp : Nat.Prime p) (hpr : p > 2 ^ (r - 1)) (hr : 1 < r) (hr' : r ≤ (p ^ R).totient) : 2 ^ r ∣ n.choose k ∨ p ^ R ∣ n.choose k

If $$n=2^\{\phi(p^R)\}$$ and $$p>2^\{r-1\}$$, then $$2^r \mid \binom\{n\}\{k\}$$ or $$p^R \mid \binom\{n\}\{k\}$$.

@[reducible, inline]

noncomputable abbrev S (n : ℕ) : ℕ

Equations

• S n = sSup {r : ℕ | ∀ k ∈ Finset.Ico 1 n, ∃ (p : ℕ), Nat.Prime p ∧ p ^ r ∣ n.choose k}

theorem S_ge {n r : ℕ} (hn : 1 < n) (h : ∀ k ∈ Finset.Ico 1 n, ∃ (p : ℕ), Nat.Prime p ∧ p ^ r ∣ n.choose k) : r ≤ S n

The condition 1<n is necessary to avoid the range of k being vacuous.

theorem key_cor {p r : ℕ} (hp : Nat.Prime p) (hpr : p > 2 ^ (r - 1)) (hr : 1 < r) : r ≤ S (2 ^ (p ^ r).totient)

If $$p\>2^\{r\-1\}$$, then $$S\(2^\{phi\(p^R\)\}\) ge r$$.

theorem erdos_379 : Filter.limsup (fun (n : ℕ) => ↑(S n)) Filter.atTop = ⊤

A positive resolution to Erdos problem #379.