resilience with arbitrary weight function

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.