Divergence of the sum of the reciprocal of primes #1705
Conversation
Tragicus
force-pushed
the
divsuminvprim
branch
from
838f1ae to
aa4999e
Compare
classical/unstable.v
Outdated
| Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) := | ||
| {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}. | ||
|
|
||
| Lemma mono_ext f : {mono f : m n / (m <= n)%N} -> forall n, (n <= f n)%N. |
There was a problem hiding this comment.
There is maybe a better name for mono_ext.
The identifier does not show it is about natural numbers
or that the conclusion is leq; what does ext mean?
What about mono_leq?
There was a problem hiding this comment.
Oh, my bad, these functions are called "inflationary", not something like "extensive". I feel like mono_leq is too general. Maybe something like mono_leq_infl?
theories/showcase/pnt.v
Outdated
| [set n : 'I_N.+1 |all (fun p => p < prime_seq k) (primes n)]%SET. | ||
| Let G (k N : nat) := ~: P k N. | ||
|
|
||
| Fact cardPcardG k N : #|G k N| + #|P k N| = N.+1. |
There was a problem hiding this comment.
Fact cardPcardG -> Local Lemma cardPcardG or Let cardPcardG?
Since it does not appear in the changelog, I guess this is the intent.
theories/showcase/pnt.v
Outdated
| by rewrite -[X in _ + _ = X]card_ord addn0 -cardsT => ->. | ||
| Qed. | ||
|
|
||
| Fact cardG (R : realType) (k N : nat) : |
There was a problem hiding this comment.
Fact cardG -> Local Lemma cardG or Let cardG?
(same as just above)
theories/showcase/pnt.v
Outdated
| by rewrite ltnS -x2eqx3. | ||
| Qed. | ||
|
|
||
| Fact cardP (k : nat) : |
There was a problem hiding this comment.
Fact cardP -> Local Lemma cardP or Let cardP?
Since this one does not depend on any R : realType
(it was wrongly flagged as such in the previous commit),
it could maybe be in a different section, or maybe
appear before the other intermediate lemmas, to highlight its different nature.
There was a problem hiding this comment.
I do not really see the point in putting it in a different section, it is the natural course of the proof of the theorem and it just so happens to not require a hypothesis about real numbers.
There was a problem hiding this comment.
Moreover if this turns into a Let or a Local Lemma, that indeed justifies to keep it in the same section.
theories/showcase/pnt.v
Outdated
| by rewrite -expnD addnA addnn. | ||
| Qed. | ||
|
|
||
| Theorem DivergenceSumInversePrimeNumbers (R : realType) : |
There was a problem hiding this comment.
DivergenceSumInversePrimeNumbers -> dvg_sum_inv_prime_seq?
because I think that we favor small letters and underscores
instead of caps and identifiers made up of other identifiers
appearing in the statement.
|
LGTM after @affeldt-aist remarks have been applied. |
Prime numbers sequence Divergence of the sum of inverse of the prime numbers Abel transformation (discrete and continuous) First Tchebychev function majoration
Tragicus
force-pushed
the
divsuminvprim
branch
from
5562031 to
5515349
Compare
* Starting PNT Proof Prime numbers sequence Divergence of the sum of inverse of the prime numbers Abel transformation (discrete and continuous) First Tchebychev function majoration --------- Co-authored-by: LucasMalaizier <lucasmalaizier@PCLucas> Co-authored-by: Reynald Affeldt <[email protected]>
Motivation for this change
The divergence of the sum of the reciprocal of primes theorem, extracted from #1690 because it has been ready and sitting there for too long. We can add it to the famous list of formalized theorems.
Checklist
CHANGELOG_UNRELEASED.mdReference: How to document
Merge policy
As a rule of thumb:
all compile are preferentially merged into master.
Reminder to reviewers