Erdos 1072 #1135
Erdos 1072 #1135
Conversation
| namespace Erdos1072 | ||
|
|
||
| /-- For any prime $p$, let $f(p)$ be the least integer such that $f(p)! + 1 \equiv 0 \mod p$.-/ | ||
| noncomputable def f (p : ℕ) : ℕ := sInf {n | (n)! + 1 ≡ 0 [MOD p]} |
There was a problem hiding this comment.
Are the brackets around the n really needed here?
There was a problem hiding this comment.
Either brackets or a space between n and !. I tend to find brackets easier to read than the space.
| (∃ (P : Finset ℕ), (∀ p ∈ P, p.Prime) ∧ | ||
| ∀ᵉ ε > (0 : ℝ), ∃ N₀, ∀ p ≥ N₀, p.Prime ∧ p ∉ P → f p / p < ε) | ||
| ↔ answer(sorry) := by |
There was a problem hiding this comment.
(not an expert in this sort of stuff). I feel like one could also read this statement in terms of the density of the set of primes that verify the property, which would then be a little weaker than the current version. Do you think this is worth including as a separate statement?
| -/ | ||
| @[category research open, AMS 11] | ||
| theorem erdos_1072a.variants.littleo : | ||
| (fun x ↦ (#({p | p.Prime ∧ f p = p - 1} ∩ Finset.range (x + 1)).toFinset : ℝ)) =o[atTop] |
There was a problem hiding this comment.
I'd be tempted to do this for consistency with some of the other formalisations.
| (fun x ↦ (#({p | p.Prime ∧ f p = p - 1} ∩ Finset.range (x + 1)).toFinset : ℝ)) =o[atTop] | |
| (fun x ↦ (({p | p.Prime ∧ f p = p - 1} ∩ Set.interIcc 0 x).ncard : ℝ)) =o[atTop] |
There was a problem hiding this comment.
Should that be {p | p.Prime ∧ f p = p - 1}.interIcc 0 x).ncard rather than ∩ Set.interIcc 0 x?
4 participants
Fixes #1112