From b7074c49ca24b3642045602d59689d0c4004156a Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Thu, 4 Jul 2024 17:24:22 +0900 Subject: [PATCH] renaming (#124) --- changelog.txt | 4 ++ information_theory/aep.v | 2 +- information_theory/binary_symmetric_channel.v | 2 +- information_theory/erasure_channel.v | 2 +- information_theory/typ_seq.v | 4 +- information_theory/types.v | 5 +- probability/bayes.v | 3 +- probability/fdist.v | 6 +- probability/fsdist.v | 3 +- probability/jfdist_cond.v | 20 ++++-- probability/necset.v | 3 +- probability/proba.v | 10 +-- robust/robustmean.v | 64 +++++++++---------- robust/weightedmean.v | 4 +- 14 files changed, 71 insertions(+), 61 deletions(-) diff --git a/changelog.txt b/changelog.txt index 05cddac1..c688fe5a 100644 --- a/changelog.txt +++ b/changelog.txt @@ -1,3 +1,7 @@ + + +- lemma `conv_pt_cset_is_convex` changed into a `Let` + ------------------- from 0.7.1 to 0.7.2 ------------------- diff --git a/information_theory/aep.v b/information_theory/aep.v index 01115055..cfa6708a 100644 --- a/information_theory/aep.v +++ b/information_theory/aep.v @@ -136,7 +136,7 @@ have H2 k i : `V ((\row_(i < k.+1) `-- (`log P)) ``_ i) = aep_sigma2 P. by rewrite mxE V_mlog. have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon). move/(leR_trans _); apply. -apply/Pr_incl/subsetP => ta; rewrite 2!inE => /andP[H1]. +apply/subset_Pr/subsetP => ta; rewrite 2!inE => /andP[H1]. rewrite /sum_mlog_prod [`-- (`log _)]lock /= -lock /= /scalel_RV /log_RV /neg_RV. rewrite fdist_rVE. rewrite log_prodR_sumR_mlog //. diff --git a/information_theory/binary_symmetric_channel.v b/information_theory/binary_symmetric_channel.v index 7fb19997..29637710 100644 --- a/information_theory/binary_symmetric_channel.v +++ b/information_theory/binary_symmetric_channel.v @@ -274,7 +274,7 @@ Section dH_BSC. Variable p : {prob R}. Let card_F2 : #| 'F_2 | = 2%nat. by rewrite card_Fp. Qed. Let W := BSC.c card_F2 p. -Variables (M : finType) (n : nat) (f : encT [finType of 'F_2] M n). +Variables (M : finType) (n : nat) (f : encT 'F_2 M n). Local Open Scope vec_ext_scope. diff --git a/information_theory/erasure_channel.v b/information_theory/erasure_channel.v index 3aa0cd2f..c178b5ea 100644 --- a/information_theory/erasure_channel.v +++ b/information_theory/erasure_channel.v @@ -61,7 +61,7 @@ apply/eqP; rewrite psumr_eq0/=; last first. by rewrite eqxx implybT. Qed. -Definition c : `Ch(A, [finType of option A]) := +Definition c : `Ch(A, option A) := fun a => FDist.make (f0 a) (f1 a). End EC_sect. diff --git a/information_theory/typ_seq.v b/information_theory/typ_seq.v index 549618c8..baeb8bdb 100644 --- a/information_theory/typ_seq.v +++ b/information_theory/typ_seq.v @@ -196,11 +196,11 @@ have -> : Pr P `^ n.+1 (~: p) = by rewrite ler_norml; apply/andP; split; apply/RleP; rewrite -RminusE -RoppE; rewrite -RdivE ?gt_eqF// ?ltr0n// -INRE//. - rewrite Pr_union_disj // disjoints_subset; apply/subsetP => /= i. + rewrite disjoint_Pr_setU // disjoints_subset; apply/subsetP => /= i. by rewrite !inE /= => /eqP Hi; rewrite negb_and Hi ltxx. rewrite {1}/Pr (eq_bigr (fun=> 0)); last by move=> /= v; rewrite inE => /eqP. rewrite big_const iter_addR mulR0 add0R. -apply/(leR_trans _ (aep He k0_k))/Pr_incl/subsetP => /= t. +apply/(leR_trans _ (aep He k0_k))/subset_Pr/subsetP => /= t. rewrite !inE /= => /andP[-> H3]. rewrite /log_RV /= /scalel_RV /= mulRN -mulNR. apply/ltW. diff --git a/information_theory/types.v b/information_theory/types.v index cc459edb..f3969f1a 100644 --- a/information_theory/types.v +++ b/information_theory/types.v @@ -69,7 +69,8 @@ Proof. case: P => /= d f d_f; by rewrite d_f mulRCA mulRV ?INR_eq0' // mulR1. Qed. -Lemma INR_type_fun A n (P : P_ n ( A )) a : ((type.f P) a)%:R / n%:R = type.d(*TODO: fix coercion *)P a. +Lemma INR_type_fun A n (P : P_ n ( A )) a : + ((type.f P) a)%:R / n%:R = type.d(*TODO: fix coercion *)P a. Proof. destruct P as [d f d_f] => /=. by rewrite d_f. Qed. Lemma no_0_type (A : finType) (d : {fdist A}) (t : {ffun A -> 'I_1}) : @@ -476,7 +477,7 @@ case/boolP : [exists x, x \in T_{P}] => x_T_P. exact: Pr_le1. symmetry. rewrite /Pr. - transitivity (\sum_(a | (a \in [finType of 'rV[A]_n]) && + transitivity (\sum_(a | (a \in 'rV[A]_n) && [pred x in (@row_of_tuple A n @: T_{P})] a) exp2 (- INR n * `H P)). apply eq_big => // ta'/= Hta'. diff --git a/probability/bayes.v b/probability/bayes.v index ab45adc1..1ec195f9 100644 --- a/probability/bayes.v +++ b/probability/bayes.v @@ -107,7 +107,8 @@ Section univ_types. (* heterogeneous types *) Variable n : nat. Variable types : 'I_n -> eqType. -Definition univ_types : eqType := [eqType of {dffun forall i, types i}]. +Definition univ_types : eqType := + [eqType of {dffun forall i, types i}]. Section prod_types. (* sets of indices *) diff --git a/probability/fdist.v b/probability/fdist.v index a538aef0..135cd716 100644 --- a/probability/fdist.v +++ b/probability/fdist.v @@ -660,11 +660,7 @@ Proof. by move=> Xa0; rewrite fdistD1E Xa0 mul0r; case: ifP. Qed. End fdistD1_prop. -(* TODO: move? *) -(* about_distributions_of_ordinals.*) - -Lemma fdistI0_False (R: realType) (d : R.-fdist 'I_O) - : False. +Lemma fdistI0_False (R : realType) (d : R.-fdist 'I_O) : False. Proof. move: (fdist_card_neq0 d); by rewrite card_ord. Qed. Section fdistI2. diff --git a/probability/fsdist.v b/probability/fsdist.v index 507b91d3..0839f539 100644 --- a/probability/fsdist.v +++ b/probability/fsdist.v @@ -1070,7 +1070,8 @@ rewrite /ball_ => xball. rewrite /nbhs /= /nbhs /=. rewrite /eventually /=. rewrite /filter_from /=. -suff: exists N, forall k, (N <= k)%nat -> P (\bigcup_n F n) = P (\bigcup_(i < k) F i). +suff: exists N, forall k, (N <= k)%nat -> + P (\bigcup_n F n) = P (\bigcup_(i < k) F i). case=> N HN. exists N => //. move=> j /= ij. diff --git a/probability/jfdist_cond.v b/probability/jfdist_cond.v index b3a4eee7..da994af2 100644 --- a/probability/jfdist_cond.v +++ b/probability/jfdist_cond.v @@ -73,22 +73,21 @@ split. by apply/Pr_cPr_gt0; move: H; rewrite jcPrE -setTE -EsetT. Qed. -(* TODO: rename *) -Lemma jcPr_cplt E F : Pr (P`2) F != 0 -> \Pr_[ ~: E | F] = 1 - \Pr_[E | F]. +Lemma jcPr_setC E F : Pr (P`2) F != 0 -> \Pr_[ ~: E | F] = 1 - \Pr_[E | F]. Proof. by move=> PF0; rewrite 2!jcPrE EsetT setCX cPr_cplt ?EsetT // setTE Pr_setTX. Qed. -(* TODO: rename *) -Lemma jcPr_diff E1 E2 F : \Pr_[E1 :\: E2 | F] = \Pr_[E1 | F] - \Pr_[E1 :&: E2 | F]. +Lemma jcPr_setD E1 E2 F : + \Pr_[E1 :\: E2 | F] = \Pr_[E1 | F] - \Pr_[E1 :&: E2 | F]. Proof. -rewrite jcPrE DsetT cPr_diff jcPrE; congr (_ - _). +rewrite jcPrE DsetT cPr_setD jcPrE; congr (_ - _). by rewrite 2!EsetT setIX setTI -EsetT jcPrE. Qed. -Lemma jcPr_union_eq E1 E2 F : +Lemma jcPr_setU E1 E2 F : \Pr_[E1 :|: E2 | F] = \Pr_[E1 | F] + \Pr_[E2 | F] - \Pr_[E1 :&: E2 | F]. -Proof. by rewrite jcPrE UsetT cPr_union_eq !jcPrE IsetT. Qed. +Proof. by rewrite jcPrE UsetT cPr_setU !jcPrE IsetT. Qed. Section total_probability. Variables (I : finType) (E : {set A}) (F : I -> {set B}). @@ -118,6 +117,13 @@ End total_probability. End conditional_probability. Notation "\Pr_ P [ E | F ]" := (jcPr P E F) : proba_scope. +#[deprecated(since="infotheo 0.7.3", note="renamed to `jcPr_setD`")] +Notation jcPr_diff := jcPr_setD (only parsing). +#[deprecated(since="infotheo 0.7.3", note="renamed to `jcPr_setC`")] +Notation jcPr_cplt := jcPr_setC (only parsing). +#[deprecated(since="infotheo 0.7.3", note="renamed to `jcPr_setU`")] +Notation jcPr_union_eq := jcPr_setU (only parsing). + Section jPr_Pr. Variables (U : finType) (P : {fdist U}) (A B : finType). Variables (X : {RV P -> A}) (Y : {RV P -> B}) (E : {set A}) (F : {set B}). diff --git a/probability/necset.v b/probability/necset.v index e799ab3e..592e6e65 100644 --- a/probability/necset.v +++ b/probability/necset.v @@ -348,8 +348,7 @@ HB.instance Definition _ (X Y : neset A) := HB.instance Definition _ (X : neset A) (n : nat) := isNESet.Build _ _ (iter_conv_set_neq0 X n). -(* TODO: Let insteaad of Lemma *) -Lemma conv_pt_cset_is_convex (p : {prob R}) (x : A) (Y : {convex_set A}) : +Let conv_pt_cset_is_convex (p : {prob R}) (x : A) (Y : {convex_set A}) : is_convex_set (conv_pt_set p x Y). Proof. apply/asboolP=> u v q. diff --git a/probability/proba.v b/probability/proba.v index 8d89a9a3..7e81ac2d 100644 --- a/probability/proba.v +++ b/probability/proba.v @@ -1370,13 +1370,11 @@ rewrite /cPr; apply/divR_gt0; rewrite Pr_gt0P //. by apply: contra H; rewrite setIC => /eqP F0; apply/eqP/Pr_domin_setI. Qed. -(* TODO: rename *) -Lemma cPr_diff F1 F2 E : +Lemma cPr_setD F1 F2 E : `Pr_[F1 :\: F2 | E] = `Pr_[F1 | E] - `Pr_[F1 :&: F2 | E]. Proof. by rewrite /cPr -divRBl setIDAC Pr_setD setIAC. Qed. -(* TODO: rename *) -Lemma cPr_union_eq F1 F2 E : +Lemma cPr_setU F1 F2 E : `Pr_[F1 :|: F2 | E] = `Pr_[F1 | E] + `Pr_[F2 | E] - `Pr_[F1 :&: F2 | E]. Proof. by rewrite /cPr -divRDl -divRBl setIUl Pr_setU setIACA setIid. Qed. @@ -1445,6 +1443,10 @@ Notation cPr_eq0 := cPr_eq0P (only parsing). Notation cPr_max := cPr_le1 (only parsing). #[deprecated(since="infotheo 0.7.2", note="renamed to `cPr_gt0P`")] Notation cPr_gt0 := cPr_gt0P (only parsing). +#[deprecated(since="infotheo 0.7.3", note="renamed to `cPr_setD`")] +Notation cPr_diff := cPr_setD (only parsing). +#[deprecated(since="infotheo 0.7.3", note="renamed to `cPr_setU`")] +Notation cPr_union_eq := cPr_setU (only parsing). Section fdist_cond. Variables (A : finType) (P : R.-fdist A) (E : {set A}). diff --git a/robust/robustmean.v b/robust/robustmean.v index ebad18c4..146d8708 100644 --- a/robust/robustmean.v +++ b/robust/robustmean.v @@ -276,7 +276,7 @@ Lemma cEx_sub (X : {RV P -> R}) (F G: {set U}) : `| `E_[ X | F ] - `E_[X | G] | = `| `E ((X `-cst `E_[X | G]) `* Ind F : {RV P -> R}) | / Pr P F. Proof. -move=> /[dup] /Pr_gt0 PrPF_neq0 /invR_gt0 /ltRW PrPFV_ge0 FsubG. +move=> /[dup] /Pr_gt0P PrPF_neq0 /invR_gt0 /ltRW PrPFV_ge0 FsubG. rewrite divRE -(geR0_norm (/Pr P F)) // -normRM. apply: congr1. by rewrite -[RHS]cEx_ExInd cEx_trans_min_RV. @@ -306,9 +306,9 @@ Lemma cEx_cVar (X : {RV P -> R}) (F G: {set U}) : 0 < Pr P F -> `| `E_[ X | F ] - mu | <= sqrt (var * Pr P G / Pr P F ). Proof. move=> /[dup] /invR_gt0 /ltRW PrPFV_nneg /[dup] /invR_gt0 - PrPFV_pos /[dup] /Pr_gt0 PrPF_neq0 PrPF_pos - /[dup] /(Pr_incl P) /(ltR_leR_trans PrPF_pos) - /[dup] /Pr_gt0 PrPG_neq0 PrPG_pos FsubG mu var. + PrPFV_pos /[dup] /Pr_gt0P PrPF_neq0 PrPF_pos + /[dup] /(subset_Pr P) /(ltR_leR_trans PrPF_pos) + /[dup] /Pr_gt0P PrPG_neq0 PrPG_pos FsubG mu var. rewrite cEx_sub //. pose y := sqrt (Ex P (((X `-cst mu) `^2) `* Ind F) * Ex P (Ind F)) / Pr P F. apply leR_trans with (y := y). @@ -360,7 +360,7 @@ Proof. repeat rewrite mulR1. rewrite in_setC. destruct (i \in F); simpl; lra. - all: apply Pr_gt0; try rewrite Pr_of_cplt; lra. + all: apply Pr_gt0P; try rewrite Pr_setC; lra. Qed. Lemma cEx_Inv_int (X: {RV P -> R}) F: @@ -372,7 +372,7 @@ Proof. repeat rewrite cEx_ExInd. (repeat have ->: forall x y, x != 0 -> x * (y / x) = y by move => x y Hz; rewrite mulRC -mulRA mulVR; last by []; rewrite mulR1); - try apply Pr_gt0; try rewrite Pr_of_cplt; try lra. + try apply Pr_gt0P; try rewrite Pr_setC; try lra. apply Rplus_eq_reg_r with (r:= Pr P F * `E X). rewrite -addRA Rplus_opp_l addR0 -addRA addRC. apply Rplus_eq_reg_r with (r:=`E (X `* Ind (~: F):{RV P -> R})). @@ -392,9 +392,9 @@ Lemma cEx_Inv' (X: {RV P -> R}) (F G : {set U}) : `| `E_[X | F] - `E_[X | G]| = (Pr P (G :\: F)) / (Pr P F) * `| `E_[X | (G :\: F)] - `E_[X | G]|. Proof. move=> PrPF_gt0 /[dup] /setIidPr GIFF FsubG /[dup] /(ltR_trans PrPF_gt0) - /[dup] /Pr_gt0 /invR_neq0' /eqP PrPG_neq0 PrPG_gt0 PrPF_PrPG. -have : 0 < Pr P (G :\: F) by rewrite Pr_diff subR_gt0 GIFF. -move => /[dup] /Pr_gt0 PrPGF_neq0 PrPGF_gt0. + /[dup] /Pr_gt0P /invR_neq0' /eqP PrPG_neq0 PrPG_gt0 PrPF_PrPG. +have : 0 < Pr P (G :\: F) by rewrite Pr_setD subR_gt0 GIFF. +move => /[dup] /Pr_gt0P PrPGF_neq0 PrPGF_gt0. rewrite !cEx_sub ?subsetDl // !divRE mulRCA. rewrite Ind_setD//. rewrite !coqRE mulrAC divff// mul1r -!coqRE. @@ -412,9 +412,9 @@ Lemma cEx_Inv (X: {RV P -> R}) F : 0 < Pr P F -> Pr P F < 1 -> `| `E_[X | F] - `E X| = (1 - Pr P F) / Pr P F * `| `E_[X | (~: F)] - `E X|. Proof. -move=> *; rewrite Ex_cExT -Pr_of_cplt -setTD; apply cEx_Inv' => //. -apply ltR_neqAle; split; last by apply/Pr_incl/subsetT. -by apply/eqP; rewrite Pr_setT -Pr_lt1. +move=> *; rewrite Ex_cExT -Pr_setC -setTD; apply cEx_Inv' => //. +apply ltR_neqAle; split; last by apply/subset_Pr/subsetT. +by apply/eqP; rewrite Pr_setT -Pr_lt1P. Qed. Lemma cvariance_ge0 (X : {RV P -> R}) F : 0 <= `V_[X | F]. @@ -585,7 +585,7 @@ have [Pr_FG_eq|/eqP Pr_FG_neq] := eqVneq (Pr P F) (Pr P G). by move=> i /GFP0 ->; rewrite mulR0. exact/sqrt_pos. have [?|/eqP PrF_neq0] := eqVneq (Pr P F) 0; first nra. -have ? := Pr_incl P FG. +have ? := subset_Pr P FG. have ? := Pr_ge0 P F. have [?|/eqP PrG_neq0] := eqVneq (Pr P G) 0; first by nra. have HPrFpos : 0 < Pr P F by have := Pr_ge0 P F; lra. @@ -607,7 +607,7 @@ rewrite cEx_Inv'//; last lra. apply: leR_trans. apply leR_wpmul2l; first exact: divR_ge0. apply cEx_cVar => //; last exact: subsetDl. - by rewrite Pr_diff HGnF_F subR_gt0; lra. + by rewrite Pr_setD HGnF_F subR_gt0; lra. apply: (@leR_trans (sqrt (`V_[ X | G] * (Pr P G * (1 - delta)) / (Pr P G * delta * delta)))). rewrite -(Rabs_pos_eq (Pr P (G :\: F) / Pr P F)); last exact: divR_ge0. @@ -616,7 +616,7 @@ apply: (@leR_trans rewrite !divRE !mulRA [in X in X <= _](mulRC _ (`V_[X | G])) -!mulRA. apply: leR_wpmul2l; first exact: cvariance_ge0. rewrite !mulRA mulRC !mulRA mulVR ?mul1R; last first. - by rewrite Pr_diff HGnF_F; apply/eqP; nra. + by rewrite Pr_setD HGnF_F; apply/eqP; nra. rewrite mulRC (mulRC (/Pr P F)) -mulRA -invRM; [|exact/gtR_eqF|exact/gtR_eqF]. rewrite mulRA; apply/leR_pdivr_mulr; first by nra. rewrite mulRAC; apply/leR_pdivl_mulr; first by apply: Rmult_lt_0_compat; nra. @@ -625,7 +625,7 @@ apply: (@leR_trans rewrite (mulRC (Pr P G)) -mulRA; apply: leR_pmul => //. - apply: mulR_ge0 => //; apply/mulR_ge0; last exact/ltRW. by apply/mulR_ge0 => //; exact/ltRW. - - by rewrite Pr_diff HGnF_F; nra. + - by rewrite Pr_setD HGnF_F; nra. - by rewrite mulRCA; apply: leR_pmul; nra. apply sqrt_le_1_alt. rewrite divRE invRM; [|exact/gtR_eqF/mulR_gt0|exact/gtR_eqF]. @@ -669,21 +669,21 @@ move=> bad mu_hat mu sigma Hmin_outliers Hmax_outliers Hbad_ratio Hdrop_ratio have H : Pr P good = 1 - eps by apply/esym/subR_eq; rewrite -Hbad_ratio Pr_cplt. (* On the other hand, we remove at most 4ε good points *) have max_good_drop : Pr P (good :&: drop) <= 4 * eps. - by rewrite -Hdrop_ratio; exact/Pr_incl/subsetIr. + by rewrite -Hdrop_ratio; exact/subset_Pr/subsetIr. pose eps' := Pr P (bad :\: drop) / Pr P (~: drop). have Hcompl : Pr P (good :\: drop) / Pr P (~: drop) = 1 - eps'. - apply/esym/subR_eq; rewrite /eps' -mulRDl -Pr_union_disj. - by rewrite -setDUl setUCr setTD mulRV// Pr_of_cplt; apply/eqP; lra. + apply/esym/subR_eq; rewrite /eps' -mulRDl -disjoint_Pr_setU. + by rewrite -setDUl setUCr setTD mulRV// Pr_setC; apply/eqP; lra. by rewrite -setI_eq0 -setDIl setICr set0D. have eps'_ge0 : 0 <= eps'. - by apply: mulR_ge0 => //; apply/ltRW/invR_gt0; rewrite Pr_of_cplt; lra. + by apply: mulR_ge0 => //; apply/ltRW/invR_gt0; rewrite Pr_setC; lra. have eps'_le1 : eps' <= 1. - rewrite /eps'; apply/leR_pdivr_mulr; first by rewrite Pr_of_cplt; lra. - by rewrite mul1R; exact/Pr_incl/subsetDr. + rewrite /eps'; apply/leR_pdivr_mulr; first by rewrite Pr_setC; lra. + by rewrite mul1R; exact/subset_Pr/subsetDr. (* Remaining good points: 1 - (4 * eps) / (1 - eps) *) pose delta := 1 - (4 * eps) / (1 - eps). have min_good_remain : delta <= Pr P (good :\: drop) / Pr P good. - rewrite /delta Pr_diff H. + rewrite /delta Pr_setD H. apply: (@leR_trans ((1 - eps - 4 * eps) / (1 - eps))). apply/leR_pdivl_mulr; first lra. by rewrite mulRDl -mulNR -(mulRA _ (/ _)) Rinv_l; lra. @@ -702,10 +702,10 @@ have Exgood_bound : `| `E_[X | good :\: drop ] - `E_[X | good] | <= - suff : `E_[X | (good :\: drop)] = `E_[X | good]. by move=> ->; rewrite subRR normR0; exact: sqrt_pos. apply: eq_bigr => i _; rewrite gdg; congr (_ * _ * _). - rewrite setIDA Pr_diff -setIA. + rewrite setIDA Pr_setD -setIA. (* NB: lemma? *) apply/subR_eq; rewrite addRC; apply/subR_eq; rewrite subRR; apply/esym. - move: gdg; rewrite Pr_diff => /subR_eq; rewrite addRC => /subR_eq. + move: gdg; rewrite Pr_setD => /subR_eq; rewrite addRC => /subR_eq. by rewrite subRR [in X in _ -> X]setIC => /esym; exact: Pr_domin_setI. - apply cresilience. + apply (@ltR_pmul2r (1 - eps)); first lra. @@ -731,7 +731,7 @@ have Exbad_bound : 0 < Pr P (bad :\: drop) -> move: ibaddrop; rewrite inE => /andP[idrop ibad]. by rewrite leRNgt => /Hquantile_drop_bad => /(_ ibad); apply/negP. have max_bad_remain : Pr P (bad :\: drop) <= eps / Pr P (~: drop). - rewrite Pr_of_cplt Hdrop_ratio Pr_diff Hbad_ratio. + rewrite Pr_setC Hdrop_ratio Pr_setD Hbad_ratio. apply: (@leR_trans eps); first exact/leR_subl_addr/leR_addl. by apply/leR_pdivl_mulr; [lra|nra]. have Ex_not_drop : `E_[ X | ~: drop ] = @@ -741,7 +741,7 @@ have Ex_not_drop : `E_[ X | ~: drop ] = have good_bad : Pr P (good :\: drop) + Pr P (bad :\: drop) = Pr P (~: drop). rewrite -(_ : good :\: drop :|: bad :\: drop = ~: drop); last first. by rewrite -setDUl setUCr setTD. - rewrite Pr_union_eq. + rewrite Pr_setU. apply/subR_eq; rewrite subR_opp addRC; apply/esym/subR_eq; rewrite subRR. suff : (good :\: drop) :&: (bad :\: drop) = set0. by move=> ->; rewrite Pr_set0. @@ -750,7 +750,7 @@ have Ex_not_drop : `E_[ X | ~: drop ] = - rewrite bd0 addR0 in good_bad. rewrite bd0 mulR0 addR0 good_bad. rewrite /Rdiv -mulRA mulRV ?mulR1; last first. - by apply/Pr_gt0; rewrite -good_bad Pr_diff H; lra. + by apply/Pr_gt0P; rewrite -good_bad Pr_setD H; lra. rewrite 2!cEx_ExInd good_bad; congr (_ / _). apply/eq_bigr => u _. rewrite /ambient_dist -!mulRA; congr (_ * _). @@ -759,9 +759,9 @@ have Ex_not_drop : `E_[ X | ~: drop ] = have bad_drop0 : u \in bad :\: drop -> P u = 0 by apply Pr_set0P. case: ifPn => idrop //=. by case: ifPn => // igood; rewrite bad_drop0 ?mulR0// !inE idrop. - - apply/eqR_divl_mulr; first by rewrite Pr_of_cplt; apply/eqP; nra. + - apply/eqR_divl_mulr; first by rewrite Pr_setC; apply/eqP; nra. rewrite !cEx_ExInd -!mulRA. - rewrite Rinv_l ?mulR1; last by rewrite Pr_of_cplt; nra. + rewrite Rinv_l ?mulR1; last by rewrite Pr_setC; nra. rewrite Rinv_l ?mulR1; last nra. rewrite Rinv_l // mulR1. rewrite [in RHS]/Ex -big_split; apply: eq_bigr => i _ /=. @@ -790,12 +790,12 @@ apply: (@leR_trans (sqrt (`V_[ X | good] / eps) * eps' + by rewrite !(mulR0,add0R,subR0,mulR1). have [->|/eqP eps'1] := eqVneq eps' 1. rewrite !(subRR,mulR0,addR0,mulR1); apply: Exbad_bound. - apply Pr_gt0; apply: contra_notN eps'0 => /eqP. + apply Pr_gt0P; apply: contra_notN eps'0 => /eqP. by rewrite /eps' => ->; rewrite div0R. have [bd0|bd0] := eqVneq (Pr P (bad :\: drop)) 0. by exfalso; apply/eps'0; rewrite /eps' bd0 div0R. apply: leR_add; (apply/leR_pmul2r; first lra). - - exact/Exbad_bound/Pr_gt0. + - exact/Exbad_bound/Pr_gt0P. - exact: Exgood_bound. rewrite /sigma /Rdiv !sqrt_mult //; last 8 first. - exact: cvariance_ge0. diff --git a/robust/weightedmean.v b/robust/weightedmean.v index 5631f330..76d05010 100644 --- a/robust/weightedmean.v +++ b/robust/weightedmean.v @@ -769,7 +769,7 @@ apply (@le_trans _ _ ((1 - eps) * (`V_[X | S] + (`E_[X | S] - `E (WP.-RV X))^+2) apply (@le_trans _ _ ((1 - eps) * (`V_[X | S] + (Num.sqrt (`V_[X | S] * 2 * eps / (2 - eps)) + Num.sqrt (`V (WP.-RV X) * 2 * eps / (1 - eps)))^+2))). apply ler_wpM2l. - by rewrite subr_ge0; exact/RleP/Pr_1. + by rewrite subr_ge0; exact/RleP/Pr_le1. rewrite lerD2l -ler_abs_sqr. rewrite [x in _ <= x]ger0_norm; first exact: (bound_mean_emean C eps_max). exact/addr_ge0/sqrtr_ge0/sqrtr_ge0. @@ -877,7 +877,7 @@ Lemma bound_empirical_variance_cplt_S : 2/denom * `V (WP.-RV X) <= \sum_(i in cplt_S) C i * P i * tau i. Proof. have ? := pr_S_gt0 eps_max01 low_eps. -have /RleP pr1_cplt_S := Pr_1 P cplt_S. +have /RleP pr1_cplt_S := Pr_le1 P cplt_S. have -> : \sum_(i in cplt_S) C i * P i * tau i = `V (WP.-RV X) * (\sum_(i in U) C i * P i) - (\sum_(i in S) C i * P i * tau i).