Add LoadPath "./interval". Require Import ssreflect ssrnat seq fintype ssrbool eqtype ssrfun bigops matrix ssralg . Require Import Reals. Require Import Fourier. Require Import Rstruct. Set Implicit Arguments. Unset Strict Implicit. Import Prenex Implicits. Delimit Scope ring_scope with Ri. Delimit Scope nat_scope with Dn. (* - general results on the set of indexes; - lemmas for min and max on reals; - some results on sums, complements to bigops *) Section BigOpRel. Variables (R : Type) (Prel : R ->R-> Prop). Variables (nil : R) (op1 : R -> R -> R). Variable (fu: R -> R). Hypothesis (fu_nil: Prel (fu nil) ( nil)) (rel_trans: forall a b c, Prel a b->Prel b c-> Prel a c) (fu_rel1: forall a b c, Prel b c -> Prel (op1 a b) (op1 a c) ) (fu_rel: forall a b, Prel (fu (op1 a b)) (op1 (fu a) (fu b))). Lemma big_op_rel_seq: forall I (r : seq I) (P:I -> bool) F , Prel ( fu (\big[op1/nil]_(i <- r | P i) F i)) (\big[op1/nil]_(i <- r | P i) fu (F i)). Proof. move=> I r P F; rewrite unlock ; elim: r => //= i r Hr. case e: (P i);[apply rel_trans with (op1 (fu (F i)) (fu (foldr (fun (i0 : I) (x : R) => if P i0 then op1 ( (F i0)) x else x) nil r))); [apply fu_rel| apply fu_rel1;apply Hr]| apply Hr]. Qed. Lemma big_op_rel: forall (I:finType) (P: pred I) F , Prel ( fu (\big[op1/nil]_(i | P i) F i)) (\big[op1/nil]_(i | P i) fu (F i)). Proof. move=> I P F ; apply big_op_rel_seq => i; rewrite mem_enum. Qed. End BigOpRel. Implicit Arguments big_op_rel_seq [R nil op1 I r P F]. Implicit Arguments big_op_rel [R nil op1 I P F]. Section BigRel2. Variables (R1 : Type) (rel : R1 ->R1-> Prop). Variables (nil1 : R1) (op1 : R1 -> R1 -> R1). Hypothesis (rel_sym : forall x, rel x x) (relP : forall a x b y, rel a x -> rel b y -> rel (op1 a b) (op1 x y)) (rel_trans : forall b a c, rel a b->rel b c-> rel a c). Variables (R2 : Type) (nil2 : R2) (op2 : R2 -> R2 -> R2) (f : R2 -> R1). Hypothesis (f_nil : (f nil2) = (nil1)) (f_morph : forall a b, rel (f (op2 a b)) (op1 (f a) (f b))). Lemma big_morph_rel_seq : forall I (r : seq I) (P :I -> bool) F, rel (f (\big[op2/nil2]_(i <- r | P i) F i)) (\big[op1/nil1]_(i <- r | P i) f (F i)). Proof. move=> I r P F. elim: r => //= [|a r Hr]; [by rewrite ?big_nil f_nil| rewrite ?big_cons/=]. case e: (P a); last (apply: Hr). apply: (@rel_trans (op1 (f (F a)) (f (\big[op2/nil2]_(j <- r | P j) (F j))))). by apply: f_morph. by apply: relP; last apply: Hr. Qed. Lemma big_morph_rel : forall (I : finType) (P : pred I) F, rel (f (\big[op2/nil2]_(i | P i) F i)) (\big[op1/nil1]_(i | P i) f (F i)). Proof. by move=> I P F; apply: big_morph_rel_seq => i; rewrite mem_enum. Qed. End BigRel2. Implicit Arguments big_op_rel_seq [R nil op1 I r P F]. Implicit Arguments big_op_rel [R nil op1 I P F]. Section aux_index. Variable p: nat. Lemma ord1_0: forall i: 'I_1, i = ord0. move=> i; case: i => k Hk; apply: ord_inj; rewrite /=; move/leP: Hk => hk; omega. Qed. Lemma I0_seq0: enum 'I_O = Nil _. Proof. have H1: 'I_0 =1 pred0. move=> x. have h2:= ltn_ord x. move/ltP:h2=>H2. have h3: ~(x < 0)%coq_nat. by omega. by elim h3. rewrite /enum //=. rewrite (eq_filter H1). apply filter_pred0. Qed. Lemma I_not_void: forall p , (0 < p)%Dn -> Nil _ !=enum 'I_p. Proof. move=> q Hq. apply/negP. unfold not => Heq. move/eqP: Heq=>Heq. have H: size (@Nil 'I_q) = size (enum 'I_q). by rewrite Heq. rewrite {1}/size size_enum_ord in H. have H1:= Hq. rewrite lt0n H in H1. by move/eqP: H1 => H1; apply H1. Qed. Definition I0 (pr: (0 pr; move: (I_not_void pr). elim (enum 'I_p) => //. Defined. Lemma last_cons: forall r (x: R), r !=[::] -> last 0 r = last 0 (x :: r). Proof. move=> s x Hs. rewrite last_cons. move: Hs; case s; first by done. by move=> i s' _ ; rewrite !last_cons. Qed. End aux_index. Section min_max_prop. Lemma max_le: forall a b c d, a<=c-> b<=d-> Rmax a b <= Rmax c d. Proof. move => a b c d Hac Hbd. destruct (Rle_or_lt a b); destruct (Rle_or_lt c d). replace (Rmax a b) with b; replace (Rmax c d) with d; first by fourier. unfold Rmax; case (Rle_dec ); auto with real. unfold Rmax; case (Rle_dec a b); auto with real. unfold Rmax; case (Rle_dec c d); auto with real. replace (Rmax a b) with b; replace (Rmax c d) with c;first by fourier. unfold Rmax; case (Rle_dec c d); auto with real. unfold Rmax; case (Rle_dec a b); auto with real. unfold Rmax; case (Rle_dec c d); auto with real. replace (Rmax a b) with a; replace (Rmax c d) with d;first by fourier. unfold Rmax; case (Rle_dec c d); auto with real. unfold Rmax; case (Rle_dec a b); auto with real. unfold Rmax; case (Rle_dec c d); auto with real. replace (Rmax a b) with a; replace (Rmax c d) with c;first by fourier. unfold Rmax; case (Rle_dec c d); auto with real. unfold Rmax; case (Rle_dec a b); auto with real. unfold Rmax; case (Rle_dec c d); auto with real. Qed. Lemma Rmax_assoc: forall x y z, Rmax x (Rmax y z) = Rmax (Rmax x y) z. Proof. move=> x y z. destruct (Rle_or_lt x y); destruct (Rle_or_lt y z); destruct (Rle_or_lt x z). replace (Rmax y z) with z; [|unfold Rmax; case Rle_dec; auto with real]. replace (Rmax x y) with y; [|unfold Rmax; case Rle_dec; auto with real]. replace (Rmax x z) with z; [|unfold Rmax; case Rle_dec; auto with real]. replace (Rmax y z) with z; [|unfold Rmax; case Rle_dec; auto with real]. done. have Hcontr: x<=z by fourier. have Hcontr2: ~x<=z by fourier. contradiction. replace (Rmax y z) with y; [|unfold Rmax; case Rle_dec; auto with real]. replace (Rmax x y) with y; [|unfold Rmax; case Rle_dec; auto with real]. unfold Rmax; case Rle_dec; auto with real. replace (Rmax y z) with y. replace (Rmax x y ) with y. unfold Rmax; case (Rle_dec y z); auto with real. unfold Rmax; case (Rle_dec x y); auto with real. unfold Rmax; case (Rle_dec y z); auto with real. replace (Rmax y z) with z. replace (Rmax x y) with x. done. unfold Rmax; case (Rle_dec x y); auto with real. unfold Rmax; case (Rle_dec y z); auto with real. replace (Rmax y z) with z. replace (Rmax x y) with x. done. unfold Rmax; case (Rle_dec x y ); auto with real. unfold Rmax; case (Rle_dec y z); auto with real. have Hc1: ~x<=z by fourier. contradiction. replace (Rmax y z) with y. replace (Rmax x y) with x. unfold Rmax; case (Rle_dec x z); auto with real. unfold Rmax; case (Rle_dec x y ); auto with real. unfold Rmax; case (Rle_dec y z); auto with real. Qed. Lemma Rmax_left: forall r1 r2, r2 <= r1 -> Rmax r1 r2 = r1. Proof. move=> r1 r2 H; rewrite /Rmax; case (Rle_dec r1 r2); auto with real. Qed. Lemma Rmax_right: forall r1 r2, r1 <= r2 -> Rmax r1 r2 = r2. Proof. move=> r1 r2 H; rewrite /Rmax; case (Rle_dec r1 r2); auto with real. Qed. Lemma Rmax_le: forall r1 r2 r, r1 <= r -> r2 <=r -> Rmax r1 r2 <= r. Proof. move=> r1 r2 r H1 H2; rewrite /Rmax; case (Rle_dec r1 r2) =>H; fourier. Qed. Lemma Rmax_le2: forall r1 r2 r, r1 <= r /\ r2 <=r <-> Rmax r1 r2 <= r. Proof. by move=> r1 r2 r; split; [move=> [H1 H2]|]; rewrite /Rmax; case (Rle_dec r1 r2) =>H; [fourier|fourier| move=> H1; split; fourier|move=> H1; split;[|apply Rle_trans with r1; [left; apply Rnot_le_lt|]]]. Qed. Lemma Rmax_Rlt_el: forall r1 r2 r, r < Rmax r1 r2 <-> r < r1 \/ r < r2. Proof. move=> r1 r2 r; split . by rewrite /Rmax; case (Rle_dec r1 r2) =>H0 H; [right|left]. move=> H; case H => H1. by apply Rlt_le_trans with r1; [| apply RmaxLess1]. by apply Rlt_le_trans with r2; [| apply RmaxLess2]. Qed. Lemma Rmax_ge: forall r1 r2 r, r <= r1 -> r <=r2 -> r <= Rmax r1 r2. Proof. move=> r1 r2 r H1 H2; rewrite /Rmax; case (Rle_dec r1 r2) =>H; fourier. Qed. Lemma rmax4: forall r1 r2 r3 r4, r1<=r2 -> r3<=r4 -> Rmax r1 r3 <= Rmax r2 r4. Proof. move => r1 r2 r3 r4 H12 H34. rewrite /Rmax; case (Rle_dec r1 r3); case (Rle_dec r2 r4); auto with real. move => H1 H2. apply Rle_trans with r4; auto with real. move => H1 H2; by apply Rle_trans with r2. Qed. Lemma Rmax_le_compat: forall a b c, b <= c-> Rmax a b <= Rmax a c. move=> a b c Hbc. rewrite /Rmax. case ( Rle_dec a b); case (Rle_dec a c ) => H J . done. by elim H; apply Rle_trans with b. done. by right. Qed. Lemma Rmax_Rplus_le_compat: forall a b c , 0 <= c-> Rmax (a + b) c <= Rmax a c + Rmax b c. Proof. move=> a b c; rewrite /Rmax. case (Rle_dec (a + b) c); case (Rle_dec a c); case ( Rle_dec b c) => H J K Hc; try fourier. have H' := Rnot_le_lt _ _ H; fourier. have H' := Rnot_le_lt _ _ J; fourier. have H' := Rnot_le_lt _ _ J. have H'' := Rnot_le_lt _ _ H. elim (RIneq.Rle_not_lt _ _ K);fourier. Qed. Lemma Rmax_Rplus_le_compat2: forall a b c d, Rmax (a + b) (c + d) <= Rmax a c + Rmax b d. Proof. move=> a b c d; rewrite /Rmax. case (Rle_dec (a + b) (c+d)); case (Rle_dec a c); case ( Rle_dec b d) => H J K ; try fourier. have H' := Rnot_le_lt _ _ H; fourier. have H' := Rnot_le_lt _ _ J; fourier. have H' := Rnot_le_lt _ _ J. have H'' := Rnot_le_lt _ _ H. elim (RIneq.Rle_not_lt _ _ K); fourier. Qed. Lemma Rmin_assoc: forall x y z, Rmin x (Rmin y z) = Rmin (Rmin x y) z. Proof. move=> x y z. destruct (Rle_or_lt x y). replace (Rmin x y) with x ; [|unfold Rmin; case Rle_dec; auto with real]. destruct (Rle_or_lt y z). replace (Rmin y z) with y; [|unfold Rmin; case Rle_dec; auto with real]. replace (Rmin x y) with x;[|unfold Rmin; case Rle_dec; auto with real]. have H1: x<=z. apply Rle_trans with y; by fourier. replace (Rmin x z) with x. done. unfold Rmin; case Rle_dec; auto with real. replace (Rmin y z) with z; [done|unfold Rmin; case Rle_dec; auto with real]. replace (Rmin x y) with y; [|unfold Rmin; case Rle_dec; auto with real]. destruct (Rle_or_lt y z). replace (Rmin y z) with y; [|unfold Rmin; case Rle_dec; auto with real]. unfold Rmin; case Rle_dec; auto with real. replace (Rmin y z) with z; [|unfold Rmin; case Rle_dec; auto with real]. have H3: z Rmin r1 r2 = r1. Proof. move=> r1 r2 H; rewrite /Rmin; case (Rle_dec r1 r2); auto with real. Qed. Lemma Rmin_right: forall r1 r2, r2 <= r1 -> Rmin r1 r2 = r2. Proof. move=> r1 r2 H; rewrite /Rmin; case (Rle_dec r1 r2); auto with real. Qed. Lemma Rmin_le: forall r1 r2 r, r1 <= r -> r2 <=r -> Rmin r1 r2 <= r. Proof. move=> r1 r2 r H1 H2; rewrite /Rmin; case (Rle_dec r1 r2) =>H; fourier. Qed. Lemma Rmin_ge: forall r1 r2 r, r <= r1 -> r <=r2 -> r <= Rmin r1 r2. Proof. move=> r1 r2 r H1 H2; rewrite /Rmin; case (Rle_dec r1 r2) =>H; fourier. Qed. Lemma Rmin_split: forall a b, Rmin a b = a \/ Rmin a b = b. Proof. by move=> a b; rewrite /Rmin; case (Rle_dec a b) => Hab; [left|right]. Qed. End min_max_prop. Section min_max_big. Lemma big_max_le: forall (r:seq R) (F: R -> R) i0, i0 \in r -> F i0 <= \big[Rmax/F (last 0 r) ]_(i <- r) F i. Proof. move=> r F i0 Hi0. have Hnul: r != [::]. apply/eqP=> Hr; rewrite Hr in Hi0 . have Hr2:= @in_nil _ i0. by rewrite Hi0 in Hr2. move: Hnul Hi0; elim r; first by done. move=> i s IHs _ Hri0. rewrite big_cons. case Hi: (i0 == i). move/eqP: Hi => Hi; rewrite Hi; apply RmaxLess1 . apply Rle_trans with (\big[Rmax/F (last 0 (i :: s))]_(j <- s) F j); last by apply RmaxLess2. rewrite in_cons in Hri0; rewrite Hi in Hri0; rewrite orFb in Hri0. have Hnul: s != [::]. apply/eqP=> Hr; rewrite Hr in Hri0 . have Hr2:= @in_nil _ i0. by rewrite Hri0 in Hr2. by rewrite -(last_cons i Hnul); apply IHs. Qed. Lemma big_max_exists: forall (r:seq R) (F: R -> R), r != [::] -> {i0 |i0 \in r /\ \big[Rmax/F (last 0 r) ]_(i <- r) F i = F i0}. Proof. move=> r F Hr. move: Hr; elim r; first by done. move=> i0 s Ih _. case Hs: (s != [::]). elim (Ih Hs) => i1 [Hi0 Hi1]. elim (Rle_dec (F i0) (F i1)) => Hdec. exists i1; split. by rewrite in_cons; rewrite Hi0; apply orbT. by rewrite big_cons -(last_cons i0 Hs) Hi1 Rmax_right. exists i0; split; [apply mem_head|rewrite big_cons -(last_cons i0 Hs) Hi1 Rmax_left;[done|]]. by left; apply: Rnot_le_gt. exists i0; rewrite big_cons. by move/eqP: Hs => Hs; split; [apply mem_head|rewrite Hs big_nil /last //= Rmax_right; [|right]]. Qed. Lemma big_min_exists: forall (r:seq R) (F: R -> R), r != [::] -> {i0 | i0 \in r /\ \big[Rmin/F (last 0 r) ]_(i <- r) F i = F i0}. Proof. move=> r F Hr. move: Hr; elim r; first by done. move=> i0 s Ih _. case Hs: (s != [::]). elim (Ih Hs) => i1 [Hi0 Hi1]. elim (Rle_dec (F i0) (F i1)) => Hdec. by exists i0; split; [apply mem_head|rewrite big_cons -(last_cons i0 Hs) Hi1 Rmin_left]. exists i1; split. by rewrite in_cons; rewrite Hi0; apply orbT. rewrite big_cons -(last_cons i0 Hs) Hi1 Rmin_right;[done|]. by left; apply: Rnot_le_gt. exists i0; rewrite big_cons. by move/eqP: Hs => Hs; split; [apply mem_head| rewrite Hs big_nil /last //= Rmin_right; [|right]]. Qed. Lemma big_min_le: forall (r: seq R) (F : R-> R) i0, i0 \in r -> \big[Rmin/F (last 0 r) ]_(i <- r) F i <= F i0. Proof. move=> r F i0 Hi0. have Hnul: r != [::]. apply/eqP=> Hr; rewrite Hr in Hi0 . have Hr2:= @in_nil _ i0. by rewrite Hi0 in Hr2. move: Hnul Hi0; elim r; first by done. move=> i s IHs _ Hri0. rewrite big_cons. case Hi: (i0 == i). move/eqP: Hi => Hi; rewrite Hi; apply Rmin_l . apply Rle_trans with (\big[Rmin/F (last 0 (i :: s))]_(j <- s) F j); first by apply Rmin_r. rewrite in_cons in Hri0; rewrite Hi in Hri0; rewrite orFb in Hri0. have Hnul: s != [::]. apply/eqP=> Hr; rewrite Hr in Hri0 . have Hr2:= @in_nil _ i0. by rewrite Hri0 in Hr2. by rewrite -(last_cons i Hnul); apply IHs. Qed. Lemma big_min_max_le: forall (r: seq R) (F : R-> R), r!=[::] -> \big[Rmin/F (last 0 r) ]_(i <- r) F i <= \big[Rmax/F (last 0 r) ]_(i <- r) F i. Proof. move=> r F Hr. case r; first by (rewrite !big_nil; right). move=> i s; apply Rle_trans with (F i); [apply: big_min_le|apply: big_max_le]; apply: mem_head. Qed. End min_max_big. Section patchRmax. Variable p: nat. Definition Rmax2 r1 r2: R := match (Rlt_le_dec R0 r1) with |left _ => Rmax r1 r2 |right _ => match (Rlt_le_dec R0 r2) with |left _ => Rmax r1 r2 |right _=> Rmin r1 r2 end end. Lemma com_rmax2: commutative Rmax2. Proof. move=> x y; rewrite /Rmax2; case (Rlt_le_dec R0 x) => Hx; case (Rlt_le_dec R0 y) => Hy; [by rewrite Rmax_comm |by rewrite Rmax_comm| by rewrite Rmax_comm |by rewrite Rmin_comm]. Qed. Lemma el_n_zerol: left_id R0 Rmax2. Proof. move=> x ; rewrite /Rmax2; case (Rlt_le_dec R0 x) => Hx0; case (Rlt_le_dec R0 R0) => H00. case (Rlt_irrefl R0 H00). rewrite /Rmax; case (Rle_dec R0 x) => h0x; auto with real. case (Rlt_irrefl R0 H00). rewrite /Rmin; case (Rle_dec R0 x) => h0x; auto with real. Qed. Lemma el_n_zeror: right_id R0 Rmax2 . Proof. move=>x; rewrite com_rmax2; apply el_n_zerol. Qed. Lemma ass_max2 : associative Rmax2. Proof. move=> x y z. rewrite {1 4}/Rmax2 ; case (Rlt_le_dec R0 x) => Hx0. rewrite !(com_rmax2 _ z) /Rmax2; case (Rlt_le_dec R0 z) => Hz0. rewrite !(Rmax_comm z _); apply Rmax_assoc. case (Rlt_le_dec R0 y) => Hy0 //=. case (Rlt_le_dec R0 (Rmax x y))=> Hxy //=. by rewrite !Rmax_assoc (Rmax_comm z _). have h2 : ~ Rmax x y <= 0. apply RIneq.Rlt_not_le; case (Rle_dec x y) => hxy; apply Rlt_le_trans with x ; rewrite //=; apply RmaxLess1 . by elim h2. case (Rlt_le_dec R0 (Rmax x y))=> Hrxy. rewrite Rmax_assoc (Rmax_comm z _) -Rmax_assoc. rewrite Rmax_left ; [rewrite Rmax_left;[done|]|]. apply Rle_trans with R0;[by apply Rmax_le|by left]. apply Rle_trans with R0; [by apply Rmin_le|by left]. rewrite Rmax_left in Hrxy. by case (RIneq.Rle_not_lt R0 x Hrxy). by left; apply Rle_lt_trans with R0. case (Rlt_le_dec R0 (Rmax2 y z)) => H2. rewrite {1}/Rmax ; case (Rle_dec x (Rmax2 y z)) => Hxyz. case (Rlt_le_dec R0 y) => Hy0. by rewrite Rmax_right; [|left; apply Rle_lt_trans with R0]. rewrite {2}/Rmax2; case (Rlt_le_dec R0 (Rmin x y))=> Hmin. have Hmin2: Rmin x y > 0 by rewrite //=. move: Hmin2; rewrite Rmin_Rgt=>Hmin2; case Hmin2 => H0 H1. by case (RIneq.Rle_not_lt R0 x ). rewrite com_rmax2; rewrite /Rmax2; case (Rlt_le_dec R0 z) => Hz0. by rewrite Rmax_left;[rewrite Rmax_right;[|left; apply Rle_lt_trans with R0]| left; apply Rle_lt_trans with R0]. rewrite /Rmax2 in H2. move:H2. case (Rlt_le_dec R0 y) => Hy01 H2. move: H2; rewrite Rmax_Rlt_el => H2; case H2 => H3. by case (RIneq.Rle_not_lt R0 y ). by case (RIneq.Rle_not_lt R0 z ). move: H2. case (Rlt_le_dec R0 z)=> H0z1 H2. by case (RIneq.Rle_not_lt R0 z ). case (Rmin_split y z) => hr; rewrite hr in H2. by case (RIneq.Rle_not_lt R0 y). by case (RIneq.Rle_not_lt R0 z). have H1: x <= Rmax2 y z . by left; apply Rle_lt_trans with R0. by case Hxyz. move: H2; rewrite {1}/Rmax2. case (Rlt_le_dec R0 y) => H0y H2. rewrite Rmax_right;[|apply Rle_trans with R0; fourier]. move: H2; rewrite -Rmax_le2 => H2; case H2 => Hxy. by case (RIneq.Rle_not_lt R0 y). move:H2; rewrite {1}/Rmax2. case (Rlt_le_dec R0 z) => H0z H2. move: H2; rewrite -Rmax_le2 => H2; case H2 => Hzy1 Hzy2. by case (RIneq.Rle_not_lt R0 z). case (Rlt_le_dec R0 y) => Hy0. by case (RIneq.Rle_not_lt R0 y). rewrite /Rmax2; case (Rlt_le_dec R0 (Rmin x y)) => Hmin. case (Rmin_split x y) => H; rewrite H in Hmin. by case (RIneq.Rle_not_lt R0 x). by case (RIneq.Rle_not_lt R0 y). case (Rlt_le_dec R0 z) => Hz0. by case (RIneq.Rle_not_lt R0 z). apply Rmin_assoc. Qed. Canonical Structure is_mon_law:= Monoid.Law ass_max2 el_n_zerol el_n_zeror. Canonical Structure is_ab_law:= Monoid.ComLaw com_rmax2. Lemma Rmax_Rmax2: forall x y, R0 <= x -> R0 <= y -> Rmax x y = Rmax2 x y. Proof. move=> x y Hx Hy; rewrite /Rmax2; case (Rlt_le_dec R0 x) => Hx0; first by done. case (Rlt_le_dec R0 y) => Hy0; first by done. have Hex: x=R0. by apply Rle_antisym. have Hey: y=R0. by apply Rle_antisym. rewrite Hex Hey /Rmax /Rmin; case (Rle_dec R0 R0)=> H00; auto with real. Qed. Lemma sxbigD1 : forall j (P : 'I_p -> bool) F, (forall i, R0 <= F i) -> P j -> \big[Rmax/R0]_(i

j P F HF Pj. have H1: forall P F, (forall i, R0 <= F i) -> \big[Rmax/0]_(i < p | P i) F i = \big[Rmax2/0]_(i < p | P i) F i. move=> P0 F0 Hf. apply: (@eq_big_op _ (fun r => R0 <= r)_ _); first by right. move=> x y Hx Hy; apply Rle_trans with x; [done| apply RmaxLess1]. move=> x y Hx Hy; rewrite /Rmax2; case (Rlt_le_dec R0 x) => Hx0; first by done. case (Rlt_le_dec R0 y) => Hy0; first by done. have Hex: x=R0. by apply Rle_antisym. have Hey: y=R0. by apply Rle_antisym. rewrite Hex Hey /Rmax /Rmin; case (Rle_dec R0 R0)=> H00; auto with real. move=> i Hi; apply Hf. rewrite !(H1 _ _ HF). rewrite Rmax_Rmax2. rewrite (bigD1 j) //=. apply HF. apply: big_prop; first by right. by move=> x y Hx Hy; rewrite -Rmax_Rmax2 ; [ apply Rle_trans with x ;[|apply RmaxLess1]| |]. move=>*; apply HF. Qed. Lemma Rmax_le_f_le: forall (f g: 'I_p ->R), (forall i, f i <= g i) -> \big[Rmax/0]_i f i <= \big[Rmax/0]_i g i. Proof. move => f g Hfg . by apply: big_rel; [right|move=>*; apply rmax4 |move=>*;apply Hfg]. Qed. Lemma sum_le_f_le: forall (f g: 'I_p ->R), (forall i, f i <= g i) -> \big[Rplus/R0]_i f i <= \big[Rplus/R0]_i g i. Proof. by move => f g Hfg; apply:big_rel; [right|move=>*; apply Rplus_le_compat |move=>*;apply Hfg]. Qed. Lemma distr_mult_max: forall (r:R) (f:'I_p->R), R0<=r-> r* (\big[Rmax/0]_j (f j))= \big[Rmax/R0]_j (r*f j). Proof. move => r f Hr. (*rewrite (eq_big_op (fun r => 0 <= r) Rmax2) //=.*) apply: (big_op_rel (@eq R) (fun x => Rmult r x)); [rewrite //= ; ring| by move=>a b c H1 H2; rewrite H1 -H2| by move=>a b c H; rewrite H|]. move=> a b; rewrite /Rmax; case (Rle_dec a b) =>H; case (Rle_dec (r*a) (r*b)) => Hra; try done; [by case Hra; apply Rmult_le_compat_l| case Hr => H1; [ by case H;apply Rmult_le_reg_l with r| rewrite -H1; ring]]. Qed. (*use this lemma for proving positive homogenity*) Lemma max_exists: forall p, (0 forall (f:'I_p->R), (forall i, 0 <= f i)-> exists k, \big[Rmax/0]_j (f j ) = f k. Proof. move =>q Hq v Hv. move : (I_not_void Hq). rewrite /enum -/(index_enum (ordinal_finType q)). have hu1: uniq (index_enum (ordinal_finType q)). rewrite /index_enum -enumT; apply enum_uniq. have Hfi: forall s, filter 'I_q s = s. move=> s. elim: s; first by done. by move=> t s IH; rewrite /=; f_equal. rewrite Hfi. elim: (index_enum ) hu1. by rewrite /=. move => x s IH IHun Iht. rewrite cons_uniq in IHun. move/andP: IHun => IHun; elim IHun => I1 I2. rewrite big_cons. case A:(Nil _ != s). elim (Rle_dec ((v x))(\big[Rmax/0]_(j <- s) v j))=> I3. elim (IH I2 A) => k Hk. exists k; rewrite -Hk. unfold Rmax at 1 ; case (Rle_dec ( v x) (\big[Rmax/0]_(j <- s) v j)) ; auto with real. exists x. unfold Rmax at 1 ; case (Rle_dec (v x) (\big[Rmax/0]_(j <- s) v j) ) ; auto with real. exists x. move/eqP :A=>A. rewrite -A //=. have H:= Hv x. rewrite big_nil. unfold Rmax; case (Rle_dec (v x) 0); auto with real. Qed. Lemma max_exists_seq: forall (r : seq R) f, r != [::] -> (forall i, i \in r -> 0 <= f i) -> {k: R | k \in r /\ \big[Rmax/0]_(j <- r) (f j) = f k}. Proof. move => r F Hr Hf. (* Hq v Hv. *) (*move=> r F Hr.*) move: Hr Hf; elim r; first by done. move=> i0 s Ih _ IHf. case Hs: (s != [::]). have Hfi: (forall i : real_eqType, i \in s -> 0 <= F i). by move=> i Hi; apply IHf; rewrite in_cons; apply/orP; right. elim (Ih Hs Hfi) => i1 [Hi0 Hi1]. elim (Rle_dec (F i0) (F i1)) => Hdec. exists i1; split. by rewrite in_cons; rewrite Hi0; apply orbT. by rewrite big_cons Hi1 Rmax_right. exists i0; split; [apply: mem_head|rewrite big_cons Hi1 Rmax_left;[done|]]. by left; apply: Rnot_le_gt. exists i0; rewrite big_cons. move/eqP: Hs => Hs; split; [apply: mem_head|]. rewrite Hs big_nil //=. rewrite /Rmax; case (Rle_dec (F i0) 0) => Hi0; last by done. by apply Rle_antisym; [apply IHf; apply mem_head|]. Qed. Lemma max_exists_seq2: forall (r : seq R) f, r != [::] -> {k: R | k \in r /\ \big[Rmax/f (last 0 r)]_(j <- r) (f j) = f k}. Proof. move => r F Hr . (* Hq v Hv. *) (*move=> r F Hr.*) move: Hr ; elim r; first by done. move=> i0 s Ih _ . case Hs: (s != [::]). elim (Ih Hs ) => i1 [Hi0 Hi1]. elim (Rle_dec (F i0) (F i1)) => Hdec. exists i1; split. by rewrite in_cons; rewrite Hi0; apply orbT. rewrite -(last_cons i0 Hs). by rewrite big_cons Hi1 Rmax_right. exists i0; split; [apply: mem_head|rewrite big_cons -(last_cons i0 Hs) Hi1 Rmax_left;[done|]]. by left; apply: Rnot_le_gt. exists i0; rewrite big_cons. move/eqP: Hs => Hs; split; [apply: mem_head|]. rewrite Hs big_nil //=. rewrite /Rmax; case (Rle_dec (F i0) (F i0)) => Hi0; done. Qed. Lemma desc_max: forall (v: 'I_p -> R) j, (forall i, 0 <= v i)-> \big[Rmax/0]_i (v i ) = Rmax (v j) (\big[Rmax/R0]_(iv j H; apply sxbigD1 with (P:=(fun _ :'I_p=> true)) (j:=j) (F:= (fun t => (v t))). Qed. Lemma max_max: forall (v:'I_p->R) i, (forall i, 0 <= v i) -> v i <= \big[Rmax/0]_j (v j ). Proof. move=> v i H; rewrite (desc_max i H); apply RmaxLess1. Qed. Lemma distr_plus_max: forall (r f:'I_p->R), (forall i, 0<=r i)-> (forall i, 0<=f i)-> (\big[Rmax/0]_j (f j + r j))<= \big[Rmax/0]_j (f j) + \big[Rmax/0]_j (r j). Proof. move => g f Hg Hf. have Hfg: forall i, 0 <=f i + g i . move => i; apply Rplus_le_le_0_compat; [apply Hf|apply Hg]. elim: index_enum. rewrite !big_nil; right; ring. move=> t s IH. rewrite !big_cons. apply Rle_trans with (Rmax (f t + g t) ( \big[Rmax/0]_(j <- s) f j + \big[Rmax/0]_(j <- s) g j)). by apply Rmax_le_compat. by apply Rmax_Rplus_le_compat2. Qed. (*Definition max_f f := \max_(i < p) f i. Lemma desc_max_f0 : forall f j, max_f f = maxn (f j) (\max_(i

f j. rewrite /max_f. by apply: (bigD1 j ). Qed. Lemma max_maxn: forall m n, maxn m n = max m n. Proof. move=> m n; rewrite /maxn. Print Scope nat_scope. case C: (mC; omega] . by rewrite max_l; [|move/leP:C=>C; omega]. Qed. Lemma desc_max_f: forall f j, max_f f = max (f j) (\max_(i

f j; rewrite -{1}max_maxn (desc_max_f0 f j). Qed. Lemma max_greater: forall (f:'I_p->nat) (k:'I_p), (f k <= max_f f)%coq_nat. Proof. move => f k. rewrite (desc_max_f f k). by apply le_max_l. Qed. *) End patchRmax. Section patchRmin. Variable p: nat. (*we need for the next lemmas to compute the minimum of a vector with positive values; ticky because we don't have a neutral element with respect to this opperation*) Definition less_1 r := Rmin r 1. Definition min_del (v:'I_p ->R) := \big[Rmin/1]_i (less_1 (v i)). Definition Rmin2 r1 r2: R := match (Rlt_le_dec r1 R1) with |left _ => Rmin r1 r2 |right _ => match (Rlt_le_dec r2 R1) with |left _ => Rmin r1 r2 |right _=> Rmax r1 r2 end end. Lemma com_rmin2: commutative Rmin2. Proof. move=> x y; rewrite /Rmin2; case (Rlt_le_dec x R1 ) => Hx; case (Rlt_le_dec y R1) => H; [by rewrite Rmin_comm |by rewrite Rmin_comm| by rewrite Rmin_comm |by rewrite Rmax_comm]. Qed. Lemma min_el_n_zerol: left_id R1 Rmin2. Proof. move=> x ; rewrite /Rmin2; case (Rlt_le_dec x R1 ) => Hx0; case (Rlt_le_dec R1 R1) => H00. case (Rlt_irrefl R1 H00). rewrite /Rmin; case (Rle_dec R1 x) => h0x; auto with real. case (Rlt_irrefl R1 H00). rewrite /Rmax; case (Rle_dec R1 x ) => h0x; auto with real. Qed. Lemma min_el_n_zeror: right_id R1 Rmin2 . Proof. move=>x; rewrite com_rmin2; apply min_el_n_zerol. Qed. Lemma ass_min2 : associative Rmin2. Proof. move=> x y z. rewrite {1 4}/Rmin2 ; case (Rlt_le_dec x R1) => Hx0. rewrite !(com_rmin2 _ z) /Rmin2; case (Rlt_le_dec z R1) => Hz0. rewrite !(Rmin_comm z _); apply Rmin_assoc. case (Rlt_le_dec y R1) => Hy0 //=. case (Rlt_le_dec (Rmin x y) R1)=> Hxy //=. by rewrite !Rmin_assoc (Rmin_comm z _). have h2 : ~ 1 <= Rmin x y . apply RIneq.Rlt_not_le; case (Rle_dec x y) => hxy; apply Rle_lt_trans with x ; rewrite //=; apply Rmin_l . by elim h2. case (Rlt_le_dec (Rmin x y) R1)=> Hrxy. rewrite Rmin_assoc (Rmin_comm z _) -Rmin_assoc. rewrite Rmin_left ; [rewrite Rmin_left;[done|]|]. apply Rle_trans with R1; [by left | by apply Rmin_ge ]. apply Rle_trans with R1; [by left | by apply Rmax_ge]. rewrite Rmin_left in Hrxy. by case (RIneq.Rle_not_lt x R1 Hrxy). by left; apply Rlt_le_trans with R1. case (Rlt_le_dec (Rmin2 y z) 1) => H2. rewrite {1}/Rmin ; case (Rle_dec x (Rmin2 y z)) => Hxyz. by case (RIneq.Rle_not_lt x 1 ); [|apply Rle_lt_trans with (Rmin2 y z)]. case (Rlt_le_dec y 1) => Hy0. by rewrite Rmin_right; [|left; apply Rlt_le_trans with R1]. rewrite {2}/Rmin2; case (Rlt_le_dec (Rmax x y) 1)=> Hmin. by case (RIneq.Rle_not_lt x 1 ); [|apply Rle_lt_trans with (Rmax x y); [apply RmaxLess1|]]. rewrite com_rmin2; rewrite /Rmin2; case (Rlt_le_dec z 1) => Hz0. by rewrite Rmin_left;[rewrite Rmin_right;[|left; apply Rlt_le_trans with R1]| left; apply Rlt_le_trans with R1]. rewrite /Rmin2 in H2. move:H2. case (Rlt_le_dec y 1) => Hy01 H2. by case (RIneq.Rle_not_lt y 1). move: H2. case (Rlt_le_dec z 1)=> H0z1 H2. by case (RIneq.Rle_not_lt z 1). by case (RIneq.Rle_not_lt y 1); [|apply Rle_lt_trans with (Rmax y z);[apply RmaxLess1|]]. case (Rlt_le_dec y 1) => H0y. rewrite /Rmin; case (Rle_dec x y) => Hxy. by case (RIneq.Rle_not_lt y 1); [apply Rle_trans with x|]. rewrite Rmax_right; first by done. move: H2; rewrite /Rmin2; case (Rlt_le_dec y 1) =>Hy1 H2. by case (RIneq.Rle_not_lt y 1); [apply Rle_trans with (Rmin y z); [|apply Rmin_l]|]. by case (RIneq.Rle_not_lt y 1). rewrite {2}/Rmin2; case (Rlt_le_dec (Rmax x y) 1) => Hmin. by case (RIneq.Rle_not_lt x 1); [|apply Rle_lt_trans with (Rmax x y);[apply RmaxLess1|]]. case (Rlt_le_dec z 1) => Hz. move: H2;rewrite {1}/Rmax; case (Rle_dec x (Rmin2 y z))=> Hx1 H2. move: H2; rewrite /Rmin2. case (Rlt_le_dec y 1) => H1. by case (RIneq.Rle_not_lt y 1). case (Rlt_le_dec z 1 ) => Hz1 H2. by case (RIneq.Rle_not_lt z 1); [apply Rle_trans with (Rmin y z); [|apply Rmin_r]|]. by case (RIneq.Rle_not_lt z 1). move: H2; rewrite /Rmin2. case (Rlt_le_dec y 1) => Hy. by case (RIneq.Rle_not_lt y 1). case (Rlt_le_dec z 1) => Hz2 H2. by case (RIneq.Rle_not_lt z 1); [apply Rle_trans with (Rmin y z); [|apply Rmin_r]|]. by case (RIneq.Rle_not_lt z 1). rewrite -Rmax_assoc. rewrite {2}/Rmax; case (Rle_dec x (Rmax y z)) => Hxyz. rewrite {1}Rmax_right /Rmin2; case ((Rlt_le_dec y 1)) => Hy. by case (RIneq.Rle_not_lt y 1). case ((Rlt_le_dec z 1)) => Hz1. by case (RIneq.Rle_not_lt z 1). done. by case (RIneq.Rle_not_lt y 1). case ((Rlt_le_dec z 1)) => Hz1. by case (RIneq.Rle_not_lt z 1). done. rewrite /Rmax; case (Rle_dec x (Rmin2 y z)); last by done. rewrite /Rmin2; case ((Rlt_le_dec y 1)) => Hy. by case (RIneq.Rle_not_lt y 1). case ((Rlt_le_dec z 1)) => Hz1. by case (RIneq.Rle_not_lt z 1). move=> H; case (Hxyz H). Qed. Canonical Structure is_mon_law_min:= Monoid.Law ass_min2 min_el_n_zerol min_el_n_zeror. Canonical Structure is_ab_law_min:= Monoid.ComLaw com_rmin2. Lemma Rmin_Rmin2: forall x y, x <= R1 -> y <= R1 -> Rmin x y = Rmin2 x y. Proof. move=> x y Hx Hy; rewrite /Rmin2; case (Rlt_le_dec x R1) => Hx0; first by done. case (Rlt_le_dec y R1) => Hy0; first by done. have Hex: x=R1. by apply Rle_antisym. have Hey: y=R1. by apply Rle_antisym. rewrite Hex Hey /Rmax /Rmin; case (Rle_dec R1 R1)=> H00; auto with real. Qed. Lemma smin_bigD1 : forall j (P : 'I_p -> bool) F, (forall i, F i <= R1) -> P j -> \big[Rmin/R1]_(i

j P F HF Pj. have H1: forall P F, (forall i,F i <=R1) -> \big[Rmin/1]_(i < p | P i) F i = \big[Rmin2/1]_(i < p | P i) F i. move=> P0 F0 Hf. apply: (@eq_big_op _ (fun r => r <= R1)_ _); first by right. move=> x y Hx Hy; apply Rle_trans with x; [apply Rmin_l|done]. move=> x y Hx Hy; rewrite /Rmin2; case (Rlt_le_dec x R1) => Hx0; first by done. case (Rlt_le_dec y 1) => Hy0; first by done. have Hex: x=R1. by apply Rle_antisym. have Hey: y=R1. by apply Rle_antisym. rewrite Hex Hey /Rmax /Rmin; case (Rle_dec R1 R1)=> H00; auto with real. move=> i Hi; apply Hf. rewrite !(H1 _ _ HF). rewrite Rmin_Rmin2. rewrite (bigD1 j) //=. apply HF. apply big_prop; first by right. move=> x y Hx Hy; rewrite -Rmin_Rmin2; try done. by apply Rle_trans with x; [apply Rmin_l|]. move=>*; apply HF. Qed. Lemma minbigD1 : forall j (P : 'I_p -> bool) F, (forall i, F i <= 1) -> P j -> \big[Rmin/R1]_(i

j P F HF Pj. have H1: forall P F, (forall i, F i <= 1) -> \big[Rmin/1]_(i < p | P i) F i = \big[Rmin2/1]_(i < p | P i) F i. move=> P0 F0 Hf. apply: (@eq_big_op _ (fun r => r <= 1)_ _); first by right. move=> x y Hx Hy; apply Rle_trans with x; [apply Rmin_l|done]. move=> x y Hx Hy; rewrite /Rmin2; case (Rlt_le_dec x R1) => Hx0; first by done. case (Rlt_le_dec y 1) => Hy0; first by done. have Hex: x= 1 . by apply Rle_antisym. have Hey: y= 1 . by apply Rle_antisym. rewrite Hex Hey /Rmax /Rmin; case (Rle_dec 1 1)=> H00; auto with real. move=> i Hi; apply Hf. rewrite !(H1 _ _ HF). rewrite Rmin_Rmin2. rewrite (bigD1 j) //=. apply HF. apply big_prop; first by right. move=> x y Hx Hy; rewrite -Rmin_Rmin2; try done. by apply Rle_trans with x; [apply Rmin_l|]. move=>*; apply HF. Qed. Lemma desc_min:forall v j, \big[Rmin/R1]_i less_1 (v i ) = Rmin (less_1 (v j)) (\big[Rmin/R1]_(iv j . apply: minbigD1; [by move =>*; rewrite /less_1; apply Rmin_r|done]. Qed. Lemma min_min: forall (v:'I_p->R) i, min_del v <= v i. Proof. move=> v i ; rewrite /min_del (desc_min v i). apply Rle_trans with (less_1 (v i)). apply Rmin_l. rewrite /less_1; apply Rmin_l. Qed. Lemma min_ge0: forall (v:'I_p->R), (forall j, 0< v j) -> 0 < min_del v. Proof. move=> v H; rewrite /min_del . elim (index_enum (ordinal_finType p) ). rewrite big_nil; fourier. move => x s IH. rewrite big_cons; apply Rmin_Rgt_r; split. rewrite /less_1; apply Rmin_Rgt_r; split; [ apply: H|fourier]. case S:(Nil _ !=s). by apply: IH. move/eqP:S => S; rewrite -S big_nil; fourier. Qed. End patchRmin. (*Implicit Arguments max_f [p].*) Implicit Arguments min_del [p]. Implicit Arguments min_ge0 [p]. Implicit Arguments Rmax_le_f_le [p]. Implicit Arguments sum_le_f_le [p]. Implicit Arguments distr_plus_max [p]. Open Scope R_scope. Open Scope ring_scope. Delimit Scope R_scope with Re. Section real_big. Variable p: nat. Lemma ineq_sum_el: forall v r,(0 < p)%Dn -> 0<=r->(forall x, v x < r/INR p) -> \big[Rplus/R0]_(i f r Hp Hr H. have H1: forall s, [::] !=s ->\big[Rplus/0]_(i <- s) f i < r * INR (size s)/INR p. move=> s; elim s. rewrite //=. move=> j s0 IH _. rewrite big_cons ; simpl (size (j::s0)). case A: ([::] != s0). apply Rlt_le_trans with (r/ INR p+ r * INR (size s0) / INR p )%Re. by apply Rplus_lt_compat; [ apply H|apply IH]. by right; rewrite /Rdiv (S_INR (size _)) (Rmult_plus_distr_l r _ _) Rmult_plus_distr_r Rplus_comm Rmult_1_r. move/eqP:A=>A; rewrite -A big_nil /size . replace (INR 1) with R1; last by auto with real. rewrite Rmult_1_r; toR; ring_simplify ; apply H. replace r with (r *(INR (size (index_enum (ordinal_finType p))))/INR p)%Re. apply H1; rewrite /index_enum -enumT. apply (I_not_void Hp). rewrite /index_enum -enumT; rewrite size_enum_ord; field; apply Rgt_not_eq; apply: lt_INR_0. by move/ltP : Hp. Qed. Lemma abs_sum_le_sum_abs: forall (p: nat) (f: 'I_p ->R) , Rabs (\sum_i (f i)) <= \sum_i (Rabs (f i)). Proof. move => m v. elim index_enum. by rewrite !big_nil Rabs_R0; right. move => x s IH . rewrite !big_cons. apply Rle_trans with (1:= Rabs_triang _ _). by apply Rplus_le_compat_l. Qed. Lemma echiv_sums: forall N f, sum_f_R0 f N = \sum_(i N f . induction N. rewrite big_ord_recl //=. have Heq: \sum_(i < O%nat) f (bump O%nat i) = R0. apply big_ord0. rewrite Heq /@GRing.add /=; ring. rewrite //=. have Heq: \sum_(j < N.+2) f j = \sum_(j < N.+1) f j + f (N.+1) . by rewrite big_ord_recr /=. rewrite Heq {1}Rplus_comm GRing.addrC. by apply Rplus_eq_compat_l. Qed. Lemma sum_S_eq: forall (f:nat -> R) n, \sum_(i f N; rewrite big_ord_recr /= GRing.addrC. Qed. Lemma sum_dif: forall (f:nat ->R) m n, (m < n)%nat -> \sum_(i f m n. induction n => H //=. have H0 : (m <= n)%coq_nat; [by move/ltP:H=>H; omega|]. elim (le_lt_eq_dec _ _ H0) => H1. rewrite sum_S_eq. transitivity ( \sum_(i < n.+1) f i - \sum_(i < m.+1) f i + f (n.+1)). rewrite /@GRing.add /@GRing.opp /=; ring. move/ltP:H1=>H1; rewrite (IHn H1). replace (m.+1) with (O+(m.+1))%coq_nat;[|omega]. have H2:= (@big_addn _ _ _ (O%nat) (n.+1)%nat (m.+1) (fun _ => true) f). rewrite H2. have H3:= (@big_addn _ _ _ (O%nat) ((n.+1).+1) (m.+1) (fun _ => true) f). rewrite H3. rewrite !big_mkord. replace (n.+1 - m.+1)%Dn with ((n - m.+1).+1)%Dn. replace ( (n.+1).+1 - m.+1)%Dn with ((((n - m.+1).+1).+1)%nat). have H4:= sum_S_eq (fun i => f (i + m.+1)%Dn) ((n - m.+1)). rewrite H4. replace (((n - m.+1).+1 + m.+1)%Dn) with (n.+1). rewrite /@GRing.add //=; ring. rewrite -ltn_subS; last by done. by nat_norm; nat_congr; rewrite subnK. rewrite -ltn_subS; last by done. by rewrite (subSS) leq_subS. by rewrite leq_subS. rewrite H1. rewrite sum_S_eq /GRing.opp /GRing.add /= /Rminus. rewrite Rplus_assoc Rplus_opp_r Rplus_0_r. have H2:= (@big_addn _ _ _ (O%nat) ((n.+1).+1) ((n.+1)) (fun _ => true) f). pattern (n.+1) at 2; replace (n.+1) with (O%nat+n.+1)%nat; last by done. rewrite H2 big_mkord. replace ((n.+1).+1 - n.+1)%Dn with (S O)%nat. by rewrite big_ord_recl //= big_ord0 Rplus_0_r. by rewrite (subSS) subSnn. Qed. End real_big. Implicit Arguments ineq_sum_el [p]. Implicit Arguments abs_sum_le_sum_abs[p].