The proof

Erdős problem 726

n\to \infty

ranges over integers

\sum_{p\leq n}1_{n\in (p/2,p)\pmod{p}}\frac{1}{p}\sim \frac{\log\log n}{2}

? A conjecture of Erdős, Graham, Ruzsa, and Straus [EGRS75]. By

n\in (p/2,p)\pmod{p}

we mean

n\equiv r\pmod{p}

for some integer

r

with

p/2<r<p

Back to the result The problem

Source

Main.lean · 24 lines · 1.3 kB

theorem target : ¬ (fcTypeOfName% "Erdos726.erdos_726") := by
  intro h
  have hiff := h.mp trivial
  have hmod : ∀ (n p : ℕ), (p : ℝ) ≠ 0 → (n : ℝ) % (p : ℝ) = 0 := fun n p hp0 => by
    rw [Field.mod_eq, mul_div_assoc, div_self hp0, mul_one, sub_self]
  have hzero : (fun n : ℕ ↦ ∑ p ∈ (Finset.range (n + 1)).filter
      (fun p : ℕ ↦ p.Prime ∧ (p : ℝ) / 2 < (n % p : ℝ)), (1 : ℝ) / (p : ℝ))
      = (fun _ : ℕ ↦ (0 : ℝ)) := by
    funext n
    rw [Finset.filter_false_of_mem, Finset.sum_empty]
    rintro p - ⟨hp, hlt⟩
    have hp0 : (p : ℝ) ≠ 0 := by exact_mod_cast hp.pos.ne'
    rw [hmod n p hp0] at hlt
    have hpp : (0 : ℝ) < (p : ℝ) := by exact_mod_cast hp.pos
    linarith
  rw [hzero] at hiff
  have h1 : Filter.Tendsto (fun n : ℕ ↦ Real.log (Real.log (n : ℝ)))
      Filter.atTop Filter.atTop :=
    Real.tendsto_log_atTop.comp (Real.tendsto_log_atTop.comp tendsto_natCast_atTop_atTop)
  have hg : Filter.Tendsto (fun n : ℕ ↦ Real.log (Real.log (n : ℝ)) / 2)
      Filter.atTop Filter.atTop := h1.atTop_div_const (by norm_num)
  have h0 : Filter.Tendsto (fun _ : ℕ ↦ (0 : ℝ)) Filter.atTop Filter.atTop :=
    hiff.symm.tendsto_atTop hg
  exact not_tendsto_atTop_of_tendsto_nhds tendsto_const_nhds h0

Provenance

Proof SHA-256: sha256:8accaa9a950aab97030b8114496cacf3256ca04e6186be6d7b2d32aadd32ccfe
Solver: 5FqLp5…FfZZiK
Attribution: conjectures.io