Skip to content

Commit cfbf0e6

Browse files
therythery
committed
liouville in the box
1 parent d731a8b commit cfbf0e6

4 files changed

Lines changed: 156 additions & 3 deletions

File tree

‎README.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,10 @@ Some extra material for mathcomp
7777

7878
[All prime numbers (except 2 and 3) are next to a multiple of 6](./prime6.v)
7979

80+
[Nicomachus Theorem about summation of cube](./nicomachus.v)
81+
82+
[Liouville Theorem about number's divisors](./liouville.v)
83+
8084
A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).
8185

8286
A note about addition chain is available [here](https://hal.science/hal-04971933).

‎coq-mathcomp-extra.opam‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -77,6 +77,10 @@ Some extra material for mathcomp
7777

7878
[All prime numbers (except 2 and 3) are next to a multiple of 6](./prime6.v)
7979

80+
[Nicomachus Theorem about summation of cube](./nicomachus.v)
81+
82+
[Liouville Theorem about number's divisors](./liouville.v)
83+
8084
A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).
8185

8286
A note about addition chain is available [here](https://hal.science/hal-04971933).

‎liouville.v‎

Lines changed: 144 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,33 @@
11
From mathcomp Require Import all_boot.
2+
Require Import nicomachus.
3+
4+
(******************************************************************************)
5+
(* Liouville theorem about number's divisors *)
6+
(* The proof uses a corollary of Nicomachus Theorem *)
7+
(* *)
8+
(* is_nmul F : F is multiplicative F (m * n) = F m * F n for m n coprimes *)
9+
(* ndivisors n : the number of divisors of n, ndivisors 10 = 4 *)
10+
(* *)
11+
(******************************************************************************)
12+
13+
14+
Definition is_nmul F := forall m n, coprime m n -> F (m * n) = F m * F n.
15+
16+
Lemma is_nmul_eq F1 F2 : F1 =1 F2 -> is_nmul F1 -> is_nmul F2.
17+
Proof. by move=> FE H1 m n mCn; rewrite -!FE H1. Qed.
18+
19+
Lemma is_nmulM F G : is_nmul F -> is_nmul G -> is_nmul (fun n => F n * G n).
20+
Proof.
21+
move=> HF HG m n mCn.
22+
by rewrite HF // HG // !mulnA; congr (_ * _); rewrite mulnAC.
23+
Qed.
24+
25+
Lemma is_nmulX F n : is_nmul F -> is_nmul (fun m => (F m) ^ n).
26+
Proof.
27+
move=> HF; elim: n => // n IH.
28+
apply: (is_nmul_eq (fun m => F m * F m ^ n)); first by move=> m; rewrite expnS.
29+
by apply: is_nmulM.
30+
Qed.
231

332
Lemma coprime_gcdnM i m n :
433
coprime m n -> i %| m * n -> i = gcdn i m * gcdn i n.
@@ -26,6 +55,39 @@ apply: IH => //.
2655
by rewrite -(dvdn_pmul2l (prime_gt0 pP)) mulnC mulnCA mulnA.
2756
Qed.
2857

58+
Lemma divisors_prime_eq p : prime p = (divisors p == [::1 ; p]).
59+
Proof.
60+
case: p => // [] [//|p]; apply/primeP/eqP => Hp; last first.
61+
by split => // d; rewrite dvdn_divisors // Hp !inE.
62+
apply: sorted_eq (sorted_divisors_ltn _) _ _ => //; first by apply: ltn_trans.
63+
by move=> i j /=; case: (ltngtP i j).
64+
have {Hp}[_ Hp] := Hp.
65+
apply: uniq_perm (divisors_uniq _) _ _ => // i.
66+
rewrite -dvdn_divisors // !inE.
67+
by apply/idP/idP=> [/Hp//|]; case/orP => /eqP->; rewrite ?dvd1n ?dvdnn.
68+
Qed.
69+
70+
71+
Lemma divisors_primeX p n :
72+
prime p -> divisors (p ^ n) = [seq p ^ i | i <- iota 0 n.+1].
73+
Proof.
74+
move=> pP.
75+
have p_gt1 := prime_gt1 pP.
76+
apply: sorted_eq (sorted_divisors_ltn _) _ _ => //; first by apply: ltn_trans.
77+
- by move=> i j /=; case: (ltngtP i j).
78+
- apply/(sortedP 0) => [] [//|i]; rewrite size_map size_iota ltnS => iLn /=.
79+
by case: n iLn.
80+
have i1Ln : i < n by apply: leq_ltn_trans iLn.
81+
by rewrite !(nth_map 0) ?size_iota // !nth_iota // !add1n ltn_exp2l.
82+
apply: uniq_perm (divisors_uniq _) _ _ => [|i].
83+
rewrite map_inj_uniq ?iota_uniq // => i j /eqP.
84+
by rewrite eqn_exp2l // => /eqP.
85+
rewrite -dvdn_divisors ?expn_gt0 ?prime_gt0 //.
86+
apply/(dvdn_pfactor _ _ pP)/idP => [[m mLn ->]|/mapP[m Hm ->]].
87+
by apply: map_f; rewrite mem_iota.
88+
by exists m => //; rewrite mem_iota in Hm.
89+
Qed.
90+
2991
Lemma divisorsM m n :
3092
coprime m n ->
3193
divisors (m * n) = sort leq [seq x * y | x <- divisors m, y <- divisors n].
@@ -66,10 +128,89 @@ exists (gcdn i m, gcdn i n); rewrite -!dvdn_divisors ?dvdn_gcdl ?dvdn_gcdr //=.
66128
by rewrite -coprime_gcdnM.
67129
Qed.
68130

131+
Lemma big_sort R (op : SemiGroup.com_law R) (x : R) (I : eqType)
132+
(r : seq I) (s : rel I) (P : pred I) (F : I -> R) :
133+
\big[op/x]_(i <- sort s r | P i) F i = \big[op/x]_(i <- r | P i) F i.
134+
Proof. by apply: perm_big; rewrite ?perm_sort. Qed.
135+
136+
Lemma big_divisors R (x : R) (op : SemiGroup.com_law R) (F : nat -> R) n :
137+
0 < n ->
138+
\big[op/x]_(i <- divisors n) F i = \big[op/x]_(i < n.+1 | i %| n) F i.
139+
Proof.
140+
move=> n_gt0.
141+
rewrite -(@big_mkord _ _ _ _ (fun i => i %| n)) -[RHS]big_filter.
142+
apply/perm_big/uniq_perm => [||i]; first by apply: divisors_uniq.
143+
by apply/filter_uniq/iota_uniq.
144+
rewrite -dvdn_divisors // mem_filter /index_iota mem_iota subn0 ltnS leq0n.
145+
by case: (_ %| _) (@dvdn_leq i _ n_gt0) => // ->.
146+
Qed.
147+
69148
Definition ndivisors n := size (divisors n).
70149

71-
Lemma ndivisorsM m n :
72-
coprime m n -> ndivisors (m * n) = ndivisors m * ndivisors n.
150+
Lemma ndivisors_prime p : prime p -> ndivisors p = 2.
151+
Proof. by rewrite /ndivisors divisors_prime_eq // => /eqP->. Qed.
152+
153+
Lemma ndivisors_primeX p n : prime p -> ndivisors (p ^ n) = n.+1.
154+
Proof.
155+
by move=> pP; rewrite /ndivisors divisors_primeX // size_map size_iota.
156+
Qed.
157+
158+
Lemma ndivisors_is_nmul : is_nmul ndivisors.
159+
Proof.
160+
move=> m n mCn.
161+
by rewrite [in LHS]/ndivisors divisorsM // size_sort size_allpairs.
162+
Qed.
163+
164+
Lemma big_divisorM F m n :
165+
coprime m n -> is_nmul F ->
166+
\sum_(i <- divisors (m * n)) F i =
167+
\sum_(i <- divisors m) \sum_(j <- divisors n) F (i * j).
168+
Proof.
169+
by move=> Hcm HF; rewrite divisorsM // big_sort /= big_allpairs_dep_idem //=.
170+
Qed.
171+
172+
Lemma is_nmul_sum F :
173+
is_nmul F -> is_nmul (fun n => \sum_(i <- divisors n) F i).
174+
Proof.
175+
move=> HF m n mCn.
176+
rewrite big_divisorM // big_distrl /= [LHS]big_seq_cond [RHS]big_seq_cond.
177+
apply: eq_bigr => i; rewrite andbT => Hi.
178+
rewrite big_distrr [LHS]big_seq_cond [RHS]big_seq_cond.
179+
apply: eq_bigr => j; rewrite andbT => Hj.
180+
apply: HF.
181+
case: m mCn Hi Hj => [|m].
182+
by rewrite /coprime gcd0n => /eqP->; rewrite !inE => /eqP-> /eqP->.
183+
case: n => [|n mCn].
184+
by rewrite /coprime gcdn0 => /eqP->; rewrite !inE => /eqP-> /eqP->.
185+
rewrite -!dvdn_divisors // => Hi Hj.
186+
by apply: coprime_dvdr Hj (coprime_dvdl Hi _).
187+
Qed.
188+
189+
Lemma liouville_divisors n :
190+
\sum_(i <- divisors n) (ndivisors i) ^ 3 =
191+
(\sum_(i <- divisors n) (ndivisors i)) ^ 2.
73192
Proof.
74-
by move=> mCn; rewrite [in LHS]/ndivisors divisorsM // size_sort size_allpairs.
193+
pose F n := \sum_(i <- divisors n) ndivisors i ^ 3; rewrite -/(F n).
194+
have HF : is_nmul F by apply/is_nmul_sum/is_nmulX/ndivisors_is_nmul.
195+
pose G n := (\sum_(i <- divisors n) ndivisors i) ^ 2; rewrite -/(G n).
196+
have HG : is_nmul G by apply/is_nmulX/is_nmul_sum/ndivisors_is_nmul.
197+
have [m nLm] := ubnP n.
198+
elim: m n nLm => // n IH [|[|m nLm]].
199+
- by rewrite /F /G !big_cons !big_nil.
200+
- by rewrite /F /G !big_cons !big_nil.
201+
have [p pP pDm] := pdivP (isT : 1 < m.+2).
202+
have [k kCm kE] := pfactor_coprime pP (isT : 0 < m.+2).
203+
have kCp1 : coprime k (p ^ logn p m.+2) by apply/coprimeXr; rewrite coprime_sym.
204+
have kLn : k < n.
205+
rewrite -ltnS (leq_ltn_trans _ nLm) // kE -[X in X < _]muln1 ltn_mul2l.
206+
case: (k) (kE) => //= _ _.
207+
by rewrite -[1](expn0 p) ltn_exp2l ?prime_gt1 // -pfactor_dvdn.
208+
rewrite kE HF // HG // IH //; congr (_ * _).
209+
rewrite /F /G divisors_primeX // !big_map.
210+
set u := _.+1.
211+
under eq_bigr do rewrite ndivisors_primeX //.
212+
under [in RHS]eq_bigr do rewrite ndivisors_primeX //.
213+
rewrite -[u]subn0 -[iota _ _]/(index_iota 0 u) !big_mkord.
214+
have := nicomachus u.+1.
215+
by rewrite big_ord_recl [X in _ = X ^ 2 -> _]big_ord_recl !add0n.
75216
Qed.

‎meta.yml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,10 @@ description: |-
7474
7575
[All prime numbers (except 2 and 3) are next to a multiple of 6](./prime6.v)
7676
77+
[Nicomachus Theorem about summation of cube](./nicomachus.v)
78+
79+
[Liouville Theorem about number's divisors](./liouville.v)
80+
7781
A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).
7882
7983
A note about addition chain is available [here](https://hal.science/hal-04971933).

0 commit comments

Comments
 (0)