diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f16991f32..33a3db277 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -100,6 +100,39 @@ + lemmas `mule_le0_ge0`, `mule_ge0_le0`, `pmule_rle0`, `pmule_lle0`, `nmule_lle0`, `nmule_rle0` + lemma `sube0` + + lemmas `adde_le0`, `sume_le0`, `oppe_ge0`, `oppe_le0`, + `lte_opp`, `gee_addl`, `gee_addr`, `lte_addr`, + `gte_subl`, `gte_subr`, `lte_le_sub`, `lee_sum_npos_subset`, + `lee_sum_npos`, `lee_sum_npos_ord`, `lee_sum_npos_natr`, + `lee_sum_npos_natl`, `lee_sum_npos_subfset`, `lee_opp`, + `le0_muleDl`, `le0_muleDr`, `le0_sume_distrl`, `le0_sume_distrr`, + `adde_defNN`, `minEFin`, `mine_ninftyl`, `mine_ninftyr`, `mine_pinftyl`, + `mine_pinftyr`, `oppe_max`, `oppe_min`, `mineMr`, `mineMl` + + definitions `dual_adde` + + notations for the above in scope `ereal_dual_scope` delimited by `dE` + + lemmas `dual_addeE`, `dual_sumeE`, `dual_addeE_def`, `daddEFin`, + `dsumEFin`, `dsubEFin`, `dadde0`, `dadd0e`, `daddeC`, `daddeA`, + `daddeAC`, `daddeCA`, `daddeACA`, `doppeD`, `dsube0`, `dsub0e`, `daddeK`, + `dfin_numD`, `dreal_of_extendedD`, `dsubeK`, `dsube_eq`, + `dsubee`, `dadde_eq_pinfty`, `daddooe`, `dadde_Neq_pinfty`, + `dadde_Neq_ninfty`, `desum_fset_pinfty`, `desum_pinfty`, + `desum_fset_ninfty`, `desum_ninfty`, `dadde_ge0`, `dadde_le0`, + `dsume_ge0`, `dsume_le0`, `dsube_lt0`, `dsubre_le0`, + `dsuber_le0`, `dsube_ge0`, `lte_dadd`, `lee_daddl`, `lee_daddr`, + `gee_daddl`, `gee_daddr`, `lte_daddl`, `lte_daddr`, `gte_dsubl`, + `gte_dsubr`, `lte_dadd2lE`, `lee_dadd2l`, `lee_dadd2lE`, + `lee_dadd2r`, `lee_dadd`, `lte_le_dadd`, `lee_dsub`, + `lte_le_dsub`, `lee_dsum`, `lee_dsum_nneg_subset`, + `lee_dsum_npos_subset`, `lee_dsum_nneg`, `lee_dsum_npos`, + `lee_dsum_nneg_ord`, `lee_dsum_npos_ord`, `lee_dsum_nneg_natr`, + `lee_dsum_npos_natr`, `lee_dsum_nneg_natl`, `lee_dsum_npos_natl`, + `lee_dsum_nneg_subfset`, `lee_dsum_npos_subfset`, + `lte_dsubl_addr`, `lte_dsubl_addl`, `lte_dsubr_addr`, + `lee_dsubr_addr`, `lee_dsubl_addr`, `ge0_dsume_distrl`, `dmulrEDr`, + `dmulrEDl`, `dge0_mulreDr`, `dge0_mulreDl`, `dle0_mulreDr`, `dle0_mulreDl`, + `ge0_dsume_distrr`, `le0_dsume_distrl`, `le0_dsume_distrr`, + `lee_abs_dadd`, `lee_abs_dsum`, `lee_abs_dsub`, `dadde_minl`, `dadde_minr`, + `lee_dadde`, `lte_spdaddr` - in `normedtype.v`: + lemma `mule_continuous` - in `cardinality.v`: diff --git a/theories/ereal.v b/theories/ereal.v index dd4c78829..c911a9e10 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -19,7 +19,11 @@ Require Import boolp classical_sets reals posnum topology. (* is equipped with a Canonical orderType. *) (* *) (* r%:E == injects real numbers into \bar R *) -(* +%E, -%E == addition/opposite for extended reals *) +(* +%E, -%E, *%E == addition/opposite/multiplication for extended *) +(* reals *) +(* +%dE == dual addition for extended reals *) +(* (-oo + +oo = +oo instead of -oo) *) +(* Import DualAddTheory for related lemmas *) (* x +? y == the addition of the extended real numbers x and *) (* and y is defined, i.e., it is neither +oo - oo *) (* nor -oo + oo *) @@ -91,6 +95,7 @@ Proof. by rewrite (big_nat_widenl _ 0)// big_mkord. Qed. Reserved Notation "'\bar' x" (at level 2, format "'\bar' x"). +Declare Scope ereal_dual_scope. Declare Scope ereal_scope. Import Order.TTheory GRing.Theory Num.Theory. @@ -98,17 +103,23 @@ Import numFieldTopology.Exports. Local Open Scope ring_scope. -Inductive extended (R : Type) := EFin of R | EPInf | ENInf. +Variant extended (R : Type) := EFin of R | EPInf | ENInf. Arguments EFin {R}. +Definition dual_extended := extended. + +Notation "+oo" := (@EPInf _ : dual_extended _) : ereal_dual_scope. Notation "+oo" := (@EPInf _) : ereal_scope. +Notation "-oo" := (@ENInf _ : dual_extended _) : ereal_dual_scope. Notation "-oo" := (@ENInf _) : ereal_scope. Notation "r %:E" := (@EFin _ r%R). Notation "'\bar' R" := (extended R) : type_scope. Notation "0" := (0%R%:E) : ereal_scope. Notation "1" := (1%R%:E) : ereal_scope. +Bind Scope ereal_dual_scope with dual_extended. Bind Scope ereal_scope with extended. +Delimit Scope ereal_dual_scope with dE. Delimit Scope ereal_scope with E. Local Open Scope ereal_scope. @@ -181,7 +192,7 @@ Variable (R : countType). Definition ereal_countMixin := PcanCountMixin (@codeK R). Canonical ereal_countType := CountType (extended R) ereal_countMixin. - End ERealCount. +End ERealCount. Section ERealOrder. Context {R : numDomainType}. @@ -246,23 +257,36 @@ Notation gte := (@Order.gt ereal_display _) (only parsing). Notation "@ 'gte' R" := (@Order.gt ereal_display R) (at level 10, R at level 8, only parsing). +Notation "x <= y" := (lee x y) (only printing) : ereal_dual_scope. Notation "x <= y" := (lee x y) (only printing) : ereal_scope. +Notation "x < y" := (lte x y) (only printing) : ereal_dual_scope. Notation "x < y" := (lte x y) (only printing) : ereal_scope. +Notation "x <= y <= z" := ((lee x y) && (lee y z)) (only printing) : ereal_dual_scope. Notation "x <= y <= z" := ((lee x y) && (lee y z)) (only printing) : ereal_scope. +Notation "x < y <= z" := ((lte x y) && (lee y z)) (only printing) : ereal_dual_scope. Notation "x < y <= z" := ((lte x y) && (lee y z)) (only printing) : ereal_scope. +Notation "x <= y < z" := ((lee x y) && (lte y z)) (only printing) : ereal_dual_scope. Notation "x <= y < z" := ((lee x y) && (lte y z)) (only printing) : ereal_scope. +Notation "x < y < z" := ((lte x y) && (lte y z)) (only printing) : ereal_dual_scope. Notation "x < y < z" := ((lte x y) && (lte y z)) (only printing) : ereal_scope. +Notation "x <= y" := (lee (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope. Notation "x <= y" := (lee (x : extended _) (y : extended _)) : ereal_scope. +Notation "x < y" := (lte (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope. Notation "x < y" := (lte (x : extended _) (y : extended _)) : ereal_scope. +Notation "x >= y" := (y <= x) (only parsing) : ereal_dual_scope. Notation "x >= y" := (y <= x) (only parsing) : ereal_scope. -Notation "x > y" := (y < x) (only parsing) : ereal_scope. +Notation "x > y" := (y < x) (only parsing) : ereal_dual_scope. Notation "x > y" := (y < x) (only parsing) : ereal_scope. +Notation "x <= y <= z" := ((x <= y) && (y <= z)) : ereal_dual_scope. Notation "x <= y <= z" := ((x <= y) && (y <= z)) : ereal_scope. +Notation "x < y <= z" := ((x < y) && (y <= z)) : ereal_dual_scope. Notation "x < y <= z" := ((x < y) && (y <= z)) : ereal_scope. +Notation "x <= y < z" := ((x <= y) && (y < z)) : ereal_dual_scope. Notation "x <= y < z" := ((x <= y) && (y < z)) : ereal_scope. +Notation "x < y < z" := ((x < y) && (y < z)) : ereal_dual_scope. Notation "x < y < z" := ((x < y) && (y < z)) : ereal_scope. Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E) = (x <= y)%R. @@ -334,6 +358,17 @@ Definition adde_subdef x y := Definition adde := nosimpl adde_subdef. +Definition dual_adde_subdef x y := + match x, y with + | x%:E , y%:E => (x + y)%R%:E + | +oo, _ => +oo + | _ , +oo => +oo + | -oo, _ => -oo + | _ , -oo => -oo + end. + +Definition dual_adde := nosimpl dual_adde_subdef. + Definition oppe x := match x with | r%:E => (- r)%:E @@ -354,40 +389,71 @@ Definition abse x := if x is r%:E then `|r|%:E else +oo. End ERealArith. +Notation "+%dE" := dual_adde. Notation "+%E" := adde. Notation "-%E" := oppe. +Notation "x + y" := (dual_adde x%dE y%dE) : ereal_dual_scope. Notation "x + y" := (adde x y) : ereal_scope. +Notation "x - y" := (dual_adde x%dE (oppe y%dE)) : ereal_dual_scope. Notation "x - y" := (adde x (oppe y)) : ereal_scope. +Notation "- x" := (oppe (x%dE : dual_extended _)) : ereal_dual_scope. Notation "- x" := (oppe x) : ereal_scope. Notation "*%E" := mule. +Notation "x * y" := (mule (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope. Notation "x * y" := (mule x y) : ereal_scope. +Notation "`| x |" := (abse (x%dE : dual_extended _)) : ereal_dual_scope. Notation "`| x |" := (abse x) : ereal_scope. Arguments abse {R}. +Notation "f \+ g" := (fun x => f x + g x)%dE : ereal_dual_scope. Notation "f \+ g" := (fun x => f x + g x)%E : ereal_scope. +Notation "\sum_ ( i <- r | P ) F" := + (\big[+%dE/0%:E]_(i <- r | P%B) F%dE) : ereal_dual_scope. Notation "\sum_ ( i <- r | P ) F" := (\big[+%E/0%:E]_(i <- r | P%B) F%E) : ereal_scope. +Notation "\sum_ ( i <- r ) F" := + (\big[+%dE/0%:E]_(i <- r) F%dE) : ereal_dual_scope. Notation "\sum_ ( i <- r ) F" := (\big[+%E/0%:E]_(i <- r) F%E) : ereal_scope. +Notation "\sum_ ( m <= i < n | P ) F" := + (\big[+%dE/0%:E]_(m <= i < n | P%B) F%dE) : ereal_dual_scope. Notation "\sum_ ( m <= i < n | P ) F" := (\big[+%E/0%:E]_(m <= i < n | P%B) F%E) : ereal_scope. +Notation "\sum_ ( m <= i < n ) F" := + (\big[+%dE/0%:E]_(m <= i < n) F%dE) : ereal_dual_scope. Notation "\sum_ ( m <= i < n ) F" := (\big[+%E/0%:E]_(m <= i < n) F%E) : ereal_scope. +Notation "\sum_ ( i | P ) F" := + (\big[+%dE/0%:E]_(i | P%B) F%dE) : ereal_dual_scope. Notation "\sum_ ( i | P ) F" := (\big[+%E/0%:E]_(i | P%B) F%E) : ereal_scope. +Notation "\sum_ i F" := + (\big[+%dE/0%:E]_i F%dE) : ereal_dual_scope. Notation "\sum_ i F" := (\big[+%E/0%:E]_i F%E) : ereal_scope. +Notation "\sum_ ( i : t | P ) F" := + (\big[+%dE/0%:E]_(i : t | P%B) F%dE) (only parsing) : ereal_dual_scope. Notation "\sum_ ( i : t | P ) F" := (\big[+%E/0%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope. +Notation "\sum_ ( i : t ) F" := + (\big[+%dE/0%:E]_(i : t) F%dE) (only parsing) : ereal_dual_scope. Notation "\sum_ ( i : t ) F" := (\big[+%E/0%:E]_(i : t) F%E) (only parsing) : ereal_scope. +Notation "\sum_ ( i < n | P ) F" := + (\big[+%dE/0%:E]_(i < n | P%B) F%dE) : ereal_dual_scope. Notation "\sum_ ( i < n | P ) F" := (\big[+%E/0%:E]_(i < n | P%B) F%E) : ereal_scope. +Notation "\sum_ ( i < n ) F" := + (\big[+%dE/0%:E]_(i < n) F%dE) : ereal_dual_scope. Notation "\sum_ ( i < n ) F" := (\big[+%E/0%:E]_(i < n) F%E) : ereal_scope. +Notation "\sum_ ( i 'in' A | P ) F" := + (\big[+%dE/0%:E]_(i in A | P%B) F%dE) : ereal_dual_scope. Notation "\sum_ ( i 'in' A | P ) F" := (\big[+%E/0%:E]_(i in A | P%B) F%E) : ereal_scope. +Notation "\sum_ ( i 'in' A ) F" := + (\big[+%dE/0%:E]_(i in A) F%dE) : ereal_dual_scope. Notation "\sum_ ( i 'in' A ) F" := (\big[+%E/0%:E]_(i in A) F%E) : ereal_scope. @@ -461,6 +527,9 @@ Local Notation "x +? y" := (adde_def x y). Lemma adde_defC x y : x +? y = y +? x. Proof. by rewrite /adde_def andbC (andbC (x == -oo)) (andbC (x == +oo)). Qed. +Lemma adde_defNN x y : - x +? - y = x +? y. +Proof. by move: x y => [x| |] [y| |]. Qed. + Lemma ge0_adde_def : {in [pred x | x >= 0] &, forall x y, x +? y}. Proof. by move=> [x| |] [y| |]. Qed. @@ -645,16 +714,31 @@ Qed. Lemma adde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y. Proof. by move: x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed. +Lemma adde_le0 x y : x <= 0 -> y <= 0 -> x + y <= 0. +Proof. +move: x y => [r0||] [r1||]// ? ?; rewrite !lee_fin -(addr0 0%R); exact: ler_add. +Qed. + Lemma oppe_gt0 x : (0 < - x) = (x < 0). Proof. move: x => [x||] //; exact: oppr_gt0. Qed. Lemma oppe_lt0 x : (- x < 0) = (0 < x). Proof. move: x => [x||] //; exact: oppr_lt0. Qed. +Lemma oppe_ge0 x : (0 <= - x) = (x <= 0). +Proof. move: x => [x||] //; exact: oppr_ge0. Qed. + +Lemma oppe_le0 x : (- x <= 0) = (0 <= x). +Proof. move: x => [x||] //; exact: oppr_le0. Qed. + Lemma sume_ge0 T (f : T -> \bar R) (P : pred T) : (forall t, P t -> 0 <= f t) -> forall l, 0 <= \sum_(i <- l | P i) f i. Proof. by move=> f0 l; elim/big_rec : _ => // t x Pt; apply/adde_ge0/f0. Qed. +Lemma sume_le0 T (f : T -> \bar R) (P : pred T) : + (forall t, P t -> f t <= 0) -> forall l, \sum_(i <- l | P i) f i <= 0. +Proof. by move=> f0 l; elim/big_rec : _ => // t x Pt; apply/adde_le0/f0. Qed. + Lemma mule_ninfty_pinfty : -oo * +oo = -oo :> \bar R. Proof. by rewrite /mule /= lte_0_pinfty. Qed. @@ -713,6 +797,7 @@ Lemma mule_ge0_le0 x y : 0 <= x -> y <= 0 -> x * y <= 0. Proof. by move=> x0 y0; rewrite muleC mule_le0_ge0. Qed. End ERealArithTh_numDomainType. +Notation "x +? y" := (adde_def x%dE y%dE) : ereal_dual_scope. Notation "x +? y" := (adde_def x y) : ereal_scope. Notation maxe := (@Order.max ereal_display _). @@ -723,6 +808,169 @@ Notation mine := (@Order.min ereal_display _). Notation "@ 'mine' R" := (@Order.min ereal_display R) (at level 10, R at level 8, only parsing) : fun_scope. +Module DualAddTheoryNumDomain. + +Section DualERealArithTh_numDomainType. + +Local Open Scope ereal_dual_scope. + +Context {R : numDomainType}. + +Implicit Types x y z : \bar R. + +Lemma dual_addeE x y : (x + y)%dE = - ((- x) + (- y))%E. +Proof. by case: x => [x| |]; case: y => [y| |] //=; rewrite opprD !opprK. Qed. + +Lemma dual_sumeE I (r : seq I) (P : pred I) (F : I -> \bar R) : + (\sum_(i <- r | P i) F i)%dE = - (\sum_(i <- r | P i) (- F i)%E)%E. +Proof. +apply: (big_ind2 (fun x y => x = - y)%E) => [|_ x _ y -> ->|i _]. +- by rewrite oppe0. +- by rewrite dual_addeE !oppeK. +- by rewrite oppeK. +Qed. + +Lemma dual_addeE_def x y : x +? y -> (x + y)%dE = (x + y)%E. +Proof. by case: x => [x| |]; case: y. Qed. + +Lemma daddEFin (r r' : R) : (r + r')%R%:E = r%:E + r'%:E. +Proof. by []. Qed. + +Lemma dsumEFin I r P (F : I -> R) : + \sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%R%:E. +Proof. by rewrite dual_sumeE sumEFin sumrN NEFin oppeK. Qed. + +Lemma dsubEFin (r r' : R) : (r - r')%R%:E = r%:E - r'%:E. +Proof. by []. Qed. + +Lemma daddeC : commutative (S := \bar R) +%dE. +Proof. by move=> x y; rewrite !dual_addeE addeC. Qed. + +Lemma dadde0 : right_id (0 : \bar R) +%dE. +Proof. by move=> x; rewrite dual_addeE eqe_oppLRP oppe0 adde0. Qed. + +Lemma dadd0e : left_id (0 : \bar R) +%dE. +Proof. by move=> x;rewrite dual_addeE eqe_oppLRP oppe0 add0e. Qed. + +Lemma daddeA : associative (S := \bar R) +%dE. +Proof. by move=> x y z; rewrite !dual_addeE !oppeK addeA. Qed. + +Canonical dadde_monoid := Monoid.Law daddeA dadd0e dadde0. +Canonical dadde_comoid := Monoid.ComLaw daddeC. + +Lemma daddeAC : right_commutative (S := \bar R) +%dE. +Proof. by move=> x y z; rewrite !dual_addeE !oppeK addeAC. Qed. + +Lemma daddeCA : left_commutative (S := \bar R) +%dE. +Proof. by move=> x y z; rewrite !dual_addeE !oppeK addeCA. Qed. + +Lemma daddeACA : @interchange (\bar R) +%dE +%dE. +Proof. by move=> x y z u; rewrite !dual_addeE !oppeK addeACA. Qed. + +Lemma doppeD x y : y \is a fin_num -> - (x + y) = - x - y. +Proof. by move: y => [y| |] _ //; rewrite !dual_addeE !oppeK oppeD. Qed. + +Lemma dsube0 x : x - 0 = x. +Proof. by move: x => [x| |] //; rewrite -dsubEFin subr0. Qed. + +Lemma dsub0e x : 0 - x = - x. +Proof. by move: x => [x| |] //; rewrite -dsubEFin sub0r. Qed. + +Lemma dfin_numD x y : + (x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num). +Proof. by move: x y => [x| |] [y| |]. Qed. + +Lemma dreal_of_extendedD : + {in (@fin_num R) &, {morph real_of_extended : x y / x + y >-> (x + y)%R}}. +Proof. by move=> [r| |] [s| |]. Qed. + +Lemma daddeK x y : x \is a fin_num -> y + x - x = y. +Proof. by move=> fx; rewrite !dual_addeE oppeK addeK ?oppeK; case: x fx. Qed. + +Lemma dsubeK x y : y \is a fin_num -> x - y + y = x. +Proof. by move=> fy; rewrite !dual_addeE oppeK subeK ?oppeK; case: y fy. Qed. + +Lemma dsubee x : x \is a fin_num -> x - x = 0. +Proof. by move=> fx; rewrite dual_addeE subee ?oppe0; case: x fx. Qed. + +Lemma dsube_eq x y z : x \is a fin_num -> (y +? z) -> + (x - z == y) = (x == y + z). +Proof. +by move: x y z => [x| |] [y| |] [z| |] // _ _; rewrite !eqe subr_eq. +Qed. + +Lemma dadde_eq_pinfty x y : (x + y == +oo) = ((x == +oo) || (y == +oo)). +Proof. by move: x y => [?| |] [?| |]. Qed. + +Lemma daddooe x : x != +oo -> -oo + x = -oo. +Proof. by case: x. Qed. + +Lemma dadde_Neq_pinfty x y : x != -oo -> y != -oo -> + (x + y != +oo) = (x != +oo) && (y != +oo). +Proof. by move: x y => [x| |] [y| |]. Qed. + +Lemma dadde_Neq_ninfty x y : x != +oo -> y != +oo -> + (x + y != -oo) = (x != -oo) && (y != -oo). +Proof. by move: x y => [x| |] [y| |]. Qed. + +Lemma desum_fset_pinfty + (T : choiceType) (s : {fset T}) (P : pred T) (f : T -> \bar R) : + \sum_(i <- s | P i) f i = +oo <-> exists i, [/\ i \in s, P i & f i = +oo]. +Proof. +rewrite dual_sumeE eqe_oppLRP /= esum_fset_ninfty. +by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP. +Qed. + +Lemma desum_pinfty n (f : 'I_n -> \bar R) : + (\sum_(i < n) f i == +oo) = [exists i, f i == +oo]. +Proof. +rewrite dual_sumeE eqe_oppLR esum_ninfty. +by under eq_existsb => i do rewrite eqe_oppLR. +Qed. + +Lemma desum_fset_ninfty + (T : choiceType) (s : {fset T}) (P : pred T) (f : T -> \bar R) : + (forall i, P i -> f i != +oo) -> + \sum_(i <- s | P i) f i = -oo <-> exists i, [/\ i \in s, P i & f i = -oo]. +Proof. +move=> fioo. +rewrite dual_sumeE eqe_oppLRP /= esum_fset_pinfty => [|i Pi]; last first. + by rewrite eqe_oppLR fioo. +by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP. +Qed. + +Lemma desum_ninfty n (f : 'I_n -> \bar R) : (forall i, f i != +oo) -> + (\sum_(i < n) f i == -oo) = [exists i, f i == -oo]. +Proof. +move=> finoo. +rewrite dual_sumeE eqe_oppLR /= esum_pinfty => [|i]; rewrite ?eqe_oppLR //. +by under eq_existsb => i do rewrite eqe_oppLR. +Qed. + +Lemma dadde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y. +Proof. rewrite dual_addeE oppe_ge0 -!oppe_le0; exact: adde_le0. Qed. + +Lemma dadde_le0 x y : x <= 0 -> y <= 0 -> x + y <= 0. +Proof. rewrite dual_addeE oppe_le0 -!oppe_ge0; exact: adde_ge0. Qed. + +Lemma dsume_ge0 T (f : T -> \bar R) (P : pred T) : + (forall n, P n -> 0 <= f n) -> forall l, 0 <= \sum_(i <- l | P i) f i. +Proof. +move=> u0 l; rewrite dual_sumeE oppe_ge0 sume_le0 // => t Pt. +rewrite oppe_le0; exact: u0. +Qed. + +Lemma dsume_le0 T (f : T -> \bar R) (P : pred T) : + (forall n, P n -> f n <= 0) -> forall l, \sum_(i <- l | P i) f i <= 0. +Proof. +move=> u0 l; rewrite dual_sumeE oppe_le0 sume_ge0 // => t Pt. +rewrite oppe_ge0; exact: u0. +Qed. + +End DualERealArithTh_numDomainType. + +End DualAddTheoryNumDomain. + Section ERealArithTh_realDomainType. Context {R : realDomainType}. Implicit Types (x y z u a b : \bar R) (r : R). @@ -817,6 +1065,9 @@ Proof. by rewrite muleC mulrninfty. Qed. Definition mulrinfty := (mulrpinfty, mulpinftyr, mulrninfty, mulninftyr). +Lemma lte_opp x y : (- x < - y) = (y < x). +Proof. by rewrite lte_oppl oppeK. Qed. + Lemma lte_add a b x y : a < b -> x < y -> a + x < b + y. Proof. move: a b x y=> [a| |] [b| |] [x| |] [y| |]; rewrite ?(lte_pinfty,lte_ninfty)//. @@ -832,12 +1083,33 @@ Qed. Lemma lee_addr x y : 0 <= y -> x <= y + x. Proof. by rewrite addeC; exact: lee_addl. Qed. +Lemma gee_addl x y : y <= 0 -> x + y <= x. +Proof. +move: x y => -[ x [y| |]//= | [| |]// | [| | ]//]; + by [rewrite !lee_fin ger_addl | move=> _; exact: lee_ninfty]. +Qed. + +Lemma gee_addr x y : y <= 0 -> y + x <= x. +Proof. rewrite addeC; exact: gee_addl. Qed. + Lemma lte_addl y x : y \is a fin_num -> 0 < x -> y < y + x. Proof. by move: x y => [x| |] [y| |] _ //; rewrite ?lte_pinfty ?lte_ninfty // !lte_fin ltr_addl. Qed. +Lemma lte_addr y x : y \is a fin_num -> 0 < x -> y < x + y. +Proof. rewrite addeC; exact: lte_addl. Qed. + +Lemma gte_subl y x : y \is a fin_num -> 0 < x -> y - x < y. +Proof. +move: y x => [x| |] [y| |] _ //; rewrite addeC /= ?lte_ninfty //. +by rewrite !lte_fin gtr_addr ltr_oppl oppr0. +Qed. + +Lemma gte_subr y x : y \is a fin_num -> 0 < x -> - x + y < y. +Proof. rewrite addeC; exact: gte_subl. Qed. + Lemma lte_add2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b). Proof. move: a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(lte_pinfty, lte_ninfty) //. @@ -882,6 +1154,14 @@ move: x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; by rewrite !lee_fin; exact: ler_sub. Qed. +Lemma lte_le_sub z u x y : z \is a fin_num -> u \is a fin_num -> + x < z -> u <= y -> x - y < z - u. +Proof. +move: z u => [z| |] [u| |] _ _ //. +move: x y => [x| |] [y| |]; rewrite ?(lte_pinfty,lte_ninfty)//. +by rewrite !lte_fin => xltr tley; apply: ltr_le_add; rewrite // ler_oppl opprK. +Qed. + Lemma lte_pmul2r z : z \is a fin_num -> 0 < z -> {mono *%E^~ z : x y / x < y}. Proof. move: z => [z| |] _ // z0 [x| |] [y| |] //. @@ -919,6 +1199,14 @@ move=> QP PQf; rewrite big_mkcond [X in _ <= X]big_mkcond lee_sum// => i. by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP. Qed. +Lemma lee_sum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar R) : + {subset Q <= P} -> {in [predD P & Q], forall i, f i <= 0} -> + \sum_(i <- s | P i) f i <= \sum_(i <- s | Q i) f i. +Proof. +move=> QP PQf; rewrite big_mkcond [X in _ <= X]big_mkcond lee_sum// => i. +by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP. +Qed. + Lemma lee_sum_nneg (I : eqType) (s : seq I) (P Q : pred I) (f : I -> \bar R) : (forall i, P i -> ~~ Q i -> 0 <= f i) -> \sum_(i <- s | P i && Q i) f i <= \sum_(i <- s | P i) f i. @@ -927,6 +1215,14 @@ move=> PQf; rewrite [X in _ <= X](bigID Q) /= -[X in X <= _]adde0 lee_add //. by rewrite sume_ge0// => i /andP[]; exact: PQf. Qed. +Lemma lee_sum_npos (I : eqType) (s : seq I) (P Q : pred I) + (f : I -> \bar R) : (forall i, P i -> ~~ Q i -> f i <= 0) -> + \sum_(i <- s | P i) f i <= \sum_(i <- s | P i && Q i) f i. +Proof. +move=> PQf; rewrite [X in X <= _](bigID Q) /= -[X in _ <= X]adde0 lee_add //. +by rewrite sume_le0// => i /andP[]; exact: PQf. +Qed. + Lemma lee_sum_nneg_ord (f : nat -> \bar R) (P : pred nat) : (forall n, P n -> 0 <= f n) -> {homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}. @@ -935,6 +1231,14 @@ move=> f0 i j le_ij; rewrite (big_ord_widen_cond j) // big_mkcondr /=. by rewrite lee_sum // => k ?; case: ifP => // _; exact: f0. Qed. +Lemma lee_sum_npos_ord (f : nat -> \bar R) (P : pred nat) : + (forall n, P n -> f n <= 0)%E -> + {homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}. +Proof. +move=> f0 m n ?; rewrite [X in _ <= X](big_ord_widen_cond n) // big_mkcondr /=. +rewrite lee_sum // => i ?; case: ifP => // _; exact: f0. +Qed. + Lemma lee_sum_nneg_natr (f : nat -> \bar R) (P : pred nat) m : (forall n, (m <= n)%N -> P n -> 0 <= f n) -> {homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}. @@ -944,6 +1248,15 @@ apply: (@lee_sum_nneg_ord (fun k => f (k + m)%N) (fun k => P (k + m)%N)); by [move=> n /f0; apply; rewrite leq_addl | rewrite leq_sub2r]. Qed. +Lemma lee_sum_npos_natr (f : nat -> \bar R) (P : pred nat) m : + (forall n, (m <= n)%N -> P n -> f n <= 0) -> + {homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}. +Proof. +move=> f0 i j le_ij; rewrite -[m]add0n !big_addn !big_mkord. +apply: (@lee_sum_npos_ord (fun k => f (k + m)%N) (fun k => P (k + m)%N)); + by [move=> n /f0; apply; rewrite leq_addl | rewrite leq_sub2r]. +Qed. + Lemma lee_sum_nneg_natl (f : nat -> \bar R) (P : pred nat) n : (forall m, (m < n)%N -> P m -> 0 <= f m) -> {homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}. @@ -953,6 +1266,15 @@ rewrite lee_sum_nneg_subset// => [k | k /and3P[_ /f0->//]]. by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->]. Qed. +Lemma lee_sum_npos_natl (f : nat -> \bar R) (P : pred nat) n : + (forall m, (m < n)%N -> P m -> f m <= 0) -> + {homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}. +Proof. +move=> f0 i j le_ij; rewrite !big_geq_mkord/=. +rewrite lee_sum_npos_subset// => [k | k /and3P[_ /f0->//]]. +by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->]. +Qed. + Lemma lee_sum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T) (f : T -> \bar R) : {subset A <= B} -> {in [predD B & A], forall t, P t -> 0 <= f t} -> @@ -966,6 +1288,19 @@ rewrite big_fset /= big_seq_cond sume_ge0 // => t /andP[tB tA]. by case: ifPn => // Pt; rewrite f0 // !inE tA. Qed. +Lemma lee_sum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T) + (f : T -> \bar R) : {subset A <= B} -> + {in [predD B & A], forall t, P t -> f t <= 0} -> + \sum_(t <- B | P t) f t <= \sum_(t <- A | P t) f t. +Proof. +move=> AB f0; rewrite big_mkcond (big_fsetID _ (mem A) B) /=. +rewrite -[X in _ <= X]adde0 lee_add //. + rewrite -big_mkcond /= {3}(_ : A = [fset x in B | x \in A]%fset) //. + by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB. +rewrite big_fset /= big_seq_cond sume_le0 // => t /andP[tB tA]. +by case: ifPn => // Pt; rewrite f0 // !inE tA. +Qed. + Lemma lte_subl_addr x y z : y \is a fin_num -> (x - y < z) = (x < z + y). Proof. move: x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?lte_pinfty ?lte_ninfty //. @@ -1168,6 +1503,33 @@ Qed. Lemma ge0_muleDr x y z : 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z. Proof. by move=> y0 z0; rewrite !(muleC x) ge0_muleDl. Qed. +Lemma le0_muleDl x y z : y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x. +Proof. +rewrite /mule/=; move: x y z => [r| |] [s| |] [t| |] //= s0 t0. +- by rewrite mulrDl. +- by case: ltgtP => // -[] <-; rewrite mulr0 adde0. +- by case: ltgtP => // -[] <-; rewrite mulr0 adde0. +- by case: ltgtP => //; rewrite adde0. +- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin. + case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e. + + rewrite !lte_fin -[in LHS](addr0 0%R) ltNge ler_add // ?ltW //=. + by rewrite !ltNge ltW //. + + by case: (ltgtP t). +- by rewrite lte_pinfty; case: ltgtP s0. +- by rewrite lte_pinfty; case: ltgtP t0. +- by rewrite lte_pinfty. +- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin. + case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e. + + rewrite !lte_fin -[in LHS](addr0 0%R) ltNge ler_add // ?ltW //=. + by rewrite !ltNge ltW // -lee_fin t0; case: eqP. + + by case: (ltgtP t). +- by rewrite ltNge s0 /=; case: eqP. +- by rewrite ltNge t0 /=; case: eqP. +Qed. + +Lemma le0_muleDr x y z : y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z. +Proof. by move=> y0 z0; rewrite !(muleC x) le0_muleDl. Qed. + Lemma gee_pmull y x : y \is a fin_num -> 0 < x -> y <= 1 -> y * x <= x. Proof. move: x y => [x| |] [y| |] _ //=. @@ -1213,6 +1575,25 @@ Proof. by move=> F0; rewrite muleC ge0_sume_distrl//; under eq_bigr do rewrite muleC. Qed. +Lemma le0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : + (forall i, P i -> F i <= 0) -> + (\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x). +Proof. +elim: s x P F => [x P F F0|h t ih x P F F0]; first by rewrite 2!big_nil mul0e. +rewrite big_cons; case: ifPn => Ph; last by rewrite big_cons (negbTE Ph) ih. +by rewrite le0_muleDl ?sume_le0// ?F0// ih// big_cons Ph. +Qed. + +Lemma le0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : + (forall i, P i -> F i <= 0) -> + x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i). +Proof. +by move=> F0; rewrite muleC le0_sume_distrl//; under eq_bigr do rewrite muleC. +Qed. + +Lemma lee_opp x y : (- x <= - y) = (y <= x). +Proof. by rewrite lee_oppl oppeK. Qed. + Lemma lee_abs x : x <= `|x|. Proof. by move: x => [x| |]//=; rewrite lee_fin ler_norm. Qed. @@ -1283,6 +1664,12 @@ by have [ab|ba] := leP r1 r2; [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW]. Qed. +Lemma minEFin r1 r2 : mine r1%:E r2%:E = (Num.min r1 r2)%:E. +Proof. +by have [ab|ba] := leP r1 r2; + [apply/min_idPl; rewrite lee_fin|apply/min_idPr; rewrite lee_fin ltW]. +Qed. + Lemma adde_maxl : left_distributive (@adde R) maxe. Proof. move=> x y z; have [xy|yx] := leP x y. @@ -1309,6 +1696,31 @@ Proof. by move=> x; have [//|] := leP -oo x; rewrite ltNge lee_ninfty. Qed. Lemma maxe_ninftyr : right_id (-oo : \bar R) maxe. Proof. by move=> x; rewrite maxC maxe_ninftyl. Qed. +Lemma mine_ninftyl : left_zero (-oo : \bar R) mine. +Proof. by move=> x; have [|//] := leP x -oo; rewrite lee_ninfty_eq => /eqP. Qed. + +Lemma mine_ninftyr : right_zero (-oo : \bar R) mine. +Proof. by move=> x; rewrite minC mine_ninftyl. Qed. + +Lemma mine_pinftyl : left_id (+oo : \bar R) mine. +Proof. by move=> x; have [//|] := leP x +oo; rewrite ltNge lee_pinfty. Qed. + +Lemma mine_pinftyr : right_id (+oo : \bar R) mine. +Proof. by move=> x; rewrite minC mine_pinftyl. Qed. + +Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}. +Proof. +move=> [x| |] [y| |] //=. +- by rewrite maxEFin minEFin -NEFin oppr_max. +- by rewrite maxe_pinftyr mine_ninftyr. +- by rewrite mine_pinftyr. +- by rewrite mine_ninftyl. +- by rewrite maxe_ninftyl mine_pinftyl. +Qed. + +Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}. +Proof. by move=> x y; rewrite -[RHS]oppeK oppe_max !oppeK. Qed. + Lemma maxeMr z x y : z \is a fin_num -> 0 < z -> z * maxe x y = maxe (z * x) (z * y). Proof. @@ -1321,10 +1733,327 @@ Lemma maxeMl z x y : z \is a fin_num -> 0 < z -> maxe x y * z = maxe (x * z) (y * z). Proof. by move=> zfin z0; rewrite muleC maxeMr// !(muleC z). Qed. +Lemma mineMr z x y : z \is a fin_num -> 0 < z -> + z * mine x y = mine (z * x) (z * y). +Proof. +by move=> ? ?; rewrite -eqe_oppP -muleN oppe_min maxeMr// !muleN -oppe_min. +Qed. + +Lemma mineMl z x y : z \is a fin_num -> 0 < z -> + mine x y * z = mine (x * z) (y * z). +Proof. by move=> zfin z0; rewrite muleC mineMr// !(muleC z). Qed. + End ERealArithTh_realDomainType. Arguments lee_sum_nneg_ord {R}. +Arguments lee_sum_npos_ord {R}. Arguments lee_sum_nneg_natr {R}. +Arguments lee_sum_npos_natr {R}. Arguments lee_sum_nneg_natl {R}. +Arguments lee_sum_npos_natl {R}. + +Module DualAddTheoryRealDomain. + +Section DualERealArithTh_realDomainType. + +Import DualAddTheoryNumDomain. + +Local Open Scope ereal_dual_scope. + +Context {R : realDomainType}. +Implicit Types x y z a b : \bar R. + +Lemma dsube_lt0 x y : (x - y < 0) = (x < y). +Proof. by rewrite dual_addeE oppe_lt0 sube_gt0 lte_opp. Qed. + +Lemma dsube_ge0 x y : (0 <= y - x) = (x <= y). +Proof. by rewrite dual_addeE oppe_ge0 sube_le0 lee_opp. Qed. + +Lemma dsuber_le0 x y : y \is a fin_num -> (x - y <= 0) = (x <= y). +Proof. +by move=> ?; rewrite dual_addeE oppe_le0 suber_ge0 ?fin_numN// lee_opp. +Qed. + +Lemma dsubre_le0 y x : y \is a fin_num -> (y - x <= 0) = (y <= x). +Proof. +by move=> ?; rewrite dual_addeE oppe_le0 subre_ge0 ?fin_numN// lee_opp. +Qed. + +Lemma lte_dadd a b x y : a < b -> x < y -> a + x < b + y. +Proof. rewrite !dual_addeE lte_opp -lte_opp -(lte_opp y); exact: lte_add. Qed. + +Lemma lee_daddl x y : 0 <= y -> x <= x + y. +Proof. rewrite dual_addeE lee_oppr -oppe_le0; exact: gee_addl. Qed. + +Lemma lee_daddr x y : 0 <= y -> x <= y + x. +Proof. rewrite dual_addeE lee_oppr -oppe_le0; exact: gee_addr. Qed. + +Lemma gee_daddl x y : y <= 0 -> x + y <= x. +Proof. rewrite dual_addeE lee_oppl -oppe_ge0; exact: lee_addl. Qed. + +Lemma gee_daddr x y : y <= 0 -> y + x <= x. +Proof. rewrite dual_addeE lee_oppl -oppe_ge0; exact: lee_addr. Qed. + +Lemma lte_daddl y x : y \is a fin_num -> 0 < x -> y < y + x. +Proof. rewrite -fin_numN dual_addeE lte_oppr => ? ?; exact: gte_subl. Qed. + +Lemma lte_daddr y x : y \is a fin_num -> 0 < x -> y < x + y. +Proof. rewrite -fin_numN dual_addeE lte_oppr addeC; exact: gte_subl. Qed. + +Lemma gte_dsubl y x : y \is a fin_num -> 0 < x -> y - x < y. +Proof. rewrite -fin_numN dual_addeE lte_oppl oppeK; exact: lte_addl. Qed. + +Lemma gte_dsubr y x : y \is a fin_num -> 0 < x -> - x + y < y. +Proof. rewrite -fin_numN dual_addeE lte_oppl oppeK; exact: lte_addr. Qed. + +Lemma lte_dadd2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b). +Proof. +by move=> ?; rewrite !dual_addeE lte_opp lte_add2lE ?fin_numN// lte_opp. +Qed. + +Lemma lee_dadd2l x a b : a <= b -> x + a <= x + b. +Proof. rewrite !dual_addeE lee_opp -lee_opp; exact: lee_add2l. Qed. + +Lemma lee_dadd2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b). +Proof. +by move=> ?; rewrite !dual_addeE lee_opp lee_add2lE ?fin_numN// lee_opp. +Qed. + +Lemma lee_dadd2r x a b : a <= b -> a + x <= b + x. +Proof. rewrite !dual_addeE lee_opp -lee_opp; exact: lee_add2r. Qed. + +Lemma lee_dadd a b x y : a <= b -> x <= y -> a + x <= b + y. +Proof. rewrite !dual_addeE lee_opp -lee_opp -(lee_opp y); exact: lee_add. Qed. + +Lemma lte_le_dadd a b x y : a \is a fin_num -> b \is a fin_num -> + a < x -> b <= y -> a + b < x + y. +Proof. rewrite -fin_numN !dual_addeE lte_opp -lte_opp; exact: lte_le_sub. Qed. + +Lemma lee_dsub x y z t : x <= y -> t <= z -> x - z <= y - t. +Proof. rewrite !dual_addeE lee_oppl oppeK -lee_opp !oppeK; exact: lee_add. Qed. + +Lemma lte_le_dsub z u x y : z \is a fin_num -> u \is a fin_num -> + x < z -> u <= y -> x - y < z - u. +Proof. +rewrite -(fin_numN z) !dual_addeE lte_opp !oppeK -lte_opp; exact: lte_le_add. +Qed. + +Lemma lee_dsum I (f g : I -> \bar R) s (P : pred I) : + (forall i, P i -> f i <= g i) -> + \sum_(i <- s | P i) f i <= \sum_(i <- s | P i) g i. +Proof. +move=> Pfg; rewrite !dual_sumeE lee_opp. +apply: lee_sum => i Pi; rewrite lee_opp; exact: Pfg. +Qed. + +Lemma lee_dsum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar R) : + {subset Q <= P} -> {in [predD P & Q], forall i, 0 <= f i} -> + \sum_(i <- s | Q i) f i <= \sum_(i <- s | P i) f i. +Proof. +move=> QP PQf; rewrite !dual_sumeE lee_opp. +apply: lee_sum_npos_subset => [//|i iPQ]; rewrite oppe_le0; exact: PQf. +Qed. + +Lemma lee_dsum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar R) : + {subset Q <= P} -> {in [predD P & Q], forall i, f i <= 0} -> + \sum_(i <- s | P i) f i <= \sum_(i <- s | Q i) f i. +Proof. +move=> QP PQf; rewrite !dual_sumeE lee_opp. +apply: lee_sum_nneg_subset => [//|i iPQ]; rewrite oppe_ge0; exact: PQf. +Qed. + +Lemma lee_dsum_nneg (I : eqType) (s : seq I) (P Q : pred I) + (f : I -> \bar R) : (forall i, P i -> ~~ Q i -> 0 <= f i) -> + \sum_(i <- s | P i && Q i) f i <= \sum_(i <- s | P i) f i. +Proof. +move=> PQf; rewrite !dual_sumeE lee_opp. +apply: lee_sum_npos => i Pi nQi; rewrite oppe_le0; exact: PQf. +Qed. + +Lemma lee_dsum_npos (I : eqType) (s : seq I) (P Q : pred I) + (f : I -> \bar R) : (forall i, P i -> ~~ Q i -> f i <= 0) -> + \sum_(i <- s | P i) f i <= \sum_(i <- s | P i && Q i) f i. +Proof. +move=> PQf; rewrite !dual_sumeE lee_opp. +apply: lee_sum_nneg => i Pi nQi; rewrite oppe_ge0; exact: PQf. +Qed. + +Lemma lee_dsum_nneg_ord (f : nat -> \bar R) (P : pred nat) : + (forall n, P n -> 0 <= f n)%E -> + {homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}. +Proof. +move=> f0 m n mlen; rewrite !dual_sumeE lee_opp. +apply: (lee_sum_npos_ord (fun i => - f i)%E) => [i Pi|//]. +rewrite oppe_le0; exact: f0. +Qed. + +Lemma lee_dsum_npos_ord (f : nat -> \bar R) (P : pred nat) : + (forall n, P n -> f n <= 0)%E -> + {homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}. +Proof. +move=> f0 m n mlen; rewrite !dual_sumeE lee_opp. +apply: (lee_sum_nneg_ord (fun i => - f i)%E) => [i Pi|//]. +rewrite oppe_ge0; exact: f0. +Qed. + +Lemma lee_dsum_nneg_natr (f : nat -> \bar R) (P : pred nat) m : + (forall n, (m <= n)%N -> P n -> 0 <= f n) -> + {homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}. +Proof. +move=> f0 i j le_ij; rewrite !dual_sumeE lee_opp. +apply: lee_sum_npos_natr => [n ? ?|//]; rewrite oppe_le0; exact: f0. +Qed. + +Lemma lee_dsum_npos_natr (f : nat -> \bar R) (P : pred nat) m : + (forall n, (m <= n)%N -> P n -> f n <= 0) -> + {homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}. +Proof. +move=> f0 i j le_ij; rewrite !dual_sumeE lee_opp. +apply: lee_sum_nneg_natr => [n ? ?|//]; rewrite oppe_ge0; exact: f0. +Qed. + +Lemma lee_dsum_nneg_natl (f : nat -> \bar R) (P : pred nat) n : + (forall m, (m < n)%N -> P m -> 0 <= f m) -> + {homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}. +Proof. +move=> f0 i j le_ij; rewrite !dual_sumeE lee_opp. +apply: lee_sum_npos_natl => [m ? ?|//]; rewrite oppe_le0; exact: f0. +Qed. + +Lemma lee_dsum_npos_natl (f : nat -> \bar R) (P : pred nat) n : + (forall m, (m < n)%N -> P m -> f m <= 0) -> + {homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}. +Proof. +move=> f0 i j le_ij; rewrite !dual_sumeE lee_opp. +apply: lee_sum_nneg_natl => [m ? ?|//]; rewrite oppe_ge0; exact: f0. +Qed. + +Lemma lee_dsum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T) + (f : T -> \bar R) : {subset A <= B} -> + {in [predD B & A], forall t, P t -> 0 <= f t} -> + \sum_(t <- A | P t) f t <= \sum_(t <- B | P t) f t. +Proof. +move=> AB f0; rewrite !dual_sumeE lee_opp. +apply: lee_sum_npos_subfset => [//|? ? ?]; rewrite oppe_le0; exact: f0. +Qed. + +Lemma lee_dsum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T) + (f : T -> \bar R) : {subset A <= B} -> + {in [predD B & A], forall t, P t -> f t <= 0} -> + \sum_(t <- B | P t) f t <= \sum_(t <- A | P t) f t. +Proof. +move=> AB f0; rewrite !dual_sumeE lee_opp. +apply: lee_sum_nneg_subfset => [//|? ? ?]; rewrite oppe_ge0; exact: f0. +Qed. + +Lemma lte_dsubl_addr x y z : y \is a fin_num -> (x - y < z) = (x < z + y). +Proof. +by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr oppeK lte_subl_addr. +Qed. + +Lemma lte_dsubl_addl x y z : z \is a fin_num -> (x - y < z) = (x < y + z). +Proof. +move=> zfin. +by rewrite !dual_addeE lte_oppl lte_oppr lte_subr_addr ?fin_numN// addeC. +Qed. + +Lemma lte_dsubr_addr x y z : y \is a fin_num -> (x < y - z) = (x + z < y). +Proof. +move=> yfin. +by rewrite !dual_addeE lte_oppl lte_oppr lte_subl_addl ?fin_numN// addeC. +Qed. + +Lemma lee_dsubr_addr x y z : z \is a fin_num -> (x <= y - z) = (x + z <= y). +Proof. +by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subl_addr ?fin_numN. +Qed. + +Lemma lee_dsubl_addr x y z : y \is a fin_num -> (x - y <= z) = (x <= z + y). +Proof. +by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subr_addr ?fin_numN. +Qed. + +Lemma dmulrEDr x y z : x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z. +Proof. by move=> *; rewrite !dual_addeE muleN mulrEDr ?adde_defNN// !muleN. Qed. + +Lemma dmulrEDl x y z : x \is a fin_num -> y +? z -> (y + z) * x = y * x + z * x. +Proof. by move=> *; rewrite -!(muleC x) dmulrEDr. Qed. + +Lemma dge0_muleDl x y z : 0 <= y -> 0 <= z -> (y + z) * x = y * x + z * x. +Proof. by move=> *; rewrite !dual_addeE mulNe le0_muleDl ?oppe_le0 ?mulNe. Qed. + +Lemma dge0_muleDr x y z : 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z. +Proof. by move=> *; rewrite !dual_addeE muleN le0_muleDr ?oppe_le0 ?muleN. Qed. + +Lemma dle0_muleDl x y z : y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x. +Proof. by move=> *; rewrite !dual_addeE mulNe ge0_muleDl ?oppe_ge0 ?mulNe. Qed. + +Lemma dle0_muleDr x y z : y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z. +Proof. by move=> *; rewrite !dual_addeE muleN ge0_muleDr ?oppe_ge0 ?muleN. Qed. + +Lemma ge0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : + (forall i, P i -> 0 <= F i) -> + (\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x). +Proof. +move=> F0; rewrite !dual_sumeE !mulNe le0_sume_distrl => [|i Pi]. +- by under eq_bigr => i _ do rewrite mulNe. +- by rewrite oppe_le0 F0. +Qed. + +Lemma ge0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : + (forall i, P i -> 0 <= F i) -> + x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i). +Proof. +by move=> F0; rewrite muleC ge0_dsume_distrl//; under eq_bigr do rewrite muleC. +Qed. + +Lemma le0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : + (forall i, P i -> F i <= 0) -> + (\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x). +Proof. +move=> F0; rewrite !dual_sumeE mulNe ge0_sume_distrl => [|i Pi]. +- by under eq_bigr => i _ do rewrite mulNe. +- by rewrite oppe_ge0 F0. +Qed. + +Lemma le0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) : + (forall i, P i -> F i <= 0) -> + x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i). +Proof. +by move=> F0; rewrite muleC le0_dsume_distrl//; under eq_bigr do rewrite muleC. +Qed. + +Lemma lee_abs_dadd x y : `|x + y| <= `|x| + `|y|. +Proof. +by move: x y => [x| |] [y| |] //; rewrite /abse -daddEFin lee_fin ler_norm_add. +Qed. + +Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I -> \bar R) (P : pred I) : + `|\sum_(i <- s | P i) F i| <= \sum_(i <- s | P i) `|F i|. +Proof. +elim/big_ind2 : _ => //; first by rewrite abse0. +by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dadd _ _)). +Qed. + +Lemma lee_abs_dsub x y : `|x - y| <= `|x| + `|y|. +Proof. +by move: x y => [x| |] [y| |] //; rewrite /abse -daddEFin lee_fin ler_norm_sub. +Qed. + +Lemma dadde_minl : left_distributive (@dual_adde R) mine. +Proof. by move=> x y z; rewrite !dual_addeE oppe_min adde_maxl oppe_max. Qed. + +Lemma dadde_minr : right_distributive (@dual_adde R) mine. +Proof. by move=> x y z; rewrite !dual_addeE oppe_min adde_maxr oppe_max. Qed. + +End DualERealArithTh_realDomainType. +Arguments lee_dsum_nneg_ord {R}. +Arguments lee_dsum_npos_ord {R}. +Arguments lee_dsum_nneg_natr {R}. +Arguments lee_dsum_npos_natr {R}. +Arguments lee_dsum_nneg_natl {R}. +Arguments lee_dsum_npos_natl {R}. + +End DualAddTheoryRealDomain. Lemma lee_opp2 {R : realDomainType} : {mono @oppe R : x y /~ x <= y}. Proof. @@ -1482,6 +2211,32 @@ Proof. by move=> r0; rewrite muleC lee_ndivr_mull// muleC. Qed. End realFieldType_lemmas. +Module DualAddTheoryRealField. + +Section DualRealFieldType_lemmas. +Local Open Scope ereal_dual_scope. +Variable R : realFieldType. +Implicit Types x y : \bar R. + +Lemma lee_dadde x y : (forall e : {posnum R}, x <= y + e%:num%:E) -> x <= y. +Proof. by move=> xye; apply: lee_adde => e; case: x {xye} (xye e). Qed. + +Lemma lte_spdaddr (r : R) x y : 0 < y -> r%:E <= x -> r%:E < x + y. +Proof. +move: y x => [y| |] [x| |] //=; rewrite ?lte_fin ?ltt_fin ?lte_pinfty //. +exact: ltr_spaddr. +Qed. + +End DualRealFieldType_lemmas. + +End DualAddTheoryRealField. + +Module DualAddTheory. +Export DualAddTheoryNumDomain. +Export DualAddTheoryRealDomain. +Export DualAddTheoryRealField. +End DualAddTheory. + Section ereal_supremum. Variable R : realFieldType. Local Open Scope classical_set_scope.