Module mathcomp.analysis.showcase.pnt
From mathcomp Require Import boot order ssralg ssrnum ssrint intervalinterval_inference.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import classical_sets boolp topology.
From mathcomp Require Import reals ereal sequences.
# The Prime Number Theorem
This file aims at formalizing Daboussi's proof of the prime number theorem.
The main theorem proved so far is the divergence of the sum of the
reciprocals of the prime numbers.
```
prime_seq == the sequence of prime numbers
```
Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope classical_set_scope.
Local Open Scope set_scope.
Local Open Scope nat_scope.
Import Order.POrderTheory GRing.Theory Num.Theory.
Section prime_seq.
Let
next_prime_subproof
Source code
: { : 'I_(n`! - n).+1 | prime (n.+1 + i)}.Source code
Proof.
suff: [exists : 'I_(n`! - n).+1, prime (n.+1 + (tnth (ord_tuple _) i))].
rewrite (existsb_tnth (fun : 'I_(n`! - n).+1 => prime (n.+1 + x))).
move=> /(nth_find ord0) ni.
by eexists; apply: ni.
apply/existsP/not_existsP => noprime.
set q := pdiv n`!.+1.
have qprime : prime q by apply/pdiv_prime/fact_gt0.
have [qlei|iltq] := leqP q n.
have /dvdn_fact : 0 < q <= n by rewrite pdiv_gt0.
by rewrite (@dvdn_add_eq _ _ 1) ?Euclid_dvd1// addn1 pdiv_dvd.
have qlt : q - n.+1 < (n`! - n).+1.
by rewrite -subSn// subSS -subSn ?fact_geq//; exact/leq_sub2r/pdiv_leq.
apply: (noprime (Ordinal qlt)).
by rewrite tnth_ord_tuple subnKC// ltnW.
Qed.
rewrite (existsb_tnth (fun : 'I_(n`! - n).+1 => prime (n.+1 + x))).
move=> /(nth_find ord0) ni.
by eexists; apply: ni.
apply/existsP/not_existsP => noprime.
set q := pdiv n`!.+1.
have qprime : prime q by apply/pdiv_prime/fact_gt0.
have [qlei|iltq] := leqP q n.
have /dvdn_fact : 0 < q <= n by rewrite pdiv_gt0.
by rewrite (@dvdn_add_eq _ _ 1) ?Euclid_dvd1// addn1 pdiv_dvd.
have qlt : q - n.+1 < (n`! - n).+1.
by rewrite -subSn// subSS -subSn ?fact_geq//; exact/leq_sub2r/pdiv_leq.
apply: (noprime (Ordinal qlt)).
by rewrite tnth_ord_tuple subnKC// ltnW.
Qed.
Definition
next_prime
Source code
: nat :=atan_unlock_subterm : unlockable (fun (R : realType) (x : R) => [get x0 : _ | [set y | (- (trigonometry_functions.pi / 2) < y < trigonometry_functions.pi / 2)%R /\ tan y = x]%classic x0]) atan_unlock_subterm is not universe polymorphic atan_unlock_subterm is transparent Expands to: Constant mathcomp.analysis.elementary_functions.trigonometry_functions.atan_unlock_subterm Declared in library mathcomp.analysis.elementary_functions.trigonometry_functions, line 1120, characters 0-106
Source code
n.+1 + [arg min_( < val (next_prime_subproof n) | prime (n.+1 + i)) val i].
Lemma
prime_next_prime
Source code
: prime (next_prime n).Source code
Proof.
Lemma
next_prime_min
Source code
( : nat) : i < j < next_prime i -> ~~ prime j.Source code
Proof.
Lemma
next_prime_lt
Source code
: n < next_prime n.Source code
Proof.
rewrite /next_prime.
case: arg_minnP => [|i _ _]; first by case: next_prime_subproof.
exact: leq_addr.
Qed.
case: arg_minnP => [|i _ _]; first by case: next_prime_subproof.
exact: leq_addr.
Qed.
Definition
prime_seq
Source code
: nat := iter n next_prime 2.atan_unlock_subterm : unlockable (fun (R : realType) (x : R) => [get x0 : _ | [set y | (- (trigonometry_functions.pi / 2) < y < trigonometry_functions.pi / 2)%R /\ tan y = x]%classic x0]) atan_unlock_subterm is not universe polymorphic atan_unlock_subterm is transparent Expands to: Constant mathcomp.analysis.elementary_functions.trigonometry_functions.atan_unlock_subterm Declared in library mathcomp.analysis.elementary_functions.trigonometry_functions, line 1120, characters 0-106
Source code
Lemma
leq_prime_seq
Source code
: {mono prime_seq : / m <= n}.Source code
Proof.
move=> m n.
apply: (@Order.NatMonotonyTheory.incn_inP _ nat predT) => // {m n} [n /= _ _].
exact: next_prime_lt.
Qed.
apply: (@Order.NatMonotonyTheory.incn_inP _ nat predT) => // {m n} [n /= _ _].
exact: next_prime_lt.
Qed.
Lemma
mem_prime_seq
Source code
( : nat) : (p \in range prime_seq) = prime p.Source code
Proof.
apply/idP/idP => [|primep].
by rewrite inE => -[] [|n] _ <- //=; apply: prime_next_prime.
case: (@Order.TotalTheory.arg_maxP _ _ 'I_p.+1 ord0
(fun => prime_seq m <= p) prime_seq) => /= [|n pgepsi pptargmax].
exact: prime_gt1.
have pltpsni1: p < prime_seq n.+1.
move: (valP n). rewrite leq_eqVlt => /orP [|nltp].
rewrite eqSS => /eqP ->.
exact/mono_leq_infl/leq_prime_seq.
have := contra (pptargmax (Ordinal nltp)).
rewrite [(_ <= _)%O](leq_prime_seq (Ordinal nltp) n) ltnn => /(_ erefl).
by rewrite ltnNge.
move: pgepsi.
rewrite leq_eqVlt => /predU1P[<-|psnltp]; first by rewrite inE.
have := @next_prime_min (prime_seq n) p; rewrite psnltp pltpsni1 => /(_ erefl).
by rewrite primep.
Qed.
by rewrite inE => -[] [|n] _ <- //=; apply: prime_next_prime.
case: (@Order.TotalTheory.arg_maxP _ _ 'I_p.+1 ord0
(fun => prime_seq m <= p) prime_seq) => /= [|n pgepsi pptargmax].
exact: prime_gt1.
have pltpsni1: p < prime_seq n.+1.
move: (valP n). rewrite leq_eqVlt => /orP [|nltp].
rewrite eqSS => /eqP ->.
exact/mono_leq_infl/leq_prime_seq.
have := contra (pptargmax (Ordinal nltp)).
rewrite [(_ <= _)%O](leq_prime_seq (Ordinal nltp) n) ltnn => /(_ erefl).
by rewrite ltnNge.
move: pgepsi.
rewrite leq_eqVlt => /predU1P[<-|psnltp]; first by rewrite inE.
have := @next_prime_min (prime_seq n) p; rewrite psnltp pltpsni1 => /(_ erefl).
by rewrite primep.
Qed.
End prime_seq.
Section dvg_sum_inv_prime_seq.
Let ( : nat) :=
[set : 'I_N.+1 | all (fun => p < prime_seq k) (primes n)]%SET.
Let ( : nat) := ~: P k N.
Let
cardPcardG
Source code
: #|G k N| + #|P k N| = N.+1.Source code
Proof.
Let
cardG
Source code
( : realType) ( : nat) :Source code
(\sum_(k <= <oo) ((prime_seq k0)%:R^-1 : R)%:E < (2^-1)%:E)%E
-> N > 0 -> (#|G k N|%:R < (N%:R / 2) :> R)%R.
Proof.
set E := fun => [set : 'I_N.+1 | (prime_seq i) \in (primes n)].
set Parts := fun => [set ([set in [seq (insubd ord0 x : 'I_N.+1) |
<- iota ((val y).+1 - (prime_seq i)) (prime_seq i)]]
: {set 'I_N.+1}) | in (E i)]%SET.
move=> Rklthalf Nneq0.
suff cardEi : forall , k <= i ->
(#|E i|%:R <= N%:R / (prime_seq i)%:R :>R)%R => [|i klti].
have -> : G k N = \bigcup_(k <= < N.+1) E i.
apply/eqP; rewrite finset.eqEsubset; apply/andP; split; last first.
apply/fintype.subsetP => x.
rewrite big_geq_mkord => /bigcupP[i /= klei].
rewrite inE => pidvdx.
rewrite !inE -has_predC; apply/hasP; exists (prime_seq i) => //=.
by rewrite -leqNgt leq_prime_seq.
apply/fintype.subsetP => /= x.
rewrite !inE -has_predC => /hasP[p/=].
rewrite mem_primes => /andP[+ /andP[xneq0 pdvdx]].
rewrite -mem_prime_seq inE => /= -[i _ peqpi].
move: peqpi pdvdx => <- {p} pidvdx.
rewrite -leqNgt => pklepi.
rewrite big_geq_mkord; apply/bigcupP.
have ileqN : i < N.+1.
apply: (leq_ltn_trans _ (ltn_ord x)).
apply: (leq_trans _ (dvdn_leq xneq0 pidvdx)).
exact/mono_leq_infl/leq_prime_seq.
exists (Ordinal ileqN) => /=; first by rewrite -leq_prime_seq.
by rewrite inE mem_primes xneq0 pidvdx/= andbT -mem_prime_seq inE.
apply: (le_lt_trans (ler_wpMn2l ler01 (card_big_setU _ _ E))).
apply: (@le_lt_trans _ _ (N%:R * \sum_(k <= < N.+1) (prime_seq i)%:R^-1)%R).
rewrite mulr_sumr raddf_sum /= ler_sum_nat// => i /andP[+ _].
exact: cardEi.
rewrite -lte_fin.
apply: (@le_lt_trans _ _ (N%:R%:E * \sum_(k <= <oo) (prime_seq i)%:R^-1%:E)%E).
rewrite EFinM lee_pmul ?lee_fin//; first by rewrite sumr_ge0.
rewrite raddf_sum; apply: nneseries_lim_ge => n _ _.
by rewrite lee_fin invr_ge0.
rewrite EFinM -lte_pdivrMl ?ltr0n// muleA -EFinM mulVf ?mul1e//.
by rewrite pnatr_eq0 -lt0n.
rewrite ler_pdivlMr.
rewrite ltr0n.
have : prime_seq i \in range prime_seq by rewrite inE.
by rewrite mem_prime_seq; apply: prime_gt0.
have Eigtpi x3 : x3 \in E i -> prime_seq i - x3.+1 = 0.
have OnotinE : ord0 \notin E i => [|x3inEi]; first by rewrite /E inE.
apply/eqP; rewrite subn_eq0; apply/leqW/dvdn_leq.
case: x3 x3inEi => /= x3; have [-> N1lt0|//] := posnP x3.
by rewrite /E inE.
move: x3inEi; rewrite /E inE mem_primes -mem_prime_seq mem_range.
by case: (x3 > 0).
have: finset.trivIset (Parts i).
apply/finset.trivIsetP => _ _ /imsetP [] x xinEi -> /imsetP [] y yinEi ->.
wlog : x y xinEi yinEi / x <= y.
move: (leq_total x y) => /orP [xley Hw| ylex Hw].
exact: (Hw x y).
by rewrite eq_sym disjoint_sym; apply: (Hw y x).
rewrite -[x <= y]/(x <= y)%O.
rewrite le_eqVlt => /predU1P[->|xy _]; first by rewrite eqxx.
rewrite -setI_eq0 -finset.subset0.
apply/fintype.subsetP => x0.
rewrite finset.in_setI !inE => /andP[] /mapP[]/= x1 x1x -> /mapP[]/= x2 x2y.
move=> /(congr1 val); rewrite !val_insubd; move: x1x x2y.
rewrite !mem_iota !addnCB (Eigtpi x) // (Eigtpi y) // !addn0 !ltnS.
have xiN ( : 'I_N.+1) ( : nat) : b <= a -> b <= N.
by move/leq_trans; apply; rewrite -ltnS.
move=> /andP [] _ /[dup] + /xiN -> /andP [] + /xiN -> x1eqx2.
rewrite -x1eqx2 => /(leq_trans _)/[apply].
rewrite -(leq_add2r (prime_seq i)) addnCB Eigtpi// addn0.
rewrite -(@leq_sub2rE x) ?leq_addr// subDnCA// subnn addn0 (subSn (ltW xy)).
rewrite ltnNge dvdn_leq// ?subn_gt0//.
have dvdni z : z \in E i -> prime_seq i %| z.
by rewrite inE mem_primes => /andP[] _ /andP[].
by apply: dvdn_sub; apply: dvdni.
set i1toN := [set : 'I_N.+1] :\ ord0.
have cardNeqN: #|i1toN| = N.
rewrite /i1toN. apply/eqP.
rewrite -(eqn_add2r (ord0 \in [set :'I_N.+1]%SET)). apply/eqP.
have ord0inI: ord0 \in [set: 'I_N.+1]%SET by rewrite inE.
rewrite [in RHS]ord0inI [N + 1]addn1 addnC.
by rewrite -(cardsD1 ord0 [set: 'I_N.+1]) cardsT card_ord.
rewrite -[X in (_ <= X%:R)%R]cardNeqN /finset.trivIset => /eqP.
have cardeltPi: forall , X \in Parts i -> #|X| = (prime_seq i) => [X|].
rewrite /(Parts i) => /finset.imsetP [] x xinEi -> {X}.
rewrite cardsE.
suff /card_uniqP -> : uniq ([seq insubd ord0 x0 |
<- iota ((\val x).+1 - prime_seq i) (prime_seq i)] : seq 'I_N.+1).
by rewrite size_map size_iota.
apply/(uniqP ord0) => x1 y1 /=.
rewrite !inE size_map size_iota => x1lt y1lt.
rewrite !(nth_map 0) ?size_iota //.
rewrite !nth_iota => // /(congr1 val). rewrite !val_insubd /=.
rewrite [X in X < _]addBnA.
- by rewrite -subn_eq0; apply/eqP/Eigtpi.
- exact: ltnW.
rewrite -(@prednK (prime_seq i - x1)) ?subn_gt0// !subSS.
rewrite (leq_ltn_trans _ (ltn_ord x)); first exact: sub_ord_proof.
rewrite [X in X < _]addBnA.
- by rewrite -subn_eq0; apply/eqP/Eigtpi.
- exact: ltnW.
rewrite -(@prednK (prime_seq i - y1)) ?subn_gt0 // !subSS.
suff -> : x - (prime_seq i - y1).-1 < N.+1 by apply: addnI.
exact/(leq_ltn_trans _ (ltn_ord x))/sub_ord_proof.
under eq_bigr do rewrite cardeltPi//.
rewrite sum_nat_const.
suff -> : #|Parts i| = #|E i|.
suff Pisubi1toN : finset.cover (Parts i) \subset i1toN => [eqcard|].
suff: #|E i| * prime_seq i <= #|i1toN| by rewrite -natrM ler_nat.
exact: (leq_trans (eq_leq eqcard) (subset_leq_card Pisubi1toN)).
rewrite /(Parts i) cover_imset. apply/bigcupsP => i0 i0inEi.
apply/fintype.subsetP => x.
case: (boolP (x == ord0)) => [/eqP ->|xneq0 _]; last first.
by rewrite /i1toN inE !inE xneq0.
rewrite inE /in_mem /= => /mapP /= [] x0.
rewrite mem_iota subnK => [|/andP [] x0b1 x0b2].
by rewrite -subn_eq0; apply/eqP /Eigtpi.
have x0b3: x0 < N.+1 => [|/(congr1 val)].
exact: (leq_ltn_trans _ (ltn_ord i0)).
rewrite val_insubd x0b3 => /= /eqP.
suff xpos: x0 > 0 by rewrite ltn_eqF.
apply: (leq_ltn_trans (leq0n (i0.+1 - prime_seq i).-1)).
rewrite -(ltn_add2r 1) !addn1 prednK // subn_gt0 ltnS.
rewrite dvdn_leq //; last first.
move: i0inEi.
by rewrite /E inE mem_primes -mem_prime_seq mem_range; case: (i0 > 0).
case: i0 i0inEi x0b1 x0b2 => /= i0.
case: (posnP i0) => // -> N1lt0.
by rewrite /E inE.
rewrite /(Parts i) card_in_imset // /injective => x1 x2.
wlog: x1 x2 / x1 <= x2 => [Hw|x1lex2 x1inEi x2inEi enseq].
move: (leq_total x1 x2) => /orP [] => // [|x2lex1 x1inEi x2inEi /eqP].
exact: (Hw x1 x2).
rewrite eq_sym => /eqP enseq.
apply/eqP. rewrite eq_sym. apply/eqP.
exact: (Hw x2 x1).
apply: le_anti. apply/andP. split; first exact: x1lex2.
have: x2 \in [set in [seq insubd ord0 x0
| <- iota ((\val x1).+1 - prime_seq i) (prime_seq i)]].
rewrite enseq inE /in_mem /=. apply/mapP => /=.
exists x2; last by apply: val_inj; rewrite !val_insubd ltn_ord.
rewrite mem_iota subnK; first by rewrite -subn_eq0; apply/eqP /Eigtpi.
by rewrite ltnSn -ltnS ltn_subrL prime_gt0 // -mem_prime_seq mem_range.
rewrite inE /in_mem /= => /mapP /= [] x3.
rewrite mem_iota subnK => [|/andP [] x3b1 x3b2 /(congr1 val)].
by rewrite -subn_eq0; apply/eqP /Eigtpi.
have x3b3: x3 < N.+1 by apply: (leq_ltn_trans _ (ltn_ord x1)).
rewrite val_insubd x3b3 /= => x2eqx3. move: x3b2.
by rewrite ltnS -x2eqx3.
Qed.
set Parts := fun => [set ([set in [seq (insubd ord0 x : 'I_N.+1) |
<- iota ((val y).+1 - (prime_seq i)) (prime_seq i)]]
: {set 'I_N.+1}) | in (E i)]%SET.
move=> Rklthalf Nneq0.
suff cardEi : forall , k <= i ->
(#|E i|%:R <= N%:R / (prime_seq i)%:R :>R)%R => [|i klti].
have -> : G k N = \bigcup_(k <= < N.+1) E i.
apply/eqP; rewrite finset.eqEsubset; apply/andP; split; last first.
apply/fintype.subsetP => x.
rewrite big_geq_mkord => /bigcupP[i /= klei].
rewrite inE => pidvdx.
rewrite !inE -has_predC; apply/hasP; exists (prime_seq i) => //=.
by rewrite -leqNgt leq_prime_seq.
apply/fintype.subsetP => /= x.
rewrite !inE -has_predC => /hasP[p/=].
rewrite mem_primes => /andP[+ /andP[xneq0 pdvdx]].
rewrite -mem_prime_seq inE => /= -[i _ peqpi].
move: peqpi pdvdx => <- {p} pidvdx.
rewrite -leqNgt => pklepi.
rewrite big_geq_mkord; apply/bigcupP.
have ileqN : i < N.+1.
apply: (leq_ltn_trans _ (ltn_ord x)).
apply: (leq_trans _ (dvdn_leq xneq0 pidvdx)).
exact/mono_leq_infl/leq_prime_seq.
exists (Ordinal ileqN) => /=; first by rewrite -leq_prime_seq.
by rewrite inE mem_primes xneq0 pidvdx/= andbT -mem_prime_seq inE.
apply: (le_lt_trans (ler_wpMn2l ler01 (card_big_setU _ _ E))).
apply: (@le_lt_trans _ _ (N%:R * \sum_(k <= < N.+1) (prime_seq i)%:R^-1)%R).
rewrite mulr_sumr raddf_sum /= ler_sum_nat// => i /andP[+ _].
exact: cardEi.
rewrite -lte_fin.
apply: (@le_lt_trans _ _ (N%:R%:E * \sum_(k <= <oo) (prime_seq i)%:R^-1%:E)%E).
rewrite EFinM lee_pmul ?lee_fin//; first by rewrite sumr_ge0.
rewrite raddf_sum; apply: nneseries_lim_ge => n _ _.
by rewrite lee_fin invr_ge0.
rewrite EFinM -lte_pdivrMl ?ltr0n// muleA -EFinM mulVf ?mul1e//.
by rewrite pnatr_eq0 -lt0n.
rewrite ler_pdivlMr.
rewrite ltr0n.
have : prime_seq i \in range prime_seq by rewrite inE.
by rewrite mem_prime_seq; apply: prime_gt0.
have Eigtpi x3 : x3 \in E i -> prime_seq i - x3.+1 = 0.
have OnotinE : ord0 \notin E i => [|x3inEi]; first by rewrite /E inE.
apply/eqP; rewrite subn_eq0; apply/leqW/dvdn_leq.
case: x3 x3inEi => /= x3; have [-> N1lt0|//] := posnP x3.
by rewrite /E inE.
move: x3inEi; rewrite /E inE mem_primes -mem_prime_seq mem_range.
by case: (x3 > 0).
have: finset.trivIset (Parts i).
apply/finset.trivIsetP => _ _ /imsetP [] x xinEi -> /imsetP [] y yinEi ->.
wlog : x y xinEi yinEi / x <= y.
move: (leq_total x y) => /orP [xley Hw| ylex Hw].
exact: (Hw x y).
by rewrite eq_sym disjoint_sym; apply: (Hw y x).
rewrite -[x <= y]/(x <= y)%O.
rewrite le_eqVlt => /predU1P[->|xy _]; first by rewrite eqxx.
rewrite -setI_eq0 -finset.subset0.
apply/fintype.subsetP => x0.
rewrite finset.in_setI !inE => /andP[] /mapP[]/= x1 x1x -> /mapP[]/= x2 x2y.
move=> /(congr1 val); rewrite !val_insubd; move: x1x x2y.
rewrite !mem_iota !addnCB (Eigtpi x) // (Eigtpi y) // !addn0 !ltnS.
have xiN ( : 'I_N.+1) ( : nat) : b <= a -> b <= N.
by move/leq_trans; apply; rewrite -ltnS.
move=> /andP [] _ /[dup] + /xiN -> /andP [] + /xiN -> x1eqx2.
rewrite -x1eqx2 => /(leq_trans _)/[apply].
rewrite -(leq_add2r (prime_seq i)) addnCB Eigtpi// addn0.
rewrite -(@leq_sub2rE x) ?leq_addr// subDnCA// subnn addn0 (subSn (ltW xy)).
rewrite ltnNge dvdn_leq// ?subn_gt0//.
have dvdni z : z \in E i -> prime_seq i %| z.
by rewrite inE mem_primes => /andP[] _ /andP[].
by apply: dvdn_sub; apply: dvdni.
set i1toN := [set : 'I_N.+1] :\ ord0.
have cardNeqN: #|i1toN| = N.
rewrite /i1toN. apply/eqP.
rewrite -(eqn_add2r (ord0 \in [set :'I_N.+1]%SET)). apply/eqP.
have ord0inI: ord0 \in [set: 'I_N.+1]%SET by rewrite inE.
rewrite [in RHS]ord0inI [N + 1]addn1 addnC.
by rewrite -(cardsD1 ord0 [set: 'I_N.+1]) cardsT card_ord.
rewrite -[X in (_ <= X%:R)%R]cardNeqN /finset.trivIset => /eqP.
have cardeltPi: forall , X \in Parts i -> #|X| = (prime_seq i) => [X|].
rewrite /(Parts i) => /finset.imsetP [] x xinEi -> {X}.
rewrite cardsE.
suff /card_uniqP -> : uniq ([seq insubd ord0 x0 |
<- iota ((\val x).+1 - prime_seq i) (prime_seq i)] : seq 'I_N.+1).
by rewrite size_map size_iota.
apply/(uniqP ord0) => x1 y1 /=.
rewrite !inE size_map size_iota => x1lt y1lt.
rewrite !(nth_map 0) ?size_iota //.
rewrite !nth_iota => // /(congr1 val). rewrite !val_insubd /=.
rewrite [X in X < _]addBnA.
- by rewrite -subn_eq0; apply/eqP/Eigtpi.
- exact: ltnW.
rewrite -(@prednK (prime_seq i - x1)) ?subn_gt0// !subSS.
rewrite (leq_ltn_trans _ (ltn_ord x)); first exact: sub_ord_proof.
rewrite [X in X < _]addBnA.
- by rewrite -subn_eq0; apply/eqP/Eigtpi.
- exact: ltnW.
rewrite -(@prednK (prime_seq i - y1)) ?subn_gt0 // !subSS.
suff -> : x - (prime_seq i - y1).-1 < N.+1 by apply: addnI.
exact/(leq_ltn_trans _ (ltn_ord x))/sub_ord_proof.
under eq_bigr do rewrite cardeltPi//.
rewrite sum_nat_const.
suff -> : #|Parts i| = #|E i|.
suff Pisubi1toN : finset.cover (Parts i) \subset i1toN => [eqcard|].
suff: #|E i| * prime_seq i <= #|i1toN| by rewrite -natrM ler_nat.
exact: (leq_trans (eq_leq eqcard) (subset_leq_card Pisubi1toN)).
rewrite /(Parts i) cover_imset. apply/bigcupsP => i0 i0inEi.
apply/fintype.subsetP => x.
case: (boolP (x == ord0)) => [/eqP ->|xneq0 _]; last first.
by rewrite /i1toN inE !inE xneq0.
rewrite inE /in_mem /= => /mapP /= [] x0.
rewrite mem_iota subnK => [|/andP [] x0b1 x0b2].
by rewrite -subn_eq0; apply/eqP /Eigtpi.
have x0b3: x0 < N.+1 => [|/(congr1 val)].
exact: (leq_ltn_trans _ (ltn_ord i0)).
rewrite val_insubd x0b3 => /= /eqP.
suff xpos: x0 > 0 by rewrite ltn_eqF.
apply: (leq_ltn_trans (leq0n (i0.+1 - prime_seq i).-1)).
rewrite -(ltn_add2r 1) !addn1 prednK // subn_gt0 ltnS.
rewrite dvdn_leq //; last first.
move: i0inEi.
by rewrite /E inE mem_primes -mem_prime_seq mem_range; case: (i0 > 0).
case: i0 i0inEi x0b1 x0b2 => /= i0.
case: (posnP i0) => // -> N1lt0.
by rewrite /E inE.
rewrite /(Parts i) card_in_imset // /injective => x1 x2.
wlog: x1 x2 / x1 <= x2 => [Hw|x1lex2 x1inEi x2inEi enseq].
move: (leq_total x1 x2) => /orP [] => // [|x2lex1 x1inEi x2inEi /eqP].
exact: (Hw x1 x2).
rewrite eq_sym => /eqP enseq.
apply/eqP. rewrite eq_sym. apply/eqP.
exact: (Hw x2 x1).
apply: le_anti. apply/andP. split; first exact: x1lex2.
have: x2 \in [set in [seq insubd ord0 x0
| <- iota ((\val x1).+1 - prime_seq i) (prime_seq i)]].
rewrite enseq inE /in_mem /=. apply/mapP => /=.
exists x2; last by apply: val_inj; rewrite !val_insubd ltn_ord.
rewrite mem_iota subnK; first by rewrite -subn_eq0; apply/eqP /Eigtpi.
by rewrite ltnSn -ltnS ltn_subrL prime_gt0 // -mem_prime_seq mem_range.
rewrite inE /in_mem /= => /mapP /= [] x3.
rewrite mem_iota subnK => [|/andP [] x3b1 x3b2 /(congr1 val)].
by rewrite -subn_eq0; apply/eqP /Eigtpi.
have x3b3: x3 < N.+1 by apply: (leq_ltn_trans _ (ltn_ord x1)).
rewrite val_insubd x3b3 /= => x2eqx3. move: x3b2.
by rewrite ltnS -x2eqx3.
Qed.
Let
cardP
Source code
( : nat) : #|P k (2 ^ (k.*2 + 2))| <= (2 ^ (k.*2 + 1)).+1.Source code
Proof.
set N := 2 ^ (k.*2 + 2).
pose P' := P k N :\ ord0.
set A := k.-tuple bool.
set B := 'I_(2 ^ (k + 1)).+1.
pose a := odd (logn (prime_seq i) n).
have eqseq : forall , n < k ->
[seq <- [seq prime_seq i | <- index_iota 0 k] | i \in primes n]
= primes n.
move=> + k0; case=> [|n nlek]; first by rewrite filter_pred0.
apply: lt_sorted_eq => [||elt].
- apply: lt_sorted_filter.
rewrite sorted_map.
apply: (@sub_sorted _ ltn); last exact: iota_ltn_sorted.
by rewrite ltEnat => i j /=; rewrite (leqW_mono leq_prime_seq).
- exact: sorted_primes.
rewrite mem_filter andb_idr// mem_primes -mem_prime_seq => /andP[].
rewrite inE => -[] i _ <- /andP[] _ /dvdn_leq/wrap[]// idn.
apply: map_f; rewrite mem_iota leq0n/= add0n subn0.
exact/(leq_ltn_trans _ nlek)/(leq_trans _ idn)/mono_leq_infl/leq_prime_seq.
have binB ( : 'I_N.+1) :
(\prod_( < k) (prime_seq i) ^ (logn (prime_seq i) n)./2) <
(2 ^ (k + 1)).+1.
have [->/=|nneq0] := eqVneq n ord0.
under eq_bigr do rewrite logn0 -divn2 div0n expn0.
by rewrite big1_eq -[X in _ < X]addn1 -[X in X < _]add0n ltn_add2r expn_gt0.
rewrite -ltn_sqr expn_prod.
under eq_bigr do rewrite -expnM muln2 halfK.
apply: (@leq_ltn_trans
(\prod_( < k) prime_seq i ^ (logn (prime_seq i) n))).
apply: leq_prod => i _. rewrite leq_exp2l; last exact: leq_subr.
by apply: prime_gt1; rewrite -mem_prime_seq inE.
apply: (@leq_ltn_trans n); last first.
apply: (ltn_trans (ltn_ord n)); rewrite /N.
rewrite -[X in X ^ 2]addn1 sqrnD exp1n addn1 -expnM mulnDl.
rewrite muln1 -expnS addn1 mul1n [in X in _ < X]mulnC.
by rewrite mul2n -addn1 leq_add2l// expn_gt0.
rewrite [X in _ <= X]prod_prime_decomp ?lt0n// prime_decompE big_map /=.
rewrite -(big_mkord predT (fun =>
(prime_seq i) ^ logn (prime_seq i) n)) -(big_map prime_seq predT
(fun => i ^ logn i n)) /=.
rewrite (bigID (mem (primes n))) /=.
rewrite [X in _ * X]big1 => [[//|][//|] i ip|].
apply/eqP; rewrite -(expn0 i.+2) eqn_exp2l//.
by move: ip; rewrite -logn_gt0 lt0n negbK.
rewrite muln1 -big_filter.
have [nltk|klen] := ltnP n k; first by rewrite (eqseq n).
rewrite -[in X in _ <= X](eqseq n n.+1); first exact: ltnSn.
rewrite -[X in index_iota _ X.+1](subnKC (leq_trans klen (ltnSn n))).
rewrite -addnS -subSn//.
rewrite !big_filter /index_iota !subn0 iotaD map_cat big_cat add0n /=.
by apply/leq_pmulr/prodn_gt0 => i; exact: pfactor_gt0.
set f : 'I_N.+1 -> A * B := fun => ([tuple a n i | < k], Ordinal (binB n)).
set g : A * B -> nat := fun => let (, ) := c in
b ^ 2 * \prod_( < k) (prime_seq i) ^ (tnth a i).
have finj x y : x \in P' k N -> y \in P' k N -> f x = f y -> x = y.
move=> xinPkN yinPkN /(congr1 g).
suff: forall , x \in P' k N -> g (f x) = x.
by move=> /[dup] /(_ _ xinPkN) -> /(_ _ yinPkN) ->; apply: val_inj.
move=> {yinPkN y} {}x {}xinPkN /=.
rewrite expn_prod.
under eq_bigr do rewrite -expnM muln2 halfK.
rewrite -big_split /=.
under eq_bigr => i _.
rewrite -expnD tnth_mktuple /a subnK.
by case: (boolP (odd (logn (prime_seq i) x))); first exact: odd_gt0.
over.
have [xeq0|xneq0] := eqVneq x ord0.
by move: xeq0 xinPkN => ->; rewrite /P' !inE.
rewrite [RHS]prod_prime_decomp ?lt0n// prime_decompE big_map /=.
rewrite [in LHS](bigID (fun : 'I_k => prime_seq i \in primes x)) /=.
under [X in _ * X = _]eq_bigr => i.
rewrite mem_primes lognE => /negbTE ->.
rewrite expn0; over.
rewrite big1_eq muln1 -(big_map _ (fun => prime_seq i \in primes x)
(fun => prime_seq i ^ logn (prime_seq i) x))
-(big_map _ _ (fun => j ^ logn j x)) -big_filter.
apply: congr_big => //.
rewrite -map_comp functions.compE.
apply: lt_sorted_eq => [||elt].
- apply: lt_sorted_filter.
rewrite map_comp sorted_map -[X in map _ X]filter_predT val_enum_ord.
apply: (@sub_sorted _ ltn); last exact: iota_ltn_sorted.
rewrite ltEnat => i j /=.
by rewrite (leqW_mono leq_prime_seq).
- exact: sorted_primes.
rewrite mem_filter; apply: andb_idr.
move: xinPkN; rewrite /P' /P inE => /andP[_].
rewrite inE => /allP primesxlepk eltinprimesx.
have [] : prime elt /\ elt < prime_seq k.
split; last exact: primesxlepk.
by apply/(@allP _ _ (primes x)) => //; exact: all_prime_primes.
rewrite -mem_prime_seq inE => /= -[i _ <-] pilepk.
rewrite map_comp; apply: map_f.
rewrite -[X in map _ X]filter_predT val_enum_ord mem_iota /= add0n.
by rewrite -(leqW_mono leq_prime_seq).
have -> : P k N = P' k N :|: [set ord0].
by rewrite /P' finset.setUC finset.setD1K // inE.
rewrite finset.setUC cardsU1 [in X in X + _]/P' !inE /= add1n ltnS.
rewrite -(card_in_imset finj).
have imfleqAB :
#|[set f x | in P' k N]| <= #|finset.setX [set: A] (~: [set ord0 : B])|.
apply/subset_leq_card/fintype.subsetP => y.
rewrite !inE => /imsetP [] x xinPkN -> /=.
apply: (contra_not_neq (@congr1 _ _ val _ _)) => /=.
apply/eqP; rewrite -lt0n; apply: prodn_gt0 => i.
by rewrite expn_gt0 prime_gt0//= -mem_prime_seq inE.
apply: (leq_trans imfleqAB).
rewrite cardsX cardsE card_tuple card_bool cardsC1 card_ord.
by rewrite -expnD addnA addnn.
Qed.
pose P' := P k N :\ ord0.
set A := k.-tuple bool.
set B := 'I_(2 ^ (k + 1)).+1.
pose a := odd (logn (prime_seq i) n).
have eqseq : forall , n < k ->
[seq <- [seq prime_seq i | <- index_iota 0 k] | i \in primes n]
= primes n.
move=> + k0; case=> [|n nlek]; first by rewrite filter_pred0.
apply: lt_sorted_eq => [||elt].
- apply: lt_sorted_filter.
rewrite sorted_map.
apply: (@sub_sorted _ ltn); last exact: iota_ltn_sorted.
by rewrite ltEnat => i j /=; rewrite (leqW_mono leq_prime_seq).
- exact: sorted_primes.
rewrite mem_filter andb_idr// mem_primes -mem_prime_seq => /andP[].
rewrite inE => -[] i _ <- /andP[] _ /dvdn_leq/wrap[]// idn.
apply: map_f; rewrite mem_iota leq0n/= add0n subn0.
exact/(leq_ltn_trans _ nlek)/(leq_trans _ idn)/mono_leq_infl/leq_prime_seq.
have binB ( : 'I_N.+1) :
(\prod_( < k) (prime_seq i) ^ (logn (prime_seq i) n)./2) <
(2 ^ (k + 1)).+1.
have [->/=|nneq0] := eqVneq n ord0.
under eq_bigr do rewrite logn0 -divn2 div0n expn0.
by rewrite big1_eq -[X in _ < X]addn1 -[X in X < _]add0n ltn_add2r expn_gt0.
rewrite -ltn_sqr expn_prod.
under eq_bigr do rewrite -expnM muln2 halfK.
apply: (@leq_ltn_trans
(\prod_( < k) prime_seq i ^ (logn (prime_seq i) n))).
apply: leq_prod => i _. rewrite leq_exp2l; last exact: leq_subr.
by apply: prime_gt1; rewrite -mem_prime_seq inE.
apply: (@leq_ltn_trans n); last first.
apply: (ltn_trans (ltn_ord n)); rewrite /N.
rewrite -[X in X ^ 2]addn1 sqrnD exp1n addn1 -expnM mulnDl.
rewrite muln1 -expnS addn1 mul1n [in X in _ < X]mulnC.
by rewrite mul2n -addn1 leq_add2l// expn_gt0.
rewrite [X in _ <= X]prod_prime_decomp ?lt0n// prime_decompE big_map /=.
rewrite -(big_mkord predT (fun =>
(prime_seq i) ^ logn (prime_seq i) n)) -(big_map prime_seq predT
(fun => i ^ logn i n)) /=.
rewrite (bigID (mem (primes n))) /=.
rewrite [X in _ * X]big1 => [[//|][//|] i ip|].
apply/eqP; rewrite -(expn0 i.+2) eqn_exp2l//.
by move: ip; rewrite -logn_gt0 lt0n negbK.
rewrite muln1 -big_filter.
have [nltk|klen] := ltnP n k; first by rewrite (eqseq n).
rewrite -[in X in _ <= X](eqseq n n.+1); first exact: ltnSn.
rewrite -[X in index_iota _ X.+1](subnKC (leq_trans klen (ltnSn n))).
rewrite -addnS -subSn//.
rewrite !big_filter /index_iota !subn0 iotaD map_cat big_cat add0n /=.
by apply/leq_pmulr/prodn_gt0 => i; exact: pfactor_gt0.
set f : 'I_N.+1 -> A * B := fun => ([tuple a n i | < k], Ordinal (binB n)).
set g : A * B -> nat := fun => let (, ) := c in
b ^ 2 * \prod_( < k) (prime_seq i) ^ (tnth a i).
have finj x y : x \in P' k N -> y \in P' k N -> f x = f y -> x = y.
move=> xinPkN yinPkN /(congr1 g).
suff: forall , x \in P' k N -> g (f x) = x.
by move=> /[dup] /(_ _ xinPkN) -> /(_ _ yinPkN) ->; apply: val_inj.
move=> {yinPkN y} {}x {}xinPkN /=.
rewrite expn_prod.
under eq_bigr do rewrite -expnM muln2 halfK.
rewrite -big_split /=.
under eq_bigr => i _.
rewrite -expnD tnth_mktuple /a subnK.
by case: (boolP (odd (logn (prime_seq i) x))); first exact: odd_gt0.
over.
have [xeq0|xneq0] := eqVneq x ord0.
by move: xeq0 xinPkN => ->; rewrite /P' !inE.
rewrite [RHS]prod_prime_decomp ?lt0n// prime_decompE big_map /=.
rewrite [in LHS](bigID (fun : 'I_k => prime_seq i \in primes x)) /=.
under [X in _ * X = _]eq_bigr => i.
rewrite mem_primes lognE => /negbTE ->.
rewrite expn0; over.
rewrite big1_eq muln1 -(big_map _ (fun => prime_seq i \in primes x)
(fun => prime_seq i ^ logn (prime_seq i) x))
-(big_map _ _ (fun => j ^ logn j x)) -big_filter.
apply: congr_big => //.
rewrite -map_comp functions.compE.
apply: lt_sorted_eq => [||elt].
- apply: lt_sorted_filter.
rewrite map_comp sorted_map -[X in map _ X]filter_predT val_enum_ord.
apply: (@sub_sorted _ ltn); last exact: iota_ltn_sorted.
rewrite ltEnat => i j /=.
by rewrite (leqW_mono leq_prime_seq).
- exact: sorted_primes.
rewrite mem_filter; apply: andb_idr.
move: xinPkN; rewrite /P' /P inE => /andP[_].
rewrite inE => /allP primesxlepk eltinprimesx.
have [] : prime elt /\ elt < prime_seq k.
split; last exact: primesxlepk.
by apply/(@allP _ _ (primes x)) => //; exact: all_prime_primes.
rewrite -mem_prime_seq inE => /= -[i _ <-] pilepk.
rewrite map_comp; apply: map_f.
rewrite -[X in map _ X]filter_predT val_enum_ord mem_iota /= add0n.
by rewrite -(leqW_mono leq_prime_seq).
have -> : P k N = P' k N :|: [set ord0].
by rewrite /P' finset.setUC finset.setD1K // inE.
rewrite finset.setUC cardsU1 [in X in X + _]/P' !inE /= add1n ltnS.
rewrite -(card_in_imset finj).
have imfleqAB :
#|[set f x | in P' k N]| <= #|finset.setX [set: A] (~: [set ord0 : B])|.
apply/subset_leq_card/fintype.subsetP => y.
rewrite !inE => /imsetP [] x xinPkN -> /=.
apply: (contra_not_neq (@congr1 _ _ val _ _)) => /=.
apply/eqP; rewrite -lt0n; apply: prodn_gt0 => i.
by rewrite expn_gt0 prime_gt0//= -mem_prime_seq inE.
apply: (leq_trans imfleqAB).
rewrite cardsX cardsE card_tuple card_bool cardsC1 card_ord.
by rewrite -expnD addnA addnn.
Qed.
Theorem
dvg_sum_inv_prime_seq
Source code
( : realType) :Source code
(\sum_(0 <= < n) (((prime_seq i)%:R : R)^-1)%:E)%R @[ --> \oo] --> +oo%E.
Proof.
set un := fun => (((prime_seq i)%:R : R)^-1)%:E.
set Sn := fun => (\sum_(0 <= < n) (un i))%R.
have unpos n : 0 <= n -> true -> (0 <= un n)%E => [_ _|].
by rewrite /un lee_fin invr_ge0 ler0n.
have := is_cvg_nneseries unpos.
have := leey (limn Sn).
rewrite le_eqVlt => /predU1P[-> //|].
have := nneseries_ge0 unpos.
move leqlimnSn : (limn Sn) => l.
case: l leqlimnSn => // l leqlimnSn _ _ /subsetP llimnSn.
have /llimnSn : `](l - (1/2))%:E, (l + (1/2))%:E[ \in nbhs (l%:E).
rewrite inE; exists (1/2)%R => /=; first exact: divr_gt0.
exact/subset_ball_prop_in_itv.
rewrite inE => -[] k /= _ /subsetP/(_ k).
set N := 2 ^ (k.*2 + 2).
set PN := P k N.
set GN := G k N.
rewrite inE /= leqnn set_interval.set_itvoo inE /= EFinB EFinD -leqlimnSn.
move=> /(_ erefl) /andP[+ _].
rewrite lte_subel_addl; first by rewrite leqlimnSn.
rewrite -lteBlDr; first exact/sum_fin_numP.
rewrite (nneseries_split _ k); first by move=> k0 _; exact: unpos.
rewrite /Sn add0n addrAC subee; first exact/sum_fin_numP.
rewrite add0e div1r => Rklthalf.
suff: N.+1 < N.+1 by rewrite ltnn.
rewrite -[X in X < _](cardPcardG k N).
have Neq : N./2 + (2 ^ (k.*2 + 1)).+1 = N.+1.
by rewrite /N 2!addnS expnS mul2n doubleK addnn.
rewrite -[X in _ < X]Neq -addSn.
apply: leq_add; last exact: cardP.
rewrite -(ltr_nat R).
have -> : (N./2%:R = N%:R / 2 :> R)%R.
by rewrite /N addnS expnS [in LHS]mul2n doubleK natrM mulrC mulKf.
by apply: (@cardG R) => //; rewrite /N expn_gt0.
Qed.
set Sn := fun => (\sum_(0 <= < n) (un i))%R.
have unpos n : 0 <= n -> true -> (0 <= un n)%E => [_ _|].
by rewrite /un lee_fin invr_ge0 ler0n.
have := is_cvg_nneseries unpos.
have := leey (limn Sn).
rewrite le_eqVlt => /predU1P[-> //|].
have := nneseries_ge0 unpos.
move leqlimnSn : (limn Sn) => l.
case: l leqlimnSn => // l leqlimnSn _ _ /subsetP llimnSn.
have /llimnSn : `](l - (1/2))%:E, (l + (1/2))%:E[ \in nbhs (l%:E).
rewrite inE; exists (1/2)%R => /=; first exact: divr_gt0.
exact/subset_ball_prop_in_itv.
rewrite inE => -[] k /= _ /subsetP/(_ k).
set N := 2 ^ (k.*2 + 2).
set PN := P k N.
set GN := G k N.
rewrite inE /= leqnn set_interval.set_itvoo inE /= EFinB EFinD -leqlimnSn.
move=> /(_ erefl) /andP[+ _].
rewrite lte_subel_addl; first by rewrite leqlimnSn.
rewrite -lteBlDr; first exact/sum_fin_numP.
rewrite (nneseries_split _ k); first by move=> k0 _; exact: unpos.
rewrite /Sn add0n addrAC subee; first exact/sum_fin_numP.
rewrite add0e div1r => Rklthalf.
suff: N.+1 < N.+1 by rewrite ltnn.
rewrite -[X in X < _](cardPcardG k N).
have Neq : N./2 + (2 ^ (k.*2 + 1)).+1 = N.+1.
by rewrite /N 2!addnS expnS mul2n doubleK addnn.
rewrite -[X in _ < X]Neq -addSn.
apply: leq_add; last exact: cardP.
rewrite -(ltr_nat R).
have -> : (N./2%:R = N%:R / 2 :> R)%R.
by rewrite /N addnS expnS [in LHS]mul2n doubleK natrM mulrC mulKf.
by apply: (@cardG R) => //; rewrite /N expn_gt0.
Qed.
End dvg_sum_inv_prime_seq.