proof of weber_majority_weak

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.