Divergence of the sum of the reciprocal of primes (#1705)

* 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]>

Author: 3 people

CHANGELOG_UNRELEASED.md

@@ -39,6 +39,15 @@
 - in `constructive_ereal.v`:
   + lemma `lt0_adde`
 
+- in `unstable.v`
+  + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`,
+    `card_big_setU`
+
+- file `pnt.v`
+  + definitions `next_prime`, `prime_seq`
+  + lemmas `leq_prime_seq`, `mem_prime_seq`
+  + theorem `dvg_sum_inv_prime_seq`
+
 ### Changed
 
 - in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:

_CoqProject

@@ -120,5 +120,6 @@ theories/kernel.v
 theories/pi_irrational.v
 theories/gauss_integral.v
 theories/showcase/summability.v
+theories/showcase/pnt.v
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.v

classical/unstable.v

@@ -35,6 +35,47 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
+Lemma coprime_prodr (I : Type) (r : seq I) (P : {pred I}) (F : I -> nat) (a : I)
+    (l : seq I) :
+  all (coprime (F a)) [seq F i | i <- [seq i <- l | P i]] ->
+  coprime (F a) (\prod_(j <- l | P j) F j).
+Proof.
+elim: l => /= [_|h t ih]; first by rewrite big_nil coprimen1.
+rewrite big_cons; case: ifPn => // Ph.
+rewrite map_cons => /= /andP[FaFh FatP].
+by rewrite coprimeMr FaFh/= ih.
+Qed.
+
+Lemma Gauss_dvd_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat)
+    (n : nat) :
+  pairwise coprime [seq F i | i <- [seq i <- r | P i]] ->
+  reflect (forall i, i \in r -> P i -> F i %| n)
+          (\prod_(i <- r | P i) F i %| n).
+Proof.
+elim: r => /= [_|a l HI].
+  by rewrite big_nil dvd1n; apply: ReflectT => i; rewrite in_nil.
+rewrite big_cons; case: ifP => [Pa|nPa]; last first.
+  move/HI/equivP; apply; split=> [Fidvdn i|Fidvdn i il].
+    by rewrite in_cons => /predU1P[->|]; [rewrite nPa|exact: Fidvdn].
+  by apply: Fidvdn; rewrite in_cons il orbT.
+rewrite map_cons pairwise_cons => /andP[allcoprimea pairwisecoprime].
+rewrite Gauss_dvd; last exact: coprime_prodr.
+apply: (equivP (andPP idP (HI pairwisecoprime))).
+split=> [[Fadvdn Fidvdn] i|Fidvdn].
+  by rewrite in_cons => /predU1P[->//|]; exact: Fidvdn.
+split=> [|i il].
+  by apply: Fidvdn => //; exact: mem_head.
+by apply: Fidvdn; rewrite in_cons il orbT.
+Qed.
+
+Lemma expn_prod (I : eqType) (r : seq I) (P : {pred I}) (F : I -> nat)
+    (n : nat) :
+  ((\prod_(i <- r | P i) F i) ^ n = \prod_(i <- r | P i) (F i) ^ n)%N.
+Proof.
+elim: r => [|a l]; first by rewrite !big_nil exp1n.
+by rewrite !big_cons; case: ifPn => // Pa <-; rewrite expnMn.
+Qed.
+
 Section max_min.
 Variable R : realFieldType.
 
@@ -97,6 +138,12 @@ Qed.
 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_leq_infl f : {mono f : m n / (m <= n)%N} -> forall n, (n <= f n)%N.
+Proof.
+move=> fincr; elim=> [//| n HR]; rewrite (leq_ltn_trans HR)//.
+by rewrite ltn_neqAle fincr (inj_eq (incn_inj fincr)) -ltn_neqAle.
+Qed.
+
 (* NB: these lemmas have been introduced to develop the theory of bounded variation *)
 Section path_lt.
 Context d {T : orderType d}.
@@ -177,6 +224,14 @@ Arguments big_rmcond_in {R idx op I r} P.
 
 Reserved Notation "`1- x" (format "`1- x", at level 2).
 
+Lemma card_big_setU (I : Type) (T : finType) (r : seq I) (P : {pred I})
+    (F : I -> {set T}) :
+  (#|\bigcup_(i <- r | P i)  F i| <= \sum_(i <- r | P i) #|F i|)%N.
+Proof.
+elim/big_ind2 : _ => // [|m A n B Am Bn]; first by rewrite cards0.
+by rewrite (leq_trans (leq_card_setU _ _))// leq_add.
+Qed.
+
 Section onem.
 Variable R : numDomainType.
 Implicit Types r : R.