-
Notifications
You must be signed in to change notification settings - Fork 15
/
Copy pathconvex.v
3073 lines (2574 loc) · 111 KB
/
convex.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* infotheo: information theory and error-correcting codes in Coq *)
(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *)
From HB Require Import structures.
From mathcomp Require Import all_ssreflect ssralg fingroup perm matrix.
From mathcomp Require Import mathcomp_extra boolp classical_sets Rstruct.
From mathcomp Require Import ssrnum archimedean ereal.
From mathcomp Require Import lra Rstruct reals.
Require Import Reals.
Require Import ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb.
Require Import realType_ext fdist.
From mathcomp Require vector.
Undelimit Scope R_scope.
Delimit Scope R_scope with coqR.
(******************************************************************************)
(* Convexity *)
(* *)
(* This file provides the definition of convex spaces over a choiceType and *)
(* of real cones, and use them to define convex sets, hulls, to show that *)
(* probability distributions form convex spaces, and to define convex *)
(* functions. *)
(* *)
(* Convex spaces: *)
(* convType == the type of convex spaces, i.e., a choiceType with an *)
(* operator x <| p |> y where p is a probability *)
(* satisfying the following axioms: *)
(* conv1 == a <| 1%:pr |> b = a. *)
(* convmm == a <| p |> a = a. *)
(* convC == a <| p |> b = b <| p.~%:pr |> a. *)
(* convA == a <| p |> (b <| q |> c) = *)
(* (a <| [r_of p, q] |> b) <| [s_of p, q] |> c. *)
(* <|>_d f == generalization of the conv operator . <| . |> . *)
(* type: forall A n, {fdist 'I_n} -> ('I_n -> A) -> A *)
(* d is a finite distribution {fdist 'I_n}, f is a *)
(* sequence of points 'I_n -> A, A is a convType *)
(* {affine T -> U} == affine function: homomorphism between convex spaces *)
(* <$>_d f := <|>_d (f \o enum_val) *)
(* type: forall A T, {fdist T} -> (T -> A) -> A *)
(* d is a finite distribution {fdist T}, f is a sequence *)
(* of points T -> A, A is a convType, T, is a finType *)
(* segment x y := (fun p => conv p x y) @` [set: prob] *)
(* *)
(* scaled == Zero or a pair of a positive real (Rpos) with a point *)
(* in some type (i.e., a "scaled point" noted p *: a, *)
(* scope scaled_scope *)
(* S1 a := 1%:pos *: a *)
(* isQuasiRealCone == mixin of quasi real cones *)
(* see Def. 4.5 of [Varacca & Winskell, MSCS, 2006] *)
(* addpt == addition *)
(* scalept == scaling *)
(* \ssum_(i <- r) F == iterated addpt *)
(* isRealCone == mixin of real cones *)
(* Def. 4.5 of [Varacca & Winskell, MSCS, 2006] *)
(* The mixins for real cones are instantiated with the type scaled A where *)
(* A is a convType, addpt := rx + qy = (r+q)(x <| r/(r+q) |> y), and *)
(* scalept := scalept r qy = (r*q)y. *)
(* Moreover, when A is a convType, scaled A can be equipped with a *)
(* structure of convex space by taking *)
(* convpt p x y := addpt (scalept p x) (scalept p.~ y). This is the canonical *)
(* embedding of convex spaces into real cones. *)
(* *)
(* More lemmas about convex spaces, including key lemmas by Stone: *)
(* convACA == the entropic identity, i.e., *)
(* (a <|q|> b) <|p|> (c <|q|> d) = *)
(* (a <|p|> c) <|q|> (b <|p|> d) *)
(* *)
(* hull X == the convex hull of set X : set T where T is a convType *)
(* is_convex_set == Boolean predicate that characterizes convex sets over a *)
(* convType *)
(* {convex_set A} == an object X of type "set A" where A is a convType and X *)
(* is convex *)
(* *)
(* Instances of convex spaces: *)
(* R_convType == R *)
(* funConvType == functions A -> B with A a choiceType and B a convType *)
(* depfunConvType == functions forall (a:A), B a with A a choiceType and B i *)
(* is a A -> convType *)
(* pairConvType == pairs of convTypes *)
(* fdist_convType == finite distributions *)
(* *)
(* orderedconvType == ordered convex space, a convType augmented with an *)
(* order *)
(* Instances: R, T -> U (T convType, U orderedConvType), opposite (see mkOpp) *)
(* *)
(* Reference: R. Affeldt, J. Garrigue, T. Saikawa. Formal adventures in *)
(* convex and conical spaces. CICM 2020 *)
(* *)
(* Definitions of convex, concave, affine functions *)
(* affine_functionP == a function is affine iff it is convex and concave *)
(* *)
(* Lemmas: *)
(* image_preserves_convex_hull == the image of a convex hull is the convex *)
(* hull of the image *)
(* *)
(* Application to real analysis: *)
(* Definition of convex sets for R *)
(* Lemma second_derivative_convexf_pt == twice derivable is convex *)
(******************************************************************************)
Reserved Notation "x <| p |> y" (format "x <| p |> y", at level 49).
Reserved Notation "{ 'convex_set' T }" (format "{ 'convex_set' T }").
Reserved Notation "'<|>_' d f" (at level 36, f at level 36, d at level 0,
format "<|>_ d f").
Reserved Notation "'<$>_' d f" (at level 36, f at level 36, d at level 0,
format "<$>_ d f").
Reserved Notation "\ssum_ ( i <- r | P ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \ssum_ ( i <- r | P ) '/ ' F ']'").
Reserved Notation "\ssum_ ( i <- r ) F"
(at level 41, F at level 41, i, r at level 50,
format "'[' \ssum_ ( i <- r ) '/ ' F ']'").
Reserved Notation "\ssum_ ( i | P ) F"
(at level 41, F at level 41, i at level 50,
format "'[' \ssum_ ( i | P ) '/ ' F ']'").
Reserved Notation "\ssum_ i F"
(at level 41, F at level 41, i at level 0, right associativity,
format "'[' \ssum_ i '/ ' F ']'").
Reserved Notation "\ssum_ ( i : t ) F"
(at level 41, F at level 41, i at level 50).
Reserved Notation "\ssum_ ( i < n | P ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \ssum_ ( i < n | P ) '/ ' F ']'").
Reserved Notation "\ssum_ ( i < n ) F"
(at level 41, F at level 41, i, n at level 50,
format "'[' \ssum_ ( i < n ) '/ ' F ']'").
Reserved Notation "{ 'affine' T '->' R }"
(at level 36, T, R at next level, format "{ 'affine' T '->' R }").
Reserved Notation "p *: a" (at level 40).
Declare Scope convex_scope.
Declare Scope ordered_convex_scope.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.
Local Open Scope reals_ext_scope.
Local Open Scope fdist_scope.
Import Order.POrderTheory GRing.Theory Num.Theory.
Local Notation "{ 'fdist' T }" := (_ .-fdist T) : fdist_scope.
#[export] Hint Extern 0 (0 <= _)%coqR =>
solve [apply/RleP/(FDist.ge0 _)] : core.
#[export] Hint Extern 0 (_ <= 1)%coqR =>
solve [apply/RleP/(FDist.le1 _)] : core.
#[export] Hint Extern 0 (0 <= Prob.p _)%coqR =>
solve [apply/RleP/(prob_ge0 _)] : core.
#[export] Hint Extern 0 (Prob.p _ <= 1)%coqR =>
solve [apply/RleP/(prob_le1 _)] : core.
#[export] Hint Extern 0 (onem _ <= 1)%coqR =>
exact/RleP/onem_le1 : core.
#[export] Hint Extern 0 (0 <= onem _)%coqR =>
exact/RleP/onem_ge0 : core.
Fixpoint Convn (A : Type) (f : {prob R} -> A -> A -> A) n : {fdist 'I_n} -> ('I_n -> A) -> A :=
match n return forall (e : {fdist 'I_n}) (g : 'I_n -> A), A with
| O => fun e g => False_rect A (fdistI0_False e)
| m.+1 => fun e g =>
match Bool.bool_dec (e ord0 == 1%coqR) true with
| left _ => g ord0
| right H => let G := fun i => g (fdist_del_idx ord0 i) in
f (probfdist e ord0) (g ord0) (Convn f (fdist_del (Bool.eq_true_not_negb _ H)) G)
end
end.
HB.mixin Record isConvexSpace0 T of Choice T := {
conv : {prob R} -> T -> T -> T ;
convn : forall n, {fdist 'I_n} -> ('I_n -> T) -> T ;
convnE : forall n d g, convn n d g = Convn conv d g ;
conv1 : forall a b, conv 1%:pr a b = a ;
convmm : forall p a, conv p a a = a ;
convC : forall p a b, conv p a b = conv (onem (Prob.p p))%:pr b a ;
convA : forall (p q : {prob R}) (a b c : T),
conv p a (conv q b c) = conv [s_of p, q] (conv [r_of p, q] a b) c }.
#[short(type=convType)]
HB.structure Definition ConvexSpace := {T of isConvexSpace0 T & }.
Arguments convn {s n}.
Notation "a <| p |> b" := (conv p a b) : convex_scope.
Local Open Scope convex_scope.
Section convex_space_lemmas.
Variables A : convType.
Implicit Types a b : A.
Import Reals_ext.
Lemma conv0 a b : a <| 0%:pr |> b = b.
Proof.
by rewrite convC /= (_ : _ %:pr = 1%:pr) ?conv1 //; apply/val_inj/onem0.
Qed.
Let Convn_fdist1 (n : nat) (j : 'I_n) (g : 'I_n -> A) :
convn (fdist1 j) g = g j.
Proof.
elim: n j g => [[] [] //|n IH j g /=].
rewrite convnE {1}/Convn.
case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb b01].
rewrite fdist1E; case j0 : (_ == _) => /=.
by move=> _; rewrite (eqP j0).
by move/eqP; rewrite eq_sym R1E oner_eq0.
rewrite (_ : probfdist _ _ = 0%:pr) ?conv0; last first.
apply val_inj => /=; move: b01; rewrite !fdist1E => j0.
by case j0' : (_ == _) => //; rewrite j0' eqxx in j0.
have j0 : ord0 != j by apply: contra b01 => /eqP <-; rewrite fdist1xx.
have j0' : 0 < j by rewrite lt0n; apply: contra j0 => /eqP j0; apply/eqP/val_inj.
move=> [:H]; have @j' : 'I_n.
by apply: (@Ordinal _ j.-1 _); abstract: H; rewrite prednK // -ltnS.
rewrite (_ : fdist_del b01 = fdist1 j'); last first.
apply/fdist_ext => /= k.
rewrite fdist_delE fdistD1E /= !fdist1E /= (negbTE j0) subr0 divr1.
congr (GRing.natmul _ (nat_of_bool _)).
move R : (k == _) => [|].
- apply/eqP/val_inj; rewrite /= /bump leq0n add1n.
by move/eqP : R => -> /=; rewrite prednK // lt0n.
- apply: contraFF R => /eqP.
move/(congr1 val) => /=; rewrite /bump leq0n add1n => kj.
by apply/eqP/val_inj; rewrite /= -kj.
rewrite -/(Convn _ _) -convnE IH /fdist_del_idx ltn0; congr g.
by apply val_inj; rewrite /= /bump leq0n add1n prednK // lt0n.
Qed.
Let ConvnIE n (g : 'I_n.+1 -> A) (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%coqR) :
convn d g = (g ord0) <| probfdist d ord0 |>
(convn (fdist_del i1) (fun x => g (fdist_del_idx ord0 x))).
Proof.
rewrite !convnE /=; case: Bool.bool_dec => /= [|/Bool.eq_true_not_negb] H.
exfalso; by rewrite (eqP H) eqxx in i1.
by rewrite (eq_irrelevance H i1).
Qed.
Let ConvnI1E (g : 'I_1 -> A) (e : {fdist 'I_1}) : convn e g = g ord0.
Proof.
rewrite convnE /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H.
exfalso; move/eqP: H; apply.
by apply/eqP; rewrite fdist1E1 (fdist1I1 e).
Qed.
Let ConvnI2E (g : 'I_2 -> A) (d : {fdist 'I_2}) :
convn d g = (g ord0) <| probfdist d ord0 |> (g (lift ord0 ord0)).
Proof.
have [/eqP|i1] := eqVneq (d ord0) 1%coqR.
rewrite fdist1E1 => /eqP ->; rewrite Convn_fdist1.
rewrite (_ : probfdist _ _ = 1%:pr) ?conv1 //.
by apply val_inj; rewrite /= fdist1xx.
rewrite ConvnIE; congr (conv _ _ _).
by rewrite ConvnI1E /fdist_del_idx ltnn.
Qed.
End convex_space_lemmas.
Section segment.
Variable A : convType.
Definition segment (x y : A) : set A := (fun p => conv p x y) @` [set: {prob R}].
Lemma segment_sym u v : (segment u v `<=` segment v u)%classic.
Proof. by move=> x [p _ <-]; exists ((Prob.p p).~%:pr); rewrite -?convC. Qed.
Lemma segmentC u v : segment u v = segment v u.
Proof. by rewrite eqEsubset; split; exact: segment_sym. Qed.
Lemma segmentL x y : segment x y x. Proof. by exists 1%:pr; rewrite ?conv1. Qed.
Lemma segmentR x y : segment x y y. Proof. by exists 0%:pr; rewrite ?conv0. Qed.
End segment.
Definition affine (U V : convType) (f : U -> V) :=
forall p, {morph f : a b / a <| p |> b >-> a <| p |> b}.
HB.mixin Record isAffine (U V : convType) (f : U -> V) := {
affine_conv : affine f }.
HB.structure Definition Affine (U V : convType) := {f of isAffine U V f}.
Notation "{ 'affine' T '->' R }" := (Affine.type T R) : convex_scope.
Section affine_function_instances.
Variables (U V W : convType) (f : {affine V -> W}) (h : {affine U -> V}).
Let affine_idfun : affine (@idfun U). Proof. by []. Qed.
HB.instance Definition _ := isAffine.Build _ _ idfun affine_idfun.
Let affine_comp : affine (f \o h).
Proof. by move=> x y t /=; rewrite 2!affine_conv. Qed.
HB.instance Definition _ := isAffine.Build _ _ (f \o h) affine_comp.
End affine_function_instances.
Declare Scope scaled_scope.
Delimit Scope scaled_scope with scaled.
Section scaled.
Variable A : Type.
(* Note: we need the argument of Scaled to be an Rpos, because otherwise
addpt cannot make a commutative monoid:
1) if addpt (Scaled 0 x) (Scaled 0 y) = Scaled 0 x commutativity fails
so at least we need addpt (Scaled 0 x) (Scaled 0 y) = Zero
2) if addpt (Scaled 0 x) Zero = Zero then left/right identity fail
2) if addpt (Scaled 0 x) Zero = Scaled 0 x then associativity fails
addpt (Scaled 0 x) (addpt (Scaled 0 y) (Scaled 0 z)) = Scaled 0 x
addpt (addpt (Scaled 0 x) (Scaled 0 y)) (Scaled 0 z) = Scaled 0 z
So we cannot allow 0 as argument to Scaled. *)
Inductive scaled := Scaled of Rpos & A | Zero.
Definition sum_of_scaled (m : scaled) : Rpos * A + unit :=
match m with Scaled r a => inl _ (r, a) | Zero => inr _ tt end.
Local Notation "p *: a" := (Scaled p a).
Definition scaled_of_sum (m : (Rpos * A) + unit) :=
match m with inl p => p.1 *: p.2 | inr n => Zero end.
Lemma sum_of_scaledK : cancel sum_of_scaled scaled_of_sum.
Proof. by case. Qed.
Definition S1 a : scaled := 1%:pos *: a.
Lemma Scaled_inj p : injective (Scaled p).
Proof. by move=> x y []. Qed.
Definition S1_inj : injective S1 := @Scaled_inj Rpos1.
Definition raw_weight (pt : scaled) : R := if pt is r *: _ then r else 0.
Lemma weight_ge0 pt : (0 <= raw_weight pt)%coqR.
Proof. by case: pt => /= [[x] /= /RltP/ltRW //|]. Qed.
Definition weight := mkNNFun weight_ge0.
Definition point pt : (weight pt > 0)%coqR -> A :=
match pt with
| t *: a => fun=> a
| Zero => fun H : (weight Zero > 0)%coqR => match ltRR 0 H with end
end.
Lemma point_Scaled p x H : @point (p *: x) H = x.
Proof. by []. Qed.
Lemma Scaled_point x H : mkRpos H *: @point x H = x.
Proof.
by case: x H => [p x|] H; [congr (_ *: _); apply val_inj | case: (ltRR 0)].
Qed.
End scaled.
Arguments Zero {A}.
Arguments point {A} pt.
Arguments weight {A}.
Notation "p *: a" := (Scaled p a) : scaled_scope.
HB.instance Definition _ (A : eqType) := Equality.copy (scaled A) (can_type (@sum_of_scaledK A)).
HB.instance Definition _ (A : choiceType) := Choice.copy (scaled A) (can_type (@sum_of_scaledK A)).
Section scaled_eqType.
Variable A : eqType.
Lemma S1_neq0 a : S1 a != @Zero A. Proof. by []. Qed.
(* NB: should go away once we do not need coqR anymore *)
Lemma weight_gt0 a : a != @Zero A -> (0 < weight a)%coqR.
Proof. by case: a => // p x _ /=. Qed.
Lemma weight_gt0b a : a != @Zero A -> (weight a > 0)%mcR.
Proof. by move=> ?; exact/RltP/weight_gt0. Qed.
Definition weight_neq0 a (a0 : a != @Zero A) := Rpos.mk (weight_gt0b a0).
Local Notation "[ 'point' 'of' x ]" := (@point _ _ (@weight_gt0 _ x))
(at level 0, format "[ 'point' 'of' x ]").
Local Notation "[ 'weight' 'of' x ]" := (weight_neq0 x)
(at level 0, format "[ 'weight' 'of' x ]").
Lemma point_S1 a : [point of S1_neq0 a] = a.
Proof. by []. Qed.
Lemma weight0_Zero a : weight a = 0%coqR -> a = @Zero A.
Proof. by case: a => //= r c /esym Hr; move/ltR_eqF: (Rpos_gt0 r) => /eqP. Qed.
End scaled_eqType.
Notation "[ 'point' 'of' x ]" := (@point _ _ (@weight_gt0 _ _ x))
(at level 0, format "[ 'point' 'of' x ]").
Notation "[ 'weight' 'of' x ]" := (weight_neq0 x)
(at level 0, format "[ 'weight' 'of' x ]").
HB.mixin Record isQuasiRealCone A of Choice A := {
addpt : A -> A -> A ;
zero : A ;
addptC : commutative addpt ;
addptA : associative addpt ;
addpt0 : right_id zero addpt ;
scalept : R -> A -> A ;
scale0pt : forall x, scalept 0%coqR x = zero ;
scale1pt : forall x, scalept 1%coqR x = x ;
scaleptDr : forall r, {morph scalept r : x y / addpt x y >-> addpt x y} ;
scaleptA : forall p q x, (0 <= p)%coqR -> (0 <= q)%coqR ->
scalept p (scalept q x) = scalept (p * q)%coqR x }.
#[short(type=quasiRealCone)]
HB.structure Definition QuasiRealCone := { A of isQuasiRealCone A & }.
Section quasireal_cone_theory.
Variable A : quasiRealCone.
Lemma add0pt : left_id (@zero A) addpt.
Proof. by move=> ?; rewrite addptC addpt0. Qed.
Lemma scalept0 p : (0 <= p)%coqR -> scalept p zero = @zero A.
Proof.
by move=> p0; rewrite -[in LHS](scale0pt zero) scaleptA// mulR0 scale0pt.
Qed.
HB.instance Definition _ :=
Monoid.isComLaw.Build A (@zero A) (@addpt A) addptA addptC add0pt.
Definition big_morph_scalept q :=
@big_morph _ _ (@scalept A q) zero addpt zero _ (@scaleptDr A q).
Local Notation "\ssum_ ( i <- r ) F" := (\big[addpt/@zero A]_(i <- r) F).
Local Notation "\ssum_ ( i : t ) F" := (\big[addpt/@zero A]_(i : t) F) (only parsing).
Local Notation "\ssum_ i F" := (\big[addpt/@zero A]_i F).
Local Notation "\ssum_ ( i | P ) F" := (\big[addpt/@zero A]_(i | P) F).
Local Notation "\ssum_ ( i < n | P ) F" := (\big[addpt/@zero A]_(i < n | P%B) F).
Local Notation "\ssum_ ( i < n ) F" := (\big[addpt/@zero A]_(i < n) F).
Definition barycenter (pts : seq A) := \ssum_(x <- pts) x.
Lemma barycenter_map (T : finType) (F : T -> A) :
barycenter [seq F i | i <- enum T] = \ssum_i F i.
Proof. by rewrite /barycenter big_map big_filter. Qed.
Lemma scalept_barycenter p (H : (0 <= p)%coqR) pts :
scalept p (barycenter pts) = barycenter [seq scalept p i | i <- pts].
Proof. by rewrite big_morph_scalept ?scalept0// /barycenter big_map. Qed.
Lemma ssum_perm n (F : 'I_n -> A) (pe : 'S_n) :
\ssum_(i < n) F i = \ssum_(i < n) F (pe i).
Proof.
rewrite -!barycenter_map /barycenter big_map map_comp big_map.
exact/perm_big/perm_eq_perm.
Qed.
End quasireal_cone_theory.
Notation "\ssum_ ( i <- r ) F" := (\big[addpt/@zero _]_(i <- r) F).
Notation "\ssum_ ( i <- r | P ) F" := (\big[addpt/@zero _]_(i <- r | P ) F).
Notation "\ssum_ ( i : t ) F" := (\big[addpt/@zero _]_(i : t) F) (only parsing).
Notation "\ssum_ i F" := (\big[addpt/@zero _]_i F).
Notation "\ssum_ ( i | P ) F" := (\big[addpt/@zero _]_(i | P) F).
Notation "\ssum_ ( i < n | P ) F" := (\big[addpt/@zero _]_(i < n | P%B) F).
Notation "\ssum_ ( i < n ) F" := (\big[addpt/@zero _]_(i < n) F).
HB.mixin Record isRealCone A of QuasiRealCone A := {
scaleptDl : forall (p q : R) (x : A), (0 <= p)%coqR -> (0 <= q)%coqR ->
scalept (p + q)%coqR x = addpt (scalept p x) (scalept q x)
}.
#[short(type=realCone)]
HB.structure Definition RealCone := { A of isRealCone A & }.
Section real_cone_theory.
Variable A : realCone.
Lemma scalept_sum (B : finType) (P : pred B) (F : B ->R^+) (x : A) :
scalept (\sum_(i | P i) F i) x = \ssum_(b | P b) scalept (F b) x.
Proof.
apply: (@proj1 _ (0 <= \sum_(i | P i) F i))%coqR.
apply: (big_ind2 (fun y q => scalept q x = y /\ (0 <= q)))%coqR.
+ by split; [rewrite scale0pt//|exact/Rle_refl].
+ move=> _ x2 _ y2 [<- ?] [<- ?].
by rewrite scaleptDl //; split => //; exact: addR_ge0.
+ by move=> i _; split => //; exact/nneg_f_ge0.
Qed.
Section barycenter_fdist_convn.
Variables (n : nat) (B : finType).
Variable p : R.-fdist 'I_n.
Variable q : 'I_n -> R.-fdist B.
Variable h : B -> A.
Lemma ssum_fdist_convn :
(* TODO: \ssum_(j in B) notation? *)
\ssum_(i < n) scalept (p i) (\ssum_(j <- enum B) scalept (q i j) (h j)) =
\ssum_(j <- enum B) scalept (fdist_convn p q j) (h j).
Proof.
transitivity (\ssum_i \ssum_(i0 <- enum B) scalept (p i) (scalept (q i i0) (h i0))).
by apply eq_bigr => i _; rewrite big_morph_scalept// scalept0.
rewrite exchange_big /=; apply eq_bigr => j _; rewrite fdist_convnE.
have HF i : (0 <= p i * q i j)%coqR by exact/mulR_ge0.
rewrite (scalept_sum _ (mkNNFun HF)) /=; apply eq_bigr => i _.
by rewrite scaleptA.
Qed.
End barycenter_fdist_convn.
End real_cone_theory.
Section real_cone_instance.
Import Order.TotalTheory.
Variable A : convType.
Local Open Scope R_scope.
Local Open Scope convex_scope.
Local Open Scope scaled_scope.
Let addpt (a b : scaled A) :=
match a, b with
| r *: x, q *: y => (r + q)%:pos *: (x <| (((r / (r + q))%:pos))%:pr |> y)
| _, Zero => a
| Zero, _ => b
end.
Let addptC' : commutative addpt.
Proof.
move=> [r x|] [q y|] //=; congr (_ *: _); first by apply: val_inj; rewrite /= addRC.
rewrite convC; congr (_ <| _ |> _); apply/val_inj => /=.
by rewrite RdivE RplusE onem_divRxxy.
Qed.
Let addptA' : associative addpt.
Proof.
move=> [p x|] [q y|] [r z|] //=; congr (_ *: _); first by apply val_inj; rewrite /= addRA.
rewrite convA; congr (_<| _ |> _); first exact: s_of_Rpos_probA.
congr (_ <| _ |> _).
rewrite /=.
exact: r_of_Rpos_probA. (* TODO: clean *)
Qed.
Let addpt0 : right_id (@Zero A) addpt. Proof. by case. Qed.
Let add0pt : left_id (@Zero A) addpt. Proof. by case. Qed.
Let scalept p (x : scaled A) :=
match Rlt_dec 0 p, x with
| left Hr, q *: y => (mkRpos Hr * q)%:pos *: y
| _, _ => Zero
end.
Let scale0pt x : scalept 0 x = Zero.
Proof. by rewrite /scalept; case: Rlt_dec => // Hr; case: (ltRR 0). Qed.
Let scalept0 p : scalept p Zero = Zero.
Proof. by rewrite /scalept; case: Rlt_dec. Qed.
Let scale1pt x : scalept 1 x = x.
Proof.
case: x => [r c|]; last by rewrite scalept0.
by rewrite /scalept/=; case: Rlt_dec => //= ?; congr (_ *: _); apply/val_inj => /=; rewrite mul1R.
Qed.
Let scaleptDr r : {morph scalept r : x y / addpt x y >-> addpt x y}.
Proof.
rewrite /scalept; case: Rlt_dec => // r_gt0 x y.
case: x => [p x|]; last by rewrite !add0pt.
case: y => [q y|]; last by rewrite !addpt0.
congr (_ *: _); first by apply val_inj => /=; rewrite mulRDr.
congr (_ <| _ |> _); apply val_inj; rewrite /= -mulRDr divRM ?gtR_eqF//.
by rewrite /Rdiv -(mulRAC r) mulRV ?mul1R // gtR_eqF.
Qed.
Let scalept_gt0 p (q : Rpos) x (p_gt0 : 0 < p) :
scalept p (q *: x) = (mkRpos p_gt0 * q)%:pos *: x.
Proof.
by rewrite /scalept; case: Rlt_dec => // Hr; congr (_ *: _); exact/val_inj.
Qed.
Let scaleptA p q x : 0 <= p -> 0 <= q -> scalept p (scalept q x) = scalept (p * q) x.
Proof.
case=> Hp; last by rewrite -Hp mul0R !scale0pt.
case=> Hq; last by rewrite -Hq mulR0 scale0pt scalept0.
case: x => [r x|]; rewrite ?scalept0 // !scalept_gt0; first exact: mulR_gt0.
by move=> Hpq; congr (_ *: _); apply val_inj => /=; rewrite mulRA.
Qed.
HB.instance Definition _ :=
isQuasiRealCone.Build (scaled A) addptC' addptA' addpt0 scale0pt scale1pt scaleptDr scaleptA.
Let scaleptDl p q x : 0 <= p -> 0 <= q ->
scalept (p + q) x = addpt (scalept p x) (scalept q x).
Proof.
case=> p0; last by rewrite -p0 scale0pt add0R add0pt.
case=> q0; last by rewrite -q0 scale0pt addR0 addpt0.
case: x => [r c|]; last by rewrite !scalept0.
rewrite !scalept_gt0 => [|pq0 /=]; first by apply addR_gt0.
by rewrite convmm; congr (_ *: _); apply val_inj; rewrite /= mulRDl.
Qed.
HB.instance Definition _ := @isRealCone.Build (scaled A) scaleptDl.
End real_cone_instance.
Section convpt_convex_space.
Variable A : convType.
Let convpt (p : {prob R}) (x y : scaled A) :=
addpt (scalept (Prob.p p) x) (scalept (Prob.p p).~ y).
Let convpt1 a b : convpt (1%:pr) a b = a.
Proof. by rewrite /convpt onem1 scale1pt scale0pt addpt0. Qed.
Let convptmm (p : {prob R}) a : convpt p a a = a.
Proof.
rewrite /convpt -scaleptDl//.
by rewrite RplusE onemKC scale1pt //.
Qed.
Let convptC (p : {prob R}) a b : convpt p a b = convpt ((Prob.p p).~)%:pr b a.
Proof. by rewrite [RHS]addptC onemK. Qed.
Let convptA (p q : {prob R}) a b c :
convpt p a (convpt q b c) = convpt [s_of p, q] (convpt [r_of p, q] a b) c.
Proof.
rewrite /convpt.
rewrite !scaleptDr !scaleptA //.
rewrite -[RHS]addptA; congr addpt.
by rewrite (p_is_rs p q) mulRC.
rewrite RmultE pq_is_rs mulrC -RmultE.
by rewrite s_of_pqE onemK RmultE.
Qed.
Let convn := Convn convpt.
HB.instance Definition _ :=
@isConvexSpace0.Build (scaled A) convpt convn (fun _ _ _ => erefl) convpt1 convptmm convptC convptA.
Lemma convptE p (a b : scaled A) : a <| p |> b = convpt p a b.
Proof. by []. Qed.
End convpt_convex_space.
Section scaled_convex.
Variable A : convType.
Local Open Scope R_scope.
Local Open Scope convex_scope.
Local Open Scope scaled_scope.
Lemma scalept_Scaled p q (x : A) : scalept p (q *: x) = scalept (p * q) (S1 x).
Proof.
rewrite /scalept /=.
case: Rlt_dec => Hp; case: Rlt_dec => Hpq //.
- congr (_ *: _); apply val_inj; by rewrite /= mulR1.
- elim Hpq; by apply /mulR_gt0.
- elim Hp; move/pmulR_lgt0: Hpq; exact.
Qed.
Lemma scalept_gt0 p (q : Rpos) (x : A) (H : 0 < p) :
scalept p (q *: x) = (mkRpos H * q)%:pos *: x.
Proof.
rewrite /scalept /= ; case: Rlt_dec => // Hr.
by congr (_ *: _); apply val_inj.
Qed.
Lemma addptE a b (a0 : a != @Zero A) (b0 : b != Zero) :
let p := [weight of a0] in
let q := [weight of b0] in
let x := [point of a0] in
let y := [point of b0] in
addpt a b = (p + q)%:pos *: (x <| ((p / (p + q))%:pos)%:pr |> y).
Proof.
move: a b => [p x|//] [pb y|//] /= in a0 b0 *.
by congr (_ *: (_ <| _ |> _)); exact: val_inj.
Qed.
Lemma weight_addpt : {morph @weight A : x y / addpt x y >-> x + y}.
Proof. move=> [p x|] [q y|] //=; by rewrite (add0R, addR0). Qed.
Lemma weight0 : weight (@Zero A) = 0. Proof. by []. Qed.
Lemma scalept_weight p (x : scaled A) : 0 <= p -> weight (scalept p x) = p * weight x.
Proof.
case=> [p0|<-]; last by rewrite scale0pt mul0R.
case: x => [r y|]; first by rewrite /= /scalept/=; case: Rlt_dec.
by rewrite scalept0 ?mulR0//; exact/ltRW.
Qed.
Lemma weight_barycenter (pts : seq (scaled A)) :
weight (barycenter pts) = \sum_(x <- pts) weight x.
Proof. by rewrite (big_morph weight weight_addpt weight0). Qed.
Section adjunction.
Lemma affine_S1 : affine (@S1 A).
Proof.
move=> p x y.
have /RleP[p0|p0] := prob_ge0 p; last first.
by rewrite (_ : p = 0%:pr) ?conv0 //; exact/val_inj.
have /RleP[p1|p1] := prob_le1 p; last first.
by rewrite (_ : p = 1%:pr) ?conv1 //; exact/val_inj.
rewrite convptE (scalept_gt0 _ _ p0) (@scalept_gt0 (Prob.p p).~).
exact/RltP/onem_gt0/RltP.
move=> mp0; congr (_ *: _) => /=.
apply/val_inj => /=; rewrite !mulR1.
by rewrite RplusE onemKC.
by congr (_ <| _ |> _); apply val_inj; rewrite /= !mulR1 addRC subRK divR1.
Qed.
HB.instance Definition _ := isAffine.Build _ _ (@S1 A) affine_S1.
End adjunction.
End scaled_convex.
Notation "'<|>_' d f" := (Convn (@conv _) d f) : convex_scope.
Section convex_space_prop1.
Variables T : convType.
Implicit Types a b : T.
Lemma convA0 (p q r s : {prob R}) a b c :
Prob.p p = (Prob.p r * Prob.p s)%coqR :> R -> ((Prob.p s).~ = (Prob.p p).~ * (Prob.p q).~)%coqR ->
a <| p |> (b <| q |> c) = (a <| r |> b) <| s |> c.
Proof.
move=> H1 H2.
have [r0|r0] := eqVneq r 0%:pr.
rewrite r0 conv0 (_ : p = 0%:pr) ?conv0; last first.
by apply/val_inj; rewrite /= H1 r0 mul0R.
congr (_ <| _ |> _); move: H2; rewrite H1 r0 mul0R onem0 mul1R.
by move/(congr1 (@onem R)); rewrite !onemK => ?; exact/val_inj.
have [s0|s0] := eqVneq s 0%:pr.
have p0 : p = 0%:pr by apply/val_inj; rewrite /= H1 s0 mulR0.
rewrite s0 conv0 p0 // ?conv0.
rewrite (_ : q = 0%:pr) ?conv0 //.
move: H2; rewrite p0 onem0 mul1R => /(congr1 (@onem R)); rewrite !onemK => sq.
by rewrite -s0; exact/val_inj.
rewrite convA; congr ((_ <| _ |> _) <| _ |> _).
apply val_inj; rewrite /= s_of_pqE.
move/(congr1 (@onem R)) : H2.
by rewrite onemK => ->.
exact: (@r_of_pq_is_r _ _ _ _ s).
Qed.
Lemma convA' (r s : {prob R}) a b c :
a <| [p_of r, s] |> (b <| [q_of r, s] |> c) = (a <| r |> b) <| s |> c.
Proof.
have [/eqP|H] := eqVneq [p_of r, s] 1%:pr.
by move=> /p_of_rs1P[-> ->]; rewrite p_of_r1 3!conv1.
have [->|s0] := eqVneq s 0%:pr; first by rewrite p_of_r0 q_of_r0 3!conv0.
by rewrite convA s_of_pqK// r_of_pqK.
Qed.
(* NB: this is defined here and not in realType_ext.v because it uses the scope %coqR *)
Lemma onem_probR_ge0 (p: {prob R}) : (0 <= (Prob.p p).~)%coqR.
Proof. exact/RleP/onem_ge0/prob_le1. Qed.
Hint Resolve onem_probR_ge0 : core.
Lemma convACA (a b c d : T) p q :
(a <|q|> b) <|p|> (c <|q|> d) = (a <|p|> c) <|q|> (b <|p|> d).
Proof.
apply: S1_inj; rewrite ![in LHS]affine_conv/= !convptE.
rewrite !scaleptDr !scaleptA// !(mulRC (Prob.p p)) !(mulRC (Prob.p p).~) addptA addptC.
rewrite (addptC (scalept (Prob.p q * Prob.p p) _)) !addptA -addptA -!scaleptA -?scaleptDr//.
by rewrite !(addptC (scalept _.~ _)) !affine_conv.
Qed.
Lemma convDr (x y z : T) (p q : {prob R}) :
x <| p |> (y <| q |> z) = (x <| p |> y) <| q |> (x <| p |> z).
Proof. by rewrite -{1}(convmm q x) convACA. Qed.
Lemma convACA' (a b c d : T) (p q r : {prob R}) :
(*
let p1 := (q * p)%:opr in
let p2 := (q.~ * r)%:opr in
let r1 := (q * p.~)%:opr in
let r2 := (q.~ * r.~)%:opr in
let q' := ((p1 + p2) / (p1 + p2 + (r1 + r2)))%:opr in
let p' := (p1 / (p1 + p2))%:opr in
let r' := (r1 / (r1 + r2))%:opr in
(a <|p|> b) <|q|> (c <|r|> d) = (a <|p'|> c) <|q'|> (b <|r'|> d).
*)
exists p' q' r', (a <|p|> b) <|q|> (c <|r|> d) = (a <|p'|> c) <|q'|> (b <|r'|> d).
Proof.
rewrite (convC p) convA convC !convA.
set C0 := _.~%:pr.
set C1 := _.~%:pr.
rewrite -convA' (convC _ d) convC.
by eexists; eexists; eexists; congr ((_ <|_|> _) <|_|> (_ <|_|> _)).
Qed.
Local Open Scope vec_ext_scope.
Section with_affine_projection.
Variable U : convType.
Variable prj : {affine T -> U}.
Local Open Scope scaled_scope.
Definition map_scaled (x : scaled T) : scaled U :=
if x is p *: a then p *: prj a else Zero.
Lemma affine_map_scaled : affine map_scaled.
Proof.
move=> p [q x|] [r y|] /=; rewrite 2!convptE ?scalept0 //.
- rewrite !(scalept_Scaled (Prob.p p)) !(scalept_Scaled (Prob.p p).~) /= /scalept /=.
case: Rlt_dec => Hpq; case: Rlt_dec => Hpr //=; congr (_ *: _).
by rewrite affine_conv.
- by rewrite !addpt0 !(scalept_Scaled (Prob.p p)) /= /scalept /=; case: Rlt_dec.
- by rewrite !add0pt !(scalept_Scaled (Prob.p p).~) /= /scalept/=; case: Rlt_dec.
Qed.
HB.instance Definition _ := isAffine.Build _ _ map_scaled affine_map_scaled.
Lemma S1_Convn_proj n (g : 'I_n -> T) d :
S1 (prj (<|>_d g)) = \ssum_(i < n) scalept (d i) (S1 (prj (g i))).
Proof.
elim: n g d => [|n IH] g d.
by move: (FDist.f1 d); rewrite /= big_ord0 => /Rlt_not_eq; case.
rewrite /=; case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb]Hd.
rewrite (bigD1 ord0) //= Hd big1 /=.
rewrite addpt0 (@scalept_gt0 _ 1).
by congr (_ *: _); apply val_inj; rewrite /= mulR1.
move=> i Hi; have := FDist.f1 d.
rewrite (bigD1 ord0) ?inE // Hd /= -RplusE addRC => /(f_equal (Rminus^~ R1)).
rewrite addRK subRR => /eqP.
rewrite psumr_eq0// => /allP/= => /(_ i).
by rewrite mem_index_enum Hi implyTb => /(_ isT)/eqP ->; rewrite scale0pt.
set d' := fdist_del Hd.
set g' := fun i => g (fdist_del_idx ord0 i).
rewrite /index_enum -enumT (bigD1_seq ord0) ?enum_uniq ?mem_enum //=.
rewrite -big_filter (perm_big (map (lift ord0) (enum 'I_n))); last first.
exact: perm_filter_enum_ord.
rewrite 2!affine_conv/=; congr addpt.
rewrite IH -barycenter_map scalept_barycenter //.
rewrite /barycenter 2!big_map [in RHS]big_map.
apply eq_bigr => i _.
rewrite scaleptA // fdist_delE fdistD1E /=.
rewrite (mulrC (fun_of_fin (FDist.f d) (lift ord0 i))).
rewrite RmultE mulrA mulrV ?mul1r //.
move: (Hd); apply contra; rewrite R0E R1E => /eqP Hd'.
by rewrite -onem0 -Hd' onemK.
Qed.
End with_affine_projection.
Lemma S1_Convn n (g : 'I_n -> T) d :
S1 (<|>_d g) = \ssum_(i < n) scalept (d i) (S1 (g i)).
Proof. by rewrite (S1_Convn_proj [the {affine _ ->_} of idfun]). Qed.
Lemma fdist_convn_add n m p (g : 'I_(n + m) -> T) (d : {fdist 'I_n})
(e : {fdist 'I_m}) :
<|>_(fdist_add d e p) g =
<|>_d (g \o @lshift n m) <| p |> <|>_e (g \o @rshift n m).
Proof.
apply: S1_inj; rewrite affine_conv/= !S1_Convn convptE big_split_ord/=.
do 2 rewrite [in RHS]big_morph_scalept ?scalept0//.
congr addpt; apply eq_bigr => i _;
rewrite (scaleptA _ _ (S1 _)) //;
by rewrite fdist_addE (split_lshift, split_rshift).
Qed.
End convex_space_prop1.
Section convex_space_prop2.
Variables T U : convType.
Implicit Types a b : T.
Lemma Convn_comp (f : {affine T -> U}) n (g : 'I_n -> T) (d : {fdist 'I_n}) :
f (<|>_d g) = <|>_d (f \o g).
Proof. by apply S1_inj; rewrite S1_Convn S1_Convn_proj. Qed.
Lemma eq_Convn n (g1 g2 : 'I_n -> T) (d1 d2 : {fdist 'I_n}) :
g1 =1 g2 -> d1 =1 d2 -> <|>_d1 g1 = <|>_d2 g2.
Proof.
move=> Hg Hd; apply S1_inj; rewrite !S1_Convn.
by apply congr_big => // i _; rewrite Hg Hd.
Qed.
Lemma eq_dep_Convn n (g : 'I_n -> T) (d : {fdist 'I_n})
n0 (g0 : 'I_n0 -> T) (d0 : {fdist 'I_n0}) (Hn : n = n0)
(Hg : eq_rect n (fun m => 'I_m -> T) g n0 Hn = g0)
(Hd : eq_rect n (fun m => {fdist 'I_m}) d n0 Hn = d0) :
<|>_d g = <|>_d0 g0.
Proof.
refine (match Hd with erefl => _ end).
refine (match Hg with erefl => _ end).
refine (match Hn with erefl => _ end).
reflexivity.
Qed.
Lemma Convn_proj n (g : 'I_n -> T) (d : {fdist 'I_n}) i :
d i = R1 -> <|>_d g = g i.
Proof.
move=> Hd; apply: S1_inj.
rewrite S1_Convn (bigD1 i)//=.
rewrite big1; first by rewrite addpt0 Hd scale1pt.
move=> j Hj.
by move/eqP/fdist1P: Hd => -> //; rewrite scale0pt.
Qed.
Lemma Convn_fdist1 (n : nat) (j : 'I_n) (g : 'I_n -> T) :
<|>_(fdist1 j) g = g j.
Proof. by apply Convn_proj; rewrite fdist1xx. Qed.
Lemma ConvnI1E
(g : 'I_1 -> T) (e : {fdist 'I_1}) : <|>_ e g = g ord0.
Proof.
rewrite /=; case: Bool.bool_dec => // /Bool.eq_true_not_negb H.
exfalso; move/eqP: H; apply.
by apply/eqP; rewrite fdist1E1 (fdist1I1 e).
Qed.
Lemma ConvnI1_eq_rect n (g : 'I_n -> T) (d : {fdist 'I_n}) (Hn1 : n = 1) :
<|>_d g = eq_rect n (fun n => 'I_n -> T) g 1 Hn1 ord0.
Proof.
set d' := eq_rect n (fun n0 => {fdist 'I_n0}) d 1 Hn1.
set g' := eq_rect n (fun n0 => 'I_n0 -> T) g 1 Hn1.
suff -> : <|>_d g = <|>_d' g' by rewrite ConvnI1E.
by eapply eq_dep_Convn.
Qed.
Lemma ConvnI1_eq n (g : 'I_n -> T) (d : {fdist 'I_n})
(n1 : n = 1) (i : 'I_n) : <|>_d g = g i.
Proof.
rewrite ConvnI1_eq_rect.
have -> /= : eq_rect n (fun n0 : nat => 'I_n0 -> T) g 1 n1 =
g \o eq_rect 1 (fun n0 : nat => 'I_1 -> 'I_n0) idfun n (esym n1)
by subst n.
have /(_ i) I_n_contr : forall a b : 'I_n, a = b
by rewrite n1 => a b; rewrite (ord1 a) (ord1 b).
by rewrite -(I_n_contr (eq_rect 1 (fun n => 'I_1 -> 'I_n) idfun n (esym n1) ord0)).
Qed.
Global Arguments ConvnI1_eq [n g d n1].
Lemma ConvnIE n (g : 'I_n.+1 -> T) (d : {fdist 'I_n.+1}) (i1 : d ord0 != 1%coqR) :
<|>_d g = g ord0 <| probfdist d ord0 |>
<|>_(fdist_del i1) (fun x => g (fdist_del_idx ord0 x)).
Proof.
rewrite /=; case: Bool.bool_dec => /= [|/Bool.eq_true_not_negb] H.
exfalso; by rewrite (eqP H) eqxx in i1.
by rewrite (eq_irrelevance H i1).
Qed.
Lemma ConvnI2E' (g : 'I_2 -> T) (d : {fdist 'I_2}) :
<|>_d g = g ord0 <| probfdist d ord0 |> g (lift ord0 ord0).
Proof.
have [/eqP|i1] := eqVneq (d ord0) 1%coqR.
rewrite fdist1E1 => /eqP ->; rewrite Convn_fdist1.
rewrite (_ : probfdist _ _ = 1%:pr) ?conv1 //.
by apply val_inj; rewrite /= fdist1xx.
rewrite ConvnIE; congr (_ <| _ |> _).
by rewrite ConvnI1E /fdist_del_idx ltnn.
Qed.
Lemma ConvnI2E (g : 'I_2 -> T) (d : {fdist 'I_2}) :
convn d g = (g ord0) <| probfdist d ord0 |> (g (lift ord0 ord0)).
Proof.
have [/eqP|i1] := eqVneq (d ord0) 1%coqR.
rewrite fdist1E1 convnE => /eqP ->; rewrite Convn_fdist1.
rewrite (_ : probfdist _ _ = 1%:pr) ?conv1 //.
by apply val_inj; rewrite /= fdist1xx.
rewrite convnE ConvnIE; congr (conv _ _ _).
by rewrite ConvnI1E /fdist_del_idx ltnn.
Qed.
End convex_space_prop2.
HB.factory Record isConvexSpace T of Choice T := {
conv : {prob R} -> T -> T -> T ;
conv1 : forall a b, conv 1%:pr a b = a ;
convmm : forall p a, conv p a a = a ;
convC : forall p a b, conv p a b = conv (onem (Prob.p p))%:pr b a ;
convA : forall (p q : {prob R}) (a b c : T),
conv p a (conv q b c) = conv [s_of p, q] (conv [r_of p, q] a b) c }.
HB.builders Context T of isConvexSpace T.
Definition convn := Convn conv.
Let conv0 a b : conv 0%:pr a b = b.
Proof.
by rewrite convC /= (_ : _ %:pr = 1%:pr) ?conv1 //; apply/val_inj/onem0.
Qed.
Let Convn_fdist1 (n : nat) (j : 'I_n) (g : 'I_n -> T) :
convn (fdist1 j) g = g j.
Proof.
elim: n j g => [[] [] //|n IH j g /=].
rewrite /convn {1}/Convn.
case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb b01].
rewrite fdist1E; case j0 : (_ == _) => /=.
by move=> _; rewrite (eqP j0).
by move/eqP; rewrite eq_sym R1E oner_eq0.
rewrite (_ : probfdist _ _ = 0%:pr) ?conv0; last first.
apply val_inj => /=; move: b01; rewrite !fdist1E => j0.
by case j0' : (_ == _) => //; rewrite j0' eqxx in j0.
have j0 : ord0 != j by apply: contra b01 => /eqP <-; rewrite fdist1xx.
have j0' : 0 < j by rewrite lt0n; apply: contra j0 => /eqP j0; apply/eqP/val_inj.
move=> [:H]; have @j' : 'I_n.
by apply: (@Ordinal _ j.-1 _); abstract: H; rewrite prednK // -ltnS.
rewrite (_ : fdist_del b01 = fdist1 j'); last first.
apply/fdist_ext => /= k.
rewrite fdist_delE fdistD1E /= !fdist1E /= (negbTE j0) subr0 divr1.
congr (GRing.natmul _ (nat_of_bool _)).
move R : (k == _) => [|].
- apply/eqP/val_inj; rewrite /= /bump leq0n add1n.
by move/eqP : R => -> /=; rewrite prednK // lt0n.