From a2c4c12491e3c82c697e3d79dd3e9cb9c90b1016 Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Fri, 19 Jul 2024 01:55:22 +0900 Subject: [PATCH] wip robustmean.v --- robust/robustmean.v | 970 ++++++++++++++++++++++++-------------------- 1 file changed, 521 insertions(+), 449 deletions(-) diff --git a/robust/robustmean.v b/robust/robustmean.v index 146d8708..f9f6b3e7 100644 --- a/robust/robustmean.v +++ b/robust/robustmean.v @@ -1,15 +1,16 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum matrix. From mathcomp Require boolp. -From mathcomp Require Import Rstruct reals. -Require Import Reals Lra. -From infotheo Require Import ssrR Reals_ext realType_ext logb ssr_ext ssralg_ext. +From mathcomp Require Import Rstruct reals mathcomp_extra. +From mathcomp Require Import lra. +From infotheo Require Import ssrR realType_ext logb ssr_ext ssralg_ext. From infotheo Require Import bigop_ext fdist proba. +From HB Require Import structures. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. -Local Open Scope R_scope. +Local Open Scope ring_scope. Local Open Scope reals_ext_scope. Local Open Scope fdist_scope. Local Open Scope proba_scope. @@ -27,11 +28,140 @@ Import Order.POrderTheory Order.Theory Num.Theory GRing.Theory. (* *) (******************************************************************************) -Definition mul_RV (U : finType) (P : {fdist U}) (X Y : {RV P -> R}) - : {RV P -> R} := fun x => X x * Y x. +Reserved Notation "A :^: B" (at level 52, left associativity). + +Lemma setDIlW (T : finType) (A B C : {set T}) : + A :&: B :\: C = A :&: B :\: C :&: B. +Proof. +apply/setP=> x; rewrite !inE. +by case: (x \in A); case: (x \in B); case: (x \in C). +Qed. + +Lemma setIDACW (T : finType) (A B C : {set T}) : + (A :\: B) :&: C = A :&: C :\: B :&: C. +Proof. by rewrite setIDAC setDIlW. Qed. + +Lemma setDAC (T : finType) (A B C : {set T}) : + A :\: B :\: C = A :\: C :\: B. +Proof. by rewrite setDDl setUC -setDDl. Qed. + +(* symmetric difference *) +Definition adds (T : finType) (A B : {set T}) := (A :\: B :|: B :\: A). +Notation "A :^: B" := (adds A B). + +Section adds_lemmas. +Variable (T : finType). +Implicit Types (A B C : {set T}). +Local Notation "+%S" := (@adds T). +Local Notation "-%S" := idfun. +Local Notation "0" := (@set0 T). + +Lemma addsA : associative +%S. +Proof. +move=> x y z; apply/setP=> i; rewrite !inE. +by case: (i \in x); case: (i \in y); case: (i \in z). +Qed. +Lemma addsC : commutative +%S. +Proof. by move=> *; rewrite /adds setUC. Qed. +Lemma add0s : left_id 0 +%S. +Proof. by move=> ?; rewrite /adds set0D setD0 set0U. Qed. +Lemma addNs : left_inverse 0 -%S +%S. +Proof. by move=> *; rewrite /adds /= setDv setU0. Qed. +Lemma setI_addl : left_distributive (@setI T) +%S. +Proof. by move=> *; rewrite [in LHS]/adds setIUl !setIDACW. Qed. +End adds_lemmas. + +From mathcomp Require Import all_algebra. +Search subsetv. + +Lemma setIUAdd (T : finType) (A B : {set T}) : + (A :^: B) :|: (A :&: B) = A :|: B. +Proof. by apply/setP=> x; rewrite !inE; case: (x \in A); case: (x \in B). Qed. + +Lemma setIIAdd_disj (T : finType) (A B : {set T}) : + [disjoint (A :^: B) & (A :&: B)]. +Proof. +rewrite -setI_eq0; apply/eqP/setP=> x; rewrite !inE. +by case: (x \in A); case: (x \in B). +Qed. + +Definition big_union_disj := big_union. + +Lemma big_union (R : Type) (idx : R) (M : Monoid.com_law idx) + (A : finType) (X1 X2 : {set A}) (f : A -> R) : + \big[M/idx]_(a in (X1 :&: X2)) f a = idx -> + \big[M/idx]_(a in (X1 :|: X2)) f a = + M (\big[M/idx]_(a in X1) f a) (\big[M/idx]_(a in X2) f a). +Proof. +move=> I0. +rewrite -setIUAdd big_union_disj 1?disjoint_sym ?setIIAdd_disj //. +rewrite I0 Monoid.opm1 big_union_disj; last first. + by rewrite -setI_eq0 setIDA setIC Order.SetSubsetOrder.setIDv // set0D. +set lhs := LHS. +rewrite -(setID X1 X2) big_union_disj; last first. + by rewrite -setI_eq0 setIC -setIA Order.SetSubsetOrder.setIDv // setI0. +rewrite I0 Monoid.op1m. +rewrite -[in X in M _ X](setID X2 X1) big_union_disj; last first. + by rewrite -setI_eq0 setIC -setIA Order.SetSubsetOrder.setIDv // setI0. +by rewrite setIC I0 Monoid.op1m. +Qed. + +(* TODO: define RV_ringType mimicking fct_ringType *) +Section mul_RV. +Context {R : realType}. +Variables (U : finType) (P : R.-fdist U). +Definition mul_RV (X Y : {RV P -> R}) : {RV P -> R} := fun x => X x * Y x. Notation "X `* Y" := (mul_RV X Y) : proba_scope. Arguments mul_RV /. +Lemma mul_RVA : associative mul_RV. +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite mulrA. Qed. +Lemma mul_RVC : commutative mul_RV. +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite mulrC. Qed. +Lemma mul_RVAC : right_commutative mul_RV. +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite mulrAC. Qed. +Lemma mul_RVCA : left_commutative mul_RV. +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite mulrCA. Qed. +Lemma mul_RVACA : interchange mul_RV mul_RV. +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite mulrACA. Qed. +Lemma mul_RVDr : right_distributive mul_RV (@add_RV _ U P). +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite mulrDr. Qed. +Lemma mul_RVDl : left_distributive mul_RV (@add_RV _ U P). +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite mulrDl. Qed. +Lemma mul_RVBr (f g h : {RV (P) -> (R)}) : f `* (g `- h) = f `* g `- f `* h. +Proof. by apply: boolp.funext=> u /=; rewrite mulrBr. Qed. +Lemma mul_RVBl (f g h : {RV (P) -> (R)}) : (f `- g) `* h = f `* h `- g `* h. +Proof. by apply: boolp.funext=> u /=; rewrite mulrBl. Qed. +End mul_RV. +Notation "X `* Y" := (mul_RV X Y) : proba_scope. +Arguments mul_RV /. + +Section add_RV. +Context {R : realType}. +Variables (U : finType) (P : R.-fdist U). +Arguments add_RV /. +Lemma add_RVA : associative (@add_RV _ U P). +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite addrA. Qed. +Lemma add_RVC : commutative (@add_RV _ U P). +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite addrC. Qed. +Lemma add_RVAC : right_commutative (@add_RV _ U P). +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite addrAC. Qed. +Lemma add_RVCA : left_commutative (@add_RV _ U P). +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite addrCA. Qed. +Lemma add_RVACA : interchange (@add_RV _ U P) (@add_RV _ U P). +Proof. by move=> *; apply: boolp.funext=> u /=; rewrite addrACA. Qed. +End add_RV. + +Section scalelr. +Context {R : realType}. +Variables (U : finType) (P : R.-fdist U). +Lemma scalel_RVE m (X : {RV P -> R}) : scalel_RV m X = const_RV P m `* X. +Proof. by apply: boolp.funext=> ? /=; rewrite /scalel_RV /const_RV. Qed. +Lemma scaler_RVE m (X : {RV P -> R}) : scaler_RV X m = X `* const_RV P m. +Proof. by apply: boolp.funext=> ? /=; rewrite /scaler_RV /const_RV. Qed. +End scalelr. + + Section conj_intro_pattern. (* /[conj] by Cyril Cohen : *) (* https://coq.zulipchat.com/#narrow/stream/237664-math-comp-users/topic/how.20to.20combine.20two.20top.20assumptions.20with.20.60conj.60 *) @@ -41,7 +171,9 @@ End conj_intro_pattern. Notation "[conj]" := (ltac:(apply and_curry)) (only parsing) : ssripat_scope. Section RV_ring. -Variables (U : finType) (P : {fdist U}). +Context {R : realType}. +Variables (U : finType) (P : R.-fdist U). + (* Import topology.*) (* Lemma add_RV_addr (X Y : {RV P -> R}) : X `+ Y = (X + Y)%mcR. *) @@ -92,66 +224,67 @@ Proof. by move: H=> /[swap] /in_preim1 ->; rewrite eqxx. Qed. -Lemma Ind_subset (A : finType) (X Y : {set A}) : - X \subset Y <-> forall a, Ind X a <= Ind Y a. +Lemma Ind_subset {R : realType} (A : finType) (X Y : {set A}) : + X \subset Y <-> forall a, Ind X a <= Ind Y a :> R. Proof. rewrite /Ind; split => H. move=> a; case: ifPn. - - by move/(subsetP H) ->; apply/RleP. - - by case: (a \in Y) => _ //; apply/RleP. + - by move/subsetP ->. + - by case: (a \in Y). apply/subsetP => a aX. -by move: (H a); rewrite aX; case: (a \in Y) => //; move/RleP; rewrite ler10. +by move: (H a); rewrite aX; case: (a \in Y) => //; rewrite ler10. Qed. End sets_functions. Section probability. -Variables (U : finType) (P : {fdist U}). +Context {R : realType}. +Variables (U : finType) (P : R.-fdist U). Lemma sq_RVE (X : {RV P -> R}) : X `^2 = X `* X. -Proof. by rewrite /sq_RV/comp_RV/=; apply: boolp.funext => x; rewrite mulR1. Qed. +Proof. by []. Qed. -Lemma Ind_ge0 (X : {set U}) (x : U) : 0 <= Ind X x. -Proof. by rewrite /Ind; case: ifPn => // _; apply Rle_refl. Qed. +Lemma Ind_ge0 (X : {set U}) (x : U) : 0 <= Ind X x:> R. +Proof. by rewrite /Ind; case: ifPn. Qed. Lemma Ind_setD (X Y : {set U}) : Y \subset X -> Ind (X :\: Y) = Ind X `- Ind Y :> {RV P -> R}. Proof. move/subsetP=> YsubX; rewrite /Ind /sub_RV. apply boolp.funext => u /=. case: ifPn; rewrite inE ?negb_and; - first by case/andP => /negbTE -> ->; rewrite subR0. -case/orP; first by move => /negbNE /[dup] /YsubX -> ->; rewrite subRR. + first by case/andP => /negbTE -> ->; rewrite subr0. +case/orP; first by move => /negbNE /[dup] /YsubX -> ->; rewrite subrr. move/contraNN: (YsubX u) => YsubX'. move=> /[dup] /YsubX' /negbTE -> /negbTE ->. -by rewrite subRR. +by rewrite subrr. Qed. Lemma cEx_ExInd (X : {RV P -> R}) F : `E_[X | F] = `E (X `* Ind (A:=U) F : {RV P -> R}) / Pr P F. Proof. rewrite /Pr /cEx (* need some lemmas to avoid unfolds *) -big_distrl /=. -apply: congr2 => //. +apply: congr2=> //. under eq_bigr => i _. rewrite big_distrr. have -> : \sum_(i0 in finset (preim X (pred1 i)) :&: F) (i * P i0) = \sum_(i0 in finset (preim X (pred1 i)) :&: F) - (X i0 * @Ind U F i0 * P i0). + (X i0 * @Ind _ U F i0 * P i0). apply congr_big => // i0. rewrite in_setI /Ind => /andP[] /in_preim1 -> ->. - by rewrite !coqRE mulr1. + by rewrite mulr1. have H1 : \sum_(i0 in finset (preim X (pred1 i)) :\: F) X i0 * Ind F i0 * P i0 = 0. (* This should be true because all elements of the sum are 0 *) rewrite big1 // => i1. rewrite in_setD => /andP [H2 H3]. - by rewrite !coqRE /Ind (negbTE H2) mulr0 mul0r. + by rewrite /Ind (negbTE H2) mulr0 mul0r. have : \sum_(i0 in finset (preim X (pred1 i))) X i0 * Ind F i0 * P i0 = \sum_(i0 in finset (preim X (pred1 i)) :&: F) X i0 * Ind F i0 * P i0 + \sum_(i0 in finset (preim X (pred1 i)) :\: F) X i0 * Ind F i0 * P i0 by apply big_setID. - rewrite !coqRE H1 addr0 => <-. + rewrite H1 addr0 => <-. under eq_bigl do rewrite in_preim1'. by over. by rewrite -partition_big_fin_img. @@ -162,7 +295,7 @@ Proof. rewrite cEx_ExInd. congr (_ / _). rewrite /Ex /ambient_dist /Ind. -under eq_bigr => i _ do rewrite /mul_RV 2!fun_if if_arg mulR0 mul0R mulR1. +under eq_bigr do rewrite /mul_RV 2!fun_if if_arg mulr0 mul0r mulr1. rewrite [in RHS]big_mkcond /=. exact: eq_bigr. Qed. @@ -177,7 +310,8 @@ suff : `E ((a `cst* X `+ b `cst* Y) `^2) = by rewrite !E_add_RV !E_scalel_RV. apply eq_bigr => i H. unfold ambient_dist, "`cst*", "`+", "`^2", "`o", "^", "`*". -nra. +rewrite !expr2 /=. +lra. Qed. Lemma Ex_square_eq0 X : @@ -185,72 +319,62 @@ Lemma Ex_square_eq0 X : Proof. split=> [XP|EX20]. - rewrite /Ex big1// => u _. - have [|->] := XP u; last by rewrite mulR0. - by rewrite /sq_RV /comp_RV /= => ->; rewrite !mul0R. -- have XP : forall x, x \in U -> (X `^2: {RV P -> R}) x * P x = 0. - move=> x Ux. - apply: (psumr_eq0P _ EX20) => // i Ui. - rewrite mulr_ge0//. - apply/RleP. - by apply: sq_RV_ge0. - move=> x. - have := XP x. - rewrite inE => /(_ erefl) /mulR_eq0[|->]; last by right. - by rewrite /sq_RV /comp_RV /= mulR1 => /mulR_eq0[|] ->; left. + have [|->] := XP u; last by rewrite mulr0. + by rewrite sq_RVE /mul_RV=> ->; rewrite !mul0r. +- move=> x; rewrite !(rwP eqP); apply/orP. + rewrite -(sqrf_eq0 (X x)) (_ : _ ^+ 2 = (X `^2: {RV P -> R}) x) // -mulf_eq0. + have -> // := psumr_eq0P _ EX20 => *. + by rewrite mulr_ge0 // sq_RV_ge0. Qed. Lemma Cauchy_Schwarz_proba (X Y : {RV P -> R}): - Rsqr (`E (X `* Y : {RV P -> R})) <= `E (X `^2) * `E (Y `^2). + (`E (X `* Y : {RV P -> R})) ^+ 2 <= `E (X `^2) * `E (Y `^2). Proof. -pose a := sqrt (`E (Y `^2)). -pose b := sqrt (`E (X `^2)). -have ? : 0 <= `E (X `^2) by apply: Ex_ge0; exact: sq_RV_ge0. -have ? : 0 <= `E (Y `^2) by apply: Ex_ge0; exact: sq_RV_ge0. +pose a : R := Num.sqrt (`E (Y `^2)). +pose b : R := Num.sqrt (`E (X `^2)). +have EXge0 : 0 <= `E (X `^2) by exact/Ex_ge0/sq_RV_ge0. +have EYge0 : 0 <= `E (Y `^2) by exact/Ex_ge0/sq_RV_ge0. have H2ab : 2 * a * b * (b * a) = a * a * `E (X `^2) + b * b * `E (Y `^2). - rewrite -(Rsqr_sqrt (`E (X `^2)))//. - rewrite -(Rsqr_sqrt (`E (Y `^2)))//. - by rewrite -/a -/b /Rsqr; nra. -have [a0|a0] := Req_dec a 0. - apply sqrt_eq_0 in a0 => //. + by rewrite -(sqr_sqrtr EXge0) -/b -(sqr_sqrtr EYge0) -/a !expr2; lra. +have [|a0] := eqVneq a 0. + move/eqP; rewrite sqrtr_eq0. move/(conj EYge0)/andP/le_anti/esym=> a0. have HY : forall y, Y y = 0 \/ P y = 0 by apply/Ex_square_eq0/a0. have -> : `E (X `* Y: {RV P -> R}) = 0. apply/eqP. rewrite psumr_eq0. apply/allP => u _; rewrite inE /=. - by case : (HY u) => -> ; rewrite mulR0 ?mul0R. + by case: (HY u) => ->; rewrite ?mulr0 ?mul0r. move => u _; rewrite /= . - by case : (HY u) => -> ; rewrite mulR0 ?mul0R. - by rewrite Rsqr_0; apply/mulR_ge0. -have [b0|b0] := Req_dec b 0. (* todo: replace with eqVneq.. *) - apply sqrt_eq_0 in b0 => //. + by case : (HY u) => -> ; rewrite ?mulr0 ?mul0r. + by rewrite expr0n; exact/mulr_ge0. +have [|b0] := eqVneq b 0. + move/eqP; rewrite sqrtr_eq0. move/(conj EXge0)/andP/le_anti/esym=> b0. have HX : forall x, X x = 0 \/ P x = 0 by apply /Ex_square_eq0/b0. have -> : `E (X `* Y: {RV P -> R}) = 0. apply/eqP; rewrite psumr_eq0 /mul_RV; last first. - by move=> u _; case : (HX u) => -> ; rewrite ?mulR0 ?mul0R. + by move=> u _; case : (HX u) => -> ; rewrite ?mulr0 ?mul0r. apply/allP => u _; rewrite inE/=. - by case : (HX u) => -> ; rewrite ?mulR0 ?mul0R. - by rewrite Rsqr_0; apply/mulR_ge0. -have {}a0 : 0 < a (*removes a0 hypothesis and reuse it*) - by apply/ltR_neqAle; split; [exact/nesym|exact/sqrt_pos]. -have {}b0 : 0 < b - by apply/ltR_neqAle; split; [exact/nesym|exact/sqrt_pos]. -rewrite -(Rsqr_sqrt (_ * _)); last by apply/mulR_ge0. -rewrite sqrt_mult// -/a -/b. -apply: neg_pos_Rsqr_le. -- rewrite -(@leR_pmul2r (2 * a * b)); last first. - by apply mulR_gt0 => //; apply mulR_gt0. - rewrite -subR_ge0 mulNR subR_opp addRC mulRC H2ab. - rewrite (mulRC (`E (X `* Y))) -Ex_square_expansion. - by apply: Ex_ge0; exact: sq_RV_ge0. -- apply/(@leR_pmul2l (2 * a * b)); first by do 2 apply: mulR_gt0 => //. - apply/subR_ge0; rewrite H2ab -(Rmult_opp_opp b) -addR_opp -mulNR -mulRN. - by rewrite -Ex_square_expansion; apply: Ex_ge0; exact: sq_RV_ge0. + by case : (HX u) => -> ; rewrite ?mulr0 ?mul0r. + by rewrite expr0n; exact/mulr_ge0. +have {}a0 : 0 < a. (*removes a0 hypothesis and reuse it*) + by rewrite lt_neqAle eq_sym; apply/andP; split=> //; exact/sqrtr_ge0. +have {}b0 : 0 < b. + by rewrite lt_neqAle eq_sym; apply/andP; split=> //; exact/sqrtr_ge0. +rewrite -[leRHS]sqr_sqrtr ?mulr_ge0 // sqrtrM // -/a -/b. +rewrite -subr_le0 -oppr_ge0 opprB subr_sqr. +rewrite mulr_ge0 // -[X in _ + X]opprK subr_ge0 ?opprK. +- rewrite -(@ler_pM2l _ (2 * a * b)); last by do 2 apply: mulr_gt0 => //. + rewrite -subr_ge0 H2ab -2!mulNr -mulrN -(mulrNN a a) -Ex_square_expansion. + exact/Ex_ge0/sq_RV_ge0. +- rewrite -(@ler_pM2l _ (2 * a * b)); last by do 2 apply: mulr_gt0 => //. + rewrite -subr_ge0 -mulrN opprK H2ab -Ex_square_expansion. + exact/Ex_ge0/sq_RV_ge0. Qed. Lemma I_square F : Ind F = ((Ind F) `^2 : {RV P -> R}). Proof. rewrite sq_RVE boolp.funeqE /Ind /mul_RV => x. -by case: ifPn; rewrite ?mulR0 ?mulR1. +by case: ifPn; rewrite ?mulr0 ?mulr1. Qed. Lemma I_double (F : {set U}) : Ind F = (Ind F) `* (Ind F) :> {RV P -> R}. @@ -265,9 +389,9 @@ Lemma cEx_trans_min_RV (X : {RV P -> R}) m F : Pr P F != 0 -> Proof. move=> PF0. rewrite !cExE. -under eq_bigr do rewrite /trans_min_RV mulRDl. -rewrite big_split/= divRDl; congr (_ + _). -by rewrite -big_distrr/= -Rmult_div_assoc divRR ?mulR1. +under eq_bigr do rewrite /trans_min_RV mulrDl. +rewrite big_split/= mulrDl; congr (_ + _). +by rewrite -big_distrr /= -mulrA divff // mulr1. Qed. Lemma cEx_sub (X : {RV P -> R}) (F G: {set U}) : @@ -276,16 +400,15 @@ 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_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. +move=> PrPF_gt0 FsubG. +rewrite -[X in _ / X]ger0_norm ?ltW // -normf_div. +by rewrite -cEx_ExInd cEx_trans_min_RV // lt0r_neq0 // PrPF_gt0. Qed. Lemma Ex_cExT (X : {RV P -> R}) : `E X = `E_[X | [set: U]]. Proof. rewrite /cEx. -under eq_bigr do rewrite setIT Pr_setT divR1 -pr_eqE. +under eq_bigr do rewrite setIT Pr_setT divr1 -pr_eqE. (* The names of lemmas for Pr are inconsistent: some begin with "Pr" while others "pr" *) by rewrite -Ex_comp_RV; congr `E. @@ -299,112 +422,111 @@ Local Notation "`V_[ X | F ]" := (cVar X F). Lemma Var_cVarT (X : {RV P -> R}) : `V X = `V_[X | [set: U]]. Proof. by rewrite /cVar -!Ex_cExT. Qed. +Lemma cvariance_ge0 (X : {RV P -> R}) F : 0 <= `V_[X | F]. +Proof. +have [H|] := boolP (0 < Pr P F)%mcR; last first. + rewrite -leNgt. + have:= Pr_ge0 P F => /[conj] /andP /le_anti H. + rewrite /cVar /cEx; apply big_ind; [by []|exact: addr_ge0|move=> i _]. + by rewrite setIC Pr_domin_setI // mulr0 mul0r. +rewrite /cVar cEx_ExInd mulr_ge0 ?invr_ge0 ?(ltW H) //. +apply/Ex_ge0=> u /=. +by rewrite mulr_ge0 ?Ind_ge0 // sq_RV_ge0. +Qed. + +Lemma variance_ge0 (X : {RV P -> R}) : 0 <= `V X. +Proof. by have := cvariance_ge0 X setT; rewrite -Var_cVarT. Qed. + Lemma cEx_cVar (X : {RV P -> R}) (F G: {set U}) : 0 < Pr P F -> F \subset G -> let mu := `E_[X | G] in let var := `V_[X | G] in - `| `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_gt0P PrPF_neq0 PrPF_pos - /[dup] /(subset_Pr P) /(ltR_leR_trans PrPF_pos) - /[dup] /Pr_gt0P PrPG_neq0 PrPG_pos FsubG mu var. + `| `E_[ X | F ] - mu | <= Num.sqrt (var * Pr P G / Pr P F ). +Proof. +move=> PrPF_pos. +move=> /[dup] /(Pr_incl P) /(lt_le_trans PrPF_pos)=> PrPG_pos. +move=> FsubG /=. +set mu:= `E_[X | G]. +set var:= `V_[X | G]. +have EG_ge0 : 0 <= `E (((X `-cst mu) `^2) `* Ind G). + by apply:Ex_ge0=>*; apply:mulr_ge0; [exact:sq_RV_ge0|exact:Ind_ge0]. +have EF_ge0 : 0 <= `E (((X `-cst mu) `^2) `* Ind F). + by apply:Ex_ge0=>*; apply:mulr_ge0; [exact:sq_RV_ge0|exact:Ind_ge0]. 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). - rewrite divRE leR_pmul2r // -sqrt_Rsqr_abs. - apply sqrt_le_1_alt. - have -> : (X `-cst mu) `* Ind F = (X `-cst mu) `* Ind F `* Ind F. - by rewrite {1}I_double boolp.funeqE=> u; rewrite /mul_RV mulRA. - apply/(leR_trans (Cauchy_Schwarz_proba _ _))/leR_eqVlt; left. - congr (_ * _); congr (`E _); last by rewrite -I_square. - apply: boolp.funext => x/=. - rewrite [in RHS]I_square. - by rewrite /sq_RV/=/comp_RV/mul_RV !mulR1 -mulRA [in LHS](mulRC (Ind F x)) !mulRA. -rewrite /y divRE -(sqrt_Rsqr (/ Pr P F)) // -sqrt_mult_alt; last first. - move=> *; apply mulR_ge0; last by rewrite E_Ind. - by apply: Ex_ge0 => u; apply: mulR_ge0; [apply pow2_ge_0 | apply Ind_ge0]. -apply sqrt_le_1_alt. -rewrite /var /cVar -/mu cEx_ExInd !E_Ind /Rsqr. -rewrite mulRCA -!mulRA mulRV // mulR1 mulRC. -rewrite [X in _ * X / _]mulRC mulRV // mulR1 divRE. -apply leR_wpmul2r => //. -apply leR_sumR=> i iU. -rewrite -mulRA -[X in _ <= X]mulRA; apply leR_wpmul2l; first exact: sq_RV_ge0. -by apply leR_pmul => //; [exact: Ind_ge0 | move/Ind_subset: FsubG; apply | apply/RleP]. +pose y := Num.sqrt (Ex P (((X `-cst mu) `^2) `* Ind F) * Ex P (Ind F)) / Pr P F. +apply: (@le_trans _ _ y). + rewrite ler_pM2r ?invr_gt0 // -sqrtr_sqr. + apply: ler_wsqrtr. + rewrite [in leLHS]I_double mul_RVA. + apply/(le_trans (Cauchy_Schwarz_proba _ _)). + rewrite sq_RVE -![in leLHS]mul_RVA (mul_RVC (Ind F)) -![in leLHS]mul_RVA. + by rewrite -I_double !mul_RVA -I_square -sq_RVE le_refl. +rewrite /y /var /cVar -/mu cEx_ExInd. +rewrite -!mulrA !sqrtrM ?invr_ge0 ?(ltW PrPG_pos) //. +rewrite -[in leLHS](sqr_sqrtr (ltW PrPF_pos)) invfM !mulrA. +rewrite -!sqrtrV ?(@ltW _ _ 0) // ler_pM2r ?sqrtr_gt0 ?invr_gt0//. +rewrite E_Ind -![in leLHS]mulrA -[in leLHS]sqrtrM ?(@ltW _ _ 0) //. +rewrite mulfV ?lt0r_neq0 //. +rewrite -![in leRHS]mulrA -[in leRHS]sqrtrM ?invr_ge0 ?(@ltW _ _ 0) //. +rewrite mulVf ?lt0r_neq0 //. +rewrite !sqrtr1 !mulr1 ler_sqrt //. +apply: ler_sum=> u uU; rewrite ler_pM 1?mulr_ge0 ?sq_RV_ge0 ?Ind_ge0 //. +rewrite ler_pM ?sq_RV_ge0 ?Ind_ge0 //. +by have/Ind_subset := FsubG; apply. Qed. (*prove A1 and A3 for later use*) Lemma cEx_Var (X : {RV P -> R}) F : 0 < Pr P F -> - `| `E_[ X | F ] - `E X | <= sqrt (`V X / Pr P F ). + `| `E_[ X | F ] - `E X | <= Num.sqrt (`V X / Pr P F ). Proof. move=> H; rewrite Ex_cExT Var_cVarT. move: (@cEx_cVar X F [set: U] H) => /=. -by rewrite Pr_setT mulR1 subsetT; apply. +by rewrite Pr_setT mulr1 subsetT; apply. Qed. Lemma cEx_cptl (X: {RV P -> R}) F: 0 < Pr P F -> Pr P F < 1 -> `E_[X | F] * Pr P F + `E_[X | (~: F)] * Pr P (~: F) = `E X. Proof. - move => PrFgt0 PrFlt1. - repeat rewrite cEx_ExInd. - unfold Rdiv. - repeat rewrite big_distrl. - rewrite -big_split. - apply congr_big; auto. - move => i HiU. simpl. - unfold "`p_", Ind. - repeat rewrite -mulRA. - repeat rewrite mulVR. - repeat rewrite mulR1. - rewrite in_setC. - destruct (i \in F); simpl; lra. - all: apply Pr_gt0P; try rewrite Pr_setC; lra. +move => PrFgt0 PrFlt1. +rewrite !cEx_ExInd. +rewrite -!mulrA [in LHS]mulVf ?lt0r_neq0 //. +rewrite mulVf ?Pr_of_cplt ?subr_eq0 1?eq_sym ?neq_lt ?PrFlt1 // !mulr1. +rewrite /Ex -big_split /=. +apply: eq_bigr=> i _. +rewrite /Ind inE. +by case: ifP=> _ /=; rewrite mulr1 mulr0 mul0r ?addr0 ?add0r. Qed. Lemma cEx_Inv_int (X: {RV P -> R}) F: 0 < Pr P F -> Pr P F < 1 -> Pr P F * (`E_[X | F] - `E X) = Pr P (~: F) * - (`E_[X | (~: F)] - `E X). Proof. - move => H H0. - rewrite mulRDr oppRD mulRDr oppRK mulRN mulRN. - 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_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})). - rewrite -addRA Rplus_opp_l addR0 -big_split. - rewrite mulRDl -addRA mulNR Rplus_opp_l addR0 mul1R. - apply congr_big; auto. - move => i HiU. simpl. - unfold "`p_". - rewrite -mulRDl. - congr (_ * _). - rewrite /Ind/mul_RV in_setC. - elim (i \in F); simpl; lra. +move => H H0. +apply/eqP; rewrite -subr_eq0. +rewrite opprD opprK !mulrDr addrAC. +rewrite opprD !mulrN opprK addrA. +rewrite !(mulrC (Pr _ _)) cEx_cptl //. +rewrite Pr_of_cplt mulrDr mulr1 opprD mulrN opprK !addrA. +by rewrite subrr add0r subrr. Qed. Lemma cEx_Inv' (X: {RV P -> R}) (F G : {set U}) : 0 < Pr P F -> F \subset G -> Pr P F < Pr P G -> `| `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_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. -rewrite (_ : _ `* (_ `- _) = (X `-cst `E_[X | G]) `* Ind G `- (X `-cst `E_[X | G]) `* Ind F); last first. (* TODO: use ring_RV *) - by rewrite /mul_RV/sub_RV; apply: boolp.funext => u /=; rewrite mulRBr. -rewrite E_sub_RV. -have -> : Ex P ((X `-cst `E_[X | G]) `* Ind G) = 0. - apply normR0_eq0. - by rewrite -(@eqR_mul2r (/ Pr P G)) // -divRE -cEx_sub // subRR normR0 mul0R. -by rewrite sub0R normRN. +move=> PrPF_gt0 /[dup] /setIidPr GIFF FsubG /[dup] /(lt_trans PrPF_gt0) + /[dup] /Pr_gt0 /invr_neq0 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. +rewrite !cEx_sub ?subsetDl // mulrCA. +rewrite Ind_setD // mulrAC divff// mul1r. +congr (_ / _); apply/eqP. +rewrite mul_RVBr E_sub_RV -subr_eq0 -normr_le0. +apply: le_trans; first exact: ler_dist_normD. +rewrite addrCA subrr addr0 normr_le0. +apply/eqP/normr0_eq0/(divIf (lt0r_neq0 PrPG_gt0)). +by rewrite mul0r -cEx_sub // subrr normr0. Qed. (* NB: not used *) @@ -412,246 +534,232 @@ 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_setC -setTD; apply cEx_Inv' => //. -apply ltR_neqAle; split; last by apply/subset_Pr/subsetT. -by apply/eqP; rewrite Pr_setT -Pr_lt1P. +move=> *; rewrite Ex_cExT -Pr_of_cplt -setTD; apply cEx_Inv' => //. +by rewrite lt_neqAle Pr_incl // andbT Pr_setT -Pr_lt1. Qed. -Lemma cvariance_ge0 (X : {RV P -> R}) F : 0 <= `V_[X | F]. -Proof. -have [/RltP H|] := boolP (0 < Pr P F)%mcR; last first. - rewrite -leNgt => /RleP. - move: (Pr_ge0 P F) => /[conj] /eqR_le H. - rewrite /cVar /cEx; apply big_ind; [exact/RleP|exact: addR_ge0|move=> i _]. - by rewrite setIC Pr_domin_setI // mulR0 divRE mul0R; exact/RleP. -rewrite /cVar cEx_ExInd /Ex /ambient_dist divRE big_distrl /=. -apply/RleP; apply: sumr_ge0 => u _; rewrite !coqRE mulr_ge0//; last first. - by rewrite invr_ge0; apply/RleP. -apply: mulr_ge0 => //; apply: mulr_ge0; first by apply/RleP; exact: sq_RV_ge0. -by rewrite /Ind; by case: ifPn. -Qed. - -Lemma variance_ge0 (X : {RV P -> R}) : 0 <= `V X. -Proof. by have := cvariance_ge0 X setT; rewrite -Var_cVarT. Qed. - -Lemma Ind_one F : Pr P F <> 0 -> `E_[Ind F : {RV P -> R} | F] = 1. +Lemma Ind_one F : Pr P F != 0 -> `E_[Ind F : {RV P -> R} | F] = 1. Proof. move=> F0; rewrite cEx_ExInd. have -> : Ind F `* Ind F = Ind F. - by move=> f; rewrite /mul_RV /Ind boolp.funeqE => u; case: ifPn; rewrite ?(mulR0,mulR1). -by rewrite E_Ind divRE mulRV//; exact/eqP. + by move=>*; rewrite /Ind boolp.funeqE=>? /=; case: ifPn; rewrite ?mulr0 ?mulr1. +by rewrite E_Ind mulrV // unitfE. Qed. Lemma cEx_add_RV (X Y : {RV (P) -> (R)}) F: `E_[(X `+ Y) | F] = `E_[X | F] + `E_[Y | F]. Proof. - rewrite !cEx_ExInd -mulRDl. - congr (_ * _). - rewrite -E_add_RV. +rewrite !cEx_ExInd -mulrDl. +congr (_ * _). +rewrite -E_add_RV. apply congr_big => // i HiU. - by rewrite /mul_RV mulRDl. + by rewrite /mul_RV mulrDl. Qed. Lemma cEx_sub_RV (X Y: {RV P -> R}) F: `E_[X `- Y | F] = `E_[X|F] - `E_[Y|F]. Proof. - rewrite !cEx_ExInd. - unfold Rminus. - rewrite -mulNR. - rewrite big_morph_oppR -mulRDl. - congr (_ * _). - rewrite -big_split /=. - apply eq_bigr => u _. - by rewrite -mulNR -mulRDl -mulNR -mulRDl. +rewrite !cEx_ExInd -mulrBl. +congr (_ * _). +by rewrite mul_RVBl E_sub_RV. Qed. Lemma cEx_const_RV (k : R) F: 0 < Pr P F -> `E_[(const_RV P k) | F] = k. Proof. - move => HPrPF. - by rewrite cEx_ExInd E_scalel_RV E_Ind /Rdiv -mulRA mulRV; [rewrite mulR1 | apply gtR_eqF]. +by move=> ?; rewrite cEx_ExInd E_scalel_RV E_Ind -mulrA mulfV ?mulr1 ?gt_eqF. Qed. +(* NB: It is pointless to retain both `*cst (scaler_RV) and `cst* (scalel_RV) + since R is commutative; moreover, the name scalel does not follow the + naming scheme of mathcomp (r in scaler should stand for rings). *) Lemma const_RC (X: {RV P -> R}) k: X `*cst k = k `cst* X. -Proof. - unfold "`*cst", "`cst*". - rewrite boolp.funeqE => x. - by rewrite mulRC. -Qed. +Proof. by rewrite boolp.funeqE => ?; exact: mulrC. Qed. Lemma cEx_scaler_RV (X : {RV (P) -> (R)}) (k : R) F: `E_[(X `*cst k) | F] = `E_[X | F] * k. Proof. - rewrite !cEx_ExInd mulRC mulRA. - congr (_ * _). - rewrite -E_scalel_RV const_RC. - apply eq_bigr => i _. - unfold "`cst*". - by rewrite mulRA. +rewrite !cEx_ExInd mul_RVAC mulrAC /Ex; congr (_ / _). +rewrite big_distrl /=. +by under [LHS]eq_bigr do rewrite /= mulrAC. Qed. Lemma cEx_scalel_RV (X : {RV (P) -> (R)}) (k : R) F: `E_[(k `cst* X) | F] = k * `E_[X | F]. -Proof. - by rewrite mulRC -cEx_scaler_RV const_RC. -Qed. +Proof. by rewrite mulrC -cEx_scaler_RV const_RC. Qed. Lemma cEx_trans_add_RV (X: {RV P -> R}) m F: -0 < Pr P F -> - `E_[X `+cst m | F] = `E_[X | F] + m. -Proof. - move => HPrPF_gt0. - have: `E_[const_RV P m | F] = m by apply cEx_const_RV. - move => HcExm. - by rewrite -{2}HcExm -cEx_add_RV. -Qed. + 0 < Pr P F -> `E_[X `+cst m | F] = `E_[X | F] + m. +Proof. by move=> ?; rewrite cEx_add_RV cEx_const_RV. Qed. Lemma cEx_trans_RV_id_rem (X: {RV P -> R}) m F: - `E_[(X `-cst m) `^2 | F] = `E_[((X `^2 `- (2 * m `cst* X)) `+cst m ^ 2) | F]. + `E_[(X `-cst m) `^2 | F] = `E_[((X `^2 `- ((2 * m)%mcR `cst* X)) `+cst m ^+ 2) | F]. Proof. - rewrite !cEx_ExInd. - congr (_ * _). - apply eq_bigr => a _. - rewrite /sub_RV /trans_add_RV /trans_min_RV /sq_RV /= /comp_RV /scalel_RV /=. - by rewrite /ambient_dist; field. +rewrite !cEx_ExInd; congr (_ * _); apply: eq_bigr => a _. +rewrite /sub_RV /trans_add_RV /trans_min_RV /sq_RV /= /comp_RV /scalel_RV /=. +lra. Qed. Lemma cEx_Pr_eq0 (X: {RV P -> R}) F: Pr P F = 0 -> `E_[X | F] = 0. -Proof. -move => PrF0. -by rewrite cEx_ExInd PrF0 !coqRE invr0 mulr0. -Qed. +Proof. by move=> PrF0; rewrite cEx_ExInd PrF0 invr0 mulr0. Qed. Lemma cVarE (X : {RV (P) -> (R)}) F: - `V_[X | F] = `E_[X `^2 | F] - `E_[X | F] ^ 2. + `V_[X | F] = `E_[X `^2 | F] - `E_[X | F] ^+ 2. Proof. - have: 0 <= Pr P F by apply Pr_ge0. - case => [HPr_gt0 | HPr_eq0]. - rewrite /cVar cEx_trans_RV_id_rem. - rewrite cEx_trans_add_RV; last by []. - rewrite cEx_sub_RV cEx_scalel_RV. - field. - by rewrite /cVar !cEx_Pr_eq0; first (simpl; rewrite mul0R subR0). +have: 0 <= Pr P F by apply Pr_ge0. +rewrite le_eqVlt; case/orP => [ /eqP /esym HPr_eq0 | HPr_gt0]. + by rewrite /cVar !cEx_Pr_eq0 // expr0n /= subr0. +rewrite /cVar cEx_trans_RV_id_rem. +rewrite cEx_trans_add_RV //. +rewrite cEx_sub_RV cEx_scalel_RV !expr2. +lra. Qed. Lemma cVarDist (X : {RV P -> R}) F x: 0 < Pr P F -> - `E_[(X `-cst x) `^2 | F] = - `V_[X | F] + (`E_[X | F] - x)². -Proof. - move => HPrPF. - unfold Rsqr. - rewrite cVarE. - simpl; rewrite mulR1 mulRDl !mulRDr !addRA -(mulRC (- _)) -!addRA addRA addRA -(addRA _ (- _)) (addRC (- _)). - have ->: `E_[X | F] * `E_[X | F] + - (`E_[X | F] * `E_[X | F]) = 0 by apply subRR. - rewrite addR0 -!cEx_scalel_RV. - have <-: `E_[(const_RV P (-x * -x)) | F] = (-x * -x) by apply cEx_const_RV. - rewrite -!cEx_add_RV !cEx_ExInd. - congr (_ * _). - apply eq_bigr => i _. - repeat congr (_ * _); - unfold "`-cst", "`^2", "`o", "`cst*", const_RV, "`+"; - simpl. - by rewrite !mulR1 mulRDl !mulRDr !addRA -(mulRC (-_)). + `E_[(X `-cst x) `^2 | F] = `V_[X | F] + (`E_[X | F] - x) ^+ 2. +Proof. +move=> ?. +rewrite cEx_trans_RV_id_rem cVarE cEx_add_RV cEx_sub_RV. +rewrite cEx_const_RV // cEx_scalel_RV. +lra. +Qed. + +Lemma cEx_sub_eq (X : {RV P -> R}) (F G : {set U}) : + F \subset G -> Pr P F = Pr P G -> `E_[ X | F ] = `E_[ X | G ]. +Proof. +move=> ? Pr_FG_eq; apply/eqP. +rewrite -subr_eq0 -normr_eq0 distrC. +rewrite !cEx_ExInd Pr_FG_eq -mulrBl -E_sub_RV -mul_RVBr -Ind_setD //. +rewrite normrM mulf_eq0; apply/orP; left. +rewrite normr_eq0 -sqrf_eq0 -normr_le0 normrX real_normK ?num_real //. +apply: le_trans; first exact: Cauchy_Schwarz_proba. +by rewrite -I_square Ind_setD // E_sub_RV !E_Ind Pr_FG_eq subrr mulr0. +Qed. + +Lemma cEx_union (X : {RV P -> R}) (F G H : {set U}) : + F \subset G :|: H -> + Pr P (F :&: G) + Pr P (F :&: H) = Pr P F -> + `E_[ X | F :&: G ] * Pr P (F :&: G) + `E_[ X | F :&: H ] * Pr P (F :&: H) = + `E_[ X | F ] * Pr P F. +Proof. +move=> FsubGUH. +have[F0|Fneq0]:= eqVneq (Pr P F) 0. + by rewrite !Pr_domin_setI // F0 !mulr0 addr0. +have[FIG0|FIGneq0]:= eqVneq (Pr P (F :&: G)) 0. + rewrite FIG0 mulr0 !add0r => FIHF. + by congr (_ * _)=> //; apply: cEx_sub_eq=> //; exact: subsetIl. +have[FIH0|FIHneq0]:= eqVneq (Pr P (F :&: H)) 0. + rewrite FIH0 mulr0 !addr0=> FIGF. + by congr (_ * _)=> //; apply: cEx_sub_eq=> //; exact: subsetIl. +move=> FGHF. +rewrite !cExE -!mulrA !mulVf // !mulr1 -big_union /=; last first. + have/setIidPl/(congr1 (Pr P)):= FsubGUH. + rewrite setIUr Pr_union_eq FGHF=> /eqP. + rewrite -subr_eq0 addrAC subrr add0r oppr_eq0 => /eqP /psumr_eq0P P0. + by rewrite big1 // => *; rewrite P0 // mulr0. +by rewrite -setIUr; have/setIidPl->:= FsubGUH. +Qed. + +(* similarly to total_prob or total_prob_cond *) +Lemma total_cEx (X : {RV P -> R}) (I : finType) (E : {set U}) + (F : I -> {set U}) : + Pr P E = \sum_(i in I) Pr P (E :&: F i) -> + E \subset cover [set F x | x : I] -> + `E_[ X | E ] * Pr P E = + \sum_(i in I) `E_[ X | E :&: F i] * Pr P (E :&: F i). +Proof. +Abort. + +Lemma cExID (X : {RV P -> R}) (F G : {set U}) : + `E_[ X | F :&: G ] * Pr P (F :&: G) + `E_[ X | F :\: G ] * Pr P (F :\: G) = + `E_[ X | F ] * Pr P F. +Proof. +rewrite setDE cEx_union ?setUCr //. +rewrite -big_union /=; last by rewrite setICA -setIA setICr !setI0 big_set0. +by rewrite -setIUr setUCr setIT. Qed. + End probability. Notation "`V_[ X | F ]" := (cVar X F) : proba_scope. -Arguments Ind_one {U P}. +Arguments Ind_one {R U P}. +Arguments cEx_sub_eq {R U P X} F G. Section resilience. -Variables (U : finType) (P : {fdist U}). +Context {R : realType}. +Variables (U : finType) (P : R.-fdist U). Lemma cresilience (delta : R) (X : {RV P -> R}) (F G : {set U}) : 0 < delta -> delta <= Pr P F / Pr P G -> F \subset G -> `| `E_[ X | F ] - `E_[ X | G ] | <= - sqrt (`V_[ X | G ] * 2 * (1 - delta) / delta). + Num.sqrt (`V_[ X | G ] * 2 * (1 - delta) / delta). Proof. move => delta_gt0 delta_FG /[dup] /setIidPr HGnF_F FG. -have [Pr_FG_eq|/eqP Pr_FG_neq] := eqVneq (Pr P F) (Pr P G). - have FGFG : F :|: G :\: F = G. - by have := setID G F; have := setIidPl FG; rewrite setIC => ->. - have GFP0 : \sum_(u in G :\: F) P u = 0. - move: Pr_FG_eq. - rewrite -[in X in _ = X -> _]FGFG [in X in _ = X -> _]/Pr. - rewrite big_union/=; last by apply/setDidPl; rewrite setDDl setUid. - by move=> /eqP; rewrite addRC -subr_eq => /eqP <-; rewrite /Pr subrr. - have {}GFP0 : forall u, u \in G :\: F -> P u = 0. - by move/psumr_eq0P : GFP0; exact. - rewrite !cExE Pr_FG_eq -Rdiv_minus_distr. - rewrite -[in X in `|(_ - X) / _|]FGFG. - rewrite big_union/=; last by apply/setDidPl; rewrite setDDl setUid. - rewrite subRD subRR sub0R big1 ?oppR0 ?div0R ?normR0; last first. - by move=> i /GFP0 ->; rewrite mulR0. - exact/sqrt_pos. -have [?|/eqP PrF_neq0] := eqVneq (Pr P F) 0; first nra. -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. -have HPrGpos : 0 < Pr P G by have := Pr_ge0 P G; lra. +have [Pr_FG_eq|Pr_FG_neq] := eqVneq (Pr P F) (Pr P G). + by rewrite (cEx_sub_eq F G) // subrr normr0 sqrtr_ge0. +have FltG: Pr P F < Pr P G by rewrite lt_neqAle Pr_FG_neq Pr_incl. +have [PrF0|PrF_neq0] := eqVneq (Pr P F) 0. + by have:= lt_le_trans delta_gt0 delta_FG; rewrite PrF0 mul0r ltxx. +have HPrFpos : 0 < Pr P F by rewrite lt_neqAle eq_sym Pr_ge0 andbT. +have [PrG0|PrG_neq0] := eqVneq (Pr P G) 0. + by have:= Pr_incl P FG; rewrite PrG0 => /(lt_le_trans HPrFpos); rewrite ltxx. +have HPrGpos : 0 < Pr P G by rewrite lt_neqAle eq_sym Pr_ge0 andbT. have delta_lt1 : delta < 1. - by apply/(leR_ltR_trans delta_FG)/ltR_pdivr_mulr => //; lra. -case : (Rle_or_lt delta (1/2)) => delta_12. + apply/(le_lt_trans delta_FG). + by rewrite ltr_pdivrMr // mul1r. +have/orP[]:= le_total delta (1/2)=> delta_12. (*Pr P F <= 1/2 , A.3 implies the desired result*) - apply: (leR_trans (cEx_cVar _ _ _)) => //. - apply sqrt_le_1_alt. - rewrite !divRE -!mulRA; apply (leR_wpmul2l (cvariance_ge0 _ _)). - apply: (@leR_trans (1 / delta)). - rewrite (leR_pdivl_mulr delta)//. - rewrite mulRC -leR_pdivl_mulr; last exact: divR_gt0. - rewrite div1R invRM ?gtR_eqF //; last exact: invR_gt0. - by rewrite invRK ?gtR_eqF // mulRC. - by rewrite !divRE mulRA leR_pmul2r; [lra|exact: invR_gt0]. -rewrite cEx_Inv'//; last lra. -apply: leR_trans. - apply leR_wpmul2l; first exact: divR_ge0. + apply: (le_trans (cEx_cVar _ _ _)) => //. + rewrite ler_wsqrtr //. + rewrite -!mulrA; apply (ler_wpM2l (cvariance_ge0 _ _)). + apply: (@le_trans _ _ (1 / delta)). + rewrite ler_pdivlMr //. + rewrite mulrC -ler_pdivlMr; last exact: divr_gt0. + by rewrite div1r invfM invrK mulrC. + by rewrite mulrA ler_pM2r; [lra|rewrite invr_gt0]. +have delta_neq0: delta != 0 by lra. +have delta_pos: 0 < delta by lra. +have FG_pos: 0 < Pr P F / Pr P G by exact: (lt_le_trans delta_gt0 delta_FG). +rewrite cEx_Inv' //. +have PrGDF_pos: 0 < Pr P (G :\: F) by rewrite Pr_diff HGnF_F subr_gt0. +apply: le_trans. + apply: ler_wpM2l; first by rewrite ltW // divr_gt0. apply cEx_cVar => //; last exact: subsetDl. - 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. - rewrite -sqrt_Rsqr_abs; rewrite -sqrt_mult_alt; last exact: Rle_0_sqr. - apply sqrt_le_1_alt. - 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_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. - move/leR_pdivl_mulr : delta_FG => /(_ HPrGpos) => delta_FG. - apply Rmult_le_compat_r with (r:= Pr P G) in delta_FG => //. - 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_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]. -rewrite mulRA; apply/leR_pmul2r; first exact/invR_gt0. -rewrite -!mulRA; apply: leR_wpmul2l; first exact: cvariance_ge0. -rewrite invRM; [|exact/gtR_eqF|exact/gtR_eqF]. -rewrite mulRCA (mulRA (Pr P G)) mulRV ?mul1R; last exact/gtR_eqF. -rewrite mulRC; apply/leR_wpmul2r; first lra. -by rewrite -div1R; apply/leR_pdivr_mulr => //; nra. +apply: (@le_trans _ _ (Num.sqrt (`V_[ X | G] * (delta^-1 - 1) / delta))). + rewrite -[X in X * Num.sqrt _]gtr0_norm ?divr_gt0 // -sqrtr_sqr. + rewrite -sqrtrM ?sqr_ge0 // ler_wsqrtr //. + rewrite mulrC -!mulrA ler_wpM2l ?cvariance_ge0 //. + rewrite mulrC exprMn !mulrA mulVf // -?Pr_gt0 // mul1r. + rewrite Pr_diff HGnF_F mulrDl mulNr mulfV //. + rewrite mulrAC -mulrA -invf_div. + apply: ler_pM. + - by rewrite subr_ge0 -invr1 lef_pV2 ?posrE // ler_pdivrMr // mul1r Pr_incl. + - by rewrite invr_ge0 ltW. + - by rewrite lerD // lef_pV2. + - by rewrite lef_pV2. +rewrite ler_wsqrtr // -!mulrA ler_wpM2l ?cvariance_ge0 //. +rewrite [X in 2 * X]mulrDl mulNr mulfV // div1r mulrC ler_wpM2r //. + by rewrite subr_ge0 -[leLHS]invrK lef_pV2 ?posrE ?invr1 // ltW. +by rewrite -lef_pV2 ?posrE ?invr_gt0 // invrK -div1r. Qed. (* NB: not used, unconditional version of cresilience *) Lemma resilience (delta : R) (X : {RV P -> R}) F : 0 < delta -> delta <= Pr P F -> - `| `E_[ X | F ] - `E X | <= sqrt (`V X * 2 * (1 - delta) / delta). + `| `E_[ X | F ] - `E X | <= Num.sqrt (`V X * 2 * (1 - delta) / delta). Proof. move=> delta_gt0 delta_F. have := @cresilience _ X F setT delta_gt0. -rewrite Pr_setT divR1 => /(_ delta_F); rewrite -Ex_cExT -Var_cVarT. +rewrite Pr_setT divr1 => /(_ delta_F); rewrite -Ex_cExT -Var_cVarT. by apply; exact/subsetT. Qed. End resilience. Section robustmean. -Variables (U : finType) (P : {fdist U}). +Context {R : realType}. +Variables (U : finType) (P : R.-fdist U). Theorem robust_mean (good drop: {set U}) (X : {RV P -> R}) (eps : R): let bad := ~: good in @@ -661,173 +769,137 @@ Theorem robust_mean (good drop: {set U}) (X : {RV P -> R}) (eps : R): 0 < eps -> eps <= 1/8 -> Pr P bad = eps -> Pr P drop = 4 * eps -> (* All the outliers exceeding the ε-quantile are eliminated: *) - (forall y, y \in bad -> sqrt (sigma / eps) < `| X y - mu | -> y \in drop) -> - `| mu_hat - mu | <= 8 * sqrt (sigma / eps). + (forall y, y \in bad -> Num.sqrt (sigma / eps) < `| X y - mu | -> y \in drop) -> + `| mu_hat - mu | <= 8 * Num.sqrt (sigma / eps). Proof. move=> bad mu_hat mu sigma Hmin_outliers Hmax_outliers Hbad_ratio Hdrop_ratio Hquantile_drop_bad. -have H : Pr P good = 1 - eps by apply/esym/subR_eq; rewrite -Hbad_ratio Pr_cplt. +have H : Pr P good = 1 - eps by rewrite -Hbad_ratio -Pr_to_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/subset_Pr/subsetIr. + by rewrite -Hdrop_ratio; exact/Pr_incl/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 -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_setC; lra. + rewrite -(setCK good) -/bad setDE setIC -setDE. + rewrite Pr_diff setIC -setDE mulrDl mulNr mulfV //. + by rewrite -Pr_gt0 Pr_of_cplt; lra. +have eps'_ge0 : 0 <= eps' by rewrite mulr_ge0 // ?invr_ge0 Pr_ge0. have eps'_le1 : eps' <= 1. - rewrite /eps'; apply/leR_pdivr_mulr; first by rewrite Pr_setC; lra. - by rewrite mul1R; exact/subset_Pr/subsetDr. + rewrite ler_pdivrMr; last by rewrite Pr_of_cplt; lra. + by rewrite mul1r Pr_incl // 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_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. - apply/leR_pdivr_mulr; first lra. - rewrite -[X in _ <= X]mulRA mulVR ?mulR1; first lra. - by apply/eqP; lra. + rewrite /delta Pr_diff H. + apply: (@le_trans _ _ ((1 - eps - 4 * eps) / (1 - eps))). + rewrite ler_pdivlMr; last lra. + by rewrite mulrDl -mulNr -(mulrA _ _^-1) mulVf //; lra. + rewrite ler_pdivrMr; last lra. + rewrite -[X in _ <= X]mulrA mulVf ?mulr1; lra. have delta_gt0 : 0 < delta. - apply (@ltR_pmul2r (1 - eps)); first lra. - by rewrite mul0R mulRDl mul1R -mulNR -mulRA Rinv_l; lra. + rewrite -(@ltr_pM2r _ (1 - eps)); last lra. + by rewrite mul0r mulrDl mul1r -mulNr -mulrA mulVf //; lra. have delta_le1 : delta <= 1. - apply (@leR_pmul2r (1 - eps)); first lra. - by rewrite mul1R mulRDl mul1R -mulNR -mulRA Rinv_l ?mulR1; lra. + rewrite -(@ler_pM2r _ (1 - eps)); last lra. + by rewrite mul1r mulrDl mul1r -mulNr -mulrA mulVf ?mulr1 //; lra. have Exgood_bound : `| `E_[X | good :\: drop ] - `E_[X | good] | <= - sqrt (`V_[X | good] * 2 * (1 - delta) / delta). + Num.sqrt (`V_[X | good] * 2 * (1 - delta) / delta). have [gdg|gdg] := eqVneq (Pr P (good :\: drop)) (Pr P 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_setD -setIA. - (* NB: lemma? *) - apply/subR_eq; rewrite addRC; apply/subR_eq; rewrite subRR; apply/esym. - move: gdg; rewrite Pr_setD => /subR_eq; rewrite addRC => /subR_eq. - by rewrite subRR [in X in _ -> X]setIC => /esym; exact: Pr_domin_setI. + by move=> ->; rewrite subrr normr0 sqrtr_ge0. + by apply: cEx_sub_eq => //; exact: subsetDl. - apply cresilience. - + apply (@ltR_pmul2r (1 - eps)); first lra. - by rewrite mul0R; apply: mulR_gt0 => //; lra. + + rewrite -(@ltr_pM2r _ (1 - eps)); last lra. + by rewrite mul0r mulr_gt0 //; lra. + lra. + exact: subsetDl. have Exbad_bound : 0 < Pr P (bad :\: drop) -> - `| `E_[ X | bad :\: drop ] - mu | <= sqrt (sigma / eps). + `| `E_[ X | bad :\: drop ] - mu | <= Num.sqrt (sigma / eps). move=> Pr_bd. - rewrite -(mulR1 mu) -(@Ind_one U P (bad :\: drop)); last lra. - rewrite 2!cEx_ExInd -addR_opp -mulNR mulRA -(I_double P) -mulRDl big_distrr /=. - rewrite /Ex -big_split /= [X in `|X */ _|](_ : _ = - \sum_(i in U) (X i - mu) * @Ind U (bad :\: drop) i * P i); last first. - by apply: eq_bigr => u _; rewrite -mulRA mulNR addR_opp -mulRBl mulRA. - rewrite normRM (geR0_norm (/ _)); last exact/ltRW/invR_gt0. - apply/leR_pdivr_mulr => //; apply: (leR_trans (leR_sumR_Rabs _ _)). + rewrite -(mulr1 mu) -(@Ind_one _ U P (bad :\: drop)); last lra. + rewrite 2!cEx_ExInd -mulNr mulrA -(I_double P) -mulrDl big_distrr /=. + rewrite /Ex -big_split /= [X in `|X / _|](_ : _ = + \sum_(i in U) (X i - mu) * @Ind _ U (bad :\: drop) i * P i); last first. + by apply: eq_bigr => u _; rewrite -mulrA mulNr -mulrBl mulrA. + rewrite normrM (@ger0_norm _ _^-1); last by rewrite ltW // invr_gt0. + rewrite ler_pdivrMr //; apply: (le_trans (ler_norm_sum _ _ _)). rewrite (bigID [pred i | i \in bad :\: drop]) /=. - rewrite [X in _ + X]big1 ?addR0; last first. - by move=> u /negbTE abaddrop; rewrite /Ind abaddrop mulR0 mul0R normR0. - rewrite /Pr big_distrr /=. apply leR_sumR => i ibaddrop. - rewrite normRM (geR0_norm (P i))//; apply: leR_wpmul2r => //. - rewrite /Ind ibaddrop mulR1. + rewrite [X in _ + X]big1 ?addr0; last first. + by move=> u /negbTE abaddrop; rewrite /Ind abaddrop mulr0 mul0r normr0. + rewrite /Pr big_distrr /=; apply: ler_sum => i ibaddrop. + rewrite normrM (@ger0_norm _ (P i)) // ler_wpM2r //. + rewrite /Ind ibaddrop mulr1. move: ibaddrop; rewrite inE => /andP[idrop ibad]. - by rewrite leRNgt => /Hquantile_drop_bad => /(_ ibad); apply/negP. + by rewrite leNgt -(rwP negP) => /(Hquantile_drop_bad _ ibad); exact/negP. have max_bad_remain : Pr P (bad :\: drop) <= eps / Pr P (~: drop). - 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]. + rewrite Pr_of_cplt Hdrop_ratio Pr_diff Hbad_ratio. + apply: (@le_trans _ _ eps); first by rewrite lerBlDr lerDl Pr_ge0. + by rewrite ler_pdivlMr; [nra|lra]. have Ex_not_drop : `E_[ X | ~: drop ] = (`E_[ X | good :\: drop ] * Pr P (good :\: drop) + `E_[ X | bad :\: drop ] * Pr P (bad :\: drop)) / Pr P (~: 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_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. - by rewrite !setDE setIACA setIid setICr set0I. - have [bd0|/eqP bd0 {good_bad}] := eqVneq (Pr P (bad :\: drop)) 0. - - rewrite bd0 addR0 in good_bad. - rewrite bd0 mulR0 addR0 good_bad. - rewrite /Rdiv -mulRA mulRV ?mulR1; last first. - 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 (_ * _). - (* NB: lemma? *) - rewrite /Ind !inE. - 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_setC; apply/eqP; nra. - rewrite !cEx_ExInd -!mulRA. - 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 _ /=. - rewrite /ambient_dist -!mulRA -mulRDr -mulRDl ; congr (X i * (_ * _)). - (* NB: lemma? *) - rewrite /Ind !inE; case: ifPn => //=; rewrite ?(addR0,add0R)//. - by case: ifPn => //=; rewrite ?(addR0,add0R). -rewrite -(mulR1 mu). + rewrite !setDE (setIC good) (setIC bad) /bad -setDE cExID. + rewrite -mulrA mulfV ?mulr1 // Pr_of_cplt. + lra. +rewrite -(mulr1 mu). rewrite (_ : 1 = eps' + Pr P (good :\: drop) / Pr P (~: drop)); last first. - by rewrite Hcompl addRCA addR_opp subRR addR0. -rewrite (mulRDr mu) -addR_opp oppRD. -rewrite /mu_hat Ex_not_drop divRDl. -rewrite {2}/Rdiv -(mulRA `E_[X | _]) -divRE -/eps'. -rewrite Hcompl. -rewrite {1}/Rdiv -(mulRA `E_[X | _]) -divRE. + by rewrite Hcompl addrCA subrr addr0. +rewrite (mulrDr mu) opprD. +rewrite /mu_hat Ex_not_drop mulrDl. +rewrite -(mulrA `E_[X | _]) -/eps'. rewrite Hcompl. -rewrite -addRA addRC addRA -!mulNR -(mulRDl _ _ eps'). -rewrite -addRA -mulRDl. -rewrite (addRC (-mu)). -apply: (leR_trans (Rabs_triang _ _)). -rewrite 2!normRM (geR0_norm eps'); last lra. -rewrite (geR0_norm (1 - eps')); last lra. -apply: (@leR_trans (sqrt (`V_[ X | good] / eps) * eps' + - sqrt (`V_[ X | good] * 2 * (1 - delta) / delta) * (1 - eps'))). +rewrite -(mulrA `E_[X | _]). +rewrite -addrA addrC addrA -!mulNr -(mulrDl _ _ eps'). +rewrite -addrA -mulrDl. +rewrite (addrC (-mu)). +rewrite (le_trans (ler_normD _ _)) //. +rewrite (normrM _ eps') (@ger0_norm _ eps'); last lra. +rewrite normrM. +rewrite mulNr -/eps' (@ger0_norm _ (1 - eps')); last lra. +apply: (@le_trans _ _ (Num.sqrt (`V_[ X | good] / eps) * eps' + + Num.sqrt (`V_[ X | good] * 2 * (1 - delta) / delta) * (1 - eps'))). have [->|/eqP eps'0] := eqVneq eps' 0. - by rewrite !(mulR0,add0R,subR0,mulR1). + by rewrite !(mulr0,add0r,subr0,mulr1). have [->|/eqP eps'1] := eqVneq eps' 1. - rewrite !(subRR,mulR0,addR0,mulR1); apply: Exbad_bound. - apply Pr_gt0P; apply: contra_notN eps'0 => /eqP. - by rewrite /eps' => ->; rewrite div0R. + rewrite !(subrr, mulr0, addr0, mulr1); apply: Exbad_bound. + apply Pr_gt0; apply: contra_notN eps'0 => /eqP. + by rewrite /eps' => ->; rewrite mul0r. 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_gt0P. + by exfalso; apply/eps'0; rewrite /eps' bd0 mul0r. + apply: lerD; (rewrite ler_pM2r; last lra). + - exact/Exbad_bound/Pr_gt0. - exact: Exgood_bound. -rewrite /sigma /Rdiv !sqrt_mult //; last 8 first. +rewrite /sigma !sqrtrM //; last 4 first. - exact: cvariance_ge0. - - lra. - - by apply: mulR_ge0; [exact: cvariance_ge0|lra]. - - lra. - - apply: mulR_ge0; [|lra]. - by apply: mulR_ge0; [exact: cvariance_ge0|lra]. - - by apply/ltRW/invR_gt0; lra. + - by apply: mulr_ge0; [exact: cvariance_ge0|lra]. + - apply: mulr_ge0; [|lra]. + by apply: mulr_ge0; [exact: cvariance_ge0|lra]. - exact: cvariance_ge0. - - by apply/ltRW/invR_gt0; lra. -rewrite (mulRC 8) -!mulRA -mulRDr; apply: leR_wpmul2l; first exact: sqrt_pos. -rewrite mulRA -sqrt_mult; [|lra|lra]. -rewrite mulRA -sqrt_mult; [|lra|]; last by apply/ltRW/invR_gt0; lra. -rewrite addRC; apply/leR_subr_addr. -rewrite -mulRBr -(sqrt_Rsqr (1 - eps')); last lra. -rewrite -(sqrt_Rsqr (8 - eps')); last lra. -rewrite -sqrt_mult; last 2 first. - - by apply/mulR_ge0; [lra|apply/ltRW/invR_gt0; lra]. - - exact: Rle_0_sqr. -rewrite -sqrt_mult; last 2 first. - - by apply/ltRW/invR_gt0; lra. - - exact: Rle_0_sqr. -apply/sqrt_le_1_alt/leR_pmul. -- by apply: mulR_ge0; [lra|apply/ltRW/invR_gt0; lra]. -- exact: Rle_0_sqr. -- rewrite -divRE; apply/leR_pdivr_mulr; first lra. - rewrite (mulRC _ delta) -divRE; apply/leR_pdivl_mulr; first lra. - rewrite mulRC mulRA; apply/(@leR_pmul2r (1 - eps)); first lra. +rewrite addrCA subrr addr0. +rewrite -(mulr_natl _ 8) -!mulrA -mulrDr mul1r. +rewrite -!(mulrCA (Num.sqrt `V_[ X | good])). +apply: ler_wpM2l; first exact: sqrtr_ge0. +rewrite mulrA -sqrtrM; [|lra]. +rewrite mulrA -sqrtrM; [|lra]. +rewrite addrC -lerBrDr (mulrC 8) -mulrBr. +rewrite -(@ger0_norm _ (1 - eps')) -?sqrtr_sqr; last lra. +rewrite -(@ger0_norm _ (8 - eps')) -?sqrtr_sqr; last lra. +rewrite [leLHS]mulrC [leRHS]mulrC. +rewrite -sqrtrM ?sqr_ge0 //. +rewrite -sqrtrM ?sqr_ge0 //. +rewrite ler_sqrt 1?mulr_ge0 ?sqr_ge0 ?invr_ge0 //; last by rewrite ltW. +apply: ler_pM. +- exact: sqr_ge0. +- by rewrite !mulr_ge0 ?invr_ge0 //; lra. +- rewrite ler_sqr ?nnegrE; lra. +- rewrite ler_pdivrMr; last lra. + rewrite [leRHS]mulrC -ler_pdivrMr ?invr_gt0; last lra. + rewrite (mulrC 2) -(@ler_pM2r _ (1 - eps)); last lra. + rewrite mulrDl mul1r -(mulrA _ _^-1) invrK. +STOP rewrite mulRDl mul1R -mulNR -(mulRA _ (/ _)) Rinv_l ?mulR1; last lra. by rewrite -mulRA mulRDl oppRD oppRK mulRDl -(mulRA _ (/ _)) Rinv_l; [nra|lra]. -- by apply/Rsqr_incr_1; lra. Qed. End robustmean.