diff --git a/robust/weightedmean.v b/robust/weightedmean.v index 76d05010..d3941826 100644 --- a/robust/weightedmean.v +++ b/robust/weightedmean.v @@ -290,7 +290,7 @@ Proof. by rewrite /d; unlock; rewrite ffunE. Qed. (* NB: infotheo/proba.v has following two lemmas with very similar names Lemma Pr_XsetT E : Pr P (E `* [set: B]) = Pr (P`1) E. Lemma Pr_setTX F : Pr P ([set: A] `* F) = Pr (P`2) F. *) -Lemma Pr_setXT A : Pr P A = Pr d (A `* [set: bool]). +Lemma Pr_setXT A : Pr P A = Pr d (A `* [set: bool]). (* TODO: reverse order *) Proof. rewrite /Pr big_setX/=; apply: eq_bigr => u uS. rewrite setT_bool big_setU1//= ?inE// big_set1. @@ -468,6 +468,149 @@ Qed. End pos_evar. +Section resilience. +Variables (U : finType) (P : {fdist U}). + +Local Open Scope ring_scope. + +Lemma resilience (delta : R) (X : {RV P -> R}) (w : nneg_finfun U) + (pw0 : Weighted.total P w != 0) (w1 : forall i, w i <= 1) : + let X' := (wgt pw0).-RV X in 0 < delta <= \sum_i w i * P i -> + (`| `E X' - `E X | <= Num.sqrt (`V X * 2 * (1 - delta) / delta))%mcR. +Proof. +move=>/= /andP[delta0 delta_max]. +have w01: is01 w by rewrite /is01 => i; rewrite nneg_finfun_ge0 w1. +have -> : `E ((wgt pw0).-RV X) = `E_[Split.fst_RV w01 X | [set: U] `* [set true]]. + by rewrite Ex_cExT emean_cond_split. +rewrite Ex_cExT (Split.cEx w01). +apply: (le_trans (@cresilience' _ _ delta _ _ _ _ _ _)) => //. +- rewrite -Split.Pr_setXT Pr_setT coqRE divr1. + have -> : forall S, Pr (Split.d P w01) (S `* [set true]) = \sum_(i in S) w i * P i. (* TODO: make lemma *) + by move => S; rewrite /Pr big_setX/=; apply: eq_bigr => i _; rewrite big_set1 Split.dE. + by rewrite big_set. +- by rewrite setTX. +- rewrite ler_sqrt; last first. + rewrite !mulr_ge0// ?variance_ge0'//. + rewrite subr_ge0 (le_trans delta_max)//. + apply: le_trans; last by apply/RleP; apply: (Pr_le1 P setT). + by rewrite /Pr [leRHS]big_mkcond ler_sum// => i _; rewrite in_setT ler_piMl. + by rewrite invr_ge0 ltW. +- by rewrite Split.cVar -Var_cVarT. +Qed. + +(* +Section resilience. +Variables (U : finType) (P : {fdist U}). + +Local Open Scope ring_scope. + +From mathcomp Require Import hoelder lebesgue_integral. + +Lemma cauchy_scwarz (r s : U -> R) : + (\sum_i (r \* s) i)^+2 <= (\sum_i (r i)^+2) * (\sum_i (s i)^+2). +Proof. +(* apply hoelder *) +Admitted. + +Let resilience_sub (delta : R) (X : {RV P -> R}) (w : nneg_finfun U) (w1 : forall i, w i <= 1) + (pw0 : Weighted.total P w != 0) : + let X' := (wgt pw0).-RV X in (`| `E X' - `E X | <= Num.sqrt (`V X / \sum_i w i * P i))%mcR. +Proof. +rewrite /= -coqRE -E_trans_min_RV. +rewrite (_:`E ((wgt pw0).-RV X `-cst `E X) = `E ((wgt pw0).-RV (X `-cst `E X))) //. +rewrite emean_sum -sqrtr_sqr. +have ? : 0 <= \sum_i w i * P i. + by rewrite sumr_ge0// => i _; rewrite mulr_ge0// nneg_finfun_ge0. +rewrite ler_sqrt; last by rewrite mulr_ge0 ?variance_ge0'// invr_ge0. +rewrite exprMn [X in _ * X]expr2 mulrA ler_pM ?invr_ge0//. + by rewrite mulr_ge0 ?sqr_ge0 ?invr_ge0. +under eq_bigr => i _. + rewrite (_ : w i * P i * (X `-cst `E X) i = ((fun i => Num.sqrt (w i * P i) * (X `-cst `E X) i) \* (fun i => Num.sqrt (w i * P i))) i)//; last first. + rewrite [RHS]mulrAC -sqrtrM; last by rewrite mulr_ge0// nneg_finfun_ge0. + by rewrite -expr2 sqrtr_sqr ger0_norm; last by rewrite mulr_ge0// nneg_finfun_ge0. + over. +apply: (@le_trans _ _ (_ / (\sum_(i in U) w i * P i))). + apply: ler_pM. exact: sqr_ge0. rewrite invr_ge0//. + exact: cauchy_scwarz. + by []. +under eq_bigr => i _. + rewrite expr2 mulrAC mulrA -expr2 sqr_sqrtr; last by rewrite mulr_ge0// nneg_finfun_ge0. + rewrite -mulrA -expr2. + over. +under [X in _ * X * _]eq_bigr => i _. + rewrite sqr_sqrtr; last by rewrite mulr_ge0// nneg_finfun_ge0. + over. +rewrite /= -mulrA mulfV// mulr1 /Var [leRHS]/Ex. +apply: ler_sum => i _. +rewrite !coqRE [leRHS]mulrC ler_pM//. +- by rewrite mulr_ge0// nneg_finfun_ge0. +- exact: sqr_ge0. +- exact: ler_piMl. +- by rewrite /sq_RV/comp_RV /= !coqRE mulr1. +Qed. + +Lemma invf_ltp (F : numFieldType) : + {in Num.pos &, forall x y : F, (x < y^-1)%mcR = (y < x^-1)%mcR}. +Proof. +by move=> x y ? ?; rewrite -[in RHS](@invrK _ y) ltf_pV2// posrE invr_gt0. +Qed. + +Lemma resilience (delta : R) (X : {RV P -> R}) (w : nneg_finfun U) + (pw0 : Weighted.total P w != 0) (w1 : forall i, w i <= 1) : + let X' := (wgt pw0).-RV X in 0 < delta <= \sum_i w i * P i -> + (`| `E X' - `E X | <= Num.sqrt (`V X * 2 * (1 - delta) / delta))%mcR. +Proof. +move=> /= /andP[delta0]. +have /= := @resilience_sub delta X w w1 pw0. +set a := \sum_i w i * P i. +move=> h delta_max. +have [le12|ge12] := @ltrP R a (2^-1). + apply: (le_trans h). + rewrite ler_sqrt; last by rewrite !mulr_ge0// ?variance_ge0' ?invr_ge0//; lra. + rewrite -!mulrA ler_pM//. + - exact: variance_ge0'. + - by rewrite invr_ge0; lra. + have h1 : 0 < a; first lra. + rewrite -[leRHS]invrK lef_pinv ?posrE//; last first. + rewrite invr_gt0 mulr_gt0// mulr_gt0 ?invr_gt0//; lra. + rewrite invfM invf_div mulrCA -(mulr1 a) ler_pM//. + - lra. + - by rewrite mulr_ge0// invr_ge0// subr_ge0//; lra. + rewrite ler_pdivrMr; last lra. + by rewrite mul1r; lra. +pose w'fun := [ffun i => 1-w i]. +have w'nneg : [forall i, 0 <= w'fun i]. + by apply/forallP=> i; rewrite /w'fun ffunE; have := w1 i; lra. +pose w' := mkNNFinfun w'nneg. +have w'1 : forall i, w' i <= 1 by move=> i; rewrite /w' ffunE gerBl nneg_finfun_ge0. +have h3 : Weighted.total P w' = 1 - Weighted.total P w. + rewrite /Weighted.total. + under eq_bigr => i _. + rewrite /w' ffunE mulrDl mulNr mul1r. + over. + rewrite big_split/= sumrN. + have -> : \sum_(i in U) P i = 1. + have <- := @Pr_setT' U P. + rewrite /Pr -!coqRE. + apply eq_big => // x. + by rewrite in_setT. + by []. +have pw1 : Weighted.total P w' != 1 by rewrite h3; lra. +have pw'0 : Weighted.total P w' != 0. + rewrite h3. + rewrite subr_eq0 eq_sym. + admit. +have -> : `| `E ((wgt pw0).-RV X) - `E X | = (1-\sum_i w i * P i) / (\sum_i w i * P i) * `| `E ((wgt pw'0).-RV X )|. + admit. +rewrite -/a. +have /= := @resilience_sub delta X w' w'1 pw'0. +admit. +Admitted. +*) + +End resilience. + + Notation eps_max := (10 / 127)%mcR. Notation denom := (335 / 100)%mcR.