From 81473bf8b4b805463b316e4c6638283106ed7d66 Mon Sep 17 00:00:00 2001
From: MathisBD <mathis.bouverot@ens.psl.eu>
Date: Sun, 18 Feb 2024 23:20:05 +0100
Subject: [PATCH] proof of weber_aligned_spec_weak
---
CaseStudies/Gathering/InR2/Weber/Utils.v | 22 +++-
.../Gathering/InR2/Weber/Weber_point.v | 105 +++++++++++++++++-
2 files changed, 118 insertions(+), 9 deletions(-)
diff --git a/CaseStudies/Gathering/InR2/Weber/Utils.v b/CaseStudies/Gathering/InR2/Weber/Utils.v
index 9744c6ce..2161064a 100644
--- a/CaseStudies/Gathering/InR2/Weber/Utils.v
+++ b/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
diff --git a/CaseStudies/Gathering/InR2/Weber/Weber_point.v b/CaseStudies/Gathering/InR2/Weber/Weber_point.v
index 3820e386..b79e0221 100644
--- a/CaseStudies/Gathering/InR2/Weber/Weber_point.v
+++ b/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.
@@ -1655,19 +1744,25 @@ Qed.
Lemma weber_majority ps w :
countA_occ equiv R2_EqDec w ps > (Nat.div2 (length ps + 1)) -> OnlyWeber ps w.
-Proof. Admitted.
-
+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.
--
GitLab