proof of weber_aligned_spec_weak

CaseStudies/Gathering/InR2/Weber/Utils.v

@@ -735,7 +735,21 @@ Ltac pos_R :=
   | _ => pos_R_close
   end.
 
-Ltac simp_fct := 
+Ltac simpl_R := repeat first 
+  [ rewrite Rmult_0_l
+  | rewrite Rmult_0_r
+  | rewrite Rmult_1_l
+  | rewrite Rmult_1_r
+  | rewrite Rplus_0_l
+  | rewrite Rplus_0_r
+  | rewrite Rminus_0_l
+  | rewrite Rminus_0_r
+  | rewrite Ropp_0 
+  | rewrite sqrt_0
+  | rewrite Rsqr_0
+  ].
+
+Ltac simpl_fct := 
   cbv [fct_cte Ranalysis1.id Ranalysis1.comp plus_fct mult_fct inv_fct div_fct].
 
 Local Instance derivable_pt_lim_compat : Proper ((equiv ==> equiv) ==> equiv ==> equiv ==> iff) derivable_pt_lim.
@@ -761,9 +775,9 @@ assert (Hdiv := derivable_pt_lim_div (fct_cte 1%R) f x 0%R l). feed_n 3 Hdiv.
 { assumption. }
 { lra. }
 revert Hdiv. apply derivable_pt_lim_compat.
-+ intros x1 x2 Hx. simp_fct. simpl. rewrite Hx. lra.
++ intros x1 x2 Hx. simpl_fct. simpl. rewrite Hx. lra.
 + reflexivity.
-+ cbv [fct_cte]. simpl. lra.
++ cbv [fct_cte]. now simpl_R.
 Qed.  
 
 (* Simplify a goal of the form [derivable_pt_lim f x d], assuming 
@@ -801,5 +815,5 @@ Ltac prove_derivable_pt_lim :=
       evar (l_evar : R) ;
       replace l with l_evar ; 
       [simp_derivable | unfold l_evar] ;
-      simp_fct
+      simpl_fct
   end.
\ No newline at end of file

CaseStudies/Gathering/InR2/Weber/Weber_point.v

@@ -1625,6 +1625,95 @@ split.
   rewrite deriv_neg_iff. apply not_weber_deriv_neg. assumption.
 Qed.
 
+Lemma u_aligned_left L x :
+  line_contains L w ->
+  line_contains L x -> 
+  (L^P x < L^P w)%R ->
+  (u x = -unitary (line_dir L))%VS.
+Proof. 
+intros Hw Hx Hleft. unfold u. rewrite <-Hw, <-Hx. unfold line_proj_inv.
+rewrite opp_distr_add, (add_comm (line_org L)). rewrite add_assoc.
+rewrite <-(add_assoc _ (line_org L)), add_opp, add_origin_r. 
+rewrite <-minus_morph, add_morph. rewrite <-opp_opp. f_equal.
+rewrite <-unitary_opp, <-minus_morph. rewrite unitary_mul.
++ reflexivity.
++ rewrite <-Ropp_div, <-Rdiv_plus_distr, <-Ropp_div. 
+  enough (0 <> norm (line_dir L))%R by pos_R.
+  symmetry. rewrite norm_defined. 
+  intros Hnull. unfold line_proj in Hleft. 
+  rewrite Hnull, inner_product_origin_r, inner_product_origin_r in Hleft.
+  lra.
+Qed.
+
+Lemma u_aligned_right L x :
+  line_contains L w ->
+  line_contains L x -> 
+  (L^P x > L^P w)%R ->
+  (u x = unitary (line_dir L))%VS.
+Proof. 
+intros Hw Hx Hright. unfold u. rewrite <-Hw, <-Hx. unfold line_proj_inv.
+rewrite opp_distr_add, (add_comm (line_org L)). rewrite add_assoc.
+rewrite <-(add_assoc _ (line_org L)), add_opp, add_origin_r. 
+rewrite <-minus_morph, add_morph. rewrite unitary_mul.
++ reflexivity.
++ rewrite <-Ropp_div, <-Rdiv_plus_distr. 
+  enough (0 <> norm (line_dir L))%R by pos_R.
+  symmetry. rewrite norm_defined. 
+  intros Hnull. unfold line_proj in Hright. 
+  rewrite Hnull, inner_product_origin_r, inner_product_origin_r in Hright.
+  lra.
+Qed.
+
+Lemma aligned_sum_us L : 
+  aligned_on L (w :: ps) -> 
+  (list_sumVS (map u ps) = (INR (length (L^right w ps)) - INR (length (L^left w ps))) * unitary (line_dir L))%VS.
+Proof.
+intros Halign. rewrite aligned_on_cons_iff in Halign. destruct Halign as [Hw Halign].
+rewrite (line_left_on_right_partition L w ps) at 1.
+do 2 rewrite map_app, list_sumVS_app.
+induction ps as [| p ps' IH].
++ simpl. now simpl_R.
++ rewrite aligned_on_cons_iff in Halign. destruct Halign as [Hp Halign].
+  specialize (IH Halign).
+  unfold line_left, line_right, line_on. cbn [filter map list_sumVS].
+  case (Rtotal_order (L^P p) (L^P w)) as [Hpw | [Hpw | Hpw]].
+  - pose proof (Hrw := Hpw). rewrite <-Rltb_true in Hrw. rewrite Hrw ; clear Hrw.
+    assert (Hrw : ~(L^P w == L^P p)) by (change (L^P w <> L^P p) ; lra).
+    rewrite <-eqb_false_iff in Hrw. rewrite Hrw ; clear Hrw.
+    assert (Hrw : ~(L^P w < L^P p)%R) by lra. rewrite <-Rltb_false in Hrw.
+    rewrite Hrw ; clear Hrw. 
+    cbn [map list_sumVS length]. rewrite <-add_assoc.
+    unfold line_on, line_right, line_left in IH. rewrite IH. clear IH.
+    enough (Hu : (u p = (-1) * unitary (line_dir L))%VS).
+    { rewrite Hu. rewrite add_morph. f_equal. rewrite S_INR. lra. }
+    change (-1)%R with (Ropp 1%R). rewrite minus_morph, mul_1.
+    apply u_aligned_left ; assumption.
+  - assert (Hrw : L^P w == L^P p) by now simpl. rewrite <-eqb_true_iff in Hrw. 
+    rewrite Hrw ; clear Hrw.
+    assert (Hrw : ~(L^P w < L^P p)%R) by lra. rewrite <-Rltb_false in Hrw.
+    rewrite Hrw ; clear Hrw.
+    assert (Hrw : ~(L^P p < L^P w)%R) by lra. rewrite <-Rltb_false in Hrw.
+    rewrite Hrw ; clear Hrw. 
+    cbn [map list_sumVS length]. repeat rewrite add_assoc. rewrite (add_comm _ (u p)).
+    repeat rewrite <-add_assoc.
+    unfold line_on, line_right, line_left in IH. rewrite IH. clear IH.
+    enough (Heq : p == w).
+    { unfold u. rewrite Heq, add_opp, unitary_origin, add_origin_l. reflexivity. }
+    rewrite <-Hw, <-Hp, Hpw. reflexivity.
+  - assert (Hrw : ~(L^P w == L^P p)) by (change (L^P w <> L^P p) ; lra). rewrite <-eqb_false_iff in Hrw. 
+    rewrite Hrw ; clear Hrw.
+    assert (Hrw : (L^P w < L^P p)%R) by lra. rewrite <-Rltb_true in Hrw.
+    rewrite Hrw ; clear Hrw.
+    assert (Hrw : ~(L^P p < L^P w)%R) by lra. rewrite <-Rltb_false in Hrw.
+    rewrite Hrw ; clear Hrw. 
+    cbn [map list_sumVS length]. rewrite (add_comm (u p)).
+    repeat rewrite add_assoc. repeat rewrite add_assoc in IH.
+    unfold line_on, line_right, line_left in IH. rewrite IH. clear IH.
+    enough (Hu : (u p = 1 * unitary (line_dir L))%VS).
+    { rewrite Hu. rewrite add_morph. f_equal. rewrite S_INR. lra. }
+    rewrite mul_1. apply u_aligned_right ; assumption.
+Qed.
+
 End WeberFirstOrder.
 
 
@@ -1657,17 +1746,23 @@ Lemma weber_majority ps w :
   countA_occ equiv R2_EqDec w ps > (Nat.div2 (length ps + 1)) -> OnlyWeber ps w. 
 Proof. Admitted.  
 
-
 (* This is the first order condition for weber points,
  * in the special case of aligned points. *)
 Lemma weber_aligned_spec_weak L ps w : 
-  aligned_on L ps -> 
+  line_dir L =/= 0%VS ->
+  aligned_on L (w :: ps) -> 
     Weber ps w <-> 
     (Rabs (INR (length (L^left w ps)) - INR (length (L^right w ps))) <= INR (length (L^on w ps)))%R.
-Proof. Admitted.
+Proof. 
+intros Hdir Halign.
+rewrite weber_first_order. rewrite (aligned_sum_us Halign).
+rewrite norm_mul, norm_unitary, Rmult_1_r by assumption.
+rewrite <-(line_on_length_aligned L _ _ Halign). 
+f_equiv. rewrite <-Rabs_Ropp. f_equiv. lra.
+Qed.
 
 Lemma weber_aligned_spec L ps w : 
-  aligned_on L ps -> 
+  aligned_on L (w :: ps) -> 
     OnlyWeber ps w <-> 
     (Rabs (INR (length (L^left w ps)) - INR (length (L^right w ps))) < INR (length (L^on w ps)))%R.
 Proof. Admitted.