diff --git a/lib/ssr_ext.v b/lib/ssr_ext.v index 10d72b64..90607d87 100644 --- a/lib/ssr_ext.v +++ b/lib/ssr_ext.v @@ -1078,3 +1078,27 @@ destruct boolP. by move=> x y; have:= Bool.bool_dec x y => -[]; [left | right]. Qed. End boolP. + +Section fintype_extra. + +Lemma index_enum_cast_ord n m (e : n = m) : + index_enum 'I_m = [seq cast_ord e i | i <- index_enum 'I_n]. +Proof. +subst m; rewrite -{1}(map_id (index_enum 'I_n)). +apply eq_map=> [[x xlt]]. +by rewrite /cast_ord; congr Ordinal; exact: bool_irrelevance. +Qed. + +Lemma perm_map_bij [T : finType] [f : T -> T] (s : seq T) : bijective f -> + perm_eq (index_enum T) [seq f i | i <- index_enum T]. +Proof. +rewrite /index_enum; case: index_enum_key => /= fbij. +rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=. +case: fbij => g fg gf. +rewrite enumT enumP count_map -size_filter (@eq_in_filter _ _ + (pred1 (g (tnth (cat_tuple (enum_tuple T) (map_tuple [eta f] (enum_tuple T))) i)))). + by rewrite size_filter enumP. +by move=> x _ /=; apply/eqP/eqP => [/(congr1 g) <-|->//]. +Qed. + +End fintype_extra. diff --git a/probability/convex.v b/probability/convex.v index 574b793a..a8bb1f46 100644 --- a/probability/convex.v +++ b/probability/convex.v @@ -156,144 +156,6 @@ Local Notation "{ 'fdist' T }" := (_ .-fdist T) : fdist_scope. #[export] Hint Extern 0 (0 <= onem _)%coqR => exact/RleP/onem_ge0 : core. -(* TODO: the following lemmas are currently not in use. Maybe remove? *) -Section tmp. -Local Open Scope ring_scope. - -Lemma fdist_convn_Add (R : realType) - (n m : nat) (d1 : {fdist 'I_n}) (d2 : {fdist 'I_m}) (p : {prob R}) - (A : finType) (g : 'I_n -> {fdist A}) (h : 'I_m -> {fdist A}) : - fdist_convn (fdist_add d1 d2 p) - [ffun i => match fintype.split i with inl a => g a | inr a => h a end] = - (fdist_convn d1 g <| p |> fdist_convn d2 h)%fdist. -Proof. -apply/fdist_ext => a; rewrite !fdist_convE !fdist_convnE. -rewrite 2!big_distrr /= big_split_ord /=; congr (_ + _); - apply eq_bigr => i _; rewrite fdist_addE ffunE. -case: splitP => /= j ij. -rewrite mulrA; congr (_ * d1 _ * (g _) a); exact/val_inj. -move: (ltn_ord i); by rewrite ij -ltn_subRL subnn ltn0. -case: splitP => /= j ij. -move: (ltn_ord j); by rewrite -ij -ltn_subRL subnn ltn0. -move/eqP : ij; rewrite eqn_add2l => /eqP ij. -rewrite mulrA; congr (_ * d2 _ * (h _) a); exact/val_inj. -Qed. - -Import realType_ext. -Lemma fdist_convn_del - (R : realType) - (A : finType) (n : nat) (g : 'I_n.+1 -> {fdist A}) (P : {fdist 'I_n.+1}) - (j : 'I_n.+1) (H : (0 <= P j <= 1)) (Pj1 : P j != 1) : - let g' := fun i : 'I_n => g (fdist_del_idx j i) in - fdist_convn P g = - (g j <| @Prob.mk_ R _ H |> fdist_convn (fdist_del Pj1) g')%fdist. -Proof. -move=> g' /=; apply/fdist_ext => a. -rewrite fdist_convE /= fdist_convnE (bigD1 j) //=; congr (_ + _). -rewrite fdist_convnE big_distrr /=. -rewrite (bigID (fun i : 'I_n.+1 => (i < j)%nat)) //=. -rewrite (bigID (fun i : 'I_n => (i < j)%nat)) //=; congr (_ + _). - rewrite (@big_ord_narrow_cond _ _ _ j n.+1); first by rewrite ltnW. - move=> jn; rewrite (@big_ord_narrow_cond _ _ _ j n xpredT); first by rewrite -ltnS. - move=> jn'. - apply/eq_big. - by move=> /= i; apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. - move=> /= i _. - rewrite fdist_delE /= ltn_ord fdistD1E /= ifF /=; last first. - by apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. - rewrite mulrA mulrCA mulrV ?mulr1; last first. -rewrite unitfE. rewrite onem_neq0 ?onem_neq0 //. - congr (P _ * _); first exact/val_inj. - by rewrite /g' /fdist_del_idx /= ltn_ord; congr (g _ a); exact/val_inj. -rewrite (eq_bigl (fun i : 'I_n.+1 => (j < i)%nat)); last first. - move=> i; by rewrite -leqNgt eq_sym -ltn_neqAle. -rewrite (eq_bigl (fun i : 'I_n => (j <= i)%nat)); last first. - move=> i; by rewrite -leqNgt. -rewrite big_mkcond. -rewrite big_ord_recl ltn0 /= add0r. -rewrite [in RHS]big_mkcond. -apply eq_bigr => i _. -rewrite /bump add1n ltnS; case: ifPn => // ji. -rewrite fdist_delE fdistD1E ltnNge ji /= ifF; last first. - apply/eqP => /(congr1 val) => /=. - rewrite /bump add1n => ij. - by move: ji; apply/negP; rewrite -ij ltnn. -rewrite -[1 - P j]/(P j).~. -rewrite [_ / _]mulrC !mulrA divrr ?unitfE ?onem_neq0 // mul1r. -by rewrite /g' /fdist_del_idx ltnNge ji. -Qed. -End tmp. - -(* TODO: move*) -Section fintype_extra. - -Lemma index_enum_cast_ord n m (e : n = m) : - index_enum 'I_m = [seq cast_ord e i | i <- index_enum 'I_n]. -Proof. -subst m; rewrite -{1}(map_id (index_enum 'I_n)). -apply eq_map=> [[x xlt]]. -by rewrite /cast_ord; congr Ordinal; exact: bool_irrelevance. -Qed. - -Lemma perm_map_bij [T : finType] [f : T -> T] (s : seq T) : bijective f -> - perm_eq (index_enum T) [seq f i | i <- index_enum T]. -Proof. -rewrite /index_enum; case: index_enum_key => /= fbij. -rewrite /perm_eq -enumT -forallb_tnth; apply /forallP=>i /=. -case: fbij => g fg gf. -rewrite enumT enumP count_map -size_filter (@eq_in_filter _ _ - (pred1 (g (tnth (cat_tuple (enum_tuple T) (map_tuple [eta f] (enum_tuple T))) i)))). - by rewrite size_filter enumP. -by move=> x _ /=; apply/eqP/eqP => [/(congr1 g) <-|->//]. -Qed. - -End fintype_extra. - -Module CodomDFDist. -Section def. -Local Open Scope classical_set_scope. -Local Open Scope ring_scope. -Variables (R: realType) (A : Type) (n : nat) (g : 'I_n -> A). -Variables (e : R .-fdist 'I_n) (y : set A). -Definition f := [ffun i : 'I_n => if g i \in y then e i else 0]. -Lemma f0 i : (0 <= f i). Proof. by rewrite /f ffunE; case: ifPn. Qed. -Lemma f1 (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, x (g i) -> e i = 0) : - (\sum_(i < n) f i = 1). -Proof. -rewrite /f -(FDist.f1 e) /=. -apply eq_bigr => i _; rewrite ffunE. -case: ifPn => // /negP; rewrite in_setE => ygi. -rewrite ge //. -have : (x `|` y) (g i) by apply/gX; by exists i. -by case. -Qed. -Definition d (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, x (g i) -> e i = 0) : {fdist 'I_n} := - locked (FDist.make f0 (f1 gX ge)). -Lemma dE (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, x (g i) -> e i = 0) i : - d gX ge i = if g i \in y then e i else 0. -Proof. by rewrite /d; unlock; rewrite ffunE. Qed. -Lemma f1' (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) : - (\sum_(i < n) f i = 1). -Proof. -rewrite /f -(FDist.f1 e) /=; apply eq_bigr => i _; rewrite ffunE. -case: ifPn => // /negP; rewrite in_setE => giy. -rewrite ge //. -have : (x `|` y) (g i) by apply/gX; by exists i. -by case. -Qed. -Definition d' (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) := - locked (FDist.make f0 (f1' gX ge)). -Lemma dE' (x : set A) (gX : g @` setT `<=` x `|` y) - (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) i : - d' gX ge i = if g i \in y then e i else 0. -Proof. by rewrite /d'; unlock; rewrite ffunE. Qed. -End def. -End CodomDFDist. HB.mixin Record isConvexSpace0 T of Choice T := { conv : {prob R} -> T -> T -> T ; diff --git a/probability/convex_equiv.v b/probability/convex_equiv.v index 0f984640..fa8e2fbe 100644 --- a/probability/convex_equiv.v +++ b/probability/convex_equiv.v @@ -56,70 +56,6 @@ Import NaryConvexSpace. (* In this module we use funext to avoid explicitly handling the congruence of convn (cf. eq_convn in convex_choice.v for the iterated version). *) -(* These definitions about distributions should probably be elsewhere *) -Definition fdistE := - (fdistmapE,fdist1E,fdist_prodE,fdistXI,fdistXE,fdist_convnE,fdist_fstE). - -Module FDistPart. -Section fdistpart. -Local Open Scope fdist_scope. -Variables (n m : nat) (K : 'I_m -> 'I_n) (e : {fdist 'I_m}) (i : 'I_n). - -Definition d := (fdistX (e `X (fun j => fdist1 (K j)))) `(| i). -Definition den := (fdistX (e `X (fun j => fdist1 (K j))))`1 i. - -Lemma denE : den = fdistmap K e i. -Proof. -rewrite /den !fdistE [RHS]big_mkcond /=. -under eq_bigl do rewrite inE. -apply/eq_bigr => a _. -rewrite !fdistE /= (big_pred1 (a,i)) ?fdistE /=; - last by case=> x y; rewrite /swap /= !xpair_eqE andbC. -rewrite eq_sym 2!inE. -by case: eqP => // _; rewrite (mulr0,mulr1). -Qed. - -Lemma dE j : fdistmap K e i != 0%coqR -> - d j = (e j * (i == K j)%:R / \sum_(j | K j == i) e j)%coqR. -Proof. -rewrite -denE => NE. -rewrite jfdist_condE // {NE} /jcPr /proba.Pr. -rewrite (big_pred1 (j,i)); last first. - by move=> k; rewrite !inE [in RHS](surjective_pairing k) xpair_eqE. -rewrite (big_pred1 i); last by move=> k; rewrite !inE. -rewrite !fdistE big_mkcond [in RHS]big_mkcond /=. -rewrite -RmultE -INRE. -congr (_ / _)%R. -under eq_bigr => k do rewrite {2}(surjective_pairing k). -rewrite -(pair_bigA _ (fun k l => - if l == i - then e `X (fun j0 : 'I_m => fdist1 (K j0)) (k, l) - else R0))%R /=. -apply eq_bigr => k _. -rewrite -big_mkcond /= big_pred1_eq !fdistE /= eq_sym. -by case: ifP; rewrite (mulr1,mulr0). -Qed. -End fdistpart. - -Lemma dK n m K (e : {fdist 'I_m}) j : - e j = (\sum_(i < n) fdistmap K e i * d K e i j)%R. -Proof. -under eq_bigr => /= a _. - have [Ka0|Ka0] := eqVneq (fdistmap K e a) 0%R. - rewrite Ka0 mul0R. - have <- : (e j * (a == K j)%:R = 0)%R. - have [/eqP Kj|] := eqVneq a (K j); last by rewrite mulR0. - move: Ka0; rewrite fdistE /=. - by move/psumr_eq0P => -> //; rewrite ?(mul0R,inE) // eq_sym. - over. - rewrite FDistPart.dE // fdistE /= mulRCA mulRV ?mulR1; - last by rewrite fdistE in Ka0. -over. -move=> /=. -rewrite (bigD1 (K j)) //= eqxx mulR1. -by rewrite big1 ?addR0 // => i /negbTE ->; rewrite mulR0. -Qed. -End FDistPart. Section Axioms. Variable T : naryConvType. diff --git a/probability/fdist.v b/probability/fdist.v index 4c10305b..3de9bcba 100644 --- a/probability/fdist.v +++ b/probability/fdist.v @@ -1088,10 +1088,17 @@ Qed. End fdistX_prop. +Section fdistX_prop_ext. Lemma fdistX_prod2 {R: realType} (A B : finType) (P : fdist R A) (W : A -> fdist R B) : (fdistX (P `X W))`2 = P. Proof. by rewrite fdistX2 fdist_prod1. Qed. +End fdistX_prop_ext. + +Section fdist_prop_ext. +Definition fdistE := + (fdistmapE,fdist1E,fdist_prodE,fdistXI,fdistXE,fdist_convnE,fdist_fstE). +End fdist_prop_ext. Section fdist_rV. Local Open Scope ring_scope. @@ -1855,3 +1862,119 @@ Defined. *) End tuple_prod_cast.*) + +(* TODO: the following lemmas are currently not in use. Maybe remove? *) +Section moved_from_convex. +Local Open Scope ring_scope. + +Lemma fdist_convn_Add (R : realType) + (n m : nat) (d1 : R.-fdist 'I_n) (d2 : R.-fdist 'I_m) (p : {prob R}) + (A : finType) (g : 'I_n -> R.-fdist A) (h : 'I_m -> R.-fdist A) : + fdist_convn (fdist_add d1 d2 p) + [ffun i => match fintype.split i with inl a => g a | inr a => h a end] = + (fdist_convn d1 g <| p |> fdist_convn d2 h)%fdist. +Proof. +apply/fdist_ext => a; rewrite !fdist_convE !fdist_convnE. +rewrite 2!big_distrr /= big_split_ord /=; congr (_ + _); + apply eq_bigr => i _; rewrite fdist_addE ffunE. +case: splitP => /= j ij. +rewrite mulrA; congr (_ * d1 _ * (g _) a); exact/val_inj. +move: (ltn_ord i); by rewrite ij -ltn_subRL subnn ltn0. +case: splitP => /= j ij. +move: (ltn_ord j); by rewrite -ij -ltn_subRL subnn ltn0. +move/eqP : ij; rewrite eqn_add2l => /eqP ij. +rewrite mulrA; congr (_ * d2 _ * (h _) a); exact/val_inj. +Qed. + +Import realType_ext. +Lemma fdist_convn_del + (R : realType) + (A : finType) (n : nat) (g : 'I_n.+1 -> R.-fdist A) (P : R.-fdist 'I_n.+1) + (j : 'I_n.+1) (H : (0 <= P j <= 1)) (Pj1 : P j != 1) : + let g' := fun i : 'I_n => g (fdist_del_idx j i) in + fdist_convn P g = + (g j <| @Prob.mk_ R _ H |> fdist_convn (fdist_del Pj1) g')%fdist. +Proof. +move=> g' /=; apply/fdist_ext => a. +rewrite fdist_convE /= fdist_convnE (bigD1 j) //=; congr (_ + _). +rewrite fdist_convnE big_distrr /=. +rewrite (bigID (fun i : 'I_n.+1 => (i < j)%nat)) //=. +rewrite (bigID (fun i : 'I_n => (i < j)%nat)) //=; congr (_ + _). + rewrite (@big_ord_narrow_cond _ _ _ j n.+1); first by rewrite ltnW. + move=> jn; rewrite (@big_ord_narrow_cond _ _ _ j n xpredT); first by rewrite -ltnS. + move=> jn'. + apply/eq_big. + by move=> /= i; apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. + move=> /= i _. + rewrite fdist_delE /= ltn_ord fdistD1E /= ifF /=; last first. + by apply/negP => /eqP/(congr1 val) /=; apply/eqP; rewrite ltn_eqF. + rewrite mulrA mulrCA mulrV ?mulr1; last first. +rewrite unitfE. rewrite onem_neq0 ?onem_neq0 //. + congr (P _ * _); first exact/val_inj. + by rewrite /g' /fdist_del_idx /= ltn_ord; congr (g _ a); exact/val_inj. +rewrite (eq_bigl (fun i : 'I_n.+1 => (j < i)%nat)); last first. + move=> i; by rewrite -leqNgt eq_sym -ltn_neqAle. +rewrite (eq_bigl (fun i : 'I_n => (j <= i)%nat)); last first. + move=> i; by rewrite -leqNgt. +rewrite big_mkcond. +rewrite big_ord_recl ltn0 /= add0r. +rewrite [in RHS]big_mkcond. +apply eq_bigr => i _. +rewrite /bump add1n ltnS; case: ifPn => // ji. +rewrite fdist_delE fdistD1E ltnNge ji /= ifF; last first. + apply/eqP => /(congr1 val) => /=. + rewrite /bump add1n => ij. + by move: ji; apply/negP; rewrite -ij ltnn. +rewrite -[1 - P j]/(P j).~. +rewrite [_ / _]mulrC !mulrA divrr ?unitfE ?onem_neq0 // mul1r. +by rewrite /g' /fdist_del_idx ltnNge ji. +Qed. +End moved_from_convex. + + +Module CodomDFDist. +Import classical_sets. +Section def. +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. +Variables (R: realType) (A : Type) (n : nat) (g : 'I_n -> A). +Variables (e : R .-fdist 'I_n) (y : set A). +Definition f := [ffun i : 'I_n => if g i \in y then e i else 0]. +Lemma f0 i : (0 <= f i). Proof. by rewrite /f ffunE; case: ifPn. Qed. +Lemma f1 (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, x (g i) -> e i = 0) : + (\sum_(i < n) f i = 1). +Proof. +rewrite /f -(FDist.f1 e) /=. +apply eq_bigr => i _; rewrite ffunE. +case: ifPn => // /negP; rewrite in_setE => ygi. +rewrite ge //. +have : (x `|` y) (g i) by apply/gX; by exists i. +by case. +Qed. +Definition d (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, x (g i) -> e i = 0) : R.-fdist 'I_n := + locked (FDist.make f0 (f1 gX ge)). +Lemma dE (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, x (g i) -> e i = 0) i : + d gX ge i = if g i \in y then e i else 0. +Proof. by rewrite /d; unlock; rewrite ffunE. Qed. +Lemma f1' (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) : + (\sum_(i < n) f i = 1). +Proof. +rewrite /f -(FDist.f1 e) /=; apply eq_bigr => i _; rewrite ffunE. +case: ifPn => // /negP; rewrite in_setE => giy. +rewrite ge //. +have : (x `|` y) (g i) by apply/gX; by exists i. +by case. +Qed. +Definition d' (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) := + locked (FDist.make f0 (f1' gX ge)). +Lemma dE' (x : set A) (gX : g @` setT `<=` x `|` y) + (ge : forall i : 'I_n, (x (g i)) /\ (~ y (g i)) -> e i = 0) i : + d' gX ge i = if g i \in y then e i else 0. +Proof. by rewrite /d'; unlock; rewrite ffunE. Qed. +End def. +End CodomDFDist. diff --git a/probability/jfdist_cond.v b/probability/jfdist_cond.v index 8d0c146b..c41cb4e4 100644 --- a/probability/jfdist_cond.v +++ b/probability/jfdist_cond.v @@ -395,3 +395,67 @@ by case ab. Qed. End fdist_split. + + +Import GRing.Theory Num.Theory. + +Module FDistPart. +Section fdistpart. +Local Open Scope fdist_scope. +Variables (n m : nat) (K : 'I_m -> 'I_n) (e : {fdist 'I_m}) (i : 'I_n). + +Definition d := (fdistX (e `X (fun j => fdist1 (K j)))) `(| i). +Definition den := (fdistX (e `X (fun j => fdist1 (K j))))`1 i. + +Lemma denE : den = fdistmap K e i. +Proof. +rewrite /den !fdistE [RHS]big_mkcond /=. +under eq_bigl do rewrite inE. +apply/eq_bigr => a _. +rewrite !fdistE /= (big_pred1 (a,i)) ?fdistE /=; + last by case=> x y; rewrite /swap /= !xpair_eqE andbC. +rewrite eq_sym 2!inE. +by case: eqP => // _; rewrite (mulr0,mulr1). +Qed. + +Lemma dE j : fdistmap K e i != 0%coqR -> + d j = (e j * (i == K j)%:R / \sum_(j | K j == i) e j)%coqR. +Proof. +rewrite -denE => NE. +rewrite jfdist_condE // {NE} /jcPr /proba.Pr. +rewrite (big_pred1 (j,i)); last first. + by move=> k; rewrite !inE [in RHS](surjective_pairing k) xpair_eqE. +rewrite (big_pred1 i); last by move=> k; rewrite !inE. +rewrite !fdistE big_mkcond [in RHS]big_mkcond /=. +rewrite -RmultE -INRE. +congr (_ / _)%R. +under eq_bigr => k do rewrite {2}(surjective_pairing k). +rewrite -(pair_bigA _ (fun k l => + if l == i + then e `X (fun j0 : 'I_m => fdist1 (K j0)) (k, l) + else R0))%R /=. +apply eq_bigr => k _. +rewrite -big_mkcond /= big_pred1_eq !fdistE /= eq_sym. +by case: ifP; rewrite (mulr1,mulr0). +Qed. +End fdistpart. + +Lemma dK n m K (e : {fdist 'I_m}) j : + e j = (\sum_(i < n) fdistmap K e i * d K e i j)%R. +Proof. +under eq_bigr => /= a _. + have [Ka0|Ka0] := eqVneq (fdistmap K e a) 0%R. + rewrite Ka0 mul0R. + have <- : (e j * (a == K j)%:R = 0)%R. + have [/eqP Kj|] := eqVneq a (K j); last by rewrite mulR0. + move: Ka0; rewrite fdistE /=. + by move/psumr_eq0P => -> //; rewrite ?(mul0R,inE) // eq_sym. + over. + rewrite FDistPart.dE // fdistE /= mulRCA mulRV ?mulR1; + last by rewrite fdistE in Ka0. +over. +move=> /=. +rewrite (bigD1 (K j)) //= eqxx mulR1. +by rewrite big1 ?addR0 // => i /negbTE ->; rewrite mulR0. +Qed. +End FDistPart.