From 1da135a4405b1a95ba3d29a753db2110009b6ba2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 8 Dec 2022 20:04:30 +0900 Subject: [PATCH] more cleaning --- information_theory/channel_code.v | 2 +- information_theory/source_code.v | 6 +- information_theory/source_coding_fl_direct.v | 181 ++++++++----------- probability/convex.v | 8 +- probability/fsdist.v | 86 ++++----- 5 files changed, 120 insertions(+), 163 deletions(-) diff --git a/information_theory/channel_code.v b/information_theory/channel_code.v index f91f79a8..8ab0c92b 100644 --- a/information_theory/channel_code.v +++ b/information_theory/channel_code.v @@ -45,7 +45,7 @@ Definition decT := {ffun 'rV[B]_n -> option M}. Record code := mkCode { enc : encT ; dec : decT }. -Definition CodeRate (c : code) := (log (INR #| M |) / INR n)%R. +Definition CodeRate (c : code) := (log (#| M |%:R) / n%:R)%R. Definition preimC (phi : decT) m := ~: (phi @^-1: xpred1 (Some m)). diff --git a/information_theory/source_code.v b/information_theory/source_code.v index 545f732f..65adb6f6 100644 --- a/information_theory/source_code.v +++ b/information_theory/source_code.v @@ -22,7 +22,7 @@ Local Open Scope R_scope. Declare Scope source_code_scope. Section scode_definition. -Variables (A : finType) (B : Type) (k n : nat). +Variables (A : finType) (B : Type) (k : nat). Definition encT := 'rV[A]_k -> B. @@ -47,17 +47,15 @@ Definition E_leng_cw := `E ((INR \o size) `o f). End scode_vl_definition. Section scode_fl_definition. - Variables (A : finType) (k n : nat). Definition scode_fl := scode A 'rV[bool]_n k. -Definition SrcRate (sc : scode_fl) := INR n / INR k. +Definition SrcRate (sc : scode_fl) := n%:R / k%:R. End scode_fl_definition. Section code_error_rate. - Variables (A : finType) (B : Type) (P : fdist A). Variables (k : nat) (sc : scode A B k). diff --git a/information_theory/source_coding_fl_direct.v b/information_theory/source_coding_fl_direct.v index f6eb58d0..031f2fae 100644 --- a/information_theory/source_coding_fl_direct.v +++ b/information_theory/source_coding_fl_direct.v @@ -23,21 +23,19 @@ Import Prenex Implicits. Local Open Scope ring_scope. Section encoder_and_decoder. - -Variables (A : finType) (P : fdist A). -Variables n k : nat. +Variables (A : finType) (P : fdist A) (n k : nat). Variable S : {set 'rV[A]_k.+1}. Definition f : encT A 'rV_n k.+1 := fun x => if x \in S then - let i := seq.index x (enum S) in + let i := index x (enum S) in row_of_tuple (Tuple (size_bitseq_of_nat i.+1 n)) else \row_(j < n) false. Variable def : 'rV[A]_k.+1. -Hypothesis Hdef : def \in S. +Hypothesis def_S : def \in S. Definition phi : decT A 'rV_n k.+1 := fun x => let i := tuple2N (tuple_of_row x) in @@ -46,37 +44,33 @@ Definition phi : decT A 'rV_n k.+1 := fun x => Lemma phi_f i : phi (f i) = i -> i \in S. Proof. -rewrite /f. -case: ifP => // H1. -rewrite /phi. -rewrite (_ : tuple_of_row _ = [tuple of nseq n false]); last first. +rewrite /f; case: ifPn => // iS. +rewrite /phi (_ : tuple_of_row _ = [tuple of nseq n false]); last first. rewrite -[RHS]row_of_tupleK; congr tuple_of_row. - apply/matrixP => a b. - by rewrite !mxE /tnth nth_nseq ltn_ord. -rewrite /tuple2N /= /N_of_bitseq /= -{1}(cats0 (nseq n false)) rem_lea_false_nseq /=. -move=> Hi; by rewrite -Hi Hdef in H1. + by apply/rowP => a; rewrite !mxE /tnth nth_nseq ltn_ord. +rewrite /tuple2N /= /N_of_bitseq /= -{1}(cats0 (nseq n false)). +rewrite rem_lea_false_nseq /= => defi. +by rewrite -defi def_S in iS. Qed. Hypothesis HS : (#| S | < expn 2 n)%nat. -Lemma f_phi i : i \in S -> phi (f i) = i. +Lemma f_phi i : i \in S -> phi (f i) = i. Proof. -move=> Hi. -rewrite /f Hi /phi. -rewrite row_of_tupleK. -have H : ((seq.index i (enum S)).+1 < expn 2 n)%nat. - have H : ((seq.index i (enum S)).+1 <= #| S |)%nat. - apply seq_index_enum_card => //; by apply enum_uniq. - by apply leq_ltn_trans with #| S |. +move=> iS; rewrite /f iS /phi row_of_tupleK. +have H : ((index i (enum S)).+1 < expn 2 n)%nat. + have : ((index i (enum S)).+1 <= #| S |)%nat. + by apply seq_index_enum_card => //; exact: enum_uniq. + by move/leq_ltn_trans; exact. move Heq1 : (tuple2N _) => eq1. -case: eq1 Heq1 => [|i0] Heq1. -- case/tuple2N_0 : Heq1 => Heq1. - have H1 : (seq.index i (enum S)).+1 <> O by []. - move: (bitseq_of_nat_nseq_false H1 H); by rewrite Heq1. +case: eq1 Heq1 => [|i0 Heq1]. +- case/tuple2N_0 => Heq1. + have : (seq.index i (enum S)).+1 <> O by []. + by move=> /bitseq_of_nat_nseq_false/(_ H); rewrite Heq1. - move Heq : ((Npos i0).-1 < #| S |)%nat => []. - by rewrite -Heq1 /= N_of_bitseq_bitseq_of_nat // nth_index // mem_enum. - - rewrite -Heq1 /tuple2N N_of_bitseq_bitseq_of_nat //= (@seq_index_enum_card _ (enum S) S i) // in Heq. - by rewrite enum_uniq. + - move: Heq. + by rewrite -Heq1 /tuple2N N_of_bitseq_bitseq_of_nat// seq_index_enum_card // enum_uniq. Qed. End encoder_and_decoder. @@ -84,75 +78,66 @@ End encoder_and_decoder. Local Open Scope R_scope. Local Open Scope zarith_ext_scope. -Lemma SrcDirectBound' d D : { k | D <= INR (k * d.+1) }. +Section source_direct_bound. + +Let source_direct_bound' d D : { k | D <= (k * d.+1)%:R }. Proof. exists '| up D |. rewrite -multE (natRM '| up D | d.+1). apply (@leR_trans (IZR `| up D |)); first exact: Rle_up. rewrite INR_IZR_INZ inj_Zabs_nat -{1}(mulR1 (IZR _)). apply leR_wpmul2l; first exact/IZR_le/Zabs_pos (* TODO: ssrZ? *). -rewrite -addn1 natRD /= (_ : INR 1 = 1%R) //; move: (leR0n d) => ?; lra. +by rewrite -addn1 natRD /= (_ : 1%:R = 1%R) //; move: (leR0n d) => ?; lra. Qed. -Lemma SrcDirectBound d D : { k | D <= INR (k.+1 * d.+1) }. +Lemma source_direct_bound d D : { k | D <= (k.+1 * d.+1)%:R }. Proof. -case: (SrcDirectBound' d D) => k Hk. +case: (source_direct_bound' d D) => k Hk. destruct k as [|k]; last by exists k. exists O; rewrite mul1n. -apply (@leR_trans 0%R); by [ | apply leR0n]. +by apply (@leR_trans 0%R); last exact: leR0n. Qed. +End source_direct_bound. + Local Open Scope source_code_scope. Local Open Scope entropy_scope. Local Open Scope reals_ext_scope. Section source_coding_direct'. - -Variables (A : finType) (P : fdist A). -Variables num den : nat. - -Let r := (INR num / INR den.+1)%R. - +Variables (A : finType) (P : fdist A) (num den : nat). +Let r := (num%:R / den.+1%:R)%R. Hypothesis Hr : `H P < r. Variable epsilon : R. -Hypothesis Hepsilon : 0 < epsilon < 1. +Hypothesis epsilon01 : 0 < epsilon < 1. Definition lambda := min(r - `H P, epsilon). -Definition delta := max(aep_bound P (lambda / 2), 2 / lambda). - -Let k' := sval (SrcDirectBound den delta). - -Definition k := (k'.+1 * den.+1)%nat. - -Definition n := (k'.+1 * num)%nat. - -(* a few easy lemmas to simplify the proof *) +Lemma lambda_gt0 : 0 < lambda. +Proof. by apply Rmin_glb_lt;[move: Hr => ? ; lra|exact: epsilon01.1]. Qed. -Lemma lambda0 : 0 < lambda. -Proof. -apply Rmin_glb_lt; last by apply (proj1 Hepsilon). -move: Hr => ? ; lra. -Qed. - -Lemma halflambdaepsilon : lambda / 2 <= epsilon. +Lemma lambda2_epsilon : lambda / 2 <= epsilon. Proof. apply (@leR_trans lambda). - rewrite leR_pdivr_mulr //; apply leR_pmulr; [lra | exact/ltRW/lambda0]. -rewrite /lambda. -case: (Rlt_le_dec (r - `H P) epsilon) => ?. -- rewrite Rmin_left; lra. -- rewrite Rmin_right //; lra. + by rewrite leR_pdivr_mulr //; apply leR_pmulr; [lra | exact/ltRW/lambda_gt0]. +rewrite /lambda; case: (Rlt_le_dec (r - `H P) epsilon) => ?. +- by rewrite Rmin_left; lra. +- by rewrite Rmin_right //; lra. Qed. -Lemma halflambda0 : 0 < lambda / 2. -Proof. apply divR_gt0 => //; exact: lambda0. Qed. +Lemma lambda2_gt0 : 0 < lambda / 2. +Proof. by apply divR_gt0 => //; exact: lambda_gt0. Qed. -Lemma halflambda1 : lambda / 2 < 1. -Proof. exact (leR_ltR_trans halflambdaepsilon (proj2 Hepsilon)). Qed. +Lemma lambda2_lt1 : lambda / 2 < 1. +Proof. exact: (leR_ltR_trans lambda2_epsilon epsilon01.2). Qed. -Lemma lambdainv2 : 0 < 2 / lambda. -Proof. apply divR_gt0; [lra | exact lambda0]. Qed. +Definition delta := max(aep_bound P (lambda / 2), 2 / lambda). + +Let k' := sval (source_direct_bound den delta). + +Definition k := (k'.+1 * den.+1)%nat. + +Definition n := (k'.+1 * num)%nat. Lemma Hlambdar : `H P + lambda <= r. Proof. @@ -168,89 +153,77 @@ Local Open Scope typ_seq_scope. Theorem source_coding' : exists sc : scode_fl A k n, SrcRate sc = r /\ esrc(P , sc) <= epsilon. Proof. -move: (proj2_sig (SrcDirectBound den delta)) => Hdelta. +move: (proj2_sig (source_direct_bound den delta)) => Hdelta. have Hk : aep_bound P (lambda / 2) <= INR k by exact/(leR_trans _ Hdelta)/leR_maxl. set S := `TS P k (lambda / 2). -set def := TS_0 halflambda0 halflambda1 Hk. (*TODO: get rid of this expansion*) +set def := TS_0 lambda2_gt0 lambda2_lt1 Hk. (*TODO: get rid of this expansion*) set F := f n S. set PHI := @phi _ n _ S def. -exists (mkScode F PHI). -split. +exists (mkScode F PHI); split. rewrite /SrcRate /r /n /k 2!natRM; field. - split; exact/INR_eq0. + by split; exact/INR_eq0. set lhs := esrc(_, _). suff -> : lhs = (1 - Pr (P `^ k) (`TS P k (lambda / 2)))%R. rewrite leR_subl_addr addRC -leR_subl_addr. apply (@leR_trans (1 - lambda / 2)%R). - apply leR_add2l; rewrite leR_oppr oppRK; exact halflambdaepsilon. - by move: (Pr_TS_1 halflambda0 Hk). + by apply leR_add2l; rewrite leR_oppr oppRK; exact: lambda2_epsilon. + exact: (Pr_TS_1 lambda2_gt0). rewrite /lhs {lhs} /SrcErrRate /Pr /=. set lhs := \sum_(_ | _ ) _. suff -> : lhs = \sum_(x in 'rV[A]_k | x \notin S) P `^ k x. - have : forall a b : R, (a + b = 1 -> b = 1 - a)%R. by move=> ? ? <-; field. + have : forall a b : R, (a + b = 1 -> b = 1 - a)%R by move=> ? ? <-; field. apply. rewrite -[X in _ = X](Pr_cplt (P `^ k) (`TS P k (lambda / 2))). congr (_ + _)%R. - rewrite /Pr. - apply eq_bigl => ta /=. - by rewrite /`TS !inE. -rewrite /lhs {lhs}. -apply eq_bigl => // i. -rewrite inE /=. -apply/negPn/negPn. + by apply: eq_bigl => ta /=; rewrite !inE. +rewrite {}/lhs; apply eq_bigl => //= i. +rewrite inE /=; apply/negPn/negPn. - suff H : def \in S by move/eqP/phi_f; tauto. - exact: (TS_0_is_typ_seq halflambda0 halflambda1 Hk). -- suff S_2n : (#| S | < expn 2 n)%nat. - by move/(f_phi def S_2n)/eqP. + exact: (TS_0_is_typ_seq lambda2_gt0 lambda2_lt1 Hk). +- suff S_2n : (#| S | < expn 2 n)%nat by move/(f_phi def S_2n)/eqP. suff card_S_bound : #| S |%:R < exp2 (k%:R * r). apply/ltP/INR_lt; rewrite -natRexp2. - suff : INR n = (INR k * r)%R by move=> ->. + suff : n%:R = (k%:R * r)%R by move=> ->. rewrite /n /k /r (natRM _ den.+1) /Rdiv -mulRA. - by rewrite (mulRCA (INR den.+1)) mulRV ?INR_eq0' // mulR1 natRM. + by rewrite (mulRCA den.+1%:R) mulRV ?INR_eq0' // mulR1 natRM. suff card_S_bound : 1 + #| S |%:R <= exp2 (k%:R * r) by lra. suff card_S_bound : 1 + #| S |%:R <= exp2 (k%:R * (`H P + lambda)). apply: leR_trans; first exact: card_S_bound. - apply Exp_le_increasing => //; apply leR_wpmul2l; [exact/leR0n | exact/Hlambdar]. - apply (@leR_trans (exp2 (INR k * (lambda / 2) + - INR k * (`H P + lambda / 2)))); last first. + by apply Exp_le_increasing => //; apply leR_wpmul2l; [exact/leR0n | exact/Hlambdar]. + apply (@leR_trans (exp2 (k%:R * (lambda / 2) + k%:R * (`H P + lambda / 2)))); last first. rewrite -mulRDr addRC -addRA. rewrite (_ : forall a, a / 2 + a / 2 = a)%R; last by move=> ?; field. exact/leRR. apply (@leR_trans (exp2 (1 + INR k * (`H P + lambda / 2)))); last first. apply Exp_le_increasing => //; apply leR_add2r. move/leR_max : Hdelta => [_ Hlambda]. - apply (@leR_pmul2r (2 / lambda)%R); first exact lambdainv2. + apply (@leR_pmul2r (2 / lambda)%R); first by apply/divR_gt0 => //; exact: lambda_gt0. rewrite mul1R -mulRA -{2}(Rinv_Rdiv lambda 2); last 2 first. - by apply/eqP; rewrite gtR_eqF //; exact/lambda0. + by apply/eqP; rewrite gtR_eqF //; exact/lambda_gt0. by move=> ?; lra. - by rewrite mulRV ?mulR1 //; exact/gtR_eqF/halflambda0. + by rewrite mulRV ?mulR1 //; exact/gtR_eqF/lambda2_gt0. apply: leR_trans; first exact/leR_add2l/TS_sup. apply (@leR_trans (exp2 (INR k* (`H P + lambda / 2)) + exp2 (INR k * (`H P + lambda / 2)))%R). - + apply leR_add2r. - rewrite -exp2_0. - apply Exp_le_increasing => //. + + apply/leR_add2r. + rewrite -exp2_0; apply Exp_le_increasing => //. apply mulR_ge0; first exact: leR0n. apply addR_ge0; first exact: entropy_ge0. - apply Rlt_le; exact: halflambda0. - + rewrite (_ : forall a, a + a = 2 * a)%R; last by move=> ?; field. - rewrite {1}(_ : 2 = exp2 (log 2)); last by rewrite logK //; lra. - by rewrite -ExpD {1}/log Log_n //; exact/leRR. + apply Rlt_le; exact: lambda2_gt0. + + by rewrite addRR -{1}(logK Rlt_0_2) -ExpD {1}/log Log_n //; exact/leRR. Qed. End source_coding_direct'. Section source_coding_direct. - Variables (A : finType) (P : fdist A). -Theorem source_coding_direct : forall epsilon, 0 < epsilon < 1 -> +Theorem source_coding_direct epsilon : 0 < epsilon < 1 -> forall r : Qplus, `H P < r -> exists k n (sc : scode_fl A k n), SrcRate sc = r /\ esrc(P , sc) <= epsilon. Proof. -move=> eps Heps re HP_r. -destruct re as [num den]. -exists (k P num den eps), (n P num den eps); exact: source_coding'. +move=> Heps re HP_r; destruct re as [num den]. +by exists (k P num den epsilon), (n P num den epsilon); exact: source_coding'. Qed. End source_coding_direct. diff --git a/probability/convex.v b/probability/convex.v index 58c9092c..b24bcc5b 100644 --- a/probability/convex.v +++ b/probability/convex.v @@ -541,7 +541,7 @@ 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. + 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))%R. apply: (big_ind2 (fun y q => scalept q x = y /\ 0 <= q))%R. @@ -688,7 +688,7 @@ by rewrite pq_is_rs mulRC s_of_pqE onemK. Qed. HB.instance Definition __cone := @isConvexSpace.Build (scaled A) - (Choice.class [the choiceType of (scaled A)]) convpt convpt1 convptmm convptC + (Choice.class [the choiceType of scaled A]) convpt convpt1 convptmm convptC convptA. Lemma convptE p (a b : scaled A) : a <| p |> b = convpt p a b. @@ -802,8 +802,8 @@ Qed. 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 p) !(mulRC p.~) addptA addptC. +apply: S1_inj; rewrite ![in LHS]affine_conv/= !convptE. +rewrite !scaleptDr !scaleptA// !(mulRC p) !(mulRC p.~) addptA addptC. rewrite (addptC (scalept (q * p) _)) !addptA -addptA -!scaleptA -?scaleptDr//. by rewrite !(addptC (scalept _.~ _)) !affine_conv. Qed. diff --git a/probability/fsdist.v b/probability/fsdist.v index 8835df25..ef34e62b 100644 --- a/probability/fsdist.v +++ b/probability/fsdist.v @@ -205,7 +205,7 @@ Qed. Section fsdistbind. Variables (A B : choiceType) (p : {dist A}) (g : A -> {dist B}). -Let D := \bigcup_(d <- g @` [fset a | a in finsupp p]) finsupp d. +Let D := \bigcup_(d <- g @` finsupp p) finsupp d. Let f : {fsfun B -> R with 0} := [fsfun b in D => \sum_(a <- finsupp p) p a * (g a) b | 0]. @@ -231,14 +231,14 @@ rewrite [X in (_ + X)%R = _]big1 ?addR0; last first. rewrite (eq_bigl (fun i => i \in finsupp (g a))); last first. move=> b; rewrite andb_idl // mem_finsupp => gab0. apply/bigfcupP; exists (g a); rewrite ?mem_finsupp // andbT. - by apply/imfsetP; exists a => //; rewrite inE mem_finsupp. + by apply/imfsetP; exists a => //; rewrite mem_finsupp. rewrite -big_filter -[RHS](FSDist.f1 (g a)); apply perm_big. apply uniq_perm; [by rewrite filter_uniq | by rewrite fset_uniq |move=> b]. rewrite mem_finsupp. apply/idP/idP => [|gab0]; first by rewrite mem_filter mem_finsupp => /andP[]. rewrite mem_filter 2!mem_finsupp gab0 /= /f fsfunE ifT; last first. apply/bigfcupP; exists (g a); rewrite ?mem_finsupp // andbT. - by apply/imfsetP; exists a => //; rewrite inE mem_finsupp. + by apply/imfsetP; exists a => //; rewrite mem_finsupp. apply: contra gab0 => /eqP/psumR_seq_eq0P. rewrite fset_uniq => /(_ isT) H. suff : p a * g a b = 0. @@ -257,14 +257,12 @@ Proof. apply/fsetP => b; rewrite mem_finsupp; apply/idP/idP => [|]. by rewrite fsdistbindE; case: ifPn => //; rewrite eqxx. case/bigfcupP => dB. -rewrite andbT => /imfsetP[a] /=. -rewrite imfset_id => ap ->{dB} bga. +rewrite andbT => /imfsetP[a] /= ap ->{dB} bga. rewrite fsdistbindE; case: ifPn => [/bigfcupP[dB] | ]; last first. apply: contra => _. apply/bigfcupP; exists (g a)=> //; rewrite andbT. by apply/imfsetP; exists a => //=; rewrite imfset_id. -rewrite andbT => /imfsetP[a0] /=. -rewrite imfset_id => a0p ->{dB} bga0. +rewrite andbT => /imfsetP[a0] /= a0p ->{dB} bga0. apply/eqP => H. have : (p a0) * (g a0) b <> 0. by rewrite mulR_eq0 => -[]; apply/eqP; rewrite -mem_finsupp. @@ -285,15 +283,14 @@ Lemma fsdist1bind (A B : choiceType) (a : A) (f : A -> {dist B}) : Proof. apply/val_inj/val_inj => /=; congr fmap_of_fsfun; apply/fsfunP => b. rewrite fsdistbindE; case: ifPn => [|H]. - case/bigfcupP => /= d; rewrite andbT. - case/imfsetP => a0 /= /imfsetP[a1 /=]. - rewrite supp_fsdist1 inE => /eqP ->{a1} ->{a0} ->{d} bfa. + case/bigfcupP => /= d; rewrite andbT => /imfsetP[a0/=]. + rewrite supp_fsdist1 inE => /eqP ->{a0} ->{d} bfa. by rewrite big_seq_fsetE big_fset1/= fsdist1xx mul1R. have [->//|fab0] := eqVneq ((f a) b) 0%R. case/bigfcupP : H. exists (f a); last by rewrite mem_finsupp. rewrite andbT; apply/imfsetP; exists a => //=. -by rewrite imfset_id supp_fsdist1 inE. +by rewrite supp_fsdist1 inE. Qed. Lemma fsdistbind1 (A : choiceType) (p : {dist A}) : p >>= (@fsdist1 A) = p. @@ -301,14 +298,14 @@ Proof. apply/val_inj/val_inj => /=; congr fmap_of_fsfun; apply/fsfunP => b. rewrite fsdistbindE; case: ifPn => [|H]. case/bigfcupP => /= d; rewrite andbT. - case/imfsetP => /= a /imfsetP[a0] /= pa00 ->{a} ->{d}. + case/imfsetP => /= a ap ->{d}. rewrite supp_fsdist1 inE => /eqP ->{b}. - rewrite (big_fsetD1 a0) //= fsdist1xx mulR1 big1_fset ?addR0 // => a. - by rewrite !inE => /andP[aa0] ap _; rewrite fsdist10 ?mulR0// eq_sym. + rewrite (big_fsetD1 a) //= fsdist1xx mulR1 big1_fset ?addR0 // => a0. + by rewrite !inE => /andP[aa0] a0p _; rewrite fsdist10 ?mulR0// eq_sym. have [->//|pb0] := eqVneq (p b) 0%R. case/bigfcupP : H. exists (fsdist1 b); last by rewrite supp_fsdist1 inE. -by rewrite andbT; apply/imfsetP; exists b => //=; rewrite imfset_id mem_finsupp. +by rewrite andbT; apply/imfsetP; exists b => //=; rewrite mem_finsupp. Qed. Lemma fsdistbindA (A B C : choiceType) (m : {dist A}) (f : A -> {dist B}) @@ -319,20 +316,17 @@ apply/val_inj/val_inj => /=; congr fmap_of_fsfun; apply/fsfunP => c. rewrite !fsdistbindE; case: ifPn => [|H]; last first. rewrite ifF //; apply/negbTE; apply: contra H. case/bigfcupP => /= dC; rewrite andbT. - move=> /imfsetP[x] /=; rewrite imfset_id => mx ->{dC}. + move=> /imfsetP[x] /= mx ->{dC}. rewrite supp_fsdistbind. - case/bigfcupP => dC; rewrite andbT => /imfsetP[b] /=. - rewrite imfset_id => bfx ->{dC} cgb. + case/bigfcupP => dC; rewrite andbT => /imfsetP[b] /= bfx ->{dC} cgb. apply/bigfcupP; exists (g b) => //; rewrite andbT. apply/imfsetP; exists b => //=. - rewrite imfset_id supp_fsdistbind. - apply/bigfcupP; exists (f x) => //; rewrite andbT. - by apply/imfsetP; exists x => //=; rewrite imfset_id. + rewrite supp_fsdistbind. + by apply/bigfcupP; exists (f x) => //; rewrite andbT; apply/imfsetP; exists x. case/bigfcupP => /= dC. rewrite andbT => /imfsetP[b] /=. -rewrite imfset_id {1}supp_fsdistbind => /bigfcupP[dB]. -rewrite andbT => /imfsetP[a] /=. -rewrite imfset_id => ma ->{dB} fab0 ->{dC} gbc0. +rewrite {1}supp_fsdistbind => /bigfcupP[dB]. +rewrite andbT => /imfsetP[a] /= => ma ->{dB} fab0 ->{dC} gbc0. rewrite ifT; last first. apply/bigfcupP => /=; exists (f a >>= g); last first. rewrite supp_fsdistbind; apply/bigfcupP; exists (g b) => //. @@ -354,8 +348,7 @@ rewrite fsdistbindE. have [->|ma00] := eqVneq (m a0) 0%R. by rewrite mul0R big1_fset // => b2 _ _; rewrite 2!mul0R. case: ifPn => [/bigfcupP[dC] | Hc]. - rewrite andbT => /imfsetP[b0] /=. - rewrite imfset_id => fa0b0 ->{dC} gb0c. + rewrite andbT => /imfsetP[b0] /= fa0b0 ->{dC} gb0c. under eq_bigr do rewrite -mulRA. rewrite -(big_distrr (m a0)) /=; congr (_ * _). rewrite (big_fsetID _ (mem (finsupp (f a0)))) /=. @@ -369,16 +362,15 @@ case: ifPn => [/bigfcupP[dC] | Hc]. case/imfsetP; exists b1 => //=. rewrite inE fa0b1 andbT mem_finsupp fsdistbindE ifT. have /eqP K : (m a0 * (f a0 b1) <> R0 :> R). - rewrite mulR_eq0 => -[]. - exact/eqP. + rewrite mulR_eq0 => -[]; first exact/eqP. by apply/eqP; rewrite -mem_finsupp. apply/eqP => /psumR_seq_eq0P => L. move/eqP : K; apply. apply L => //. - - move=> a1 _; exact: mulR_ge0. + - by move=> a1 _; exact: mulR_ge0. - by rewrite mem_finsupp. apply/bigfcupP; exists (f a0) => //; rewrite andbT. - by apply/imfsetP; exists a0 => //=; rewrite imfset_id mem_finsupp. + by apply/imfsetP; exists a0 => //=; rewrite mem_finsupp. rewrite supp_fsdistbind. suff : \sum_(i <- finsupp (m >>= f)) (f a0) i * (g i) c = R0 :> R. rewrite supp_fsdistbind => L. @@ -392,9 +384,7 @@ apply/psumR_seq_eq0P. have [-> | fa0a1] := eqVneq (f a0 a1) 0%R; first by rewrite mul0R. case/bigfcupP : Hc. exists (g a1); last by rewrite mem_finsupp. - rewrite andbT. - apply/imfsetP; exists a1 => //=. - by rewrite imfset_id mem_finsupp. + by rewrite andbT; apply/imfsetP; exists a1 => //=; rewrite mem_finsupp. Qed. Definition fsdistmap (A B : choiceType) (f : A -> B) (d : {dist A}) : {dist B} := @@ -419,8 +409,7 @@ rewrite {1}/fsdistmap [in LHS]fsdistbindE; case: ifPn => Hb. by rewrite big1 // => a fab; rewrite fsdist10 ?mulR0// eq_sym. by apply eq_bigr => a /eqP ->; rewrite fsdist1xx mulR1. rewrite big_seq_cond big1 // => a /andP[ad] fab. -exfalso; move/negP : Hb; apply. -apply/bigfcupP; rewrite imfset_id; exists (fsdist1 (f a)). +exfalso; move/negP : Hb; apply; apply/bigfcupP; exists (fsdist1 (f a)). by rewrite andbT; apply/imfsetP => /=; exists a. by rewrite (eqP fab) supp_fsdist1 inE. Qed. @@ -430,10 +419,10 @@ Lemma supp_fsdistmap (A B : choiceType) (f : A -> B) d : Proof. rewrite /fsdistmap supp_fsdistbind; apply/fsetP => d'. apply/bigfcupP/imfsetP => [[D]|]. - rewrite andbT => /imfsetP[a /=]; rewrite imfset_id => ad ->{D}. + rewrite andbT => /imfsetP[a /=] ad ->{D}. by rewrite supp_fsdist1 inE => /eqP ->{d'}; exists a. case=> a /= ad -> {d'}; exists (fsdist1 (f a)). - rewrite andbT; apply/imfsetP; exists a => //=; by rewrite imfset_id. + by rewrite andbT; apply/imfsetP; exists a. by rewrite supp_fsdist1 inE. Qed. @@ -475,11 +464,11 @@ Definition fsdistjoin A (D : {dist (FSDist_choiceType A)}) : {dist A} := Lemma fsdistjoinE A (D : {dist (FSDist_choiceType A)}) x : fsdistjoin D x = \sum_(d <- finsupp D) D d * d x. Proof. -rewrite /fsdistjoin fsdistbindE 2!imfset_id; case: ifPn => // xD. +rewrite /fsdistjoin fsdistbindE; case: ifPn => // xD. rewrite big_seq (eq_bigr (fun=> 0)) ?big1 // => d dD. have [->|dx0] := eqVneq (d x) 0; first by rewrite mulR0. exfalso; move/negP : xD; apply. -by apply/bigfcupP; exists d; [rewrite dD | rewrite mem_finsupp]. +by apply/bigfcupP; exists d; [rewrite andbT inE| rewrite mem_finsupp]. Qed. Lemma fsdistjoin1 (A : choiceType) (D : {dist (FSDist_choiceType A)}) : @@ -770,8 +759,7 @@ Lemma fsdistbindEwiden (B : choiceType) (a b : {dist A}) (f : A -> {dist B}) Proof. move=> p0 b0; rewrite fsdistbindE. case: ifPn => [/bigfcupP[dB] | Hb0]. -- rewrite andbT; case/imfsetP => a1 /=. - rewrite imfset_id => a1a ->{dB} b0fa1. +- rewrite andbT; case/imfsetP => a1 /= a1a ->{dB} b0fa1. apply/big_fset_incl; first exact/finsupp_conv_subr. by move=> a2 Ha2; rewrite memNfinsupp => /eqP ->; rewrite mul0R. - apply/esym/psumR_seq_eq0P => // a1 Ha1. @@ -780,7 +768,7 @@ case: ifPn => [/bigfcupP[dB] | Hb0]. apply/eqP; rewrite -memNfinsupp. apply: contra Hb0 => Hb0. apply/bigfcupP; exists (f a1) => //; rewrite andbT. - by apply/imfsetP; exists a1 => //=; rewrite imfset_id mem_finsupp. + by apply/imfsetP; exists a1 => //=; rewrite mem_finsupp. Qed. Let conv0 (mx my : {dist A}) : mx <| 0%:pr |> my = my. @@ -861,8 +849,7 @@ have [->|p0] := eqVneq p 0%:pr. have [->|p1] := eqVneq p 1%:pr. by rewrite conv1 mul1R onem1 mul0R addR0 fsdistbindE. case: ifPn => [/bigfcupP[dB] | Hb0]. - rewrite andbT => /imfsetP[a0 /=]. - rewrite inE /= => Ha0 ->{dB} b0a0. + rewrite andbT => /imfsetP[a0 /=] /= Ha0 ->{dB} b0a0. under eq_bigr. by move=> a1 _; rewrite fsdist_convE (@mulRDl _ _ (f a1 b0)) -!mulRA; over. rewrite big_split /= -2!big_distrr /=; congr (_ * _ + _ * _)%R. @@ -879,11 +866,10 @@ rewrite fsdistbindE; case: ifPn => // abs. exfalso. move/negP : Hb0; apply. case/bigfcupP : abs => dB. -rewrite andbT => /imfsetP[a0 /=] /imfsetP[a1 /=] a1a ->{a0} ->{dB} Hb0. -apply/bigfcupP; exists (f a1) => //; rewrite andbT. -apply/imfsetP; exists a1 => //=. -rewrite imfset_id. -by move: a1 a1a {Hb0}; apply/fsubsetP. +rewrite andbT => /imfsetP[a0 /=] a0c ->{dB} Hb0. +apply/bigfcupP; exists (f a0) => //; rewrite andbT. +apply/imfsetP; exists a0 => //=. +by move: a0 a0c {Hb0}; exact/fsubsetP. Qed. End fsdist_conv_prop. @@ -1077,7 +1063,7 @@ rewrite S1_proj_Convn_finType // S1_Convn_finType. set X := LHS. under eq_bigr do rewrite fdist_of_fsE. rewrite ssum_seq_finsuppE' supp_fsdistmap. -under eq_bigr do rewrite fsdistbindE imfset_id. +under eq_bigr do rewrite fsdistbindE. have Hsupp : forall y, y \in [fset f x | x in finsupp d] -> y \in \bigcup_(d0 <- [fset fsdist1 (f a) | a in finsupp d]) finsupp d0.