Erdős Problem 1101

Reference: erdosproblems.com/1101

def Erdos1101.ASet (u : ℕ → ℕ) : Set ℕ

The set of integers not divisible by any u_i.

Equations

• Erdos1101.ASet u = {a : ℕ | ∀ (i : ℕ), ¬u i ∣ a}

noncomputable def Erdos1101.A (u : ℕ → ℕ) (n : ℕ) : ℕ

The sequence of integers A_u which are not divisible by any u_i arranged in a monotonic sequence.

Equations

• Erdos1101.A u n = Nat.nth (fun (a : ℕ) => a ∈ Erdos1101.ASet u) n

noncomputable def Erdos1101.t (u : ℕ → ℕ) (x : ℕ) : ℕ

t_x such that u_0 ... u_{t_x-1} ≤ x < u_0 ... u_{t_x}.

Equations

• Erdos1101.t u x = sSup {k : ℕ | ∏ i ∈ Finset.range k, u i ≤ x}

def Erdos1101.IsGood (u : ℕ → ℕ) : Prop

A sequence is "good" if

1. it is strictly monotone
2. it is pairwise coprime
3. the sum of reciprocals converges
4. the gap between consecutive elements in A(u) is bounded relative to t_x.

Equations

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

theorem Erdos1101.erdos_1101.polynomial : ¬∃ (u : ℕ → ℕ), IsGood u ∧ ∃ (k : ℕ), (fun (n : ℕ) => ↑(u n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ k

1. There is NO good sequence with polynomial growth.

theorem Erdos1101.erdos_1101.subexponential : ∃ (u : ℕ → ℕ), IsGood u ∧ (fun (n : ℕ) => Real.log ↑(u n)) =o[Filter.atTop] fun (n : ℕ) => ↑n

2. There is a good sequence with sub-exponential growth.