diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v index 61d3f03c9b6237c7a5683cd47fea2dbfd4b2f9c5..3820e386c1d1dd490b76f66708b42a1c8b823f6c 100644 --- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v +++ b/CaseStudies/Gathering/InR2/Weber/Weber_point.v @@ -1628,19 +1628,30 @@ Qed. End WeberFirstOrder. -Lemma list_sum_alls x n : - list_sum (alls x n) == ((INR n) * x)%R. -Proof. Admitted. - +(* This is an application of weber_first_order. *) Lemma weber_majority_weak ps w : countA_occ equiv R2_EqDec w ps >= (Nat.div2 (length ps + 1)) -> Weber ps w. Proof. intros Hcount. rewrite ge_le_iff in Hcount. rewrite weber_first_order. -(* rewrite weber_first_order. rewrite list_sumVS_norm. *) -(* rewrite (@list_sum_le _ (alls 1%R (Nat.div2 (length ps + 1)))). *) -(* + rewrite list_sum_alls, Rmult_1_r. apply le_INR. assumption. *) -(* + etransitivity ; [|exact Hcount]. *) -Admitted. +assert (Hineq : (norm (list_sumVS (map (u w) ps)) + INR (countA_occ equiv R2_EqDec w ps) <= INR (length ps))%R). +{ + clear Hcount. + induction ps as [| p ps IH]. + + simpl. rewrite Rmult_0_l, Rplus_0_l, sqrt_0. lra. + + cbn [countA_occ length map list_sumVS]. case (R2_EqDec p w) as [Hpw | Hpw]. + - unfold u at 1. rewrite Hpw, add_opp, unitary_origin, add_origin_l. + rewrite S_INR, S_INR. lra. + - transitivity (1%R + norm (list_sumVS (map (u w) ps)) + INR (countA_occ equiv R2_EqDec w ps))%R. + * apply Rplus_le_compat_r. rewrite triang_ineq. apply Rplus_le_compat_r. + unfold u. rewrite norm_unitary ; [lra |]. + intros H. rewrite R2sub_origin in H. intuition. + * rewrite S_INR. lra. +} +transitivity (INR (Nat.div2 (length ps + 1))) ; [| now apply le_INR]. +eapply Rplus_le_reg_r ; rewrite Hineq. Search INR Rle le. +rewrite <-(Rplus_le_compat_l (INR (Nat.div2 (length ps + 1))) _ _ (le_INR _ _ Hcount)). +rewrite <-plus_INR. apply le_INR. apply div2_sum_p1_ge. +Qed. Lemma weber_majority ps w : countA_occ equiv R2_EqDec w ps > (Nat.div2 (length ps + 1)) -> OnlyWeber ps w.