Irregular primes and Bernoulli numbers (extension)

This file proves a variant of the main result with an explicit constant: the count of odd primes p ≤ X that are not M_α(p)-regular is bounded by 10 · X / (log X)^(2α).

def LeanPool.PartialRegularity.Extension.isMRegular (m p : ℕ) : Prop

A prime p is m-regular if it has no Bernoulli numerator divisor in range.

Equations

• LeanPool.PartialRegularity.Extension.isMRegular m p = (Nat.Prime p ∧ Odd p ∧ ∀ (k : ℕ), 1 ≤ k → 2 * k ≤ min m (p - 3) → ¬↑p ∣ (bernoulli (2 * k)).num)

noncomputable def LeanPool.PartialRegularity.Extension.MAlpha (α : ℝ) (p : ℕ) : ℕ

The cutoff M_α(p) = ⌊sqrt p / (log p)^α⌋.

Equations

• LeanPool.PartialRegularity.Extension.MAlpha α p = ⌊√↑p / Real.log ↑p ^ α⌋₊

noncomputable def LeanPool.PartialRegularity.Extension.irregularPrimesUpTo (α : ℝ) (X : ℕ) : Set ℕ

The set of irregular primes up to X for the cutoff M_α.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.PartialRegularity.Extension.KMaxSup (α : ℝ) (X : ℕ) : ℕ

A uniform upper bound for the relevant M_α(p) values with p ≤ X.

Equations

• LeanPool.PartialRegularity.Extension.KMaxSup α X = {p ∈ Finset.range (X + 1) | Nat.Prime p}.sup (LeanPool.PartialRegularity.Extension.MAlpha α) + 1

noncomputable def LeanPool.PartialRegularity.Extension.AK (α : ℝ) (X k : ℕ) : Set ℕ

Primes counted at a fixed Bernoulli index k in the double-counting argument.

Equations

• LeanPool.PartialRegularity.Extension.AK α X k = {p : ℕ | p ≤ X ∧ Nat.Prime p ∧ Odd p ∧ 2 * k ≤ LeanPool.PartialRegularity.Extension.MAlpha α p ∧ ↑p ∣ (bernoulli (2 * k)).num}

noncomputable def LeanPool.PartialRegularity.Extension.bernoulliOmegaConst : ℝ

The explicit constant used for the Bernoulli-factor counting bound.

Equations

• LeanPool.PartialRegularity.Extension.bernoulliOmegaConst = 10

theorem LeanPool.PartialRegularity.Extension.bernoulliOmegaConst_pos : bernoulliOmegaConst > 0

theorem LeanPool.PartialRegularity.Extension.M_alpha_lt_K_max_sup (α : ℝ) (X p : ℕ) (hp : Nat.Prime p) (hpX : p ≤ X) : MAlpha α p < KMaxSup α X

theorem LeanPool.PartialRegularity.Extension.irregularPrimes_subset_union (α : ℝ) (X : ℕ) : irregularPrimesUpTo α X ⊆ ⋃ k ∈ Finset.range (KMaxSup α X), AK α X k

theorem LeanPool.PartialRegularity.Extension.A_k_zero_empty (α : ℝ) (X : ℕ) : AK α X 0 = ∅

theorem LeanPool.PartialRegularity.Extension.prime_int_dvd_natAbs (p : ℕ) (z : ℤ) (_hp : Nat.Prime p) (hdvd : ↑p ∣ z) : p ∣ z.natAbs

theorem LeanPool.PartialRegularity.Extension.bernoulli_two_mul_ne_zero (k : ℕ) (hk : k ≠ 0) : bernoulli (2 * k) ≠ 0

theorem LeanPool.PartialRegularity.Extension.bernoulli_num_natAbs_ne_zero (k : ℕ) (hk : 1 ≤ k) : (bernoulli (2 * k)).num.natAbs ≠ 0

theorem LeanPool.PartialRegularity.Extension.A_k_subset_primeFactors (α : ℝ) (X k : ℕ) (hk : 1 ≤ k) : AK α X k ⊆ ↑(bernoulli (2 * k)).num.natAbs.primeFactors

theorem LeanPool.PartialRegularity.Extension.card_A_k_bound (α : ℝ) (X k : ℕ) (hk : 1 ≤ k) : ↑(AK α X k).ncard ≤ ↑(ArithmeticFunction.cardDistinctFactors (bernoulli (2 * k)).num.natAbs)

theorem LeanPool.PartialRegularity.Extension.sorted_primes_get_ge (l : List ℕ) (hsort : l.SortedLT) (hge2 : ∀ x ∈ l, 2 ≤ x) (i : Fin l.length) : ↑i + 2 ≤ l.get i

theorem LeanPool.PartialRegularity.Extension.factorial_le_prod_primes (S : Finset ℕ) (hS : ∀ p ∈ S, Nat.Prime p) : (S.card + 1).factorial ≤ ∏ p ∈ S, p

theorem LeanPool.PartialRegularity.Extension.primeFactors_factorial_le_1 (n : ℕ) (hn : 0 < n) : (n.primeFactors.card + 1).factorial ≤ n

theorem LeanPool.PartialRegularity.Extension.rat_num_natAbs_le_of_abs_le_and_den_dvd {q : ℚ} {M D : ℕ} (hM : |↑q| ≤ ↑M) (hD : q.den ∣ D) (hpos : 0 < D) : q.num.natAbs ≤ M * D

theorem LeanPool.PartialRegularity.Extension.two_mul_factorial_sq_le_pow (k : ℕ) (hk : 1 ≤ k) : 2 * (2 * k + 1).factorial ^ 2 ≤ (2 * k + 1) ^ (4 * k + 3)

theorem LeanPool.PartialRegularity.Extension.factorial_prod_bound (k : ℕ) : (2 * k).factorial * (2 * k + 1).factorial ≤ (2 * k + 1).factorial ^ 2

theorem LeanPool.PartialRegularity.Extension.bernoulli_den_dvd_factorial_base : (bernoulli 2).den ∣ Nat.factorial 3

theorem LeanPool.PartialRegularity.Extension.gcd_mul_coprime_eq_gcd (n a d : ℕ) (hcop : a.Coprime d) : (n * a).gcd d = n.gcd d

theorem LeanPool.PartialRegularity.Extension.gcd_natAbs_mul_num_dvd_n (n : ℕ) (q : ℚ) : (↑n * q.num).natAbs.gcd q.den ∣ n

theorem LeanPool.PartialRegularity.Extension.rat_den_dvd_mul_of_int_mul (q : ℚ) (n : ℕ) (_hn : 0 < n) : q.den ∣ n * (↑n * q).den

theorem LeanPool.PartialRegularity.Extension.choose_two_k_plus_one_two_k (k : ℕ) : (2 * k + 1).choose (2 * k) = 2 * k + 1

theorem LeanPool.PartialRegularity.Extension.sum_bernoulli_eq_neg_mul (k : ℕ) (hk : 2 ≤ k) : ∑ j ∈ Finset.range (2 * k), ↑((2 * k + 1).choose j) * bernoulli j = -↑(2 * k + 1) * bernoulli (2 * k)

theorem LeanPool.PartialRegularity.Extension.den_sum_dvd_of_each_den_dvd {n : ℕ} {f : ℕ → ℚ} {D : ℕ} (_hD : 0 < D) (hf : ∀ j < n, (f j).den ∣ D) : (∑ j ∈ Finset.range n, f j).den ∣ D

theorem LeanPool.PartialRegularity.Extension.term_vanishes_for_odd_gt_one (k j : ℕ) (hj_odd : Odd j) (hj_gt : 1 < j) : ↑((2 * k + 1).choose j) * bernoulli j = 0

theorem LeanPool.PartialRegularity.Extension.term_j_zero_den_dvd (k : ℕ) (_hk : 2 ≤ k) : (↑((2 * k + 1).choose 0) * bernoulli 0).den ∣ (2 * k).factorial

theorem LeanPool.PartialRegularity.Extension.term_j_one_den_dvd (k : ℕ) (hk : 2 ≤ k) : (↑((2 * k + 1).choose 1) * bernoulli 1).den ∣ (2 * k).factorial

theorem LeanPool.PartialRegularity.Extension.term_even_den_dvd (k m : ℕ) (_hk : 2 ≤ k) (_hm_ge : 1 ≤ m) (hm_lt : m < k) (ih : (bernoulli (2 * m)).den ∣ (2 * m + 1).factorial) : (↑((2 * k + 1).choose (2 * m)) * bernoulli (2 * m)).den ∣ (2 * k).factorial

theorem LeanPool.PartialRegularity.Extension.each_term_den_dvd_factorial (k : ℕ) (hk : 2 ≤ k) (ih : ∀ (m : ℕ), 1 ≤ m → m < k → (bernoulli (2 * m)).den ∣ (2 * m + 1).factorial) (j : ℕ) (hj : j < 2 * k) : (↑((2 * k + 1).choose j) * bernoulli j).den ∣ (2 * k).factorial

theorem LeanPool.PartialRegularity.Extension.den_mul_factor_bernoulli_dvd_factorial (k : ℕ) (hk : 2 ≤ k) (ih : ∀ (m : ℕ), 1 ≤ m → m < k → (bernoulli (2 * m)).den ∣ (2 * m + 1).factorial) : (↑(2 * k + 1) * bernoulli (2 * k)).den ∣ (2 * k).factorial

theorem LeanPool.PartialRegularity.Extension.bernoulli_den_dvd_factorial_step (k : ℕ) (hk : 2 ≤ k) (ih : ∀ (m : ℕ), 1 ≤ m → m < k → (bernoulli (2 * m)).den ∣ (2 * m + 1).factorial) : (bernoulli (2 * k)).den ∣ (2 * k + 1).factorial

theorem LeanPool.PartialRegularity.Extension.bernoulli_den_dvd_factorial (k : ℕ) (hk : 1 ≤ k) : (bernoulli (2 * k)).den ∣ (2 * k + 1).factorial

theorem LeanPool.PartialRegularity.Extension.pi_sq_div_six_lt_two : Real.pi ^ 2 / 6 < 2

theorem LeanPool.PartialRegularity.Extension.tsum_inv_pow_two_mul_le (k : ℕ) (hk : 1 ≤ k) : ∑' (n : ℕ), 1 / ↑n ^ (2 * k) ≤ Real.pi ^ 2 / 6

theorem LeanPool.PartialRegularity.Extension.denom_ge_one (k : ℕ) (_hk : 1 ≤ k) : 1 ≤ 2 ^ (2 * k - 1) * Real.pi ^ (2 * k)

theorem LeanPool.PartialRegularity.Extension.bernoulli_eq_zeta_formula (k : ℕ) (hk : 1 ≤ k) : ↑(bernoulli (2 * k)) = ((-1) ^ (k + 1) * ↑(2 * k).factorial * ∑' (n : ℕ), 1 / ↑n ^ (2 * k)) / (2 ^ (2 * k - 1) * Real.pi ^ (2 * k))

theorem LeanPool.PartialRegularity.Extension.bernoulli_abs_le_formula (k : ℕ) (hk : 1 ≤ k) : |↑(bernoulli (2 * k))| ≤ ↑(2 * k).factorial * (Real.pi ^ 2 / 6) / (2 ^ (2 * k - 1) * Real.pi ^ (2 * k))

theorem LeanPool.PartialRegularity.Extension.formula_le_two_mul_factorial (k : ℕ) (hk : 1 ≤ k) : ↑(2 * k).factorial * (Real.pi ^ 2 / 6) / (2 ^ (2 * k - 1) * Real.pi ^ (2 * k)) ≤ 2 * ↑(2 * k).factorial

theorem LeanPool.PartialRegularity.Extension.bernoulli_abs_le_two_mul_factorial (k : ℕ) (hk : 1 ≤ k) : |↑(bernoulli (2 * k))| ≤ 2 * ↑(2 * k).factorial

theorem LeanPool.PartialRegularity.Extension.bernoulli_num_natAbs_le (k : ℕ) (hk : 1 ≤ k) : (bernoulli (2 * k)).num.natAbs ≤ (2 * k + 1) ^ (4 * k + 3)

theorem LeanPool.PartialRegularity.Extension.bernoulli_two_mul_ne_zero_1 (k : ℕ) (hk : 1 ≤ k) : bernoulli (2 * k) ≠ 0

theorem LeanPool.PartialRegularity.Extension.bernoulli_num_natAbs_pos (k : ℕ) (hk : 1 ≤ k) : 0 < (bernoulli (2 * k)).num.natAbs

theorem LeanPool.PartialRegularity.Extension.descFactorial_le_factorial (n k : ℕ) (hkn : k ≤ n) : n.descFactorial k ≤ n.factorial

theorem LeanPool.PartialRegularity.Extension.two_k_add_one_le_ten_k_sub (k i : ℕ) (hi : i ∈ Finset.range (8 * k)) : 2 * k + 1 ≤ 10 * k - i

theorem LeanPool.PartialRegularity.Extension.factorial_ten_k_ge_power (k : ℕ) (hk : 1 ≤ k) : (2 * k + 1) ^ (8 * k) ≤ (10 * k).factorial

theorem LeanPool.PartialRegularity.Extension.omega_bernoulli_bound (k : ℕ) (hk : 1 ≤ k) : ↑(ArithmeticFunction.cardDistinctFactors (bernoulli (2 * k)).num.natAbs) ≤ bernoulliOmegaConst * ↑k

theorem LeanPool.PartialRegularity.Extension.sq_add_one_le_two_sq (A : ℝ) (hA : A ≥ 1 + √2) : (A + 1) ^ 2 ≤ 2 * A ^ 2

theorem LeanPool.PartialRegularity.Extension.tendsto_sqrt_div_log_pow_atTop (α : ℝ) (_hα : 0 < α) : Filter.Tendsto (fun (x : ℝ) => √x / Real.log x ^ α) Filter.atTop Filter.atTop

theorem LeanPool.PartialRegularity.Extension.eventually_sqrt_div_log_ge_threshold (α : ℝ) (hα : 0 < α) : ∀ᶠ (X : ℕ) in Filter.atTop, √↑X / Real.log ↑X ^ α ≥ 1 + √2

theorem LeanPool.PartialRegularity.Extension.rpow_div_log_monotoneOn (α : ℝ) (hα : 0 < α) : MonotoneOn (fun (x : ℝ) => x ^ (1 / (2 * α)) / Real.log x) {x : ℝ | Real.exp (2 * α) ≤ x}

theorem LeanPool.PartialRegularity.Extension.rpow_div_log_pow_eq_sqrt_div_log_pow (α : ℝ) (hα : 0 < α) (x : ℝ) (hx : 0 < x) (hlogx_pos : 0 < Real.log x) : (x ^ (1 / (2 * α)) / Real.log x) ^ α = √x / Real.log x ^ α

theorem LeanPool.PartialRegularity.Extension.sqrt_div_log_monotoneOn (α : ℝ) (hα : 0 < α) : MonotoneOn (fun (x : ℝ) => √x / Real.log x ^ α) {x : ℝ | Real.exp (2 * α) ≤ x}

theorem LeanPool.PartialRegularity.Extension.sqrt_div_log_le_of_le_of_large (α : ℝ) (hα : 0 < α) (p X : ℕ) (hp_large : Real.exp (2 * α) ≤ ↑p) (hpX : p ≤ X) : √↑p / Real.log ↑p ^ α ≤ √↑X / Real.log ↑X ^ α

theorem LeanPool.PartialRegularity.Extension.eventually_sqrt_div_log_ge (α : ℝ) (hα : 0 < α) (M : ℝ) : ∀ᶠ (X : ℕ) in Filter.atTop, M ≤ √↑X / Real.log ↑X ^ α

theorem LeanPool.PartialRegularity.Extension.small_values_bounded (α : ℝ) (T : ℕ) : ∃ (C : ℝ), ∀ p < T, √↑p / Real.log ↑p ^ α ≤ C

theorem LeanPool.PartialRegularity.Extension.sqrt_div_log_eventually_le (α : ℝ) (hα : 0 < α) : ∀ᶠ (X : ℕ) in Filter.atTop, ∀ p ≤ X, √↑p / Real.log ↑p ^ α ≤ √↑X / Real.log ↑X ^ α

theorem LeanPool.PartialRegularity.Extension.K_max_sup_le_sqrt_div_log_add_one (α : ℝ) (hα : 0 < α) : ∀ᶠ (X : ℕ) in Filter.atTop, ↑(KMaxSup α X) ≤ √↑X / Real.log ↑X ^ α + 1

theorem LeanPool.PartialRegularity.Extension.two_sq_eq (α : ℝ) (X : ℕ) (hX : 1 < ↑X) : 2 * (√↑X / Real.log ↑X ^ α) ^ 2 = 2 * ↑X / Real.log ↑X ^ (2 * α)

theorem LeanPool.PartialRegularity.Extension.K_max_sup_sq_bound (α : ℝ) (hα : 0 < α) : ∀ᶠ (X : ℕ) in Filter.atTop, ↑(KMaxSup α X) ^ 2 ≤ 2 * ↑X / Real.log ↑X ^ (2 * α)

theorem LeanPool.PartialRegularity.Extension.sum_range_le_sq (K : ℕ) : ∑ k ∈ Finset.range K, ↑k ≤ ↑K ^ 2 / 2

theorem LeanPool.PartialRegularity.Extension.irregularPrimes_ncard_le_sum (α : ℝ) (X : ℕ) : ↑(irregularPrimesUpTo α X).ncard ≤ ∑ k ∈ Finset.range (KMaxSup α X), ↑(AK α X k).ncard

theorem LeanPool.PartialRegularity.Extension.irregularPrimes_isBigO (α : ℝ) (hα : 1 / 2 < α) : (fun (X : ℕ) => ↑(irregularPrimesUpTo α X).ncard) =O[Filter.atTop] fun (X : ℕ) => ↑X / Real.log ↑X ^ (2 * α)