Willans' formula for the n-th prime

The n-th prime is 1 + Σ_{i=1}^{2^n} ⌊(n / Σ_{j=1}^{i} ⌊cos² (π ((j - 1)! + 1) / j)⌋)^{1/n}⌋ (Willans, 1964). By Wilson's theorem (Mathlib's Nat.prime_iff_fac_equiv_neg_one) the inner floor is 1 exactly when j = 1 or j is prime, so the inner sum is π(i) + 1; the outer floor is 1 when π(i) < n and 0 otherwise (bounding y^n < 2^n instead of n^{1/n}), and Bertrand's postulate gives p_n ≤ 2^n, so the outer sum counts 1 ≤ i < p_n.

Main results

• Willans.floor_cos_sq_eq: floor(cos^2(pi((j-1)!+1)/j)) is 1 iff j = 1 or j is prime (Wilson)
• Willans.nth_prime_eq: Willans' formula for the n-th prime

References

• C. P. Willans, On formulae for the nth prime number, Math. Gazette 48 (1964), 413–415.

theorem Willans.floor_cos_sq_eq (j : ℕ) (hj : 1 ≤ j) : ⌊Real.cos (Real.pi * (↑(j - 1).factorial + 1) / ↑j) ^ 2⌋ = if j = 1 ∨ Nat.Prime j then 1 else 0

Wilson floor. For j ≥ 1, ⌊cos²(π((j-1)!+1)/j)⌋ is 1 if j = 1 or j is prime, and 0 otherwise.

theorem Willans.sum_floor_eq (i : ℕ) (hi : 1 ≤ i) : ∑ j ∈ Finset.Icc 1 i, ↑⌊Real.cos (Real.pi * (↑(j - 1).factorial + 1) / ↑j) ^ 2⌋ = ↑(i.primeCounting + 1)

Step 2: the inner sum is π(i) + 1.

theorem Willans.floor_root_eq (n k : ℕ) (hn : 1 ≤ n) : ⌊(↑n / ↑(k + 1)) ^ (1 / ↑n)⌋ = if k < n then 1 else 0

Step 3: the n-th root floor is an indicator.

theorem Willans.nth_prime_le (k : ℕ) : Nat.nth Nat.Prime k ≤ 2 ^ (k + 1)

p_k ≤ 2^(k+1) for the k-th prime indexed from 0.

theorem Willans.nth_prime_eq (n : ℕ) (hn : 1 ≤ n) : ↑(Nat.nth Nat.Prime (n - 1)) = 1 + ∑ i ∈ Finset.Icc 1 (2 ^ n), ↑⌊(↑n / ∑ j ∈ Finset.Icc 1 i, ↑⌊Real.cos (Real.pi * (↑(j - 1).factorial + 1) / ↑j) ^ 2⌋) ^ (1 / ↑n)⌋

Willans' formula for the n-th prime.