Add Erdos 5 #238
Add Erdos 5 #238
Conversation
| such that the limit of $(p_{n_{i+1}} - p_{n_i}) / log n_i$ equals $x$, | ||
| where $p_k$ denotes the k-th prime number. | ||
|
|
||
| Note: the condition `n 0 ≥ 2` ensures the logarithm is defined for all indices |
There was a problem hiding this comment.
I think this condition is not quite needed because log takes the junk value 0 for the remaining indices, and StrictMono will only allow log (n 0) and log (n 1) to take junk values. So these should not affect the final asymptotic assertion -- although I guess it can't hurt to leave it in
There was a problem hiding this comment.
Looking through the sources, it also looks like some of the more modern statements of this problem equivalently use
|
Thanks for the contrib! Would you be able to add some of the additional solved results on the webpage as variants as well, or add a TODO? |
| @[category research open, AMS 11] | ||
| theorem erdos_5.finite_case (x : ℝ) (hx : 0 ≤ x) : | ||
| ∃ n : ℕ → ℕ, StrictMono n ∧ n 0 ≥ 2 ∧ | ||
| Tendsto (fun i ↦ ((n (i+1)).nth Prime - (n i).nth Prime : ℝ) / log (n i)) atTop (𝓝 x) := by |
There was a problem hiding this comment.
nit: the cast to real can be removed here and in infinite_case, this will be inferred from Real.log in the denom
There was a problem hiding this comment.
Yes, I see that! Thank you!
smmercuri
added
the
Awaiting author
Co-authored-by: Calle Sönne <[email protected]>
| @[category research solved, AMS 11] | ||
| theorem infinite_case : | ||
| ∃ p : ℕ → ℕ, StrictMono p ∧ (∀ n : ℕ, (p n).Prime) ∧ | ||
| Tendsto (fun i ↦ (p (i+1) - p i) / log (p i)) atTop atTop := by |
There was a problem hiding this comment.
Given the comment above this should be modified so that only successive prime differences are considered
|
@Reklle it seems like some of the comments are already adresses, could you resolve those? |
|
@mo271, done! Sorry for the long delay |
| ∃ p : ℕ → ℕ, StrictMono p ∧ (∀ n : ℕ, (p n).Prime) ∧ | ||
| Tendsto (fun i ↦ (p (i+1) - p i) / log (p i)) atTop atTop := by |
There was a problem hiding this comment.
This is still not correct, you need to also introduce the sequence n_i. The function p you have introduced is analogous to p(i) = p_{n_i} in the problem, so p(i+1) = p_{n_{i+1}} and not p_{n_i + 1}. I would introduce the sequence n and use Nat.nth Prime as you had before.
4 participants
closes #188
I don't know how correct it is, but I decided not to introduce a separate function.