max_max_list

coq/utils/RealAdd.v

@@ -4080,6 +4080,25 @@ Proof.
   - apply Rmax_r.
 Qed.
 
+Lemma max_max2 (a1 a2 b1 b2 : R) :
+  Rabs ((Rmax a1 a2) - (Rmax b1 b2)) <=
+    Rmax (Rabs (a1 - b1)) (Rabs (a2 - b2)).
+Proof.
+   unfold Rmax; match_destr; match_destr.
+  - match_destr; lra.
+  - unfold Rabs; match_destr; match_destr.
+    + repeat match_destr_in r1; lra.
+    + repeat match_destr_in n0; lra.
+    + repeat match_destr_in r1; lra.
+    + repeat match_destr_in n0; lra.
+  - unfold Rabs; match_destr; match_destr.
+    + repeat match_destr_in r1; lra.
+    + repeat match_destr_in n0; lra.
+    + repeat match_destr_in r1; lra.
+    + repeat match_destr_in n0; lra.
+  - match_destr; lra.
+Qed.
+
 Lemma max_min_list (l : list (R * R)) : l <> nil ->
   let l1 := map fst l in
   let l2 := map snd l in
@@ -4106,6 +4125,32 @@ Proof.
   now apply Rle_max_compat_l.
 Qed.
 
+Lemma max_max_list (l : list (R * R)) : l <> nil ->
+  let l1 := map fst l in
+  let l2 := map snd l in
+  Rabs ((Rmax_list l1) - (Rmax_list l2)) <=
+    Rmax_list (map (fun '(x,y) => Rabs(x - y)) l).
+Proof.
+  simpl.
+  induction l; simpl; [congruence | intros _].
+  destruct a as [x y].
+  destruct l; [reflexivity |].
+  simpl map; cbv match.
+                      cut_to IHl; [| congruence].  
+  repeat rewrite map_cons in IHl.
+
+  revert IHl.
+  generalize (Rmax_list (fst p :: map fst l)).
+  generalize (Rmax_list (snd p :: map snd l)).
+  generalize ((Rmax_list
+                 ((let '(x0, y0) := p in Rabs (x0 - y0)) :: map (fun '(x0, y0) => Rabs (x0 - y0)) l))).
+  simpl; intros.
+  generalize (max_max2 x r1 y r0).
+  intros.
+  rewrite H.
+  now apply Rle_max_compat_l.
+Qed.
+
 Lemma max_min_list_s (l : list (R * R)) : l <> nil ->
  let '(l1, l2) := split l in
   Rabs ((Rmin_list l1) - (Rmin_list l2)) <=
@@ -4116,6 +4161,16 @@ Proof.
   destruct (split l); trivial.
 Qed.
 
+Lemma max_max_list_s (l : list (R * R)) : l <> nil ->
+ let '(l1, l2) := split l in
+  Rabs ((Rmax_list l1) - (Rmax_list l2)) <=
+    Rmax_list (map (fun '(x,y) => Rabs(x - y)) l).
+Proof.
+  generalize (max_max_list l).
+  rewrite <- fst_split, <- snd_split.
+  destruct (split l); trivial.
+Qed.
+
 Lemma max_min_list2 (l1 l2 : list R) : l1 <> nil -> length l1 = length l2 ->
   Rabs ((Rmin_list l1) - (Rmin_list l2)) <=
     Rmax_list (map (fun '(x,y) => Rabs(x - y)) (combine l1 l2)).
@@ -4127,6 +4182,17 @@ Proof.
   destruct l1; destruct l2; simpl in *; congruence.
 Qed.
 
+Lemma max_max_list2 (l1 l2 : list R) : l1 <> nil -> length l1 = length l2 ->
+  Rabs ((Rmax_list l1) - (Rmax_list l2)) <=
+    Rmax_list (map (fun '(x,y) => Rabs(x - y)) (combine l1 l2)).
+Proof.
+  intros nnil eqlen.
+  generalize (max_max_list_s (combine l1 l2)).
+  rewrite combine_split; trivial; intros HH.
+  rewrite HH; [reflexivity |].
+  destruct l1; destruct l2; simpl in *; congruence.
+Qed.
+
 End Rmax_list.
 
 Notation "Max_{ l } ( f )" := (Rmax_list (List.map f l)) (at level 50) : rmax_scope.