Conjectures associated with A087719

Define $\varsigma(n)$ the smallest prime factor of $n$ (Nat.minFac). Let $a_n$ be the least number such that the count of numbers $k \le a_n$ with $k > \varsigma(k)^n$ exceeds the count of numbers with $k \le \varsigma(k)^n$.

The conjecture states that $a_n = 3^n + 3 \cdot 2^n + 6$ for $n \ge 1$.

References: A087719

def OeisA87719.countExceeding (n m : ℕ) : ℕ

Count of numbers k in {1, ..., m} where k > (minFac k)^n.

Equations

• OeisA87719.countExceeding n m = {k ∈ Finset.Icc 1 m | k > k.minFac ^ n}.card

def OeisA87719.countNotExceeding (n m : ℕ) : ℕ

Count of numbers k in {1, ..., m} where k ≤ (minFac k)^n.

Equations

• OeisA87719.countNotExceeding n m = {k ∈ Finset.Icc 1 m | k ≤ k.minFac ^ n}.card

theorem OeisA87719.a_exists (n : ℕ) : ∃ (m : ℕ), countExceeding n m > countNotExceeding n m

There exists m such that countExceeding n m > countNotExceeding n m.

noncomputable def OeisA87719.a (n : ℕ) : ℕ

The sequence a(n): least m such that countExceeding n m > countNotExceeding n m.

Equations

• OeisA87719.a n = Nat.find ⋯

theorem OeisA87719.a_one : a 1 = 15

a(1) = 15.

theorem OeisA87719.a_two : a 2 = 27

a(2) = 27.

theorem OeisA87719.a_three : a 3 = 57

a(3) = 57.

theorem OeisA87719.a_formula {n : ℕ} (hn : n ≥ 1) : a n = 3 ^ n + 3 * 2 ^ n + 6

Conjecture: a(n) = 3^n + 3 * 2^n + 6 for n ≥ 1.