Erdős Problem 269

Reference: erdosproblems.com/269

def Erdos269.HasPrimeFactorsIn (P : Set ℕ) (n : ℕ) : Prop

A positive integer $n$ has all its prime factors in the set $P$. By convention, $1$ satisfies this for any $P$ as it has no prime divisors.

Equations

• Erdos269.HasPrimeFactorsIn P n = (n > 0 ∧ ∀ (p : ℕ), Nat.Prime p → p ∣ n → p ∈ P)

noncomputable def Erdos269.a (P : Set ℕ) : ℕ → ℕ

The infinite, strictly increasing sequence $\{a_0, a_1, \dots\}$ of integers whose prime factors all belong to P.

Equations

• Erdos269.a P = Nat.nth (Erdos269.HasPrimeFactorsIn P)

noncomputable def Erdos269.partialLcm (P : Set ℕ) (n : ℕ) : ℕ

The n-th partial least common multiple, $[a_0, \dots, a_n]$, which is the LCM of the first n integers in the sequence.

Equations

• Erdos269.partialLcm P n = (Finset.range n).lcm (Erdos269.a P)

noncomputable def Erdos269.series (P : Set ℕ) : ℝ

The sum $\sum_{n=1}^\infty \frac{1}{[a_0,\ldots,a_{n - 1}]}$.

Equations

• Erdos269.series P = ∑' (n : ℕ), 1 / ↑(Erdos269.partialLcm P n)

theorem Erdos269.erdos_269.variants.rational : (∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → P.card ≥ 2 → ∃ (q : ℚ), ↑q = series ↑P) ↔ sorry

Let $P$ be a finite set of primes with $|P| \ge 2$ and let $\{a_1 < a_2 < \dots\}$ be the set of positive integers whose prime factors are all in $P$. Is the sum $$ \sum_{n=1}^\infty \frac{1}{[a_1,\ldots,a_n]} $$ rational?

theorem Erdos269.erdos_269.variants.irrational : (∀ (P : Finset ℕ), (∀ p ∈ P, Nat.Prime p) → P.card ≥ 2 → Irrational (series ↑P)) ↔ sorry

Let $P$ be a finite set of primes with $|P| \ge 2$ and let $\{a_1 < a_2 < \dots\}$ be the set of positive integers whose prime factors are all in $P$. Is the sum $$ \sum_{n=1}^\infty \frac{1}{[a_1,\ldots,a_n]} $$ irrational?

theorem Erdos269.erdos_269.variant.infinite (P : Set ℕ) (h : ∀ p ∈ P, Nat.Prime p) (h_inf : P.Infinite) : Irrational (series P)

This theorem addresses the case where the set of primes P is infinite. In this case the sum is irrational.