Skip to content

Commit b91c720

Browse files
therythery
committed
Add Hermite's identity
1 parent 30b65bf commit b91c720

5 files changed

Lines changed: 196 additions & 13 deletions

File tree

‎README.md‎

Lines changed: 2 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,8 @@ Some extra material for mathcomp
8585

8686
[Binomial equation about taking 2 segments from n points](./binception.v)
8787

88+
[Hermite's identity](./hermite.v)
89+
8890
A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).
8991

9092
A note about addition chain is available [here](https://hal.science/hal-04971933).
@@ -108,15 +110,3 @@ A note about factorions is available [here](https://inria.hal.science/hal-052656
108110
- Related publication(s): none
109111

110112
## Building and installation instructions
111-
112-
To build and install manually, do:
113-
114-
``` shell
115-
git clone https://github.com/thery/mathcomp-extra.git
116-
cd mathcomp-extra
117-
make # or make -j <number-of-cores-on-your-machine>
118-
make install
119-
```
120-
121-
122-

‎_CoqProject‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -38,4 +38,5 @@ prime6.v
3838
liouville.v
3939
nicomachus.v
4040
repeatxy.v
41-
binception.v
41+
binception.v
42+
hermite.v

‎coq-mathcomp-extra.opam‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -85,6 +85,8 @@ Some extra material for mathcomp
8585

8686
[Binomial equation about taking 2 segments from n points](./binception.v)
8787

88+
[Hermite's identity](./hermite.v)
89+
8890
A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).
8991

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

‎hermite.v‎

Lines changed: 188 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,188 @@
1+
(******************************************************************************)
2+
(* *)
3+
(* *)
4+
(* Proof of Hermite's identity *)
5+
(* *)
6+
(* `⌊x⌋ : floor function *)
7+
(* `⌈x⌋ : nearest-int function with `⌈ n + 1/2 ⌋ = n + 1 *)
8+
(* *)
9+
(* hermite's identity : `⌊nx⌋ = \sum_(k < n) `⌊x + k / n⌋ *)
10+
(* *)
11+
(* special case when n = 2 : `⌊2x⌋ - `⌊x⌋ = `⌈x⌋ *)
12+
(******************************************************************************)
13+
14+
From mathcomp Require Import all_boot all_order all_algebra.
15+
16+
Local Open Scope ring_scope.
17+
18+
Import GRing.Theory Num.Theory Order.TTheory.
19+
20+
Section Hermite.
21+
22+
Variable R : archiRealFieldType.
23+
24+
Local Notation " `⌊ x ⌋ " := ((Num.floor x)%:~R) (format "`⌊ x ⌋" ).
25+
26+
Definition frac_part (x : R) := x - `⌊ x ⌋.
27+
28+
Local Notation " `{ x } " := (frac_part x) (format "`{ x }" ).
29+
30+
Lemma fracE (x : R) : x = `⌊x⌋ + `{x}.
31+
Proof. by rewrite /frac addrC subrK. Qed.
32+
33+
Lemma frac_le (x : R) : 0 <= `{x} < 1.
34+
Proof. by rewrite subr_ge0 ltrBlDl floor_le -(intrD _ _ 1) floorD1_gt. Qed.
35+
36+
Definition half_up (x : R) : R := `⌊x + 2^-1⌋.
37+
38+
Local Notation " `⌈ x ⌋ " := (half_up x) (format "`⌈ x ⌋" ).
39+
40+
Lemma half_up_le x : `⌊x⌋ <= `⌈x⌋.
41+
Proof.
42+
rewrite ler_int; apply: le_floor.
43+
by rewrite -[X in X <= _]addr0 lerD2l invr_ge0 (ler_nat _ 0 2).
44+
Qed.
45+
46+
Lemma half_up_gt x : `⌈x⌋ <= `⌊x⌋ + 1.
47+
Proof.
48+
rewrite -(intrD _ _ 1) -(floor1 R) -floorDrz // ler_int; apply: le_floor.
49+
by rewrite lerD2l invf_le1 // (ler_nat _ 1 2).
50+
Qed.
51+
52+
Inductive half_up_build (x : R) : R -> Prop :=
53+
half_up_build_floor : x < `⌊x⌋ + 2^-1 -> half_up_build x `⌊x⌋
54+
| half_up_build_ceil : `⌊x⌋ + 2^-1 <= x -> half_up_build x (`⌊x⌋ + 1)%R.
55+
56+
Lemma half_upP x : half_up_build x `⌈x⌋.
57+
Proof.
58+
have [xLx2|x2Lx] := leP (`⌊x⌋ + 2^-1) x; last first.
59+
suff -> : `⌈x⌋ = `⌊x⌋ by apply/half_up_build_floor.
60+
suff x2E : Num.floor (x + 2^-1) = Num.floor x.
61+
by congr (_%:~R); apply/sym_equal/eqP; rewrite floor_eq x2E floor_itv.
62+
apply/floor_def.
63+
rewrite intrD (le_trans (floor_le _) _) //=; last first.
64+
by rewrite lerDl invr_ge0 (ler_nat _ 0 2).
65+
by rewrite [1%:~R]splitr mul1r addrA ltrD2r.
66+
suff -> : `⌈x⌋ = `⌊x⌋ + 1 by apply/half_up_build_ceil.
67+
suff x2E : Num.floor (x + 2^-1) = Num.floor x + 1
68+
by rewrite /half_up x2E intrD.
69+
apply/floor_def.
70+
rewrite 2!intrD [1%:~R]splitr mul1r addrA lerD2r xLx2 /= addrA ltrD2r.
71+
by rewrite (lt_le_trans (floorD1_gt _)) // lerDl invr_ge0 (ler_nat _ 0 2).
72+
Qed.
73+
74+
Lemma half_up_half : `⌈2^-1⌋ = 1.
75+
Proof.
76+
by have := splitr (1 : R); rewrite mul1r /half_up => <-; rewrite floorK.
77+
Qed.
78+
79+
Lemma half_up_nearest (x : R) (y : int ): `|x - `⌈x⌋| <= `|x - y%:~R|.
80+
Proof.
81+
have [yLx|xLy] := leP y (Num.floor x).
82+
suff F : `|x - `⌈x⌋| <= `|x - `⌊x⌋|.
83+
apply: le_trans F _.
84+
rewrite !ger0_norm ?subr_ge0 ?floor_le //; first by rewrite lerB ?ler_int.
85+
by rewrite (le_trans _ (floor_le _)) // ler_int.
86+
have [//|xLx2] := half_upP.
87+
rewrite [X in _ <= X]ger0_norm; last by rewrite subr_ge0 floor_le.
88+
rewrite ler0_norm; last first.
89+
by rewrite subr_le0; have /ltW := floorD1_gt x; rewrite intrD.
90+
rewrite opprB.
91+
apply: le_trans (_ : 2^-1 <= _); last by rewrite lerBrDl.
92+
rewrite addrAC [X in _ + X <= _]splitr -[X in _ <= X]add0r mul1r addrA.
93+
by rewrite lerD2r addrAC lerBlDl addr0.
94+
rewrite -lezD1 in xLy.
95+
rewrite [X in _ <= X]ler0_norm ?opprB; last first.
96+
by rewrite subr_le0 (le_trans (ltW (floorD1_gt _))) // ler_int.
97+
suff F : `|x - `⌈x⌋| <= `|x - `⌊x + 1⌋|.
98+
apply: le_trans F _.
99+
rewrite ler0_norm ?opprB; last first.
100+
by rewrite subr_le0 floorDrz // floor1 (ltW (floorD1_gt _)).
101+
by rewrite lerD2r floorDrz // floor1 ler_int.
102+
have [xLx2|x2Lx] := half_upP; last by rewrite floorDrz // floor1 intrD.
103+
rewrite [X in _ <= X]ler0_norm ?opprB; last first.
104+
by rewrite subr_le0 floorDrz // floor1 (ltW (floorD1_gt _)).
105+
have xLx2' := ltW xLx2.
106+
rewrite ger0_norm; last by rewrite subr_ge0 floor_le.
107+
apply: le_trans (_ : 2^-1 <= _); first by rewrite lerBlDl.
108+
rewrite floorDrz // floor1 intrD addrAC.
109+
rewrite [X in _ <= _ + X]splitr -[X in X <= _]add0r mul1r addrA lerD2r.
110+
by rewrite addrAC subr_ge0.
111+
Qed.
112+
113+
Lemma hermite_id (n : nat) x :
114+
`⌊n%:R * x⌋ = \sum_(k < n) (`⌊x + k%:R / (n%:R:R)⌋ : R).
115+
Proof.
116+
have [//|n_gt0|->] := ltngtP n 0; last by rewrite big_ord0 mul0r floor0.
117+
have n_neq0 : n%:R != 0 :> R by rewrite (eqr_nat _ _ 0); case: (n) n_gt0.
118+
have nr_nt0 : (0 : R) < n%:R by rewrite (ltr_nat _ 0).
119+
pose g (k : nat) : R := `⌊x + k%:R / (n%:R : R)⌋.
120+
rewrite -(@big_mkord _ _ _ _ xpredT g) {}/g.
121+
rewrite (fracE x) mulrDr addrC -(intrM _ (Posz n)) floorDrz // intrD.
122+
rewrite [X in _ + X = _]floorK // intrM.
123+
under eq_bigr do rewrite -addrA addrC floorDrz // intrD.
124+
rewrite big_split /=.
125+
rewrite sumr_const_nat subn0.
126+
rewrite [in X in _ = _ + X]floorK // [X in _ + X = _]mulr_natl.
127+
suff <- : `⌊n%:R * `{ x}⌋ = (\sum_(0 <= i < n) `⌊`{ x} + i%:R / n%:R⌋ : R).
128+
by [].
129+
have /andP[x_ge0 x_lt1] := frac_le x.
130+
pose fnx := Num.floor (n%:R * `{x}).
131+
have fnx_pos : 0 <= fnx by rewrite floor_ge0 mulr_ge0.
132+
have fnxLn : (`|fnx| <= n)%N.
133+
rewrite -lez_nat intOrdered.gez0_norm //.
134+
rewrite -(ler_int R) (le_trans (floor_le _)) //.
135+
by rewrite -[X in _ <= X]mulr1 ler_pM // ltW.
136+
pose t := (n - `|fnx|)%N.
137+
pose cnx := Num.ceil (n%:R * (1 - `{x})).
138+
have cnx_pos : 0 <= cnx.
139+
by rewrite ceil_ge0 (lt_le_trans (ltrN10 R)) // mulr_ge0 // subr_ge0 ltW.
140+
have nLcnx : (`|cnx| <= n)%N.
141+
rewrite -(ler_nat R) natr_absz ger0_norm //.
142+
have /le_ceil : n%:R * (1 - `{x}) <= n%:R.
143+
by rewrite mulrBr mulr1 gerBl mulr_ge0.
144+
rewrite -/cnx -(ler_int R) //.
145+
suff /eqP->// : (Num.Def.ceil (n%:R : R))%:~R == (n%:R : R) by [].
146+
by rewrite -intrEceil.
147+
have tE : t = (`|cnx| : nat).
148+
rewrite /cnx mulrBr mulr1 addrC ceilDrz // ceilNfloor opprK addrC.
149+
have -> : Num.Def.ceil (n%:R : R) = (n : int).
150+
by apply/eqP; rewrite -(eqr_int R) -intrEceil.
151+
by rewrite -[LHS]distnEl ?intOrdered.gez0_norm.
152+
rewrite (big_cat_nat_idem _ (_ : 0 <= t)%N) //=; last 2 first.
153+
- by rewrite add0r.
154+
- by rewrite leq_subr.
155+
rewrite big_nat_cond /= big1 ?add0r => [|i iLt]; last first.
156+
rewrite andbT tE in iLt.
157+
have iLt' : (i%:~R < n%:R * (1 - `{x})).
158+
rewrite -real_ceil_gt_int; last by rewrite !realE mulr_ge0 // subr_ge0 ltW.
159+
by rewrite -ltz_nat // intOrdered.gez0_norm in iLt.
160+
have -> : 0 = 0%:~R :>R by [].
161+
congr (_%:~R); apply: floor_def.
162+
rewrite add0r addr_ge0 //=; last by rewrite divr_ge0.
163+
rewrite -[`{x}](mulfK n_neq0) -mulrDl ltr_pdivrMr // mul1r.
164+
by rewrite -ltrBrDl -[X in _ < X - _]mul1r -mulrBl mulrC.
165+
rewrite big_nat_cond (eq_bigr (fun _ => 1%R)).
166+
rewrite -big_nat_cond sumr_const_nat natrB ?tE //.
167+
rewrite -tE natrB ?opprB //.
168+
by rewrite addrC subrK natr_absz ger0_norm.
169+
move=> i; rewrite andbT => /andP[tLi iLn].
170+
rewrite tE in tLi.
171+
rewrite -[RHS]/(1%:~R).
172+
congr (_%:~R); apply: floor_def; apply/andP; split.
173+
rewrite -[`{x}](mulfK n_neq0) -mulrDl ler_pdivlMr // mul1r.
174+
rewrite -lerBlDl -[X in X - _ <= _]mul1r -mulrBl mulrC.
175+
rewrite (le_trans (ceil_ge _)) -/cnx //.
176+
by rewrite -(ler_nat R) natr_absz ger0_norm in tLi.
177+
rewrite intrD (le_lt_trans (_ : _ <= `{x} + 1)) //.
178+
by rewrite lerD // ler_pdivrMr // mul1r ler_nat ltnW.
179+
by rewrite ltr_leD.
180+
Qed.
181+
182+
Lemma hermite_id2 x : `⌊2 * x⌋ - `⌊x⌋ = `⌈x⌋.
183+
Proof.
184+
rewrite hermite_id big_ord_recr /= big_ord1 mul0r addr0.
185+
by rewrite mul1r /half_up addrAC subrr add0r.
186+
Qed.
187+
188+
End Hermite.

‎meta.yml‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -82,6 +82,8 @@ description: |-
8282
8383
[Binomial equation about taking 2 segments from n points](./binception.v)
8484
85+
[Hermite's identity](./hermite.v)
86+
8587
A note about sorting network is available [here](https://hal.inria.fr/hal-03585618).
8688
8789
A note about addition chain is available [here](https://hal.science/hal-04971933).

0 commit comments

Comments
 (0)