Skip to content

Erdős problem 950

This function was considered by de Bruijn, Erdős, and Turán, who showed that ∑n<xf(n)∼∑n<xf(n)2∼x\sum_{n<x}f(n)\sim \sum_{n<x}f(n)^2\sim x. They gave no proofs, but a proof of the (harder) second claim is given by Gorodetsky here [mathoverflow/508491].

Sources

Browse retained paths and inspect the exact material available for this Problem.

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

950.lean

Retained formal statement4 of 7

This function was considered by de Bruijn, Erdős, and Turán, who showed that ∑n<xf(n)∼∑n<xf(n)2∼x\sum_{n<x}f(n)\sim \sum_{n<x}f(n)^2\sim x. They gave no proofs, but a proof of the (harder) second claim is given by Gorodetsky here [mathoverflow/508491].

FormalConjectures/ErdosProblems/950.leanErdos950.erdos_950.variants.debruijn_erdos_turan2 linesExact file
(Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.range x, Erdos950.f n) fun x => ↑x) ∧  Asymptotics.IsEquivalent Filter.atTop (fun x => ∑ n ∈ Finset.range x, Erdos950.f n ^ 2) fun x => ↑x
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page