Built with
Alectryon , running Coq+SerAPI v8.15.0+0.15.0. Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents. Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus. On Mac, use
⌘ instead of
Ctrl .
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
(* -------------------------------------------------------------------- *)
(* Copyright (c) - 2015--2016 - IMDEA Software Institute *)
(* Copyright (c) - 2015--2018 - Inria *)
(* Copyright (c) - 2016--2018 - Polytechnique *)
(* -------------------------------------------------------------------- *)
(* TODO: merge this with table.v in real-closed
(c.f. https://github.com/math-comp/real-closed/pull/29 ) and
incorporate it into mathcomp proper where it could then be used for
bounds of intervals*)
From mathcomp Require Import all_ssreflect all_algebra finmap.Notation "[ predI _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predU _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predD _ & _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ predC _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "[ preim _ of _ ]" was already used in scope
fun_scope. [notation-overridden,parsing]Notation "_ + _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ - _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ < _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ >= _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ > _" was already used in scope nat_scope.
[notation-overridden,parsing]Notation "_ <= _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ <= _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ <= _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ < _ < _" was already used in scope
nat_scope. [notation-overridden,parsing]Notation "_ * _" was already used in scope nat_scope.
[notation-overridden,parsing]New coercion path [GRing.subring_closedM;
GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedN] : GRing.subring_closed >-> GRing.oppr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedM] : GRing.subring_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.subring_closedM; GRing.smulr_closedM] : GRing.subring_closed >-> GRing.mulr_closed.
New coercion path [GRing.subring_closed_semi;
GRing.semiring_closedD] : GRing.subring_closed >-> GRing.addr_closed is ambiguous with existing
[GRing.subring_closedB; GRing.zmod_closedD] : GRing.subring_closed >-> GRing.addr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.sdivr_closed_div;
GRing.divr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed is ambiguous with existing
[GRing.sdivr_closedM; GRing.smulr_closedM] : GRing.sdivr_closed >-> GRing.mulr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.subalg_closedBM;
GRing.subring_closedB] : GRing.subalg_closed >-> GRing.zmod_closed is ambiguous with existing
[GRing.subalg_closedZ; GRing.submod_closedB] : GRing.subalg_closed >-> GRing.zmod_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.divring_closed_div;
GRing.sdivr_closedM] : GRing.divring_closed >-> GRing.smulr_closed is ambiguous with existing
[GRing.divring_closedBM; GRing.subring_closedM] : GRing.divring_closed >-> GRing.smulr_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.divalg_closedBdiv;
GRing.divring_closedBM] : GRing.divalg_closed >-> GRing.subring_closed is ambiguous with existing
[GRing.divalg_closedZ; GRing.subalg_closedBM] : GRing.divalg_closed >-> GRing.subring_closed.
[ambiguous-paths,typechecker] New coercion path [GRing.Pred.subring_smul;
GRing.Pred.smul_mul] : GRing.Pred.subring >-> GRing.Pred.mul is ambiguous with existing
[GRing.Pred.subring_semi; GRing.Pred.semiring_mul] : GRing.Pred.subring >-> GRing.Pred.mul.
[ambiguous-paths,typechecker]
From mathcomp.classical Require Import mathcomp_extra.Notation "_ \* _" was already used in scope
ring_scope. [notation-overridden,parsing]Notation "\- _" was already used in scope ring_scope.
[notation-overridden,parsing]
Require Import signed.
(******************************************************************************)
(* Extended real numbers *)
(* *)
(* Given a type R for numbers, \bar R is the type R extended with symbols -oo *)
(* and +oo (notation scope: %E), suitable to represent extended real numbers. *)
(* When R is a numDomainType, \bar R is equipped with a canonical porderType *)
(* and operations for addition/opposite. When R is a realDomainType, \bar R *)
(* is equipped with a Canonical orderType. *)
(* *)
(* Naming convention: in definition/lemma identifiers, "e" stands for an *)
(* extended number and "y" and "Ny" for +oo ad -oo respectively. *)
(* *)
(* \bar R == coproduct of R and {+oo, -oo}; *)
(* notation for extended (R:Type) *)
(* r%:E == injects real numbers into \bar R *)
(* +%E, -%E, *%E == addition/opposite/multiplication for extended *)
(* reals *)
(* `| x |%E == the absolute value of x *)
(* x ^+ n == iterated multiplication *)
(* x *+ n == iterated addition *)
(* +%dE, (x *+ n)%dE == dual addition/dual iterated 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 *)
(* x *? y == the multiplication of the extended real numbers *)
(* x and y is not of the form 0 * +oo or 0 * -oo *)
(* (_ <= _)%E, (_ < _)%E, == comparison relations for extended reals *)
(* (_ >= _)%E, (_ > _)%E *)
(* (\sum_(i in A) f i)%E == bigop-like notation in scope %E *)
(* maxe x y, mine x y == notation for the maximum/minimum of two *)
(* extended real numbers *)
(* *)
(* Signed extended real numbers: *)
(* {posnum \bar R} == interface type for elements in \bar R that are *)
(* positive, c.f., signed.v, notation in scope %E *)
(* {nonneg \bar R} == interface types for elements in \bar R that are *)
(* non-negative, c.f. signed.v, notation in scope %E *)
(* x%:pos == explicitly casts x to {posnum \bar R}, in scope %E *)
(* x%:nng == explicitly casts x to {nonneg \bar R}, in scope %E *)
(* *)
(* Topology of extended real numbers: *)
(* contract == order-preserving bijective function *)
(* from extended real numbers to [-1; 1] *)
(* expand == function from real numbers to extended *)
(* real numbers that cancels contract in *)
(* [-1; 1] *)
(* *)
(******************************************************************************)
Set Implicit Arguments .
Unset Strict Implicit .
Unset Printing Implicit Defensive .
Reserved Notation "x %:E" (at level 2 , format "x %:E" ).
Reserved Notation "x +? y" (at level 50 , format "x +? y" ).
Reserved Notation "x *? y" (at level 50 , format "x *? y" ).
Reserved Notation "'\bar' x" (at level 2 , format "'\bar' x" ).
Reserved Notation "{ 'posnum' '\bar' R }" (at level 0 ,
format "{ 'posnum' '\bar' R }" ).
Reserved Notation "{ 'nonneg' '\bar' R }" (at level 0 ,
format "{ 'nonneg' '\bar' R }" ).
Declare Scope ereal_dual_scope.
Declare Scope ereal_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Variant extended (R : Type ) := EFin of R | EPInf | ENInf.
Arguments EFin {R}.
Lemma EFin_inj T : injective (@EFin T).
Proof .3
by move => a b; case . Qed .
Definition dual_extended := extended.
(* Notations in ereal_dual_scope should be kept *before* the
corresponding notation in ereal_scope, otherwise when none of the
scope is open (lte x y) would be displayed as (x < y)%dE, instead
of (x < y)%E, for instance. *)
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 : dual_extended _) : ereal_dual_scope.
Notation "0" := (0 %R%:E) : ereal_scope.
Notation "1" := (1 %R%:E : dual_extended _) : ereal_dual_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.
Definition er_map T T' (f : T -> T') (x : \bar T) : \bar T' :=
match x with
| r%:E => (f r)%:E
| +oo => +oo
| -oo => -oo
end .
Definition fine {R : zmodType} x : R := if x is EFin v then v else 0 .
Section EqEReal .
Variable (R : eqType).
Definition eq_ereal (x y : \bar R) :=
match x, y with
| x%:E, y%:E => x == y
| +oo, +oo => true
| -oo, -oo => true
| _, _ => false
end .
Lemma ereal_eqP : Equality.axiom eq_ereal.R : eqType
Equality.axiom eq_ereal
Proof .a
by case => [?||][?||]; apply : (iffP idP) => //= [/eqP|[]] ->. Qed .
Definition ereal_eqMixin := Equality.Mixin ereal_eqP.
Canonical ereal_eqType := Equality.Pack ereal_eqMixin.
Lemma eqe (r1 r2 : R) : (r1%:E == r2%:E) = (r1 == r2).d r1, r2 : R
(r1%:E == r2%:E) = (r1 == r2)
Proof .11
by []. Qed .
End EqEReal .
Section ERealChoice .
Variable (R : choiceType).
Definition code (x : \bar R) :=
match x with
| r%:E => GenTree.Node 0 [:: GenTree.Leaf r]
| +oo => GenTree.Node 1 [::]
| -oo => GenTree.Node 2 [::]
end .
Definition decode (x : GenTree.tree R) : option (\bar R) :=
match x with
| GenTree.Node 0 [:: GenTree.Leaf r] => Some r%:E
| GenTree.Node 1 [::] => Some +oo
| GenTree.Node 2 [::] => Some -oo
| _ => None
end .
Lemma codeK : pcancel code decode.R : choiceType
pcancel code decode
Proof .18
by case . Qed .
Definition ereal_choiceMixin := PcanChoiceMixin codeK.
Canonical ereal_choiceType := ChoiceType (extended R) ereal_choiceMixin.
End ERealChoice .
Section ERealCount .
Variable (R : countType).
Definition ereal_countMixin := PcanCountMixin (@codeK R).
Canonical ereal_countType := CountType (extended R) ereal_countMixin.
End ERealCount .
Section ERealOrder .
Context {R : numDomainType}.
Implicit Types x y : \bar R.
Definition le_ereal x1 x2 :=
match x1, x2 with
| -oo, r%:E | r%:E, +oo => r \is Num.real
| r1%:E, r2%:E => r1 <= r2
| -oo, _ | _, +oo => true
| +oo, _ | _, -oo => false
end .
Definition lt_ereal x1 x2 :=
match x1, x2 with
| -oo, r%:E | r%:E, +oo => r \is Num.real
| r1%:E, r2%:E => r1 < r2
| -oo, -oo | +oo, +oo => false
| +oo, _ | _ , -oo => false
| -oo, _ => true
end .
Lemma lt_def_ereal x y : lt_ereal x y = (y != x) && le_ereal x y.R : numDomainType x, y : \bar R
lt_ereal x y = (y != x) && le_ereal x y
Proof .1f
by case : x y => [?||][?||] //=; rewrite lt_def eqe. Qed .
Lemma le_refl_ereal : reflexive le_ereal.
Proof .27
by case => /=. Qed .
Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
Proof .2d
by case => [?||][?||]/=; rewrite ?andbF => // /le_anti ->. Qed .
Lemma le_trans_ereal : ssrbool.transitive le_ereal.
Proof .32
case => [?||][?||][?||] //=; rewrite -?comparabler0 ; first exact : le_trans.22 _r_, _r1_ : R
_r1_ <= _r_ -> _r_ >=< 0 %R -> _r1_ >=< 0 %R
by move => /le_comparable cmp /(comparabler_trans cmp).
by move => cmp /ge_comparable /comparabler_trans; apply .
Qed .
Fact ereal_display : unit. Proof .43
by []. Qed .
Definition ereal_porderMixin :=
LePOrderMixin lt_def_ereal le_refl_ereal le_anti_ereal le_trans_ereal.
Canonical ereal_porderType :=
POrderType ereal_display (extended R) ereal_porderMixin.
Lemma leEereal x y : (x <= y)%O = le_ereal x y.21 (x <= y)%O = le_ereal x y
Proof .48
by []. Qed .
Lemma ltEereal x y : (x < y)%O = lt_ereal x y.21 (x < y)%O = lt_ereal x y
Proof .4d
by []. Qed .
End ERealOrder .
Notation lee := (@Order.le ereal_display _) (only parsing ).
Notation "@ 'lee' R" :=
(@Order.le ereal_display R) (at level 10 , R at level 8 , only parsing ).
Notation lte := (@Order.lt ereal_display _) (only parsing ).
Notation "@ 'lte' R" :=
(@Order.lt ereal_display R) (at level 10 , R at level 8 , only parsing ).
Notation gee := (@Order.ge ereal_display _) (only parsing ).
Notation "@ 'gee' R" :=
(@Order.ge ereal_display R) (at level 10 , R at level 8 , only parsing ).
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_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.
Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing ) : ereal_scope.
Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing ) : ereal_scope.
Section ERealOrder_numDomainType .
Context {R : numDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma lee_fin (r s : R) : (r%:E <= s%:E) = (r <= s)%R.22 r, s : R
(r%:E <= s%:E) = (r <= s)%R
Proof .52
by []. Qed .
Lemma lte_fin (r s : R) : (r%:E < s%:E) = (r < s)%R.54 (r%:E < s%:E) = (r < s)%R
Proof .59
by []. Qed .
Lemma lee01 : 0 <= 1 :> \bar R.29 (0 : \bar R) <= (1 : \bar R)
Proof .5e
by rewrite lee_fin. Qed .
Lemma lte01 : 0 < 1 :> \bar R.29 (0 : \bar R) < (1 : \bar R)
Proof .63
by rewrite lte_fin. Qed .
Lemma leeNy_eq x : (x <= -oo) = (x == -oo).22 x : \bar R
(x <= -oo) = (x == -oo)
Proof .68
by case : x. Qed .
Lemma leye_eq x : (+oo <= x) = (x == +oo).6a (+oo <= x) = (x == +oo)
Proof .6f
by case : x. Qed .
Lemma lt0y : (0 : \bar R) < +oo. Proof .74
exact : real0. Qed .
Lemma ltNy0 : -oo < (0 : \bar R). Proof .79
exact : real0. Qed .
Lemma le0y : (0 : \bar R) <= +oo. Proof .7e
exact : real0. Qed .
Lemma leNy0 : -oo <= (0 : \bar R). Proof .83
exact : real0. Qed .
Lemma lt0e x : (0 < x) = (x != 0 ) && (0 <= x).6a (0 < x) = (x != 0 ) && (0 <= x)
Proof .88
by case : x => [r| |]//; rewrite lte_fin lee_fin lt0r. Qed .
Lemma ereal_comparable x y : (0 %E >=< x)%O -> (0 %E >=< y)%O -> (x >=< y)%O.21 (0 %E >=< x)%O -> (0 %E >=< y)%O -> (x >=< y)%O
Proof .8d
move : x y => [x||] [y||] //; rewrite /Order.comparable !lee_fin -!realE.22 x, y : R
x \is Num.real ->
y \is Num.real -> (x <= y)%R || (y <= x)%R
- 92
exact : real_comparable.
- a2
by rewrite /lee/= => ->.
- a7
by rewrite /lee/= => _ ->.
Qed .
Lemma real_ltry r : r%:E < +oo = (r \is Num.real).22 r : R
(r%:E < +oo) = (r \is Num.real)
Proof .ab
by []. Qed .
Lemma real_ltNyr r : -oo < r%:E = (r \is Num.real).ad (-oo < r%:E) = (r \is Num.real)
Proof .b2
by []. Qed .
Lemma real_leey x : (x <= +oo) = (fine x \is Num.real).6a (x <= +oo) = (fine x \is Num.real)
Proof .b7
by case : x => //=; rewrite real0. Qed .
Lemma real_leNye x : (-oo <= x) = (fine x \is Num.real).6a (-oo <= x) = (fine x \is Num.real)
Proof .bc
by case : x => //=; rewrite real0. Qed .
Lemma gee0P x : 0 <= x <-> x = +oo \/ exists2 r, (r >= 0 )%R & x = r%:E.6a 0 <= x <->
x = +oo \/ (exists2 r : R, (0 <= r)%R & x = r%:E)
Proof .c1
split => [|[->|[r r0 ->//]]]; last by rewrite real_leey/=.6a 0 <= x ->
x = +oo \/ (exists2 r : R, (0 <= r)%R & x = r%:E)
by case : x => [r r0 | _ |//]; [right ; exists r |left ].
Qed .
End ERealOrder_numDomainType .
#[global ] Hint Resolve lee01 lte01 : core.
Section ERealOrder_realDomainType .
Context {R : realDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma ltry r : r%:E < +oo.R : realDomainType ae
r%:E < +oo
Proof .ca
exact : num_real. Qed .
Lemma ltey x : (x < +oo) = (x != +oo).cd 6b
(x < +oo) = (x != +oo)
Proof .d1
by case : x => // r; rewrite ltry. Qed .
Lemma ltNyr r : -oo < r%:E. Proof .d7
exact : num_real. Qed .
Lemma ltNye x : (-oo < x) = (x != -oo).
Proof .dc
by case : x => // r; rewrite ltNyr. Qed .
Lemma leey x : x <= +oo. Proof .e1
by case : x => //= r; exact : num_real. Qed .
Lemma leNye x : -oo <= x. Proof .e6
by case : x => //= r; exact : num_real. Qed .
Definition lteey := (ltey, leey).
Definition lteNye := (ltNye, leNye).
Lemma le_total_ereal : totalPOrderMixin [porderType of \bar R].cd
totalPOrderMixin [porderType of \bar R]
Proof .eb
by move => [?||][?||]//=; rewrite (ltEereal, leEereal)/= ?num_real ?le_total .
Qed .
Canonical ereal_latticeType := LatticeType (extended R) le_total_ereal.
Canonical ereal_distrLatticeType := DistrLatticeType (extended R) le_total_ereal.
Canonical ereal_orderType := OrderType (extended R) le_total_ereal.
End ERealOrder_realDomainType .
Section ERealArith .
Context {R : numDomainType}.
Implicit Types x y z : \bar R.
Definition adde_subdef x y :=
match x, y with
| x%:E , y%:E => (x + y)%:E
| -oo, _ => -oo
| _ , -oo => -oo
| +oo, _ => +oo
| _ , +oo => +oo
end .
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
| -oo => +oo
| +oo => -oo
end .
Definition mule_subdef x y :=
match x, y with
| x%:E , y%:E => (x * y)%:E
| -oo, y | y, -oo => if y == 0 then 0 else if 0 < y then -oo else +oo
| +oo, y | y, +oo => if y == 0 then 0 else if 0 < y then +oo else -oo
end .
Definition mule := nosimpl mule_subdef.
Definition abse x := if x is r%:E then `|r|%:E else +oo.
Definition expe x n := iterop n mule x 1 .
Definition enatmul x n := iterop n adde x 0 .
Definition ednatmul x n := iterop n dual_adde x 0 .
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 "x ^+ n" := (expe x%dE n) : ereal_dual_scope.
Notation "x ^+ n" := (expe x n) : ereal_scope.
Notation "x *+ n" := (ednatmul x%dE n) : ereal_dual_scope.
Notation "x *+ n" := (enatmul x n) : ereal_scope.
Notation "\- f" := (fun x => - f x)%dE : ereal_dual_scope.
Notation "\- f" := (fun x => - f x)%E : ereal_scope.
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 "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 "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.
Section ERealOrderTheory .
Context {R : numDomainType}.
Implicit Types x y z : \bar R.
Local Tactic Notation "elift" constr (lm) ":" ident (x) :=
by case : x => [||?]; first by rewrite ?eqe ; apply : lm.
Local Tactic Notation "elift" constr (lm) ":" ident (x) ident (y) :=
by case : x y => [?||] [?||]; first by rewrite ?eqe ; apply : lm.
Local Tactic Notation "elift" constr (lm) ":" ident (x) ident (y) ident (z) :=
by case : x y z => [?||] [?||] [?||]; first by rewrite ?eqe ; apply : lm.
Lemma lee0N1 : 0 <= (-1 )%:E :> \bar R = false.29 ((0 : \bar R) <= ((-1 )%:E : \bar R)) = false
Proof .f1
by rewrite lee_fin ler0N1. Qed .
Lemma lte0N1 : 0 < (-1 )%:E :> \bar R = false.29 ((0 : \bar R) < ((-1 )%:E : \bar R)) = false
Proof .f6
by rewrite lte_fin ltr0N1. Qed .
Lemma lteN10 : - 1 %E < 0 :> \bar R.29 (- (1 ) : \bar R) < (0 : \bar R)
Proof .fb
by rewrite lte_fin ltrN10. Qed .
Lemma leeN10 : - 1 %E <= 0 :> \bar R.29 (- (1 ) : \bar R) <= (0 : \bar R)
Proof .100
by rewrite lee_fin lerN10. Qed .
Lemma fine_ge0 x : 0 <= x -> (0 <= fine x)%R.6a 0 <= x -> (0 <= fine x)%R
Proof .105
by case : x. Qed .
Lemma fine_gt0 x : 0 < x < +oo -> (0 < fine x)%R.6a 0 < x < +oo -> (0 < fine x)%R
Proof .10a
by move : x => [x| |] //=; rewrite ?ltxx ?andbF // lte_fin => /andP[]. Qed .
Lemma fine_lt0 x : -oo < x < 0 -> (fine x < 0 )%R.6a -oo < x < 0 -> (fine x < 0 )%R
Proof .10f
by move : x => [x| |] //= /andP[_]; rewrite lte_fin. Qed .
Lemma fine_le0 x : x <= 0 -> (fine x <= 0 )%R.6a x <= 0 -> (fine x <= 0 )%R
Proof .114
by case : x. Qed .
Lemma lee_tofin (r0 r1 : R) : (r0 <= r1)%R -> r0%:E <= r1%:E.22 r0, r1 : R
(r0 <= r1)%R -> r0%:E <= r1%:E
Proof .119
by []. Qed .
Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%R -> r0%:E < r1%:E.11b (r0 < r1)%R -> r0%:E < r1%:E
Proof .120
by []. Qed .
Lemma enatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.22 n : nat
+oo *+ n.+1 = +oo
Proof .125
by elim : n => //= n ->. Qed .
Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
Proof .12c
by elim : n => //= n ->. Qed .
Lemma EFin_natmul (r : R) n : (r *+ n.+1 )%:E = r%:E *+ n.+1 .22 ae 128
(r *+ n.+1 )%:E = r%:E *+ n.+1
Proof .131
by elim : n => //= n <-. Qed .
Lemma mule2n x : x *+ 2 = x + x. Proof .137
by []. Qed .
Lemma expe2 x : x ^+ 2 = x * x. Proof .13c
by []. Qed .
End ERealOrderTheory .
#[global ] Hint Resolve leeN10 lteN10 : core.
Section finNumPred .
Context {R : numDomainType}.
Implicit Type (x : \bar R).
Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
Fact fin_num_key : pred_key fin_num. by []. Qed .
Canonical fin_num_keyd := KeyedQualifier fin_num_key.
Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).6a (x \is a fin_num) = (x != -oo) && (x != +oo)
Proof .145
by []. Qed .
Lemma fin_numP x : reflect ((x != -oo) /\ (x != +oo)) (x \is a fin_num).6a reflect (x != -oo /\ x != +oo) (x \is a fin_num)
Proof .14a
by apply /(iffP idP) => [/andP//|/andP]. Qed .
Lemma fin_numEn x : (x \isn't a fin_num) = (x == -oo) || (x == +oo).6a (x \isn't a fin_num) = (x == -oo) || (x == +oo)
Proof .14f
by rewrite fin_numE negb_and ?negbK . Qed .
Lemma fin_numPn x : reflect (x = -oo \/ x = +oo) (x \isn't a fin_num).6a reflect (x = -oo \/ x = +oo) (x \isn't a fin_num)
Proof .154
by rewrite fin_numEn; apply : (iffP orP) => -[]/eqP; by [left |right ]. Qed .
Lemma fin_real x : -oo < x < +oo -> x \is a fin_num.6a -oo < x < +oo -> x \is a fin_num
Proof .159
by move => /andP[oox xoo]; rewrite fin_numE gt_eqF ?lt_eqF . Qed .
Lemma fin_num_abs x : (x \is a fin_num) = (`| x | < +oo)%E.6a (x \is a fin_num) = (`|x| < +oo)
Proof .15e
by rewrite fin_numE; case : x => // r; rewrite real_ltry normr_real. Qed .
End finNumPred .
Section ERealArithTh_numDomainType .
Context {R : numDomainType}.
Implicit Types (x y z : \bar R) (r : R).
Lemma fine_le : {in fin_num &, {homo @fine R : x y / x <= y >-> (x <= y)%R}}.29 {in fin_num &,
{homo fine : x y / x <= y >-> (x <= y)%R}}
Proof .163
by move => [? [?| |]| |]. Qed .
Lemma fine_lt : {in fin_num &, {homo @fine R : x y / x < y >-> (x < y)%R}}.29 {in fin_num &,
{homo fine : x y / x < y >-> (x < y)%R}}
Proof .168
by move => [? [?| |]| |]. Qed .
Lemma fine_abse : {in fin_num, {morph @fine R : x / `|x| >-> `|x|%R}}.29 {in fin_num, {morph fine : x / `|x| >-> `|x|%R}}
Proof .16d
by case . Qed .
Lemma abse_fin_num x : (`|x| \is a fin_num) = (x \is a fin_num).6a (`|x| \is a fin_num) = (x \is a fin_num)
Proof .172
by case : x. Qed .
Lemma fine_eq0 x : x \is a fin_num -> (fine x == 0 %R) = (x == 0 ).6a x \is a fin_num -> (fine x == 0 %R) = (x == 0 )
Proof .177
by move : x => [//| |] /=; rewrite fin_numE. Qed .
Lemma EFinN r : (- r)%:E = (- r%:E). Proof .17c
by []. Qed .
Lemma fineN x : fine (- x) = (- fine x)%R.6a fine (- x) = (- fine x)%R
Proof .181
by case : x => //=; rewrite oppr0. Qed .
Lemma EFinD r r' : (r + r')%:E = r%:E + r'%:E.22 r, r' : R
(r + r')%:E = r%:E + r'%:E
Proof .186
by []. Qed .
Lemma EFinB r r' : (r - r')%:E = r%:E - r'%:E.188 (r - r')%:E = r%:E - r'%:E
Proof .18d
by []. Qed .
Lemma EFinM r r' : (r * r')%:E = r%:E * r'%:E.188 (r * r')%:E = r%:E * r'%:E
Proof .192
by []. Qed .
Lemma sumEFin I s P (F : I -> R) :
\sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.22 I : Type s : seq I P : I -> bool F : I -> R
\sum_(i <- s | P i) (F i)%:E =
(\sum_(i <- s | P i) F i)%:E
Proof .197
by rewrite (big_morph _ EFinD erefl). Qed .
Definition adde_def x y :=
~~ ((x == +oo) && (y == -oo)) && ~~ ((x == -oo) && (y == +oo)).
Local Notation "x +? y" := (adde_def x y).
Lemma adde_defC x y : x +? y = y +? x.
Proof .1a1
by rewrite /adde_def andbC (andbC (x == -oo)) (andbC (x == +oo)). Qed .
Lemma fin_num_adde_defr x y : x \is a fin_num -> x +? y.21 x \is a fin_num -> x +? y
Proof .1a6
by move : x y => [x| |] [y | |]. Qed .
Lemma fin_num_adde_defl x y : y \is a fin_num -> x +? y.21 y \is a fin_num -> x +? y
Proof .1ab
by rewrite adde_defC; exact : fin_num_adde_defr. Qed .
Lemma adde_defN x y : x +? - y = - x +? y.
Proof .1b0
by move : x y => [x| |] [y| |]. Qed .
Lemma adde_defDr x y z : x +? y -> x +? z -> x +? (y + z).22 x, y, z : \bar R
x +? y -> x +? z -> x +? (y + z)
Proof .1b5
by move : x y z => [x||] [y||] [z||]. Qed .
Lemma adde_defEninfty x : (x +? -oo) = (x != +oo).
Proof .1bc
by case : x. Qed .
Lemma ge0_adde_def : {in [pred x | x >= 0 ] &, forall x y , x +? y}.29 {in [pred x | 0 <= x] &, forall x y , x +? y}
Proof .1c1
by move => [x| |] [y| |]. Qed .
Lemma addeC : commutative (S := \bar R) +%E.
Proof .1c6
by case => [x||] [y||] //; rewrite /adde /= addrC. Qed .
Lemma adde0 : right_id (0 : \bar R) +%E.29 right_id (0 : \bar R) +%E
Proof .1cb
by case => // r; rewrite /adde /= addr0. Qed .
Lemma add0e : left_id (0 : \bar R) +%E.29 left_id (0 : \bar R) +%E
Proof .1d0
by move => x; rewrite addeC adde0. Qed .
Lemma addeA : associative (S := \bar R) +%E.
Proof .1d5
by case => [x||] [y||] [z||] //; rewrite /adde /= addrA. Qed .
Canonical adde_monoid := Monoid.Law addeA add0e adde0.
Canonical adde_comoid := Monoid.ComLaw addeC.
Lemma adde_def_sum I h t (P : pred I) (f : I -> \bar R) :
{in P, forall i : I, f h +? f i} ->
f h +? \sum_(j <- t | P j) f j.22 19a h : I t : seq I P : pred I f : I -> \bar R
{in P, forall i : I, f h +? f i} ->
f h +? \sum_(j <- t | P j) f j
Proof .1da
move => fhi; elim /big_rec : _; first by rewrite fin_num_adde_defl.22 19a 1dd 1de 1df 1e0 fhi : {in P, forall i : I, f h +? f i}
forall (i : I) (x : \bar R),
P i -> f h +? x -> f h +? (f i + x)
by move => i x Pi fhx; rewrite adde_defDr// fhi.
Qed .
Lemma addeAC : @right_commutative (\bar R) _ +%E.
Proof .1ea
exact : Monoid.mulmAC. Qed .
Lemma addeCA : @left_commutative (\bar R) _ +%E.
Proof .1ef
exact : Monoid.mulmCA. Qed .
Lemma addeACA : @interchange (\bar R) +%E +%E.
Proof .1f4
exact : Monoid.mulmACA. Qed .
Lemma adde_gt0 x y : 0 < x -> 0 < y -> 0 < x + y.21 0 < x -> 0 < y -> 0 < x + y
Proof .1f9
by move : x y => [x| |] [y| |] //; rewrite !lte_fin; exact : addr_gt0.
Qed .
Lemma padde_eq0 x y : 0 <= x -> 0 <= y -> (x + y == 0 ) = (x == 0 ) && (y == 0 ).21 0 <= x ->
0 <= y -> (x + y == 0 ) = (x == 0 ) && (y == 0 )
Proof .1fe
move : x y => [x| |] [y| |]//; rewrite !lee_fin; first exact : paddr_eq0.99 (0 <= x)%R ->
0 <= +oo ->
(x%:E + +oo == 0 ) = (x%:E == 0 ) && (+oo == 0 )
by move => x0 _ /=; rewrite andbF.
Qed .
Lemma nadde_eq0 x y : x <= 0 -> y <= 0 -> (x + y == 0 ) = (x == 0 ) && (y == 0 ).21 x <= 0 ->
y <= 0 -> (x + y == 0 ) = (x == 0 ) && (y == 0 )
Proof .207
move : x y => [x| |] [y| |]//; rewrite !lee_fin; first exact : naddr_eq0.99 (x <= 0 )%R ->
-oo <= 0 ->
(x%:E + -oo == 0 ) = (x%:E == 0 ) && (-oo == 0 )
by move => x0 _ /=; rewrite andbF.
Qed .
Lemma realDe x y : (0 %E >=< x)%O -> (0 %E >=< y)%O -> (0 %E >=< x + y)%O.21 (0 %E >=< x)%O -> (0 %E >=< y)%O -> (0 %E >=< x + y)%O
Proof .210
case : x y => [x||] [y||] //; exact : realD. Qed .
Lemma oppe0 : - 0 = 0 :> \bar R.
Proof .215
by rewrite /= oppr0. Qed .
Lemma oppeK : involutive (A := \bar R) -%E.
Proof .21a
by case => [x||] //=; rewrite opprK. Qed .
Lemma oppe_inj : @injective (\bar R) _ -%E.
Proof .21f
exact : inv_inj oppeK. Qed .
Lemma adde_defNN x y : - x +? - y = x +? y.
Proof .224
by rewrite adde_defN oppeK. Qed .
Lemma oppe_eq0 x : (- x == 0 )%E = (x == 0 )%E.
Proof .229
by rewrite -(can_eq oppeK) oppe0. Qed .
Lemma oppeD x y : x +? y -> - (x + y) = - x - y.21 x +? y -> - (x + y) = - x - y
Proof .22e
by move : x y => [x| |] [y| |] //= _; rewrite opprD. Qed .
Lemma fin_num_oppeD x y : y \is a fin_num -> - (x + y) = - x - y.21 y \is a fin_num -> - (x + y) = - x - y
Proof .233
by move => finy; rewrite oppeD// fin_num_adde_defl. Qed .
Lemma sube0 x : x - 0 = x.
Proof .238
by move : x => [x| |] //; rewrite -EFinB subr0. Qed .
Lemma sub0e x : 0 - x = - x.
Proof .23d
by move : x => [x| |] //; rewrite -EFinB sub0r. Qed .
Lemma muleC x y : x * y = y * x.
Proof .242
by move : x y => [r||] [s||]//=; rewrite -EFinM mulrC. Qed .
Lemma onee_neq0 : 1 != 0 :> \bar R. Proof .247
exact : oner_neq0. Qed .
Lemma onee_eq0 : 1 == 0 :> \bar R = false.29 (1 == 0 :> \bar R) = false
Proof .24c
exact : oner_eq0. Qed .
Lemma mule1 x : x * 1 = x.
Proof .251
by move : x=> [r||]/=; rewrite /mule/= ?mulr1 ?(negbTE onee_neq0) ?lte_tofin .
Qed .
Lemma mul1e x : 1 * x = x.
Proof .256
by rewrite muleC mule1. Qed .
Lemma mule0 x : x * 0 = 0 .
Proof .25b
by move : x => [r| |] //=; rewrite /mule/= ?mulr0 // eqxx. Qed .
Lemma mul0e x : 0 * x = 0 .
Proof .260
by move : x => [r| |]/=; rewrite /mule/= ?mul0r // eqxx. Qed .
Canonical mule_mulmonoid := @Monoid.MulLaw _ _ mule mul0e mule0.
Lemma expeS x n : x ^+ n.+1 = x * x ^+ n.22 6b 128
x ^+ n.+1 = x * x ^+ n
Proof .265
by case : n => //=; rewrite mule1. Qed .
Definition mule_def x y :=
~~ (((x == 0 ) && (`| y | == +oo)) || ((y == 0 ) && (`| x | == +oo))).
Local Notation "x *? y" := (mule_def x y).
Lemma mule_defC x y : x *? y = y *? x.
Proof .26b
by rewrite [in LHS]/mule_def orbC. Qed .
Lemma mule_def_fin x y : x \is a fin_num -> y \is a fin_num -> x *? y.21 x \is a fin_num -> y \is a fin_num -> x *? y
Proof .270
move : x y => [x| |] [y| |] finx finy//.22 95 finx : x%:E \is a fin_num finy : y%:E \is a fin_num
x%:E *? y%:E
by rewrite /mule_def negb_or 2 !negb_and/= 2 !orbT.
Qed .
Lemma mule_def_neq0_infty x y : x != 0 -> y \isn't a fin_num -> x *? y.21 x != 0 -> y \isn't a fin_num -> x *? y
Proof .27c
by move : x y => [x| |] [y| |]// x0 _; rewrite /mule_def (negbTE x0). Qed .
Lemma mule_def_infty_neq0 x y : x \isn't a fin_num -> y!= 0 -> x *? y.21 x \isn't a fin_num -> y != 0 -> x *? y
Proof .281
by move : x y => [x| |] [y| |]// _ y0; rewrite /mule_def (negbTE y0). Qed .
Lemma neq0_mule_def x y : x * y != 0 -> x *? y.
Proof .286
move : x y => [x| |] [y| |] //; first by rewrite mule_def_fin.99 x%:E * +oo != 0 -> x%:E *? +oo
- 28b
by have [->|?] := eqVneq x 0 %R; rewrite ?mul0e ?eqxx // mule_def_neq0_infty.
- 297
by have [->|?] := eqVneq x 0 %R; rewrite ?mul0e ?eqxx // mule_def_neq0_infty.
- 29c
by have [->|?] := eqVneq y 0 %R; rewrite ?mule0 ?eqxx // mule_def_infty_neq0.
- 2a1
by have [->|?] := eqVneq y 0 %R; rewrite ?mule0 ?eqxx // mule_def_infty_neq0.
Qed .
Lemma ltpinfty_adde_def : {in [pred x | x < +oo] &, forall x y , x +? y}.29 {in [pred x | x < +oo] &, forall x y , x +? y}
Proof .2a5
by move => [x| |] [y| |]. Qed .
Lemma ltninfty_adde_def : {in [pred x | -oo < x] &, forall x y , x +? y}.29 {in [pred x | -oo < x] &, forall x y , x +? y}
Proof .2aa
by move => [x| |] [y| |]. Qed .
Lemma abse_eq0 x : (`|x| == 0 ) = (x == 0 ).
Proof .2af
by move : x => [| |] //= r; rewrite !eqe normr_eq0. Qed .
Lemma abse0 : `|0 | = 0 :> \bar R. Proof .2b4
by rewrite /abse normr0. Qed .
Lemma abse1 : `|1 | = 1 :> \bar R. Proof .2b9
by rewrite /abse normr1. Qed .
Lemma abseN x : `|- x| = `|x|.
Proof .2be
by case : x => [r||]; rewrite //= normrN. Qed .
Lemma eqe_opp x y : (- x == - y) = (x == y).21 (- x == - y) = (x == y)
Proof .2c3
move : x y => [r| |] [r'| |] //=; apply /idP/idP => [|/eqP[->]//].188 (- r)%:E == (- r')%:E -> r%:E == r'%:E
by move /eqP => -[] /eqP; rewrite eqr_opp => /eqP ->.
Qed .
Lemma eqe_oppP x y : (- x = - y) <-> (x = y).
Proof .2cc
by split => [/eqP | -> //]; rewrite eqe_opp => /eqP. Qed .
Lemma eqe_oppLR x y : (- x == y) = (x == - y).21 (- x == y) = (x == - y)
Proof .2d1
by move : x y => [r0| |] [r1| |] //=; rewrite !eqe eqr_oppLR. Qed .
Lemma eqe_oppLRP x y : (- x = y) <-> (x = - y).
Proof .2d6
split => /eqP; first by rewrite eqe_oppLR => /eqP.
by rewrite -eqe_oppLR => /eqP.
Qed .
Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).6a (- x \is a fin_num) = (x \is a fin_num)
Proof .2df
by rewrite !fin_num_abs abseN. Qed .
Lemma oppeB x y : x +? - y -> - (x - y) = - x + y.21 x +? - y -> - (x - y) = - x + y
Proof .2e4
by move => xy; rewrite oppeD// oppeK. Qed .
Lemma fin_num_oppeB x y : y \is a fin_num -> - (x - y) = - x + y.21 y \is a fin_num -> - (x - y) = - x + y
Proof .2e9
by move => ?; rewrite oppeB// adde_defN fin_num_adde_defl. Qed .
Lemma fin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).21 (x + y \is a fin_num) =
(x \is a fin_num) && (y \is a fin_num)
Proof .2ee
by move : x y => [x| |] [y| |]. Qed .
Lemma sum_fin_num (T : Type ) (s : seq T) (P : pred T) (f : T -> \bar R) :
\sum_(i <- s | P i) f i \is a fin_num =
all [pred x | x \is a fin_num] [seq f i | i <- s & P i].22 6 s : seq T P : pred T f : T -> \bar R
(\sum_(i <- s | P i) f i \is a fin_num) =
all [pred x in fin_num] [seq f i | i <- s & P i]
Proof .2f3
by rewrite -big_all big_map big_filter; exact : (big_morph _ fin_numD).
Qed .
Lemma sum_fin_numP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar R) :
reflect (forall i , i \in s -> P i -> f i \is a fin_num)
(\sum_(i <- s | P i) f i \is a fin_num).22 T : eqType 2f6 2f7 2f8
reflect
(forall i : T, i \in s -> P i -> f i \is a fin_num)
(\sum_(i <- s | P i) f i \is a fin_num)
Proof .2fc
rewrite sum_fin_num; apply : (iffP allP) => /=.2fe {in [seq f i | i <- s & P i],
forall x , x \is a fin_num} ->
forall i : T, i \in s -> P i -> f i \is a fin_num
by move => + x xs Px; apply ; rewrite map_f// mem_filter Px.
by move => + _ /mapP[x /[!mem_filter]/andP[Px xs] ->]; apply .
Qed .
Lemma fin_numB x y :
(x - y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).21 (x - y \is a fin_num) =
(x \is a fin_num) && (y \is a fin_num)
Proof .30d
by move : x y => [x| |] [y| |]. Qed .
Lemma fin_numM x y : x \is a fin_num -> y \is a fin_num ->
x * y \is a fin_num.21 x \is a fin_num ->
y \is a fin_num -> x * y \is a fin_num
Proof .312
by move : x y => [x| |] [y| |]. Qed .
Lemma fin_numX x n : x \is a fin_num -> x ^+ n \is a fin_num.267 x \is a fin_num -> x ^+ n \is a fin_num
Proof .317
by elim : n x => // n ih x finx; rewrite expeS fin_numM// ih. Qed .
Lemma fineD : {in @fin_num R &, {morph fine : x y / x + y >-> (x + y)%R}}.29 {in fin_num &,
{morph fine : x y / x + y >-> (x + y)%R}}
Proof .31c
by move => [r| |] [s| |]. Qed .
Lemma fineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.29 {in fin_num &,
{morph fine : x y / x - y >-> (x - y)%R}}
Proof .321
by move => [r| |] [s| |]. Qed .
Lemma fineM : {in @fin_num R &, {morph fine : x y / x * y >-> (x * y)%R}}.29 {in fin_num &,
{morph fine : x y / x * y >-> (x * y)%R}}
Proof .326
by move => [x| |] [y| |]. Qed .
Lemma fineK x : x \is a fin_num -> (fine x)%:E = x.6a x \is a fin_num -> (fine x)%:E = x
Proof .32b
by case : x. Qed .
Lemma EFin_sum_fine (I : Type ) s (P : pred I) (f : I -> \bar R) :
(forall i , P i -> f i \is a fin_num) ->
(\sum_(i <- s | P i) fine (f i))%:E = \sum_(i <- s | P i) f i.22 19a 19b 1df 1e0
(forall i : I, P i -> f i \is a fin_num) ->
(\sum_(i <- s | P i) fine (f i))%:E =
\sum_(i <- s | P i) f i
Proof .330
by move => h; rewrite -sumEFin; apply : eq_bigr => i Pi; rewrite fineK// h.
Qed .
Lemma sum_fine (I : Type ) s (P : pred I) (F : I -> \bar R) :
(forall i , P i -> F i \is a fin_num) ->
(\sum_(i <- s | P i) fine (F i) = fine (\sum_(i <- s | P i) F i))%R.22 19a 19b 1df F : I -> \bar R
(forall i : I, P i -> F i \is a fin_num) ->
(\sum_(i <- s | P i) fine (F i))%R =
fine (\sum_(i <- s | P i) F i)
Proof .336
by move => h; rewrite -EFin_sum_fine. Qed .
Lemma sumeN I s (P : pred I) (f : I -> \bar R) :
{in P &, forall i j , f i +? f j} ->
\sum_(i <- s | P i) - f i = - \sum_(i <- s | P i) f i.332 {in P &, forall i j : I, f i +? f j} ->
\sum_(i <- s | P i) - f i =
- (\sum_(i <- s | P i) f i)
Proof .33d
elim : s => [|a b ih h]; first by rewrite !big_nil oppe0.22 19a 1df 1e0 a : I b : seq I ih : {in P &, forall i j : I, f i +? f j} ->
\sum_(i <- b | P i) - f i =
- (\sum_(i <- b | P i) f i) h : {in P &, forall i j : I, f i +? f j}
\sum_(i <- (a :: b) | P i) - f i =
- (\sum_(i <- (a :: b) | P i) f i)
rewrite !big_cons; case : ifPn => Pa; last by rewrite ih.22 19a 1df 1e0 345 346 347 348 Pa : P a
- f a + \sum_(j <- b | P j) - f j =
- (f a + \sum_(j <- b | P j) f j)
by rewrite oppeD ?ih // adde_def_sum// => i Pi; rewrite h.
Qed .
Lemma fin_num_sumeN I s (P : pred I) (f : I -> \bar R) :
(forall i , P i -> f i \is a fin_num) ->
\sum_(i <- s | P i) - f i = - \sum_(i <- s | P i) f i.332 (forall i : I, P i -> f i \is a fin_num) ->
\sum_(i <- s | P i) - f i =
- (\sum_(i <- s | P i) f i)
Proof .351
by move => h; rewrite sumeN// => i j Pi Pj; rewrite fin_num_adde_defl// h.
Qed .
Lemma telescope_sume n m (f : nat -> \bar R) :
(forall i , (n <= i <= m)%N -> f i \is a fin_num) -> (n <= m)%N ->
\sum_(n <= k < m) (f k.+1 - f k) = f m - f n.22 n, m : nat f : nat -> \bar R
(forall i : nat, (n <= i <= m)%N -> f i \is a fin_num) ->
(n <= m)%N ->
\sum_(n <= k < m) (f k.+1 - f k) = f m - f n
Proof .356
move => nmf nm; under eq_big_nat => i /andP[ni im] do
rewrite -[f i.+1 ]fineK -1 ?[f i]fineK ?(nmf, ni, im) 1 ?ltnW //= -EFinD.22 359 35a nmf : forall i : nat, (n <= i <= m)%N -> f i \is a fin_numnm : (n <= m)%N
\sum_(n <= i < m) (fine (f i.+1 ) - fine (f i))%:E =
f m - f n
by rewrite sumEFin telescope_sumr// EFinB !fineK ?nmf ?nm ?leqnn .
Qed .
Lemma addeK x y : x \is a fin_num -> y + x - x = y.21 x \is a fin_num -> y + x - x = y
Proof .365
by move : x y => [x| |] [y| |] //; rewrite -EFinD -EFinB addrK. Qed .
Lemma subeK x y : y \is a fin_num -> x - y + y = x.21 y \is a fin_num -> x - y + y = x
Proof .36a
by move : x y => [x| |] [y| |] //; rewrite -EFinD subrK. Qed .
Lemma subee x : x \is a fin_num -> x - x = 0 .6a x \is a fin_num -> x - x = 0
Proof .36f
by move : x => [r _| |] //; rewrite -EFinB subrr. Qed .
Lemma sube_eq x y z : x \is a fin_num -> (y +? z) ->
(x - z == y) = (x == y + z).1b7 x \is a fin_num ->
y +? z -> (x - z == y) = (x == y + z)
Proof .374
by move : x y z => [x| |] [y| |] [z| |] // _ _; rewrite !eqe subr_eq.
Qed .
Lemma adde_eq_ninfty x y : (x + y == -oo) = ((x == -oo) || (y == -oo)).21 (x + y == -oo) = (x == -oo) || (y == -oo)
Proof .379
by move : x y => [?| |] [?| |]. Qed .
Lemma addye x : x != -oo -> +oo + x = +oo.6a x != -oo -> +oo + x = +oo
Proof .37e
by case : x. Qed .
Lemma addey x : x != -oo -> x + +oo = +oo.6a x != -oo -> x + +oo = +oo
Proof .383
by case : x. Qed .
Lemma addNye x : -oo + x = -oo. Proof .388
by []. Qed .
Lemma addeNy x : x + -oo = -oo. Proof .38d
by case : x. Qed .
Lemma adde_Neq_pinfty x y : x != -oo -> y != -oo ->
(x + y != +oo) = (x != +oo) && (y != +oo).21 x != -oo ->
y != -oo -> (x + y != +oo) = (x != +oo) && (y != +oo)
Proof .392
by move : x y => [x| |] [y| |]. Qed .
Lemma adde_Neq_ninfty x y : x != +oo -> y != +oo ->
(x + y != -oo) = (x != -oo) && (y != -oo).21 x != +oo ->
y != +oo -> (x + y != -oo) = (x != -oo) && (y != -oo)
Proof .397
by move : x y => [x| |] [y| |]. Qed .
Lemma adde_ss_eq0 x y : (0 <= x) && (0 <= y) || (x <= 0 ) && (y <= 0 ) ->
x + y == 0 = (x == 0 ) && (y == 0 ).21 (0 <= x) && (0 <= y) || (x <= 0 ) && (y <= 0 ) ->
(x + y == 0 ) = (x == 0 ) && (y == 0 )
Proof .39c
by move => /orP[|] /andP[]; [exact : padde_eq0|exact : nadde_eq0]. Qed .
Lemma esum_eqNyP (T : eqType) (s : seq 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].2fe \sum_(i <- s | P i) f i = -oo <->
(exists i : T, [/\ i \in s, P i & f i = -oo])
Proof .3a1
split => [|[i [si Pi fi]]].2fe \sum_(i <- s | P i) f i = -oo ->
exists i : T, [/\ i \in s, P i & f i = -oo]
rewrite big_seq_cond; elim /big_ind: _ => // [[?| |] [?| |]//|].2fe forall i : T,
(i \in s) && P i ->
f i = -oo ->
exists i0 : T, [/\ i0 \in s, P i0 & f i0 = -oo]
3a9
by move => i /andP[si Pi] fioo; exists i ; rewrite si Pi fioo.
rewrite big_mkcond (bigID (xpred1 i))/= (eq_bigr (fun _ => -oo)); last first .3ab forall i0 : T,
i0 == i -> (if P i0 then f i0 else 0 ) = -oo
by move => j /eqP ->; rewrite Pi.
rewrite big_const_seq/= [X in X + _](_ : _ = -oo)//.3ab iter (count (eq_op^~ i) s) (+%E -oo) 0 = -oo
elim : s i Pi fi si => // h t ih i Pi fi.22 2ff 2f7 2f8 h : T t : seq T ih : forall i : T,
P i ->
f i = -oo ->
i \in t ->
iter (count (eq_op^~ i) t) (+%E -oo) 0 = -oo3ac 3ae 3af
i \in h :: t ->
iter (count (eq_op^~ i) (h :: t)) (+%E -oo) 0 = -oo
rewrite inE => /predU1P[<-/=|it]; first by rewrite eqxx.22 2ff 2f7 2f8 3ca 3cb 3cc 3ac 3ae 3af it : i \in t
iter (count (eq_op^~ i) (h :: t)) (+%E -oo) 0 = -oo
by rewrite /= iterD ih//=; case : (_ == _).
Qed .
Lemma esum_eqNy (I : finType) (f : I -> \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == -oo) = [exists i in P , f i == -oo].22 I : finType 1e0 P : {pred I}
(\sum_(i | P i) f i == -oo) =
[exists i in P , f i == -oo]
Proof .3d5
apply /idP/idP => [/eqP/esum_eqNyP|/existsP[i /andP[Pi /eqP fi]]].3d7 (exists i : I,
[/\ i \in index_enum I, P i & f i = -oo]) ->
[exists i in P , f i == -oo]
by move => -[i [_ Pi fi]]; apply /existsP; exists i ; rewrite fi eqxx andbT.
by apply /eqP/esum_eqNyP; exists i .
Qed .
Lemma esum_eqyP (T : eqType) (s : seq 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].2fe (forall i : T, P i -> f i != -oo) ->
\sum_(i <- s | P i) f i = +oo <->
(exists i : T, [/\ i \in s, P i & f i = +oo])
Proof .3ea
move => finoo; split => [|[i [si Pi fi]]].22 2ff 2f6 2f7 2f8 finoo : forall i : T, P i -> f i != -oo
\sum_(i <- s | P i) f i = +oo ->
exists i : T, [/\ i \in s, P i & f i = +oo]
rewrite big_seq_cond; elim /big_ind: _ => // [[?| |] [?| |]//|].3f1 forall i : T,
(i \in s) && P i ->
f i = +oo ->
exists i0 : T, [/\ i0 \in s, P i0 & f i0 = +oo]
3f4
by move => i /andP[si Pi] fioo; exists i ; rewrite si Pi fioo.
elim : s i Pi fi si => // h t ih i Pi fi.22 2ff 2f7 2f8 3f2 3ca 3cb ih : forall i : T,
P i ->
f i = +oo ->
i \in t -> \sum_(i0 <- t | P i0) f i0 = +oo3ac 3ae 3f7
i \in h :: t -> \sum_(i <- (h :: t) | P i) f i = +oo
rewrite inE => /predU1P[<-/=|it].403 \sum_(i <- (i :: t) | P i) f i = +oo
rewrite big_cons Pi fi addye//.403 \sum_(j <- t | P j) f j != -oo
40a
by apply /eqP => /esum_eqNyP[j [jt /finoo/negbTE/eqP]].
by rewrite big_cons; case : ifPn => Ph; rewrite (ih i)// addey// finoo.
Qed .
Lemma esum_eqy (I : finType) (P : {pred I}) (f : I -> \bar R) :
(forall i , P i -> f i != -oo) ->
(\sum_(i | P i) f i == +oo) = [exists i in P , f i == +oo].22 3d8 3d9 1e0
(forall i : I, P i -> f i != -oo) ->
(\sum_(i | P i) f i == +oo) =
[exists i in P , f i == +oo]
Proof .416
move => fio; apply /idP/existsP => [/eqP /=|[/= i /andP[Pi /eqP fi]]].22 3d8 3d9 1e0 fio : forall i : I, P i -> f i != -oo
\sum_(i | P i) f i = +oo ->
exists x : I, (x \in P) && (f x == +oo)
have {}fio : (forall i , P i -> f i != -oo) by move => i Pi; exact : fio.41c
by move => /(esum_eqyP _ fio)[i [_ Pi fi]]; exists i ; rewrite fi eqxx andbT.
by apply /eqP/esum_eqyP => //; exists i .
Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `esum_eqNyP`" )]
Notation esum_ninftyP := esum_eqNyP.
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `esum_eqNy`" )]
Notation esum_ninfty := esum_eqNy.
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `esum_eqyP`" )]
Notation esum_pinftyP := esum_eqyP.
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `esum_eqy`" )]
Notation esum_pinfty := esum_eqy.
Lemma adde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.21 0 <= x -> 0 <= y -> 0 <= x + y
Proof .42a
by move : x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed .
Lemma adde_le0 x y : x <= 0 -> y <= 0 -> x + y <= 0 .21 x <= 0 -> y <= 0 -> x + y <= 0
Proof .42f
move : x y => [r0||] [r1||]// ? ?; rewrite !lee_fin -(addr0 0 %R); exact : ler_add.
Qed .
Lemma oppe_gt0 x : (0 < - x) = (x < 0 ).
Proof .434
move : x => [x||] //; exact : oppr_gt0. Qed .
Lemma oppe_lt0 x : (- x < 0 ) = (0 < x).
Proof .439
move : x => [x||] //; exact : oppr_lt0. Qed .
Lemma oppe_ge0 x : (0 <= - x) = (x <= 0 ).
Proof .43e
move : x => [x||] //; exact : oppr_ge0. Qed .
Lemma oppe_le0 x : (- x <= 0 ) = (0 <= x).
Proof .443
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.22 6 2f8 2f7
(forall t : T, P t -> 0 <= f t) ->
forall l : seq T, 0 <= \sum_(i <- l | P i) f i
Proof .448
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 .44a (forall t : T, P t -> f t <= 0 ) ->
forall l : seq T, \sum_(i <- l | P i) f i <= 0
Proof .44e
by move => f0 l; elim /big_rec : _ => // t x Pt; apply /adde_le0/f0. Qed .
Lemma mulNyy : -oo * +oo = -oo :> \bar R. Proof .453
by rewrite /mule /= lt0y. Qed .
Lemma mulyNy : +oo * -oo = -oo :> \bar R. Proof .458
by rewrite muleC mulNyy. Qed .
Lemma mulyy : +oo * +oo = +oo :> \bar R. Proof .45d
by rewrite /mule /= lt0y. Qed .
Lemma mulNyNy : -oo * -oo = +oo :> \bar R. Proof .462
by []. Qed .
Lemma real_mulry r : r \is Num.real -> r%:E * +oo = (Num.sg r)%:E * +oo.ad r \is Num.real -> r%:E * +oo = (Num.sg r)%:E * +oo
Proof .467
move => rreal; rewrite /mule/= !eqe sgr_eq0; case : ifP => [//|rn0].22 ae rreal : r \is Num.real rn0 : (r == 0 %R) = false
(if 0 < r%:E then +oo else -oo) =
(if 0 < (Num.sg r)%:E then +oo else -oo)
move : rreal => /orP[|]; rewrite le_eqVlt.22 ae 470
(0 %R == r) || (0 < r)%R ->
(if 0 < r%:E then +oo else -oo) =
(if 0 < (Num.sg r)%:E then +oo else -oo)
by rewrite eq_sym rn0/= => rgt0; rewrite lte_fin rgt0 gtr0_sg// lte01.
by rewrite rn0/= => rlt0; rewrite lt_def lt_geF// andbF ltr0_sg// lte0N1.
Qed .
Lemma real_mulyr r : r \is Num.real -> +oo * r%:E = (Num.sg r)%:E * +oo.ad r \is Num.real -> +oo * r%:E = (Num.sg r)%:E * +oo
Proof .47e
by move => rreal; rewrite muleC real_mulry. Qed .
Lemma real_mulrNy r : r \is Num.real -> r%:E * -oo = (Num.sg r)%:E * -oo.ad r \is Num.real -> r%:E * -oo = (Num.sg r)%:E * -oo
Proof .483
move => rreal; rewrite /mule/= !eqe sgr_eq0; case : ifP => [//|rn0].46e (if 0 < r%:E then -oo else +oo) =
(if 0 < (Num.sg r)%:E then -oo else +oo)
move : rreal => /orP[|]; rewrite le_eqVlt.475 (0 %R == r) || (0 < r)%R ->
(if 0 < r%:E then -oo else +oo) =
(if 0 < (Num.sg r)%:E then -oo else +oo)
by rewrite eq_sym rn0/= => rgt0; rewrite lte_fin rgt0 gtr0_sg// lte01.
by rewrite rn0/= => rlt0; rewrite lt_def lt_geF// andbF ltr0_sg// lte0N1.
Qed .
Lemma real_mulNyr r : r \is Num.real -> -oo * r%:E = (Num.sg r)%:E * -oo.ad r \is Num.real -> -oo * r%:E = (Num.sg r)%:E * -oo
Proof .496
by move => rreal; rewrite muleC real_mulrNy. Qed .
Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).
Lemma mulN1e x : - 1 %E * x = - x.
Proof .49b
rewrite -EFinN /mule/=; case : x => [x||];
do ?[by rewrite mulN1r|by rewrite eqe oppr_eq0 oner_eq0 lte_fin ltr0N1].
Qed .
Lemma muleN1 x : x * - 1 %E = - x. Proof .4a0
by rewrite muleC mulN1e. Qed .
Lemma mule_neq0 x y : x != 0 -> y != 0 -> x * y != 0 .21 x != 0 -> y != 0 -> x * y != 0
Proof .4a5
move : x y => [x||] [y||] x0 y0 //; rewrite /mule/= ?(lt0y,mulf_neq0)//;
try by (rewrite (negbTE x0); case : ifPn) ||
by (rewrite (negbTE y0); case : ifPn).
Qed .
Lemma mule_eq0 x y : (x * y == 0 ) = (x == 0 ) || (y == 0 ).21 (x * y == 0 ) = (x == 0 ) || (y == 0 )
Proof .4aa
apply /idP/idP => [|/orP[] /eqP->]; rewrite ?(mule0, mul0e)//.21 x * y == 0 -> (x == 0 ) || (y == 0 )
by apply : contraTT => /norP[]; apply : mule_neq0.
Qed .
Lemma mule_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x * y.21 0 <= x -> 0 <= y -> 0 <= x * y
Proof .4b3
move : x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin, lt0y)//.94 (0 <= x)%R -> (0 <= y)%R -> (0 <= x * y)%R
- 4b8
exact : mulr_ge0.
- 4c2
rewrite le_eqVlt => /predU1P[<- _|x0 _]; first by rewrite eqxx.22 9a x0 : (0 < x)%R
0 <=
(if x == 0 %R
then 0
else if (0 < x)%R then +oo else -oo)
4c4
by rewrite gt_eqF // x0 le0y.
- 4cd
move => _; rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite eqxx.22 9e y0 : (0 < y)%R
0 <=
(if y == 0 %R
then 0
else if (0 < y)%R then +oo else -oo)
by rewrite gt_eqF // y0 le0y.
Qed .
Lemma mule_gt0 x y : 0 < x -> 0 < y -> 0 < x * y.21 0 < x -> 0 < y -> 0 < x * y
Proof .4d7
by rewrite !lt_def => /andP[? ?] /andP[? ?]; rewrite mule_neq0 ?mule_ge0 .
Qed .
Lemma mule_le0 x y : x <= 0 -> y <= 0 -> 0 <= x * y.21 x <= 0 -> y <= 0 -> 0 <= x * y
Proof .4dc
move : x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin)//.94 (x <= 0 )%R -> (y <= 0 )%R -> (0 <= x * y)%R
- 4e1
exact : mulr_le0.
- 4eb
by rewrite lt_leAnge => -> _; case : ifP => _ //; rewrite andbF le0y.
- 4f0
by rewrite lt_leAnge => _ ->; case : ifP => _ //; rewrite andbF le0y.
Qed .
Lemma mule_le0_ge0 x y : x <= 0 -> 0 <= y -> x * y <= 0 .21 x <= 0 -> 0 <= y -> x * y <= 0
Proof .4f4
move : x y => [x| |] [y| |] //; rewrite /mule/= ?(lee_fin, lte_fin).94 (x <= 0 )%R -> (0 <= y)%R -> (x * y <= 0 )%R
- 4f9
exact : mulr_le0_ge0.
- 505
by move => x0 _; case : ifP => _ //; rewrite lt_leAnge /= x0 andbF leNy0.
- 50a
move => _; rewrite le_eqVlt => /predU1P[<-|->]; first by rewrite eqxx.9d (if y%:E == 0 then 0 else -oo) <= 0
50c
by case : ifP => _ //; rewrite leNy0.
- 513
by rewrite lt0y leNy0.
Qed .
Lemma mule_ge0_le0 x y : 0 <= x -> y <= 0 -> x * y <= 0 .21 0 <= x -> y <= 0 -> x * y <= 0
Proof .517
by move => x0 y0; rewrite muleC mule_le0_ge0. Qed .
Lemma mule_lt0_lt0 x y : x < 0 -> y < 0 -> 0 < x * y.21 x < 0 -> y < 0 -> 0 < x * y
Proof .51c
by rewrite !lt_neqAle => /andP[? ?]/andP[*]; rewrite eq_sym mule_neq0 ?mule_le0 .
Qed .
Lemma mule_gt0_lt0 x y : 0 < x -> y < 0 -> x * y < 0 .21 0 < x -> y < 0 -> x * y < 0
Proof .521
rewrite lt_def !lt_neqAle => /andP[? ?]/andP[? ?].22 23 _a_ : x != 0 _b_ : 0 <= x_a1_ : y != 0 _b1_ : y <= 0
(x * y != 0 ) && (x * y <= 0 )
by rewrite mule_neq0 ?mule_ge0_le0 .
Qed .
Lemma mule_lt0_gt0 x y : x < 0 -> 0 < y -> x * y < 0 .21 x < 0 -> 0 < y -> x * y < 0
Proof .52f
by move => x0 y0; rewrite muleC mule_gt0_lt0. Qed .
Lemma gte_opp x : 0 < x -> - x < x.
Proof .534
by case : x => //= r; rewrite !lte_fin; apply : gtr_opp. Qed .
Lemma realMe x y : (0 %E >=< x)%O -> (0 %E >=< y)%O -> (0 %E >=< x * y)%O.21 (0 %E >=< x)%O -> (0 %E >=< y)%O -> (0 %E >=< x * y)%O
Proof .539
case : x y => [x||] [y||]// rx ry;
do ?[exact : realM
|by rewrite /mule/= lt0y
|by rewrite real_mulr_infty ?realE -?lee_fin // /Num.sg;
case : ifP; [|case : ifP]; rewrite ?mul0e /Order.comparable ?lexx ;
rewrite ?mulN1e ?leNy0 ?mul1e ?le0y
|by rewrite mulNyNy /Order.comparable le0y].
Qed .
Lemma abse_ge0 x : 0 <= `|x|.
Proof .53e
by move : x => [x| |] /=; rewrite ?le0y ?lee_fin . Qed .
Lemma gee0_abs x : 0 <= x -> `|x| = x.
Proof .543
by move : x => [x| |]//; rewrite lee_fin => x0; apply /eqP; rewrite eqe ger0_norm.
Qed .
Lemma gte0_abs x : 0 < x -> `|x| = x. Proof .548
by move => /ltW/gee0_abs. Qed .
Lemma lee0_abs x : x <= 0 -> `|x| = - x.
Proof .54d
by move : x => [x| |]//; rewrite lee_fin => x0; apply /eqP; rewrite eqe ler0_norm.
Qed .
Lemma lte0_abs x : x < 0 -> `|x| = - x.
Proof .552
by move => /ltW/lee0_abs. 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 "x *? y" := (mule_def x%dE y%dE) : ereal_dual_scope.
Notation "x *? y" := (mule_def x y) : ereal_scope.
Notation maxe := (@Order.max ereal_display _).
Notation "@ 'maxe' R" := (@Order.max ereal_display R)
(at level 10 , R at level 8 , only parsing ) : fun_scope.
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 .557
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.22 19a r : seq I 1df 339
\sum_(i <- r | P i) F i =
- (\sum_(i <- r | P i) - F i)%E
Proof .55c
apply : (big_ind2 (fun x y => x = - y)%E) => [|_ x _ y -> ->|i _].
- 563
by rewrite oppe0.
- 56f
by rewrite dual_addeE !oppeK.
- 574
by rewrite oppeK.
Qed .
Lemma dual_addeE_def x y : x +? y -> (x + y)%dE = (x + y)%E.21 (x +? y)%E -> x + y = (x + y)%E
Proof .578
by case : x => [x| |]; case : y. Qed .
Lemma dEFinD (r r' : R) : (r + r')%R%:E = r%:E + r'%:E.186
Proof .18b by []. Qed .
Lemma dEFinB (r r' : R) : (r - r')%R%:E = r%:E - r'%:E.18d
Proof .190 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.22 19a 55f 19c 19d
\sum_(i <- r | P i) (F i)%:E =
(\sum_(i <- r | P i) F i)%:E
Proof .57f
by rewrite dual_sumeE fin_num_sumeN// oppeK sumEFin. Qed .
Lemma daddeC : commutative (S := \bar R) +%dE.
Proof .585
by move => x y; rewrite !dual_addeE addeC. Qed .
Lemma dadde0 : right_id (0 : \bar R) +%dE.29 right_id (0 : \bar R) +%dE
Proof .58a
by move => x; rewrite dual_addeE eqe_oppLRP oppe0 adde0. Qed .
Lemma dadd0e : left_id (0 : \bar R) +%dE.29 left_id (0 : \bar R) +%dE
Proof .58f
by move => x;rewrite dual_addeE eqe_oppLRP oppe0 add0e. Qed .
Lemma daddeA : associative (S := \bar R) +%dE.
Proof .594
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 .599
exact : Monoid.mulmAC. Qed .
Lemma daddeCA : left_commutative (S := \bar R) +%dE.
Proof .59e
exact : Monoid.mulmCA. Qed .
Lemma daddeACA : @interchange (\bar R) +%dE +%dE.
Proof .5a3
exact : Monoid.mulmACA. Qed .
Lemma realDed x y : (0 %E >=< x)%O -> (0 %E >=< y)%O -> (0 %E >=< x + y)%O.210
Proof .213 case : x y => [x||] [y||] //; exact : realD. Qed .
Lemma doppeD x y : x +? y -> - (x + y) = - x - y.21 (x +? y)%E -> - (x + y) = - x - y
Proof .5a9
by move : x y => [x| |] [y| |] //= _; rewrite opprD. Qed .
Lemma fin_num_doppeD x y : y \is a fin_num -> - (x + y) = - x - y.233
Proof .236 by move => finy; rewrite doppeD// fin_num_adde_defl. Qed .
Lemma dsube0 x : x - 0 = x.238
Proof .23b by move : x => [x| |] //; rewrite -dEFinB subr0. Qed .
Lemma dsub0e x : 0 - x = - x.23d
Proof .240 by move : x => [x| |] //; rewrite -dEFinB sub0r. Qed .
Lemma doppeB x y : x +? - y -> - (x - y) = - x + y.21 (x +? (- y)%dE)%E -> - (x - y) = - x + y
Proof .5b1
by move => xy; rewrite doppeD// oppeK. Qed .
Lemma fin_num_doppeB x y : y \is a fin_num -> - (x - y) = - x + y.2e9
Proof .2ec by move => ?; rewrite doppeB// fin_num_adde_defl// fin_numN. Qed .
Lemma dfin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).2ee
Proof .2f1 by move : x y => [x| |] [y| |]. Qed .
Lemma dfineD :
{in (@fin_num R) &, {morph fine : x y / x + y >-> (x + y)%R}}.31c
Proof .31f by move => [r| |] [s| |]. Qed .
Lemma dfineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.321
Proof .324 by move => [r| |] [s| |]. Qed .
Lemma daddeK x y : x \is a fin_num -> y + x - x = y.365
Proof .368 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.36a
Proof .36d by move => fy; rewrite !dual_addeE oppeK subeK ?oppeK ; case : y fy. Qed .
Lemma dsubee x : x \is a fin_num -> x - x = 0 .36f
Proof .372 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).1b7 x \is a fin_num ->
(y +? z)%E -> (x - z == y) = (x == y + z)
Proof .5bd
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)).21 (x + y == +oo) = (x == +oo) || (y == +oo)
Proof .5c2
by move : x y => [?| |] [?| |]. Qed .
Lemma daddye x : +oo + x = +oo. Proof .5c7
by []. Qed .
Lemma daddey x : x + +oo = +oo. Proof .5cc
by case : x. Qed .
Lemma daddNye x : x != +oo -> -oo + x = -oo.6a x != +oo -> -oo + x = -oo
Proof .5d1
by case : x. Qed .
Lemma daddeNy x : x != +oo -> x + -oo = -oo.6a x != +oo -> x + -oo = -oo
Proof .5d6
by case : x. Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" ,
note="renamed `daddye` and generalized" )]
Lemma daddooe x : x != -oo -> +oo + x = +oo. 37e
Proof .381 by rewrite daddye. Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" ,
note="renamed `daddey` and generalized" )]
Lemma daddeoo x : x != -oo -> x + +oo = +oo. 383
Proof .386 by rewrite daddey. Qed .
Lemma dadde_Neq_pinfty x y : x != -oo -> y != -oo ->
(x + y != +oo) = (x != +oo) && (y != +oo).392
Proof .395 by move : x y => [x| |] [y| |]. Qed .
Lemma dadde_Neq_ninfty x y : x != +oo -> y != +oo ->
(x + y != -oo) = (x != -oo) && (y != -oo).397
Proof .39a by move : x y => [x| |] [y| |]. Qed .
Lemma ndadde_eq0 x y : x <= 0 -> y <= 0 -> x + y == 0 = (x == 0 ) && (y == 0 ).207
Proof .20a
move : x y => [x||] [y||] //.94 (x%:E <= 0 )%E ->
(y%:E <= 0 )%E ->
(x%:E + y%:E == 0 %E) = (x%:E == 0 %E) && (y%:E == 0 %E)
- 5e0
by rewrite !lee_fin -dEFinD !eqe; exact : naddr_eq0.
- 5e8
by rewrite /adde/= (_ : -oo == 0 = false)// andbF.
Qed .
Lemma pdadde_eq0 x y : 0 <= x -> 0 <= y -> x + y == 0 = (x == 0 ) && (y == 0 ).1fe
Proof .201
move : x y => [x||] [y||] //.94 (0 <= x%:E)%E ->
(0 <= y%:E)%E ->
(x%:E + y%:E == 0 %E) = (x%:E == 0 %E) && (y%:E == 0 %E)
- 5ed
by rewrite !lee_fin -dEFinD !eqe; exact : paddr_eq0.
- 5f5
by rewrite /adde/= (_ : +oo == 0 = false)// andbF.
Qed .
Lemma dadde_ss_eq0 x y : (0 <= x) && (0 <= y) || (x <= 0 ) && (y <= 0 ) ->
x + y == 0 = (x == 0 ) && (y == 0 ).39c
Proof .39f move => /orP[|] /andP[]; [exact : pdadde_eq0|exact : ndadde_eq0]. Qed .
Lemma desum_eqyP (T : eqType) (s : seq 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].2fe \sum_(i <- s | P i) f i = +oo <->
(exists i : T, [/\ i \in s, P i & f i = +oo])
Proof .5fa
rewrite dual_sumeE eqe_oppLRP /= esum_eqNyP.2fe (exists i : T, [/\ i \in s, P i & (- f i)%E = -oo%E]) <->
(exists i : T, [/\ i \in s, P i & f i = +oo%E])
by split => -[i + /ltac :(exists i )] => [|] []; [|split ]; rewrite // eqe_oppLRP.
Qed .
Lemma desum_eqy (I : finType) (f : I -> \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == +oo) = [exists i in P , f i == +oo].3d7 (\sum_(i | P i) f i == +oo) =
[exists i in P , f i == +oo]
Proof .603
rewrite dual_sumeE eqe_oppLR esum_eqNy.3d7 [exists i in P , (- f i)%E == -oo%E] =
[exists i in P , f i == +oo%E]
by under eq_existsb => i do rewrite eqe_oppLR.
Qed .
Lemma desum_eqNyP
(T : eqType) (s : seq 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].2fe (forall i : T, P i -> f i != +oo) ->
\sum_(i <- s | P i) f i = -oo <->
(exists i : T, [/\ i \in s, P i & f i = -oo])
Proof .60c
move => fioo.22 2ff 2f6 2f7 2f8 fioo : forall i : T, P i -> f i != +oo
3a3
rewrite dual_sumeE eqe_oppLRP /= esum_eqyP => [|i Pi]; last first .22 2ff 2f6 2f7 2f8 614 3ac 3ae
(- f i)%E != -oo%E
by rewrite eqe_oppLR fioo.
by split => -[i + /ltac :(exists i )] => [|] []; [|split ]; rewrite // eqe_oppLRP.
Qed .
Lemma desum_eqNy (I : finType) (f : I -> \bar R) (P : {pred I}) :
(forall i , f i != +oo) ->
(\sum_(i | P i) f i == -oo) = [exists i in P , f i == -oo].3d7 (forall i : I, f i != +oo) ->
(\sum_(i | P i) f i == -oo) =
[exists i in P , f i == -oo]
Proof .621
move => finoo.22 3d8 1e0 3d9 finoo : forall i : I, f i != +oo
3da
rewrite dual_sumeE eqe_oppLR /= esum_eqy => [|i]; rewrite ?eqe_oppLR //.628 [exists i in P , (- f i)%E == +oo%E] =
[exists i in P , f i == -oo%E]
by under eq_existsb => i do rewrite eqe_oppLR.
Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `desum_eqNyP`" )]
Notation desum_ninftyP := desum_eqNyP.
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `desum_eqNy`" )]
Notation desum_ninfty := desum_eqNy.
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `desum_eqyP`" )]
Notation desum_pinftyP := desum_eqyP.
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `desum_eqy`" )]
Notation desum_pinfty := desum_eqy.
Lemma dadde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.42a
Proof .42d rewrite dual_addeE oppe_ge0 -!oppe_le0; exact : adde_le0. Qed .
Lemma dadde_le0 x y : x <= 0 -> y <= 0 -> x + y <= 0 .42f
Proof .42f
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.44a (forall n : T, P n -> 0 <= f n) ->
forall l : seq T, 0 <= \sum_(i <- l | P i) f i
Proof .632
move => u0 l; rewrite dual_sumeE oppe_ge0 sume_le0 // => t Pt.22 6 2f8 2f7 u0 : forall n : T, P n -> 0 <= f nl : seq T t : T Pt : P t
(- f t <= 0 )%E
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 .44a (forall n : T, P n -> f n <= 0 ) ->
forall l : seq T, \sum_(i <- l | P i) f i <= 0
Proof .640
move => u0 l; rewrite dual_sumeE oppe_le0 sume_ge0 // => t Pt.22 6 2f8 2f7 u0 : forall n : T, P n -> f n <= 0 63b 63c 63d
(0 <= - f t)%E
rewrite oppe_ge0; exact : u0.
Qed .
Lemma gte_dopp (r : \bar R) : (0 < r)%E -> (- r < r)%E.22 r : \bar R
(0 < r)%E -> (- r < r)%E
Proof .64b
by case : r => //= r; rewrite !lte_fin; apply : gtr_opp. Qed .
Lemma ednatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.125
Proof .12a by elim : n => //= n ->. Qed .
Lemma ednatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.12c
Proof .12f by elim : n => //= n ->. Qed .
Lemma EFin_dnatmul (r : R) n : (r *+ n.+1 )%:E = r%:E *+ n.+1 .131
Proof .135 by elim : n => //= n <-. Qed .
Lemma ednatmulE x n : x *+ n = (x *+ n)%E.
Proof .655
case : x => [x| |]; case : n => [//|n].22 9a 128
x%:E *+ n.+1 = (x%:E *+ n.+1 )%E
- 65a
by rewrite -EFin_natmul -EFin_dnatmul.
- 665
by rewrite enatmul_pinfty ednatmul_pinfty.
- 66a
by rewrite enatmul_ninfty ednatmul_ninfty.
Qed .
Lemma dmule2n x : x *+ 2 = x + x.137
Proof .13a by []. Qed .
End DualERealArithTh_numDomainType .
End DualAddTheoryNumDomain .
Section ERealArithTh_realDomainType .
Context {R : realDomainType}.
Implicit Types (x y z u a b : \bar R) (r : R).
Lemma fin_numElt x : (x \is a fin_num) = (-oo < x < +oo).d3 (x \is a fin_num) = (-oo < x < +oo)
Proof .66f
by rewrite fin_numE -leye_eq -leeNy_eq -2 !ltNge. Qed .
Lemma fin_numPlt x : reflect (-oo < x < +oo) (x \is a fin_num).d3 reflect (-oo < x < +oo) (x \is a fin_num)
Proof .674
by rewrite fin_numElt; exact : idP. Qed .
Lemma ltey_eq x : (x < +oo) = (x \is a fin_num) || (x == -oo).d3 (x < +oo) = (x \is a fin_num) || (x == -oo)
Proof .679
by case : x => // x //=; exact : ltry. Qed .
Lemma ltNye_eq x : (-oo < x) = (x \is a fin_num) || (x == +oo).d3 (-oo < x) = (x \is a fin_num) || (x == +oo)
Proof .67e
by case : x => // x //=; exact : ltNyr. Qed .
Lemma ge0_fin_numE x : 0 <= x -> (x \is a fin_num) = (x < +oo).d3 0 <= x -> (x \is a fin_num) = (x < +oo)
Proof .683
by move : x => [x| |] => // x0; rewrite fin_numElt ltNyr. Qed .
Lemma le0_fin_numE x : x <= 0 -> (x \is a fin_num) = (-oo < x).d3 x <= 0 -> (x \is a fin_num) = (-oo < x)
Proof .688
by move : x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed .
Lemma eqyP x : x = +oo <-> (forall A , (0 < A)%R -> A%:E <= x).d3 x = +oo <-> (forall A : R, (0 < A)%R -> A%:E <= x)
Proof .68d
split => [-> // A A0|Ax]; first by rewrite leey.cd 6b Ax : forall A : R, (0 < A)%R -> A%:E <= x
x = +oo
apply /eqP; rewrite eq_le leey /= leNgt; apply /negP.
case : x Ax => [x Ax _|//|/(_ _ ltr01)//].cd 9a Ax : forall A : R, (0 < A)%R -> A%:E <= x%:E
False
suff : ~ x%:E < (Order.max 0 x + 1 )%:E.69e ~ x%:E < (Num.max 0 x + 1 )%:E -> False
by apply ; rewrite lte_fin ltr_spaddr// le_maxr lexx orbT.
by apply /negP; rewrite -leNgt; apply /Ax/ltr_spaddr; rewrite // le_maxr lexx.
Qed .
#[deprecated(since="mathcomp-analysis 0.6.0" , note="renamed `eqyP`" )]
Notation eq_pinftyP := eqyP.
Lemma seq_psume_eq0 (I : choiceType) (r : seq I)
(P : pred I) (F : I -> \bar R) : (forall i , P i -> 0 <= F i)%E ->
(\sum_(i <- r | P i) F i == 0 )%E = all (fun i => P i ==> (F i == 0 %E)) r.cd I : choiceType 55f 1df 339
(forall i : I, P i -> 0 <= F i) ->
(\sum_(i <- r | P i) F i == 0 ) =
all (fun i : I => P i ==> (F i == 0 )) r
Proof .6ac
move => F0; apply /eqP/allP => PF0; last first .cd 6af 55f 1df 339 F0 : forall i : I, P i -> 0 <= F iPF0 : {in r, forall x : I, P x ==> (F x == 0 )}
\sum_(i <- r | P i) F i = 0
rewrite big_seq_cond big1// => i /andP[ir Pi].cd 6af 55f 1df 339 6b6 6b7 3e3 ir : i \in r 3ae
F i = 0
6b9
by have := PF0 _ ir; rewrite Pi implyTb => /eqP.
move => i ir; apply /implyP => Pi; apply /eqP.cd 6af 55f 1df 339 6b6 6bc 3e3 6c2 3ae
6c3
have rPF : {in r, forall i , P i ==> (F i \is a fin_num)}.6ca {in r, forall i : I, P i ==> (F i \is a fin_num)}
move => j jr; apply /implyP => Pj; rewrite fin_numElt; apply /andP; split .cd 6af 55f 1df 339 6b6 6bc 3e3 6c2 3ae j : I jr : j \in r Pj : P j
-oo < F j
by rewrite (lt_le_trans _ (F0 _ Pj))// ltNyr.
rewrite ltNge; apply /eqP; rewrite leye_eq; apply /eqP/negP => /eqP Fjoo.cd 6af 55f 1df 339 6b6 6bc 3e3 6c2 3ae 6d7 6d8 6d9 Fjoo : F j = +oo
6a0
have PFninfty k : P k -> F k != -oo%E.cd 6af 55f 1df 339 6b6 6bc 3e3 6c2 3ae 6d7 6d8 6d9 6e5 k : I
P k -> F k != -oo
by move => Pk; rewrite gt_eqF// (lt_le_trans _ (F0 _ Pk))// ltNyr.
have /esum_eqyP : exists i , [/\ i \in r, P i & F i = +oo%E] by exists j .6f2 ((forall i : I, P i -> F i != -oo) ->
\sum_(i0 <- r | P i0) F i0 = +oo) -> False
6e6
by move => /(_ PFninfty); rewrite PF0.
have ? : (\sum_(i <- r | P i) (fine \o F) i == 0 )%R.6d1 (\sum_(i <- r | P i) (fine \o F) i)%R == 0 %R
apply /eqP/EFin_inj; rewrite big_seq_cond -sumEFin.6d1 \sum_(i <- r | (i \in r) && P i) ((fine \o F) i)%:E =
0
702
rewrite (eq_bigr (fun i0 => F i0)); last first .6d1 forall i : I,
(i \in r) && P i -> ((fine \o F) i)%:E = F i
move => j /andP[jr Pj] /=; rewrite fineK//.cd 6af 55f 1df 339 6b6 6bc 3e3 6c2 3ae 6d2 6d7 6d8 6d9
F j \is a fin_num
70e
by have := rPF _ jr; rewrite Pj implyTb.
by rewrite -big_seq_cond PF0.
have /allP/(_ _ ir) : all (fun i => P i ==> ((fine \o F) i == 0 ))%R r.704 all (fun i : I => P i ==> ((fine \o F) i == 0 %R)) r
by rewrite -psumr_eq0// => j Pj/=; apply /fine_ge0/F0.
rewrite Pi implyTb => /= => /eqP Fi0.cd 6af 55f 1df 339 6b6 6bc 3e3 6c2 3ae 6d2 705 Fi0 : fine (F i) = 0 %R
6c3
rewrite -(@fineK _ (F i))//; last by have := rPF _ ir; rewrite Pi implyTb.
by rewrite Fi0.
Qed .
Lemma lte_add_pinfty x y : x < +oo -> y < +oo -> x + y < +oo.cd 23
x < +oo -> y < +oo -> x + y < +oo
Proof .730
by move : x y => -[r [r'| |]| |] // ? ?; rewrite -EFinD ltry. Qed .
Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I -> \bar R) :
(forall i , P i -> f i < +oo) -> \sum_(i <- s | P i) f i < +oo.cd 19a 19b 1df 1e0
(forall i : I, P i -> f i < +oo) ->
\sum_(i <- s | P i) f i < +oo
Proof .736
elim /big_ind : _ => [_|x y xoo yoo foo|i ?]; [exact : ltry| |exact ].cd 19a 19b 1df 1e0 23 xoo : (forall i : I, P i -> f i < +oo) -> x < +oo yoo : (forall i : I, P i -> f i < +oo) -> y < +oo foo : forall i : I, P i -> f i < +oo
x + y < +oo
by apply : lte_add_pinfty; [exact : xoo| exact : yoo].
Qed .
Lemma sube_gt0 x y : (0 < y - x) = (x < y).
Proof .744
by move : x y => [r | |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin subr_gt0.
Qed .
Lemma sube_le0 x y : (y - x <= 0 ) = (y <= x).732 (y - x <= 0 ) = (y <= x)
Proof .749
by rewrite !leNgt sube_gt0. Qed .
Lemma suber_ge0 y x : y \is a fin_num -> (0 <= x - y) = (y <= x).cd y, x : \bar R
y \is a fin_num -> (0 <= x - y) = (y <= x)
Proof .74e
by move : x y => [x| |] [y| |] //= _; rewrite ?(leey, lee_fin, subr_ge0).
Qed .
Lemma subre_ge0 x y : y \is a fin_num -> (0 <= y - x) = (x <= y).732 y \is a fin_num -> (0 <= y - x) = (x <= y)
Proof .755
by move : x y => [x| |] [y| |] //=; rewrite ?(leey, leNye, lee_fin) //= subr_ge0.
Qed .
Lemma sube_ge0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(0 <= y - x) = (x <= y).732 (x \is a fin_num) || (y \is a fin_num) ->
(0 <= y - x) = (x <= y)
Proof .75a
by move => /orP[?|?]; [rewrite suber_ge0|rewrite subre_ge0]. Qed .
Lemma lte_oppl x y : (- x < y) = (- y < x).
Proof .75f
by move : x y => [r| |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin ltr_oppl.
Qed .
Lemma lte_oppr x y : (x < - y) = (y < - x).
Proof .764
by move : x y => [r| |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin ltr_oppr.
Qed .
Lemma lee_oppr x y : (x <= - y) = (y <= - x).732 (x <= - y) = (y <= - x)
Proof .769
by move : x y => [r0| |] [r1| |] //=; rewrite ?(leey, leNye)// !lee_fin ler_oppr.
Qed .
Lemma lee_oppl x y : (- x <= y) = (- y <= x).732 (- x <= y) = (- y <= x)
Proof .76e
by move : x y => [r0| |] [r1| |] //=; rewrite ?(leey, leNye)// !lee_fin ler_oppl.
Qed .
Lemma muleN x y : x * - y = - (x * y).
Proof .773
move : x y => [x| |] [y| |] //=; rewrite /mule/=; try by rewrite ltry.cd 95
(x * - y)%:E = (- (x * y))%:E
- 778
by rewrite mulrN.
- 789
by rewrite !eqe !lte_fin; case : ltrgtP => //; rewrite oppe0.
- 78e
by rewrite !eqe !lte_fin; case : ltrgtP => //; rewrite oppe0.
- 793
rewrite !eqe oppr_eq0 eq_sym; case : ifP; rewrite ?oppe0 // => y0.cd 9e y0 : (0 %R == y) = false
(if 0 < (- y)%:E then +oo else -oo) =
- (if 0 < y%:E then +oo else -oo)
795
by rewrite [RHS]fun_if ltNge if_neg EFinN lee_oppl oppe0 le_eqVlt eqe y0.
- 79e
rewrite !eqe oppr_eq0 eq_sym; case : ifP; rewrite ?oppe0 // => y0.79a (if 0 < (- y)%:E then -oo else +oo) =
- (if 0 < y%:E then -oo else +oo)
by rewrite [RHS]fun_if ltNge if_neg EFinN lee_oppl oppe0 le_eqVlt eqe y0.
Qed .
Lemma mulNe x y : - x * y = - (x * y). Proof .7a6
by rewrite muleC muleN muleC. Qed .
Lemma muleNN x y : - x * - y = x * y. Proof .7ab
by rewrite mulNe muleN oppeK. Qed .
Lemma mulry r : r%:E * +oo%E = (Num.sg r)%:E * +oo%E.cc r%:E * +oo = (Num.sg r)%:E * +oo
Proof .7b0
by rewrite [LHS]real_mulry// num_real. Qed .
Lemma mulyr r : +oo%E * r%:E = (Num.sg r)%:E * +oo%E.cc +oo * r%:E = (Num.sg r)%:E * +oo
Proof .7b5
by rewrite muleC mulry. Qed .
Lemma mulrNy r : r%:E * -oo%E = (Num.sg r)%:E * -oo%E.cc r%:E * -oo = (Num.sg r)%:E * -oo
Proof .7ba
by rewrite [LHS]real_mulrNy// num_real. Qed .
Lemma mulNyr r : -oo%E * r%:E = (Num.sg r)%:E * -oo%E.cc -oo * r%:E = (Num.sg r)%:E * -oo
Proof .7bf
by rewrite muleC mulrNy. Qed .
Definition mulr_infty := (mulry, mulyr, mulrNy, mulNyr).
Lemma lte_mul_pinfty x y : 0 <= x -> x \is a fin_num -> y < +oo -> x * y < +oo.732 0 <= x -> x \is a fin_num -> y < +oo -> x * y < +oo
Proof .7c4
move : x y => [x| |] [y| |] // x0 xfin _; first by rewrite -EFinM ltry.cd 9a x0 : 0 <= x%:Exfin : x%:E \is a fin_num
x%:E * -oo < +oo
rewrite mulr_infty; move : x0; rewrite lee_fin le_eqVlt => /predU1P[<-|x0].cd 9a 7cd
(Num.sg 0 )%:E * -oo < +oo
- 7d0
by rewrite sgr0 mul0e ltry.
- 7da
by rewrite gtr0_sg // mul1e.
Qed .
Lemma mule_ge0_gt0 x y : 0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y).732 0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y)
Proof .7de
move : x y => [x| |] [y| |] //; rewrite ?lee_fin .77a (0 <= x)%R ->
(0 <= y)%R ->
(0 < x%:E * y%:E) = (0 < x%:E) && (0 < y%:E)
- 7e3
by move => x0 y0; rewrite !lte_fin; exact : mulr_ge0_gt0.
- 7ef
rewrite le_eqVlt => /predU1P[<-|x0] _; first by rewrite mul0e ltxx.cd 9a 4ca
(0 < x%:E * +oo) = (0 < x%:E) && (0 < +oo)
7f1
by rewrite ltry andbT mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- 7f9
move => _; rewrite le_eqVlt => /predU1P[<-|x0].783 (0 < +oo * 0 ) = (0 < +oo) && (0 < 0 )
by rewrite mule0 ltxx andbC.
by rewrite ltry/= mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- 80a
by move => _ _; rewrite mulyy ltry.
Qed .
Lemma gt0_mulye x : (0 < x -> +oo * x = +oo)%E.
Proof .80e
move : x => [x|_|//]; last by rewrite mulyy.77e 0 < x%:E -> +oo * x%:E = +oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty gtr0_sg// mul1e.
Qed .
Lemma lt0_mulye x : (x < 0 -> +oo * x = -oo)%E.
Proof .817
move : x => [x|//|_]; last by rewrite mulyNy.77e x%:E < 0 -> +oo * x%:E = -oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty ltr0_sg// mulN1e.
Qed .
Lemma gt0_mulNye x : (0 < x -> -oo * x = -oo)%E.
Proof .820
move : x => [x|_|//]; last by rewrite mulNyy.77e 0 < x%:E -> -oo * x%:E = -oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty gtr0_sg// mul1e.
Qed .
Lemma lt0_mulNye x : (x < 0 -> -oo * x = +oo)%E.
Proof .829
move : x => [x|//|_]; last by rewrite mulNyNy.77e x%:E < 0 -> -oo * x%:E = +oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty ltr0_sg// mulN1e.
Qed .
Lemma gt0_muley x : (0 < x -> x * +oo = +oo)%E.
Proof .832
by move => /gt0_mulye; rewrite muleC; apply . Qed .
Lemma lt0_muley x : (x < 0 -> x * +oo = -oo)%E.
Proof .837
by move => /lt0_mulye; rewrite muleC; apply . Qed .
Lemma gt0_muleNy x : (0 < x -> x * -oo = -oo)%E.
Proof .83c
by move => /gt0_mulNye; rewrite muleC; apply . Qed .
Lemma lt0_muleNy x : (x < 0 -> x * -oo = +oo)%E.
Proof .841
by move => /lt0_mulNye; rewrite muleC; apply . Qed .
Lemma mule_eq_pinfty x y : (x * y == +oo) =
[|| (x > 0 ) && (y == +oo), (x < 0 ) && (y == -oo),
(x == +oo) && (y > 0 ) | (x == -oo) && (y < 0 )].732 (x * y == +oo) =
[|| (0 < x) && (y == +oo), (x < 0 ) && (y == -oo),
(x == +oo) && (0 < y)
| (x == -oo) && (y < 0 )]
Proof .846
move : x y => [x| |] [y| |]; rewrite ?(lte_fin,andbF,andbT,orbF,eqxx,andbT)//=.77e (x%:E * +oo == +oo) = (0 < x)%R
- 84b
by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0 %R;
move => ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- 85f
by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0 %R;
move => ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- 864
by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0 %R;
move => ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- 869
by rewrite mulyy ltry.
- 86e
by rewrite mulyNy.
- 873
by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0 %R;
move => ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- 878
by rewrite mulNyy.
- 87d
by rewrite ltNyr.
Qed .
Lemma mule_eq_ninfty x y : (x * y == -oo) =
[|| (x > 0 ) && (y == -oo), (x < 0 ) && (y == +oo),
(x == -oo) && (y > 0 ) | (x == +oo) && (y < 0 )].732 (x * y == -oo) =
[|| (0 < x) && (y == -oo), (x < 0 ) && (y == +oo),
(x == -oo) && (0 < y)
| (x == +oo) && (y < 0 )]
Proof .881
have := mule_eq_pinfty x (- y); rewrite muleN eqe_oppLR => ->.732 [|| (0 < x) && (- y == +oo), (x < 0 ) && (- y == -oo),
(x == +oo) && (0 < - y)
| (x == -oo) && (- y < 0 )] =
[|| (0 < x) && (y == -oo), (x < 0 ) && (y == +oo),
(x == -oo) && (0 < y)
| (x == +oo) && (y < 0 )]
by rewrite !eqe_oppLR lte_oppr lte_oppl oppe0 (orbC _ ((x == -oo) && _)).
Qed .
Lemma lte_opp x y : (- x < - y) = (y < x).
Proof .88a
by rewrite lte_oppl oppeK. Qed .
Lemma lte_add a b x y : a < b -> x < y -> a + x < b + y.cd a, b, x, y : \bar R
a < b -> x < y -> a + x < b + y
Proof .88f
move : a b x y=> [a| |] [b| |] [x| |] [y| |]; rewrite ?(ltry,ltNyr)//.cd a, b, x, y : R
a%:E < b%:E ->
x%:E < y%:E -> a%:E + x%:E < b%:E + y%:E
by rewrite !lte_fin; exact : ltr_add.
Qed .
Lemma lee_addl x y : 0 <= y -> x <= x + y.
Proof .89c
move : x y => -[ x [y| |]//= | [| |]// | [| | ]//];
by [rewrite !lee_fin ler_addl | move => _; exact : leey].
Qed .
Lemma lee_addr x y : 0 <= y -> x <= y + x.
Proof .8a1
by rewrite addeC; exact : lee_addl. Qed .
Lemma gee_addl x y : y <= 0 -> x + y <= x.
Proof .8a6
move : x y => -[ x [y| |]//= | [| |]// | [| | ]//];
by [rewrite !lee_fin ger_addl | move => _; exact : leNye].
Qed .
Lemma gee_addr x y : y <= 0 -> y + x <= x.
Proof .8ab
rewrite addeC; exact : gee_addl. Qed .
Lemma lte_addl y x : y \is a fin_num -> (y < y + x) = (0 < x).750 y \is a fin_num -> (y < y + x) = (0 < x)
Proof .8b0
by move : x y => [x| |] [y| |] _ //; rewrite ?ltry ?ltNyr // !lte_fin ltr_addl.
Qed .
Lemma lte_addr y x : y \is a fin_num -> (y < x + y) = (0 < x).750 y \is a fin_num -> (y < x + y) = (0 < x)
Proof .8b5
rewrite addeC; exact : lte_addl. Qed .
Lemma gte_subl y x : y \is a fin_num -> (y - x < y) = (0 < x).750 y \is a fin_num -> (y - x < y) = (0 < x)
Proof .8ba
move : y x => [x| |] [y| |] _ //; rewrite addeC /= ?ltNyr ?ltry //.77a ((- y)%:E + x%:E < x%:E) = (0 < y%:E)
by rewrite !lte_fin gtr_addr ltr_oppl oppr0.
Qed .
Lemma gte_subr y x : y \is a fin_num -> (- x + y < y) = (0 < x).750 y \is a fin_num -> (- x + y < y) = (0 < x)
Proof .8c3
by rewrite addeC; exact : gte_subl. Qed .
Lemma gte_addl x y : x \is a fin_num -> (x + y < x) = (y < 0 ).732 x \is a fin_num -> (x + y < x) = (y < 0 )
Proof .8c8
by move : x y => [r| |] [s| |]// _; [rewrite !lte_fin gtr_addl|rewrite !ltNyr].
Qed .
Lemma gte_addr x y : x \is a fin_num -> (y + x < x) = (y < 0 ).732 x \is a fin_num -> (y + x < x) = (y < 0 )
Proof .8cd
by rewrite addeC; exact : gte_addl. Qed .
Lemma lte_add2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b).cd x, a, b : \bar R
x \is a fin_num -> (x + a < x + b) = (a < b)
Proof .8d2
move : a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(ltry, ltNyr)//.cd a, b, x : R
(x%:E + a%:E < x%:E + b%:E) = (a%:E < b%:E)
by rewrite !lte_fin ltr_add2l.
Qed .
Lemma lee_add2l x a b : a <= b -> x + a <= x + b.8d4 a <= b -> x + a <= x + b
Proof .8df
move : a b x => -[a [b [x /=|//|//] | []// |//] | []// | ].8db a%:E <= b%:E -> x%:E + a%:E <= x%:E + b%:E
- 8e4
by rewrite !lee_fin ler_add2l.
- 8f0
by move => r _; exact : leey.
- 8f5
by move => -[b [| |]// | []// | //] r oob; exact : leNye.
Qed .
Lemma lee_add2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b).8d4 x \is a fin_num -> (x + a <= x + b) = (a <= b)
Proof .8f9
move : a b x => [a| |] [b| |] [x| |] _ //; rewrite ?(leey, leNye)//.8db (x%:E + a%:E <= x%:E + b%:E) = (a%:E <= b%:E)
by rewrite !lee_fin ler_add2l.
Qed .
Lemma lee_add2r x a b : a <= b -> a + x <= b + x.8d4 a <= b -> a + x <= b + x
Proof .902
rewrite addeC (addeC b); exact : lee_add2l. Qed .
Lemma lee_add a b x y : a <= b -> x <= y -> a + x <= b + y.891 a <= b -> x <= y -> a + x <= b + y
Proof .907
move : a b x y => [a| |] [b| |] [x| |] [y| |]; rewrite ?(leey, leNye)//.898 a%:E <= b%:E ->
x%:E <= y%:E -> a%:E + x%:E <= b%:E + y%:E
by rewrite !lee_fin; exact : ler_add.
Qed .
Lemma lte_le_add a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.891 b \is a fin_num -> a < x -> b <= y -> a + b < x + y
Proof .910
move : x y a b => [x| |] [y| |] [a| |] [b| |] _ //=; rewrite ?(ltry, ltNyr)//.cd x, y, a, b : R
a%:E < x%:E ->
b%:E <= y%:E -> a%:E + b%:E < x%:E + y%:E
by rewrite !lte_fin; exact : ltr_le_add.
Qed .
Lemma lee_lt_add a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.891 a \is a fin_num -> a <= x -> b < y -> a + b < x + y
Proof .91b
by move => afin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed .
Lemma lee_sub x y z u : x <= y -> u <= z -> x - z <= y - u.cd x, y, z, u : \bar R
x <= y -> u <= z -> x - z <= y - u
Proof .920
move : x y z u => -[x| |] -[y| |] -[z| |] -[u| |] //=; rewrite ?(leey,leNye)//.cd x, y, z, u : R
x%:E <= y%:E ->
u%:E <= z%:E -> x%:E + (- z)%:E <= y%:E + (- u)%:E
by rewrite !lee_fin; exact : ler_sub.
Qed .
Lemma lte_le_sub z u x y : u \is a fin_num ->
x < z -> u <= y -> x - y < z - u.cd z, u, x, y : \bar R
u \is a fin_num -> x < z -> u <= y -> x - y < z - u
Proof .92d
move : z u x y => [z| |] [u| |] [x| |] [y| |] _ //=; rewrite ?(ltry, ltNyr)//.cd z, u, x, y : R
x%:E < z%:E ->
u%:E <= y%:E -> x%:E + (- y)%:E < z%:E + (- u)%:E
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}.cd z : \bar R
z \is a fin_num ->
0 < z -> {mono *%E^~ z : x y / x < y >-> x < y}
Proof .93a
move : z => [z| |] _ // z0 [x| |] [y| |] //.cd z : R z0 : 0 < z%:E95
(x%:E * z%:E < y%:E * z%:E) = (x%:E < y%:E)
- 941
by rewrite !lte_fin ltr_pmul2r.
- 959
by rewrite mulr_infty gtr0_sg// mul1e 2 !ltry.
- 95e
by rewrite mulr_infty gtr0_sg// mul1e ltNge leNye ltNge leNye.
- 963
by rewrite mulr_infty gtr0_sg// mul1e ltNge leey ltNge leey.
- 968
by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
- 96d
by rewrite mulr_infty gtr0_sg// mul1e 2 !ltNyr.
- 972
by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
Qed .
Lemma lte_pmul2l z : z \is a fin_num -> 0 < z -> {mono *%E z : x y / x < y}.93c z \is a fin_num ->
0 < z -> {mono *%E z : x y / x < y >-> x < y}
Proof .976
by move => zfin z0 x y; rewrite 2 !(muleC z) lte_pmul2r. Qed .
Lemma lte_nmul2l z : z \is a fin_num -> z < 0 -> {mono *%E z : x y /~ x < y}.93c z \is a fin_num ->
z < 0 -> {mono *%E z : y x / x < y >-> y < x}
Proof .97b
rewrite -oppe0 lte_oppr => zfin z0 x y.cd 93d zfin : z \is a fin_num z0 : 0 < - z23
(z * x < z * y) = (y < x)
by rewrite -(oppeK z) !mulNe lte_oppl oppeK -2 !mulNe lte_pmul2l ?fin_numN .
Qed .
Lemma lte_nmul2r z : z \is a fin_num -> z < 0 -> {mono *%E^~ z : x y /~ x < y}.93c z \is a fin_num ->
z < 0 -> {mono *%E^~ z : y x / x < y >-> y < x}
Proof .987
by move => zfin z0 x y; rewrite -!(muleC z) lte_nmul2l. Qed .
Lemma lee_sum 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.cd 19a f, g : I -> \bar R 19b 1df
(forall i : I, P i -> f i <= g i) ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | P i) g i
Proof .98c
by move => Pfg; elim /big_ind2 : _ => // *; apply lee_add. Qed .
Lemma lee_sum_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.cd 19a 19b P, Q : {pred I} 1e0
{subset Q <= P} ->
{in [predD P & Q], forall i : I, 0 <= f i} ->
\sum_(i <- s | Q i) f i <= \sum_(i <- s | P i) f i
Proof .993
move => QP PQf; rewrite big_mkcond [leRHS]big_mkcond lee_sum// => i.cd 19a 19b 996 1e0 QP : {subset Q <= P} PQf : {in [predD P & Q], forall i : I, 0 <= f i} 3e3
true ->
(if Q i then f i else 0 ) <= (if P i then f i else 0 )
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.995 {subset Q <= P} ->
{in [predD P & Q], forall i : I, f i <= 0 } ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | Q i) f i
Proof .9a1
move => QP PQf; rewrite big_mkcond [leRHS]big_mkcond lee_sum// => i.cd 19a 19b 996 1e0 99d PQf : {in [predD P & Q], forall i : I, f i <= 0 } 3e3
true ->
(if P i then f i else 0 ) <= (if Q i then f i else 0 )
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.cd I : eqType 19b P, Q : pred I 1e0
(forall i : 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 .9ac
move => PQf; rewrite [leRHS](bigID Q) /= -[leLHS]adde0 lee_add //.cd 9af 19b 9b0 1e0 PQf : forall i : I, P i -> ~~ Q i -> 0 <= f i
0 <= \sum_(i <- s | P i && ~~ Q i) f i
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.9ae (forall i : 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 .9ba
move => PQf; rewrite [leLHS](bigID Q) /= -[leRHS]adde0 lee_add //.cd 9af 19b 9b0 1e0 PQf : forall i : I, P i -> ~~ Q i -> f i <= 0
\sum_(i <- s | P i && ~~ Q i) f i <= 0
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}.cd 35a P : pred nat
(forall n : nat, P n -> 0 <= f n) ->
{homo (fun n : nat => \sum_(i < n | P i) f i) : i j /
(i <= j)%N >-> i <= j}
Proof .9c5
move => f0 i j le_ij; rewrite (big_ord_widen_cond j) // big_mkcondr /=.cd 35a 9c8 f0 : forall n : nat, P n -> 0 <= f ni, j : nat le_ij : (i <= j)%N
\sum_(i0 < j | P i0) (if (i0 < i)%N then f i0 else 0 ) <=
\sum_(i < j | P i) f i
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 ) ->
{homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.9c7 (forall n : nat, P n -> f n <= 0 ) ->
{homo (fun n : nat => \sum_(i < n | P i) f i) : i j /
(i <= j)%N >-> j <= i}
Proof .9d4
move => f0 m n ?; rewrite [leRHS](big_ord_widen_cond n) // big_mkcondr /=.cd 35a 9c8 f0 : forall n : nat, P n -> f n <= 0 m, n : nat _Hyp_ : (m <= n)%N
\sum_(i < n | P i) f i <=
\sum_(i < n | P i) (if (i < m)%N then f i else 0 )
by 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}.cd 35a 9c8 m : nat
(forall n : nat, (m <= n)%N -> P n -> 0 <= f n) ->
{homo (fun n : nat => \sum_(m <= i < n | P i) f i) : i j /
(i <= j)%N >-> i <= j}
Proof .9e1
move => f0 i j le_ij; rewrite -[m]add0n !big_addn !big_mkord.cd 35a 9c8 9e4 f0 : forall n : nat, (m <= n)%N -> P n -> 0 <= f n9d0 9d1
\sum_(i0 < i - m | P (i0 + m)%N) f (i0 + m)%N <=
\sum_(i < j - m | P (i + m)%N) f (i + m)%N
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}.9e3 (forall n : nat, (m <= n)%N -> P n -> f n <= 0 ) ->
{homo (fun n : nat => \sum_(m <= i < n | P i) f i) : i j /
(i <= j)%N >-> j <= i}
Proof .9ee
move => f0 i j le_ij; rewrite -[m]add0n !big_addn !big_mkord.cd 35a 9c8 9e4 f0 : forall n : nat, (m <= n)%N -> P n -> f n <= 0 9d0 9d1
\sum_(i < j - m | P (i + m)%N) f (i + m)%N <=
\sum_(i0 < i - m | P (i0 + m)%N) f (i0 + m)%N
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}.cd 35a 9c8 128
(forall m : nat, (m < n)%N -> P m -> 0 <= f m) ->
{homo (fun m : nat => \sum_(m <= i < n | P i) f i) : i j /
(i <= j)%N >-> j <= i}
Proof .9f9
move => f0 i j le_ij; rewrite !big_geq_mkord/=.cd 35a 9c8 128 f0 : forall m : nat, (m < n)%N -> P m -> 0 <= f m9d0 9d1
\sum_(i < n | P i && (j <= i)%N) f i <=
\sum_(i0 < n | P i0 && (i <= i0)%N) f i0
rewrite lee_sum_nneg_subset// => [k | k /and3P[_ /f0->//]].cd 35a 9c8 128 a02 9d0 9d1 k : 'I_n
k \in (fun i : 'I_n => P i && (j <= i)%N) ->
k \in (fun i0 : 'I_n => P i0 && (i <= i0)%N)
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}.9fb (forall m : nat, (m < n)%N -> P m -> f m <= 0 ) ->
{homo (fun m : nat => \sum_(m <= i < n | P i) f i) : i j /
(i <= j)%N >-> i <= j}
Proof .a0b
move => f0 i j le_ij; rewrite !big_geq_mkord/=.cd 35a 9c8 128 f0 : forall m : nat, (m < n)%N -> P m -> f m <= 0 9d0 9d1
\sum_(i0 < n | P i0 && (i <= i0)%N) f i0 <=
\sum_(i < n | P i && (j <= i)%N) f i
rewrite lee_sum_npos_subset// => [k | k /and3P[_ /f0->//]].cd 35a 9c8 128 a13 9d0 9d1 a08
a09
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} ->
\sum_(t <- A | P t) f t <= \sum_(t <- B | P t) f t.cd T : choiceType A, B : {fset T} 2f7 2f8
{subset A <= B} ->
{in [predD B & A], forall t : T, P t -> 0 <= f t} ->
\sum_(t <- A | P t) f t <= \sum_(t <- B | P t) f t
Proof .a1a
move => AB f0; rewrite [leRHS]big_mkcond (big_fsetID _ (mem A) B) /=.cd a1d a1e 2f7 2f8 AB : {subset A <= B} f0 : {in [predD B & A], forall t : T, P t -> 0 <= f t}
\sum_(t <- A | P t) f t <=
\sum_(i <- [fset x | x in B & x \in A]%fset)
(if P i then f i else 0 ) +
\sum_(i <- [fset x | x in B & x \notin A]%fset)
(if P i then f i else 0 )
rewrite -[leLHS]adde0 lee_add //.a24 \sum_(t <- A | P t) f t <=
\sum_(i <- [fset x | x in B & x \in A]%fset)
(if P i then f i else 0 )
rewrite -big_mkcond /= {1 }(_ : A = [fset x in B | x \in A]%fset) //.a24 A = [fset x | x in B & x \in A]%fset
a2c
by apply /fsetP=> t; rewrite !inE /= andbC; case : (boolP (_ \in _)) => // /AB.
rewrite big_fset /= big_seq_cond sume_ge0 // => t /andP[tB tA].cd a1d a1e 2f7 2f8 a25 a26 63c tB : t \in B tA : t \notin A
0 <= (if P t then f t else 0 )
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.a1c {subset A <= B} ->
{in [predD B & A], forall t : T, P t -> f t <= 0 } ->
\sum_(t <- B | P t) f t <= \sum_(t <- A | P t) f t
Proof .a3e
move => AB f0; rewrite big_mkcond (big_fsetID _ (mem A) B) /=.cd a1d a1e 2f7 2f8 a25 f0 : {in [predD B & A], forall t : T, P t -> f t <= 0 }
\sum_(i <- [fset x | x in B & x \in A]%fset)
(if P i then f i else 0 ) +
\sum_(i <- [fset x | x in B & x \notin A]%fset)
(if P i then f i else 0 ) <= \sum_(t <- A | P t) f t
rewrite -[leRHS]adde0 lee_add //.a45 \sum_(i <- [fset x | x in B & x \in A]%fset)
(if P i then f i else 0 ) <= \sum_(t <- A | P t) f t
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].cd a1d a1e 2f7 2f8 a25 a46 63c a3a a3b
(if P t then f t else 0 ) <= 0
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).cd 1b8
y \is a fin_num -> (x - y < z) = (x < z + y)
Proof .a5b
move : x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltry ?ltNyr //.cd x, y, z : R
(x%:E + (- y)%:E < z%:E) = (x%:E < z%:E + y%:E)
by rewrite !lte_fin ltr_subl_addr.
Qed .
Lemma lte_subl_addl x y z : y \is a fin_num -> (x - y < z) = (x < y + z).a5d y \is a fin_num -> (x - y < z) = (x < y + z)
Proof .a67
by move => ?; rewrite lte_subl_addr// addeC. Qed .
Lemma lte_subr_addr x y z : z \is a fin_num -> (x < y - z) = (x + z < y).a5d z \is a fin_num -> (x < y - z) = (x + z < y)
Proof .a6c
move : x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltNyr ?ltry //.a63 (x%:E < y%:E + (- z)%:E) = (x%:E + z%:E < y%:E)
by rewrite !lte_fin ltr_subr_addr.
Qed .
Lemma lte_subr_addl x y z : z \is a fin_num -> (x < y - z) = (z + x < y).a5d z \is a fin_num -> (x < y - z) = (z + x < y)
Proof .a75
by move => ?; rewrite lte_subr_addr// addeC. Qed .
Lemma lte_subel_addr x y z : x \is a fin_num -> (x - y < z) = (x < z + y).a5d x \is a fin_num -> (x - y < z) = (x < z + y)
Proof .a7a
move : x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltNyr ?ltry //.a61
by rewrite !lte_fin ltr_subl_addr.
Qed .
Lemma lte_subel_addl x y z : x \is a fin_num -> (x - y < z) = (x < y + z).a5d x \is a fin_num -> (x - y < z) = (x < y + z)
Proof .a80
by move => ?; rewrite lte_subel_addr// addeC. Qed .
Lemma lte_suber_addr x y z : x \is a fin_num -> (x < y - z) = (x + z < y).a5d x \is a fin_num -> (x < y - z) = (x + z < y)
Proof .a85
move : x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?ltNyr ?ltry //.a70
by rewrite !lte_fin ltr_subr_addr.
Qed .
Lemma lte_suber_addl x y z : x \is a fin_num -> (x < y - z) = (z + x < y).a5d x \is a fin_num -> (x < y - z) = (z + x < y)
Proof .a8a
by move => ?; rewrite lte_suber_addr// addeC. Qed .
Lemma lee_subl_addr x y z : y \is a fin_num -> (x - y <= z) = (x <= z + y).a5d y \is a fin_num -> (x - y <= z) = (x <= z + y)
Proof .a8f
move : x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?leey ?leNye //.a63 (x%:E + (- y)%:E <= z%:E) = (x%:E <= z%:E + y%:E)
by rewrite !lee_fin ler_subl_addr.
Qed .
Lemma lee_subl_addl x y z : y \is a fin_num -> (x - y <= z) = (x <= y + z).a5d y \is a fin_num -> (x - y <= z) = (x <= y + z)
Proof .a98
by move => ?; rewrite lee_subl_addr// addeC. Qed .
Lemma lee_subr_addr x y z : z \is a fin_num -> (x <= y - z) = (x + z <= y).a5d z \is a fin_num -> (x <= y - z) = (x + z <= y)
Proof .a9d
move : y x z => [y| |] [x| |] [z| |] _ //=; rewrite ?leNye ?leey //.cd y, x, z : R
(x%:E <= y%:E + (- z)%:E) = (x%:E + z%:E <= y%:E)
by rewrite !lee_fin ler_subr_addr.
Qed .
Lemma lee_subr_addl x y z : z \is a fin_num -> (x <= y - z) = (z + x <= y).a5d z \is a fin_num -> (x <= y - z) = (z + x <= y)
Proof .aa8
by move => ?; rewrite lee_subr_addr// addeC. Qed .
Lemma lee_subel_addr x y z : z \is a fin_num -> (x - y <= z) = (x <= z + y).a5d z \is a fin_num -> (x - y <= z) = (x <= z + y)
Proof .aad
move : x y z => [x| |] [y| |] [z| |] _ //=; rewrite ?leey ?leNye //.a93
by rewrite !lee_fin ler_subl_addr.
Qed .
Lemma lee_subel_addl x y z : z \is a fin_num -> (x - y <= z) = (x <= y + z).a5d z \is a fin_num -> (x - y <= z) = (x <= y + z)
Proof .ab2
by move => ?; rewrite lee_subel_addr// addeC. Qed .
Lemma lee_suber_addr x y z : y \is a fin_num -> (x <= y - z) = (x + z <= y).a5d y \is a fin_num -> (x <= y - z) = (x + z <= y)
Proof .ab7
move : y x z => [y| |] [x| |] [z| |] _ //=; rewrite ?leNye ?leey //.aa1
by rewrite !lee_fin ler_subr_addr.
Qed .
Lemma lee_suber_addl x y z : y \is a fin_num -> (x <= y - z) = (z + x <= y).a5d y \is a fin_num -> (x <= y - z) = (z + x <= y)
Proof .abc
by move => ?; rewrite lee_suber_addr// addeC. Qed .
Lemma subre_lt0 x y : x \is a fin_num -> (x - y < 0 ) = (x < y).732 x \is a fin_num -> (x - y < 0 ) = (x < y)
Proof .ac1
by move => ?; rewrite lte_subel_addr// add0e. Qed .
Lemma suber_lt0 x y : y \is a fin_num -> (x - y < 0 ) = (x < y).732 y \is a fin_num -> (x - y < 0 ) = (x < y)
Proof .ac6
by move => ?; rewrite lte_subl_addl// adde0. Qed .
Lemma sube_lt0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(x - y < 0 ) = (x < y).732 (x \is a fin_num) || (y \is a fin_num) ->
(x - y < 0 ) = (x < y)
Proof .acb
by move => /orP[?|?]; [rewrite subre_lt0|rewrite suber_lt0]. Qed .
Lemma pmule_rge0 x y : 0 < x -> (x * y >= 0 ) = (y >= 0 ).732 0 < x -> (0 <= x * y) = (0 <= y)
Proof .ad0
move => x_gt0; apply /idP/idP; last exact /mule_ge0/ltW.cd 23 x_gt0 : 0 < x
0 <= x * y -> 0 <= y
by apply : contra_le; apply : mule_gt0_lt0.
Qed .
Lemma pmule_lge0 x y : 0 < x -> (y * x >= 0 ) = (y >= 0 ).732 0 < x -> (0 <= y * x) = (0 <= y)
Proof .adb
by rewrite muleC; apply : pmule_rge0. Qed .
Lemma pmule_rlt0 x y : 0 < x -> (x * y < 0 ) = (y < 0 ).732 0 < x -> (x * y < 0 ) = (y < 0 )
Proof .ae0
by move => /pmule_rge0; rewrite !ltNge => ->. Qed .
Lemma pmule_llt0 x y : 0 < x -> (y * x < 0 ) = (y < 0 ).732 0 < x -> (y * x < 0 ) = (y < 0 )
Proof .ae5
by rewrite muleC; apply : pmule_rlt0. Qed .
Lemma pmule_rle0 x y : 0 < x -> (x * y <= 0 ) = (y <= 0 ).732 0 < x -> (x * y <= 0 ) = (y <= 0 )
Proof .aea
by move => xgt0; rewrite -oppe_ge0 -muleN pmule_rge0 ?oppe_ge0 . Qed .
Lemma pmule_lle0 x y : 0 < x -> (y * x <= 0 ) = (y <= 0 ).732 0 < x -> (y * x <= 0 ) = (y <= 0 )
Proof .aef
by rewrite muleC; apply : pmule_rle0. Qed .
Lemma pmule_rgt0 x y : 0 < x -> (x * y > 0 ) = (y > 0 ).732 0 < x -> (0 < x * y) = (0 < y)
Proof .af4
by move => xgt0; rewrite -oppe_lt0 -muleN pmule_rlt0 ?oppe_lt0 . Qed .
Lemma pmule_lgt0 x y : 0 < x -> (y * x > 0 ) = (y > 0 ).732 0 < x -> (0 < y * x) = (0 < y)
Proof .af9
by rewrite muleC; apply : pmule_rgt0. Qed .
Lemma nmule_rge0 x y : x < 0 -> (x * y >= 0 ) = (y <= 0 ).732 x < 0 -> (0 <= x * y) = (y <= 0 )
Proof .afe
by rewrite -oppe_gt0 => /pmule_rle0<-; rewrite mulNe oppe_le0. Qed .
Lemma nmule_lge0 x y : x < 0 -> (y * x >= 0 ) = (y <= 0 ).732 x < 0 -> (0 <= y * x) = (y <= 0 )
Proof .b03
by rewrite muleC; apply : nmule_rge0. Qed .
Lemma nmule_rle0 x y : x < 0 -> (x * y <= 0 ) = (y >= 0 ).732 x < 0 -> (x * y <= 0 ) = (0 <= y)
Proof .b08
by rewrite -oppe_gt0 => /pmule_rge0<-; rewrite mulNe oppe_ge0. Qed .
Lemma nmule_lle0 x y : x < 0 -> (y * x <= 0 ) = (y >= 0 ).732 x < 0 -> (y * x <= 0 ) = (0 <= y)
Proof .b0d
by rewrite muleC; apply : nmule_rle0. Qed .
Lemma nmule_rgt0 x y : x < 0 -> (x * y > 0 ) = (y < 0 ).732 x < 0 -> (0 < x * y) = (y < 0 )
Proof .b12
by rewrite -oppe_gt0 => /pmule_rlt0<-; rewrite mulNe oppe_lt0. Qed .
Lemma nmule_lgt0 x y : x < 0 -> (y * x > 0 ) = (y < 0 ).732 x < 0 -> (0 < y * x) = (y < 0 )
Proof .b17
by rewrite muleC; apply : nmule_rgt0. Qed .
Lemma nmule_rlt0 x y : x < 0 -> (x * y < 0 ) = (y > 0 ).732 x < 0 -> (x * y < 0 ) = (0 < y)
Proof .b1c
by rewrite -oppe_gt0 => /pmule_rgt0<-; rewrite mulNe oppe_gt0. Qed .
Lemma nmule_llt0 x y : x < 0 -> (y * x < 0 ) = (y > 0 ).732 x < 0 -> (y * x < 0 ) = (0 < y)
Proof .b21
by rewrite muleC; apply : nmule_rlt0. Qed .
Lemma mule_lt0 x y : (x * y < 0 ) = [&& x != 0 , y != 0 & (x < 0 ) (+) (y < 0 )].732 (x * y < 0 ) =
[&& x != 0 , y != 0 & (x < 0 ) (+) (y < 0 )]
Proof .b26
have [xlt0|xgt0|->] := ltgtP x 0 ; last by rewrite mul0e.cd 23 xlt0 : x < 0
(x * y < 0 ) = [&& ~~ false, y != 0 & true (+) (y < 0 )]
by rewrite nmule_rlt0//= -leNgt lt_def.
by rewrite pmule_rlt0//= !lt_neqAle andbA andbb.
Qed .
Lemma muleA : associative ( *%E : \bar R -> \bar R -> \bar R ).ed associative (*%E : \bar R -> \bar R -> \bar R)
Proof .b39
move => x y z.a5d x * (y * z) = x * y * z
wlog x0 : x y z / 0 < x => [hwlog|].cd 1b8 hwlog : forall x y z , 0 < x -> x * (y * z) = x * y * z
b40
have [x0| |->] := ltgtP x 0 ; [ |exact : hwlog|by rewrite !mul0e].
by apply : oppe_inj; rewrite -!mulNe hwlog ?oppe_gt0 .
wlog y0 : x y z x0 / 0 < y => [hwlog|].cd 1b8 b49 hwlog : forall x y z ,
0 < x -> 0 < y -> x * (y * z) = x * y * z
b40
have [y0| |->] := ltgtP y 0 ; [ |exact : hwlog|by rewrite !(mul0e, mule0)].cd 1b8 b49 b56 y0 : y < 0
b40 b57
by apply : oppe_inj; rewrite -muleN -2 !mulNe -muleN hwlog ?oppe_gt0 .
wlog z0 : x y z x0 y0 / 0 < z => [hwlog|].cd 1b8 b49 b5a hwlog : forall x y z ,
0 < x ->
0 < y -> 0 < z -> x * (y * z) = x * y * z
b40
have [z0| |->] := ltgtP z 0 ; [ |exact : hwlog|by rewrite !mule0].cd 1b8 b49 b5a b67 z0 : z < 0
b40 b68
by apply : oppe_inj; rewrite -!muleN hwlog ?oppe_gt0 .
case : x x0 => [x x0| |//]; last by rewrite !gt0_mulye ?mule_gt0 .cd y, z : \bar R b5a b6b 9a x0 : 0 < x%:E
x%:E * (y * z) = x%:E * y * z
case : y y0 => [y y0| |//]; last by rewrite gt0_mulye // muleC !gt0_mulye.cd 93d b6b 9a b79 9e y0 : 0 < y%:E
x%:E * (y%:E * z) = x%:E * y%:E * z
case : z z0 => [z z0| |//]; last by rewrite !gt0_muley ?mule_gt0 .cd 9a b79 9e b7f 944 945
x%:E * (y%:E * z%:E) = x%:E * y%:E * z%:E
by rewrite /mule/= mulrA.
Qed .
Local Open Scope ereal_scope.
Canonical mule_monoid := Monoid.Law muleA mul1e mule1.
Canonical mule_comoid := Monoid.ComLaw muleC.
Lemma muleCA : left_commutative ( *%E : \bar R -> \bar R -> \bar R ).ed left_commutative (*%E : \bar R -> \bar R -> \bar R)
Proof .b87
exact : Monoid.mulmCA. Qed .
Lemma muleAC : right_commutative ( *%E : \bar R -> \bar R -> \bar R ).ed right_commutative (*%E : \bar R -> \bar R -> \bar R)
Proof .b8c
exact : Monoid.mulmAC. Qed .
Lemma muleACA : interchange (@mule R) (@mule R).
Proof .b91
exact : Monoid.mulmACA. Qed .
Lemma muleDr x y z : x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z.a5d x \is a fin_num ->
y +? z -> x * (y + z) = x * y + x * z
Proof .b96
rewrite /mule/=; move : x y z => [x| |] [y| |] [z| |] //= _; try
(by case : ltgtP => // -[] <-; rewrite ?(mul0r,add0r,adde0))
|| (by case : ltgtP => //; rewrite adde0).a63 y%:E +? z%:E ->
(x * (y + z))%:E = (x * y)%:E + (x * z)%:E
by rewrite mulrDr.
Qed .
Lemma muleDl x y z : x \is a fin_num -> y +? z -> (y + z) * x = y * x + z * x.a5d x \is a fin_num ->
y +? z -> (y + z) * x = y * x + z * x
Proof .b9f
by move => ? ?; rewrite -!(muleC x) muleDr. Qed .
Lemma muleBr x y z : x \is a fin_num -> y +? - z -> x * (y - z) = x * y - x * z.a5d x \is a fin_num ->
y +? - z -> x * (y - z) = x * y - x * z
Proof .ba4
by move => ? yz; rewrite muleDr ?muleN . Qed .
Lemma muleBl x y z : x \is a fin_num -> y +? - z -> (y - z) * x = y * x - z * x.a5d x \is a fin_num ->
y +? - z -> (y - z) * x = y * x - z * x
Proof .ba9
by move => ? yz; rewrite muleDl// mulNe. Qed .
Lemma ge0_muleDl x y z : 0 <= y -> 0 <= z -> (y + z) * x = y * x + z * x.a5d 0 <= y -> 0 <= z -> (y + z) * x = y * x + z * x
Proof .bae
rewrite /mule/=; move : x y z => [r| |] [s| |] [t| |] //= s0 t0.cd r, s, t : R s0 : 0 <= s%:Et0 : 0 <= t%:E
((s + t) * r)%:E = (s * r)%:E + (t * r)%:E
- bb3
by rewrite mulrDl.
- be1
by case : ltgtP => // -[] <-; rewrite mulr0 adde0.
- be6
by case : ltgtP => // -[] <-; rewrite mulr0 adde0.
- beb
by case : ltgtP => //; rewrite adde0.
- bf0
rewrite !eqe paddr_eq0 //; move : s0; rewrite lee_fin.cd bca bb8
(0 <= s)%R ->
(if (s == 0 %R) && (t == 0 %R)
then 0
else if 0 < s%:E + t%:E then +oo else -oo) =
(if s == 0 %R then 0 else if 0 < s%:E then +oo else -oo) +
(if t == 0 %R then 0 else if 0 < t%:E then +oo else -oo)
bf2
case : (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e .cd bca bb8 s0 : (0 < s)%R
(if 0 < s%:E + t%:E then +oo else -oo) =
(if 0 < s%:E then +oo else -oo) +
(if t == 0 %R then 0 else if 0 < t%:E then +oo else -oo)
+ bfa
rewrite lte_fin -[in LHS](addr0 0 %R) ltr_le_add // lte_fin s0.bfc +oo =
+oo +
(if t == 0 %R then 0 else if 0 < t%:E then +oo else -oo)
bff
by case : ltgtP t0 => // [t0|[<-{t}]] _; [rewrite gt_eqF|rewrite eqxx].
+ c09
by move : t0; rewrite lee_fin; case : (ltgtP t).
- c0d
by rewrite ltry; case : ltgtP s0.
- c12
by rewrite ltry; case : ltgtP t0.
- c17
by rewrite ltry.
- c1c
rewrite !eqe paddr_eq0 //; move : s0; rewrite lee_fin.bf7 (0 <= s)%R ->
(if (s == 0 %R) && (t == 0 %R)
then 0
else if 0 < s%:E + t%:E then -oo else +oo) =
(if s == 0 %R then 0 else if 0 < s%:E then -oo else +oo) +
(if t == 0 %R then 0 else if 0 < t%:E then -oo else +oo)
c1e
case : (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e .bfc (if 0 < s%:E + t%:E then -oo else +oo) =
(if 0 < s%:E then -oo else +oo) +
(if t == 0 %R then 0 else if 0 < t%:E then -oo else +oo)
+ c25
rewrite lte_fin -[in LHS](addr0 0 %R) ltr_le_add // lte_fin s0.bfc -oo =
-oo +
(if t == 0 %R then 0 else if 0 < t%:E then -oo else +oo)
c28
by case : ltgtP t0 => // [t0|[<-{t}]].
+ c31
by move : t0; rewrite lee_fin; case : (ltgtP t).
- c35
by rewrite ltry; case : ltgtP s0.
- c3a
by rewrite ltry; case : ltgtP s0.
- c3f
by rewrite ltry; case : ltgtP s0.
Qed .
Lemma ge0_muleDr x y z : 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z.a5d 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z
Proof .c43
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.a5d y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x
Proof .c48
rewrite /mule/=; move : x y z => [r| |] [s| |] [t| |] //= s0 t0.cd bb6 s0 : s%:E <= 0 t0 : t%:E <= 0
bb9
- c4d
by rewrite mulrDl.
- c71
by case : ltgtP => // -[] <-; rewrite mulr0 adde0.
- c76
by case : ltgtP => // -[] <-; rewrite mulr0 adde0.
- c7b
by case : ltgtP => //; rewrite adde0.
- c80
rewrite !eqe naddr_eq0 //; move : s0; rewrite lee_fin.cd bca c51
(s <= 0 )%R ->
(if (s == 0 %R) && (t == 0 %R)
then 0
else if 0 < s%:E + t%:E then +oo else -oo) =
(if s == 0 %R then 0 else if 0 < s%:E then +oo else -oo) +
(if t == 0 %R then 0 else if 0 < t%:E then +oo else -oo)
c82
case : (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e .
+ c8a
rewrite !lte_fin -[in LHS](addr0 0 %R) ltNge ler_add // ?ltW //=.c8c -oo =
(if (0 < s)%R then +oo else -oo) +
(if t == 0 %R
then 0
else if (0 < t)%R then +oo else -oo)
c8e
by rewrite !ltNge ltW //.
+ c97
by case : (ltgtP t).
- c9b
by rewrite ltry; case : ltgtP s0.
- ca0
by rewrite ltry; case : ltgtP t0.
- ca5
by rewrite ltry.
- caa
rewrite !eqe naddr_eq0 //; move : s0; rewrite lee_fin.c87 (s <= 0 )%R ->
(if (s == 0 %R) && (t == 0 %R)
then 0
else if 0 < s%:E + t%:E then -oo else +oo) =
(if s == 0 %R then 0 else if 0 < s%:E then -oo else +oo) +
(if t == 0 %R then 0 else if 0 < t%:E then -oo else +oo)
cac
case : (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e .
+ cb3
rewrite !lte_fin -[in LHS](addr0 0 %R) ltNge ler_add // ?ltW //=.c8c +oo =
(if (0 < s)%R then -oo else +oo) +
(if t == 0 %R
then 0
else if (0 < t)%R then -oo else +oo)
cb5
by rewrite !ltNge ltW // -lee_fin t0; case : eqP.
+ cbd
by case : (ltgtP t).
- cc1
by rewrite ltNge s0 /=; case : eqP.
- cc6
by rewrite ltNge t0 /=; case : eqP.
Qed .
Lemma le0_muleDr x y z : y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z.a5d y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z
Proof .cca
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.750 y \is a fin_num -> 0 < x -> y <= 1 -> y * x <= x
Proof .ccf
move : x y => [x| |] [y| |] _ //=.77a 0 < x%:E -> y%:E <= 1 -> y%:E * x%:E <= x%:E
- cd4
by rewrite lte_fin => x0 r0; rewrite /mule/= lee_fin ger_pmull.
- cdc
by move => _; rewrite /mule/= eqe => r1; rewrite leey.
Qed .
Lemma lee_wpmul2r x : 0 <= x -> {homo *%E^~ x : y z / y <= z}.d3 0 <= x -> {homo *%E^~ x : y z / y <= z >-> y <= z}
Proof .ce0
move : x => [x|_|//].77e 0 <= x%:E -> {homo *%E^~ x%:E : y z / y <= z}
rewrite lee_fin le_eqVlt => /predU1P[<- y z|x0]; first by rewrite 2 !mule0.7f6 {homo *%E^~ x%:E : y z / y <= z}
ce8
move => [y| |] [z| |]//; first by rewrite !lee_fin// ler_pmul2r.cd 9a 4ca 9e
y%:E <= +oo -> y%:E * x%:E <= +oo * x%:E
- cf0
by move => _; rewrite mulr_infty gtr0_sg// mul1e leey.
- cfc
by move => _; rewrite mulr_infty gtr0_sg// mul1e leNye.
- d01
by move => _; rewrite 2 !mulr_infty gtr0_sg// 2 !mul1e.
move => [y| |] [z| |]//.cd y, z : R
y%:E <= z%:E -> y%:E * +oo <= z%:E * +oo
- d08
rewrite lee_fin => yz.cd d0b yz : (y <= z)%R
y%:E * +oo <= z%:E * +oo
d0d
have [z0|z0|] := ltgtP 0 %R z.
+ d1d
by rewrite [leRHS]mulr_infty gtr0_sg// mul1e leey.
+ d29
by rewrite mulr_infty ltr0_sg// ?(le_lt_trans yz)// [leRHS]mulr_infty ltr0_sg.
+ d2e
move => z0; move : yz; rewrite -z0 mul0e le_eqVlt => /predU1P[->|y0].cd d0b z0 : 0 %R = z
0 * +oo <= 0
by rewrite mul0e.
by rewrite mulr_infty ltr0_sg// mulN1e leNye.
+ d40
by move => _; rewrite mulyy leey.
+ d45
by move => _; rewrite mulNyy leNye.
+ d4a
by move => _; rewrite mulNyy leNye.
Qed .
Lemma lee_wpmul2l x : 0 <= x -> {homo *%E x : y z / y <= z}.d3 0 <= x -> {homo *%E x : y z / y <= z >-> y <= z}
Proof .d4e
by move => x0 y z yz; rewrite !(muleC x) lee_wpmul2r. Qed .
Lemma ge0_sume_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).cd 19a 19b 6b 1df 339
(forall i : I, P i -> 0 <= F i) ->
(\sum_(i <- s | P i) F i) * x =
\sum_(i <- s | P i) F i * x
Proof .d53
elim : s x P F => [x P F F0|h t ih x P F F0]; first by rewrite 2 !big_nil mul0e.cd 19a 1dd 1de ih : forall x (P : pred I) (F : I -> \bar R),
(forall i : I, P i -> 0 <= F i) ->
(\sum_(i <- t | P i) F i) * x =
\sum_(i <- t | P i) F i * x6b 1df 339 6b6
(\sum_(i <- (h :: t) | P i) F i) * x =
\sum_(i <- (h :: t) | P i) F i * x
rewrite big_cons; case : ifPn => Ph; last by rewrite big_cons (negbTE Ph) ih.cd 19a 1dd 1de d5c 6b 1df 339 6b6 Ph : P h
(F h + \sum_(j <- t | P j) F j) * x =
\sum_(i <- (h :: t) | P i) F i * x
by rewrite ge0_muleDl ?sume_ge0 // ?F0 // ih// big_cons Ph.
Qed .
Lemma ge0_sume_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).d55 (forall i : I, P i -> 0 <= F i) ->
x * (\sum_(i <- s | P i) F i) =
\sum_(i <- s | P i) x * F i
Proof .d65
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).d55 (forall i : I, P i -> F i <= 0 ) ->
(\sum_(i <- s | P i) F i) * x =
\sum_(i <- s | P i) F i * x
Proof .d6a
elim : s x P F => [x P F F0|h t ih x P F F0]; first by rewrite 2 !big_nil mul0e.cd 19a 1dd 1de ih : forall x (P : pred I) (F : I -> \bar R),
(forall i : I, P i -> F i <= 0 ) ->
(\sum_(i <- t | P i) F i) * x =
\sum_(i <- t | P i) F i * x6b 1df 339 F0 : forall i : I, P i -> F i <= 0
d5d
rewrite big_cons; case : ifPn => Ph; last by rewrite big_cons (negbTE Ph) ih.cd 19a 1dd 1de d72 6b 1df 339 d73 d62
d63
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).d55 (forall i : I, P i -> F i <= 0 ) ->
x * (\sum_(i <- s | P i) F i) =
\sum_(i <- s | P i) x * F i
Proof .d79
by move => F0; rewrite muleC le0_sume_distrl//; under eq_bigr do rewrite muleC.
Qed .
Lemma fin_num_sume_distrr (I : Type ) (s : seq I) x (P : pred I)
(F : I -> \bar R) :
x \is a fin_num -> {in P &, forall i j , F i +? F j} ->
x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) x * F i.d55 x \is a fin_num ->
{in P &, forall i j : I, F i +? F j} ->
x * (\sum_(i <- s | P i) F i) =
\sum_(i <- s | P i) x * F i
Proof .d7e
move => xfin PF; elim : s => [|h t ih]; first by rewrite !big_nil mule0.cd 19a 6b 1df 339 xfin : x \is a fin_num PF : {in P &, forall i j : I, F i +? F j} 1dd 1de ih : x * (\sum_(i <- t | P i) F i) =
\sum_(i <- t | P i) x * F i
x * (\sum_(i <- (h :: t) | P i) F i) =
\sum_(i <- (h :: t) | P i) x * F i
rewrite !big_cons; case : ifPn => Ph //.cd 19a 6b 1df 339 d86 d87 1dd 1de d88 d62
x * (F h + \sum_(j <- t | P j) F j) =
x * F h + \sum_(j <- t | P j) x * F j
by rewrite muleDr// ?ih // adde_def_sum// => i Pi; rewrite PF.
Qed .
Lemma eq_infty x : (forall r , r%:E <= x) -> x = +oo.d3 (forall r , r%:E <= x) -> x = +oo
Proof .d90
case : x => [x /(_ (x + 1 )%R)|//|/(_ 0 %R)//].77e (x + 1 )%:E <= x%:E -> x%:E = +oo
by rewrite EFinD addeC -lee_subr_addr// subee// lee_fin ler10.
Qed .
Lemma eq_ninfty x : (forall r , x <= r%:E) -> x = -oo.d3 (forall r , x <= r%:E) -> x = -oo
Proof .d99
move => *; apply : (can_inj oppeK); apply : eq_infty => r.cd 6b _Hyp_ : forall r , x <= r%:Eae
r%:E <= - x
by rewrite lee_oppr -EFinN.
Qed .
Lemma lee_opp x y : (- x <= - y) = (y <= x).732 (- x <= - y) = (y <= x)
Proof .da4
by rewrite lee_oppl oppeK. Qed .
Lemma lee_abs x : x <= `|x|.
Proof .da9
by move : x => [x| |]//=; rewrite lee_fin ler_norm. Qed .
Lemma abse_id x : `| `|x| | = `|x|.
Proof .dae
by move : x => [x| |] //=; rewrite normr_id. Qed .
Lemma lte_absl (x y : \bar R) : (`|x| < y)%E = (- y < x < y)%E.732 (`|x| < y) = (- y < x < y)
Proof .db3
by move : x y => [x| |] [y| |] //=; rewrite ?lte_fin ?ltry ?ltNyr // ltr_norml.
Qed .
Lemma eqe_absl x y : (`|x| == y) = ((x == y) || (x == - y)) && (0 <= y).732 (`|x| == y) = ((x == y) || (x == - y)) && (0 <= y)
Proof .db8
by move : x y => [x| |] [y| |] //=; rewrite ? leey// !eqe eqr_norml lee_fin.
Qed .
Lemma lee_abs_add x y : `|x + y| <= `|x| + `|y|.732 `|x + y| <= `|x| + `|y|
Proof .dbd
by move : x y => [x| |] [y| |] //; rewrite /abse -EFinD lee_fin ler_norm_add.
Qed .
Lemma lee_abs_sum (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|.cd 19a 19b 339 1df
`|\sum_(i <- s | P i) F i| <=
\sum_(i <- s | P i) `|F i|
Proof .dc2
elim /big_ind2 : _ => //; first by rewrite abse0.dc4 forall x1 x2 y1 y2 : \bar R,
`|x2| <= x1 -> `|y2| <= y1 -> `|x2 + y2| <= x1 + y1
by move => *; exact /(le_trans (lee_abs_add _ _) (lee_add _ _)).
Qed .
Lemma lee_abs_sub x y : `|x - y| <= `|x| + `|y|.732 `|x - y| <= `|x| + `|y|
Proof .dcc
by move : x y => [x| |] [y| |] //; rewrite /abse -EFinD lee_fin ler_norm_sub.
Qed .
Lemma abseM : {morph @abse R : x y / x * y}.ed {morph abse : x y / x * y}
Proof .dd1
have xoo r : `|r%:E * +oo| = `|r|%:E * +oo.cc `|r%:E * +oo| = `|r|%:E * +oo
have [r0|r0] := leP 0 %R r.
by rewrite (ger0_norm r0)// gee0_abs// mule_ge0// leey.
rewrite (ltr0_norm r0)// lte0_abs// ?EFinN ?mulNe //.
by rewrite mule_lt0 /= eqe lt_eqF//= lte_fin r0.
move => [x| |] [y| |] //=; first by rewrite normrM.cd ddc 9a
`|x%:E * -oo| = `|x|%:E * +oo
- df1
by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
- e05
by rewrite muleC xoo muleC.
- e0a
by rewrite mulyy.
- e0f
by rewrite mulyy mulyNy.
- e14
by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
- e19
by rewrite mulyy mulNyy.
- e1e
by rewrite mulyy.
Qed .
Lemma maxEFin r1 r2 : maxe r1%:E r2%:E = (Num.max r1 r2)%:E.cd 14
maxe r1%:E r2%:E = (Num.max r1 r2)%:E
Proof .e22
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.e24 mine r1%:E r2%:E = (Num.min r1 r2)%:E
Proof .e28
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.ed left_distributive +%E maxe
Proof .e2d
move => x y z; have [xy|yx] := leP x y.cd 1b8 xy : x <= y
y + z = maxe (x + z) (y + z)
by apply /esym/max_idPr; rewrite lee_add2r.
by apply /esym/max_idPl; rewrite lee_add2r// ltW.
Qed .
Lemma adde_maxr : right_distributive (@adde R) maxe.ed right_distributive +%E maxe
Proof .e40
move => x y z; have [yz|zy] := leP y z.cd 1b8 yz : y <= z
x + z = maxe (x + y) (x + z)
by apply /esym/max_idPr; rewrite lee_add2l.
by apply /esym/max_idPl; rewrite lee_add2l// ltW.
Qed .
Lemma maxye : left_zero (+oo : \bar R) maxe.ed left_zero (+oo : \bar R) maxe
Proof .e53
by move => x; have [|//] := leP +oo x; rewrite leye_eq => /eqP. Qed .
Lemma maxey : right_zero (+oo : \bar R) maxe.ed right_zero (+oo : \bar R) maxe
Proof .e58
by move => x; rewrite maxC maxye. Qed .
Lemma maxNye : left_id (-oo : \bar R) maxe.ed left_id (-oo : \bar R) maxe
Proof .e5d
by move => x; have [//|] := leP -oo x; rewrite ltNge leNye. Qed .
Lemma maxeNy : right_id (-oo : \bar R) maxe.ed right_id (-oo : \bar R) maxe
Proof .e62
by move => x; rewrite maxC maxNye. Qed .
Canonical maxe_monoid := Monoid.Law maxA maxNye maxeNy.
Canonical maxe_comoid := Monoid.ComLaw maxC.
Lemma minNye : left_zero (-oo : \bar R) mine.ed left_zero (-oo : \bar R) mine
Proof .e67
by move => x; have [|//] := leP x -oo; rewrite leeNy_eq => /eqP. Qed .
Lemma mineNy : right_zero (-oo : \bar R) mine.ed right_zero (-oo : \bar R) mine
Proof .e6c
by move => x; rewrite minC minNye. Qed .
Lemma minye : left_id (+oo : \bar R) mine.ed left_id (+oo : \bar R) mine
Proof .e71
by move => x; have [//|] := leP x +oo; rewrite ltNge leey. Qed .
Lemma miney : right_id (+oo : \bar R) mine.ed right_id (+oo : \bar R) mine
Proof .e76
by move => x; rewrite minC minye. Qed .
Canonical mine_monoid := Monoid.Law minA minye miney.
Canonical mine_comoid := Monoid.ComLaw minC.
Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.ed {morph -%E : x y / maxe x y >-> mine x y : \bar R}
Proof .e7b
move => [x| |] [y| |] //=.77a - maxe x%:E y%:E = mine (- x)%:E (- y)%:E
- e80
by rewrite maxEFin minEFin -EFinN oppr_max.
- e8e
by rewrite maxey mineNy.
- e93
by rewrite miney.
- e98
by rewrite minNye.
- e9d
by rewrite maxNye minye.
Qed .
Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.ed {morph -%E : x y / mine x y >-> maxe x y : \bar R}
Proof .ea1
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).cd z, x, y : \bar R
z \is a fin_num ->
0 < z -> z * maxe x y = maxe (z * x) (z * y)
Proof .ea6
move => + r0; have [xy|yx|->] := ltgtP x y; last by rewrite maxxx.cd ea9 r0 : 0 < zxy : x < y
z \is a fin_num -> z * y = maxe (z * x) (z * y)
- ead
by move => zfin; rewrite /maxe lte_pmul2l // xy.
- eb9
by move => zfin; rewrite maxC /maxe lte_pmul2l// yx.
Qed .
Lemma maxeMl z x y : z \is a fin_num -> 0 < z ->
maxe x y * z = maxe (x * z) (y * z).ea8 z \is a fin_num ->
0 < z -> maxe x y * z = maxe (x * z) (y * z)
Proof .ebd
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).ea8 z \is a fin_num ->
0 < z -> z * mine x y = mine (z * x) (z * y)
Proof .ec2
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).ea8 z \is a fin_num ->
0 < z -> mine x y * z = mine (x * z) (y * z)
Proof .ec7
by move => zfin z0; rewrite muleC mineMr// !(muleC z). Qed .
Lemma lee_pemull x y : 0 <= y -> 1 <= x -> y <= x * y.732 0 <= y -> 1 <= x -> y <= x * y
Proof .ecc
move : x y => [x| |] [y| |] //; last by rewrite mulyy.77a 0 <= y%:E -> 1 <= x%:E -> y%:E <= x%:E * y%:E
- ed1
by rewrite -EFinM 3 !lee_fin; exact : ler_pemull.
- edb
move => _; rewrite lee_fin => x1.cd 9a x1 : (1 <= x)%R
+oo <= x%:E * +oo
edd
by rewrite mulr_infty gtr0_sg ?mul1e // (lt_le_trans _ x1).
- ee6
rewrite lee_fin le_eqVlt => /predU1P[<- _|y0 _]; first by rewrite mule0.cd 9e 4d4
y%:E <= +oo * y%:E
by rewrite mulr_infty gtr0_sg// mul1e leey.
Qed .
Lemma lee_nemull x y : y <= 0 -> 1 <= x -> x * y <= y.732 y <= 0 -> 1 <= x -> x * y <= y
Proof .eef
move : x y => [x| |] [y| |] //; last by rewrite mulyNy.77a y%:E <= 0 -> 1 <= x%:E -> x%:E * y%:E <= y%:E
- ef4
by rewrite -EFinM 3 !lee_fin; exact : ler_nemull.
- efe
move => _; rewrite lee_fin => x1.
by rewrite mulr_infty gtr0_sg ?mul1e // (lt_le_trans _ x1).
- f07
rewrite lee_fin le_eqVlt => /predU1P[-> _|y0 _]; first by rewrite mule0.cd 9e d3a
+oo * y%:E <= y%:E
by rewrite mulr_infty ltr0_sg// mulN1e leNye.
Qed .
Lemma lee_pemulr x y : 0 <= y -> 1 <= x -> y <= y * x.732 0 <= y -> 1 <= x -> y <= y * x
Proof .f10
by move => y0 x1; rewrite muleC lee_pemull. Qed .
Lemma lee_nemulr x y : y <= 0 -> 1 <= x -> y * x <= y.732 y <= 0 -> 1 <= x -> y * x <= y
Proof .f15
by move => y0 x1; rewrite muleC lee_nemull. Qed .
Lemma mule_natl x n : n%:R%:E * x = x *+ n.cd 6b 128
(n%:R)%:E * x = x *+ n
Proof .f1a
elim : n => [|n]; first by rewrite mul0e.f1c (n%:R)%:E * x = x *+ n -> (n.+1 %:R)%:E * x = x *+ n.+1
move : x => [x| |] ih.cd 128 9a ih : (n%:R)%:E * x%:E = x%:E *+ n
(n.+1 %:R)%:E * x%:E = x%:E *+ n.+1
- f24
by rewrite -EFinM mulr_natl EFin_natmul.
- f34
by rewrite mulry gtr0_sg// mul1e enatmul_pinfty.
- f39
by rewrite mulrNy gtr0_sg// mul1e enatmul_ninfty.
Qed .
Lemma lte_pmul x1 y1 x2 y2 :
0 <= x1 -> 0 <= x2 -> x1 < y1 -> x2 < y2 -> x1 * x2 < y1 * y2.cd x1, y1, x2, y2 : \bar R
0 <= x1 ->
0 <= x2 -> x1 < y1 -> x2 < y2 -> x1 * x2 < y1 * y2
Proof .f3d
move : x1 y1 x2 y2 => [x1| |] [y1| |] [x2| |] [y2| |] //;
rewrite !(lte_fin,lee_fin).cd x1, y1, x2, y2 : R
(0 <= x1)%R ->
(0 <= x2)%R ->
(x1 < y1)%R -> (x2 < y2)%R -> (x1 * x2 < y1 * y2)%R
- f44
by move => *; rewrite ltr_pmul.
- f58
move => x10 x20 xy1 xy2.cd f4c x10 : (0 <= x1)%R x20 : (0 <= x2)%R xy1 : (x1 < y1)%R xy2 : x2%:E < +oo
x1%:E * x2%:E < y1%:E * +oo
f5a
by rewrite mulry gtr0_sg ?mul1e -?EFinM ?ltry // (le_lt_trans _ xy1).
- f66
move => x10 x20 xy1 xy2.cd f50 f60 f61 xy1 : x1%:E < +oo xy2 : (x2 < y2)%R
x1%:E * x2%:E < +oo * y2%:E
f68
by rewrite mulyr gtr0_sg ?mul1e -?EFinM ?ltry // (le_lt_trans _ xy2).
- f72
by move => *; rewrite mulyy -EFinM ltry.
Qed .
Lemma lee_pmul x1 y1 x2 y2 : 0 <= x1 -> 0 <= x2 -> x1 <= y1 -> x2 <= y2 ->
x1 * x2 <= y1 * y2.f3f 0 <= x1 ->
0 <= x2 -> x1 <= y1 -> x2 <= y2 -> x1 * x2 <= y1 * y2
Proof .f76
move : x1 y1 x2 y2 => [x1| |] [y1| |] [x2| |] [y2| |] //; rewrite !lee_fin.f46 (0 <= x1)%R ->
(0 <= x2)%R ->
(x1 <= y1)%R -> (x2 <= y2)%R -> (x1 * x2 <= y1 * y2)%R
- f7b
exact : ler_pmul.
- f97
rewrite le_eqVlt => /predU1P[<- x20 y10 _|x10 x20 xy1 _].cd f4c f61 y10 : (0 <= y1)%R
0 * x2%:E <= y1%:E * +oo
by rewrite mul0e mule_ge0// leey.
by rewrite mulr_infty gtr0_sg// ?mul1e ?leey // (lt_le_trans x10).
- fab
rewrite le_eqVlt => /predU1P[<- _ y10 _|x10 _ xy1 _].cd f83 f9f
0 * +oo <= y1%:E * +oo
by rewrite mul0e mule_ge0// leey.
rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// ?mul1e //.
exact : (lt_le_trans x10).
- fc0
move => x10; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].cd f50 f60 y20 : (0 <= y2)%R
x1%:E * 0 <= +oo * y2%:E
by rewrite mule0 mulr_infty mule_ge0// ?leey // lee_fin sgr_ge0.
by rewrite mulr_infty gtr0_sg ?mul1e ?leey // (lt_le_trans x20).
- fd4
by move => x10 x20 _ _; rewrite mulyy leey.
- fd9
rewrite le_eqVlt => /predU1P[<- _ _ _|x10 _ _ _].
by rewrite mulyy mul0e leey.
by rewrite mulyy mulr_infty gtr0_sg// mul1e.
- fe9
move => _; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].cd f8f fc8
+oo * 0 <= +oo * y2%:E
by rewrite mule0 mulr_infty mule_ge0// ?leey // lee_fin sgr_ge0.
rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg ?mul1e //.
exact : (lt_le_trans x20).
- ffe
move => _; rewrite le_eqVlt => /predU1P[<- _ _|x20 _ _].
by rewrite mule0 mulyy leey.
by rewrite mulr_infty gtr0_sg// mul1e// mulyy.
Qed .
Lemma lee_pmul2l x : x \is a fin_num -> 0 < x -> {mono *%E x : x y / x <= y}.d3 x \is a fin_num ->
0 < x -> {mono *%E x : x y / x <= y >-> x <= y}
Proof .100d
move : x => [x _|//|//] /[!(@lte_fin R)] x0 [y| |] [z| |].cd 9a 4ca d0b
(x%:E * y%:E <= x%:E * z%:E) = (y%:E <= z%:E)
- 1012
by rewrite -2 !EFinM 2 !lee_fin ler_pmul2l.
- 1029
by rewrite mulry gtr0_sg// mul1e 2 !leey.
- 102e
by rewrite mulrNy gtr0_sg// mul1e 2 !leeNy_eq.
- 1033
by rewrite mulry gtr0_sg// mul1e 2 !leye_eq.
- 1038
by rewrite mulry gtr0_sg// mul1e.
- 103d
by rewrite mulry mulrNy gtr0_sg// mul1e mul1e.
- 1042
by rewrite mulrNy gtr0_sg// mul1e 2 !leNye.
- 1047
by rewrite mulrNy mulry gtr0_sg// 2 !mul1e.
- 104c
by rewrite mulrNy gtr0_sg// mul1e.
Qed .
Lemma lee_pmul2r x : x \is a fin_num -> 0 < x -> {mono *%E^~ x : x y / x <= y}.d3 x \is a fin_num ->
0 < x -> {mono *%E^~ x : x y / x <= y >-> x <= y}
Proof .1050
by move => xfin x0 y z; rewrite -2 !(muleC x) lee_pmul2l. Qed .
Lemma lee_paddl y x z : 0 <= x -> y <= z -> y <= x + z.cd y, x, z : \bar R
0 <= x -> y <= z -> y <= x + z
Proof .1055
by move => *; rewrite -[y]add0e lee_add. Qed .
Lemma lte_paddl y x z : 0 <= x -> y < z -> y < x + z.1057 0 <= x -> y < z -> y < x + z
Proof .105c
by move => x0 /lt_le_trans; apply ; rewrite lee_paddl. Qed .
Lemma lee_paddr y x z : 0 <= x -> y <= z -> y <= z + x.1057 0 <= x -> y <= z -> y <= z + x
Proof .1061
by move => *; rewrite addeC lee_paddl. Qed .
Lemma lte_paddr y x z : 0 <= x -> y < z -> y < z + x.1057 0 <= x -> y < z -> y < z + x
Proof .1066
by move => *; rewrite addeC lte_paddl. Qed .
Lemma lte_spaddre z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.ea8 z \is a fin_num -> 0 < y -> z <= x -> z < x + y
Proof .106b
move : z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry)//.cd z, y, x : R
(0 < y)%R -> z%:E <= x%:E -> (z < x + y)%R
exact : ltr_spaddr.
Qed .
Lemma lte_spadder z x y : x \is a fin_num -> 0 < y -> z <= x -> z < x + y.ea8 x \is a fin_num -> 0 < y -> z <= x -> z < x + y
Proof .1076
move : z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry,ltNyr)//.1070
exact : ltr_spaddr.
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}.
#[global ] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply : abse_ge0] : core. Casts are ignored in patterns
[cast-in -pattern ,automation] Casts are ignored in patterns
[cast-in -pattern ,automation]
#[deprecated(since="mathcomp-analysis 0.6" , note="Use lte_spaddre instead." )]
Notation lte_spaddr := lte_spaddre.
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 .107d
by rewrite dual_addeE oppe_lt0 sube_gt0 lte_opp. Qed .
Lemma dsube_ge0 x y : (0 <= y - x) = (x <= y).732 (0 <= y - x) = (x <= y)
Proof .1082
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).732 y \is a fin_num -> (x - y <= 0 ) = (x <= y)
Proof .1087
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).750 y \is a fin_num -> (y - x <= 0 ) = (y <= x)
Proof .108c
by move => ?; rewrite dual_addeE oppe_le0 subre_ge0 ?fin_numN // lee_opp.
Qed .
Lemma dsube_le0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(y - x <= 0 ) = (y <= x).732 (x \is a fin_num) || (y \is a fin_num) ->
(y - x <= 0 ) = (y <= x)
Proof .1091
by move => /orP[?|?]; [rewrite dsuber_le0|rewrite dsubre_le0]. Qed .
Lemma lte_dadd a b x y : a < b -> x < y -> a + x < b + y.88f
Proof .88f
rewrite !dual_addeE lte_opp -lte_opp -(lte_opp y); exact : lte_add. Qed .
Lemma lee_daddl x y : 0 <= y -> x <= x + y.89c
Proof .89c
rewrite dual_addeE lee_oppr -oppe_le0; exact : gee_addl. Qed .
Lemma lee_daddr x y : 0 <= y -> x <= y + x.8a1
Proof .8a4 rewrite dual_addeE lee_oppr -oppe_le0; exact : gee_addr. Qed .
Lemma gee_daddl x y : y <= 0 -> x + y <= x.8a6
Proof .8a6
rewrite dual_addeE lee_oppl -oppe_ge0; exact : lee_addl. Qed .
Lemma gee_daddr x y : y <= 0 -> y + x <= x.8ab
Proof .8ae rewrite dual_addeE lee_oppl -oppe_ge0; exact : lee_addr. Qed .
Lemma lte_daddl y x : y \is a fin_num -> (y < y + x) = (0 < x).8b0
Proof .8b0
by rewrite -fin_numN dual_addeE lte_oppr; exact : gte_subl. Qed .
Lemma lte_daddr y x : y \is a fin_num -> (y < x + y) = (0 < x).8b5
Proof .8b8 by rewrite -fin_numN dual_addeE lte_oppr addeC; exact : gte_subl. Qed .
Lemma gte_dsubl y x : y \is a fin_num -> (y - x < y) = (0 < x).8ba
Proof .8ba
by rewrite -fin_numN dual_addeE lte_oppl oppeK; exact : lte_addl. Qed .
Lemma gte_dsubr y x : y \is a fin_num -> (- x + y < y) = (0 < x).8c3
Proof .8c6 by rewrite -fin_numN dual_addeE lte_oppl oppeK; exact : lte_addr. Qed .
Lemma gte_daddl x y : x \is a fin_num -> (x + y < x) = (y < 0 ).8c8
Proof .8cb
by rewrite -fin_numN dual_addeE lte_oppl -oppe0 lte_oppr; exact : lte_addl.
Qed .
Lemma gte_daddr x y : x \is a fin_num -> (y + x < x) = (y < 0 ).8cd
Proof .8d0 by rewrite daddeC; exact : gte_daddl. Qed .
Lemma lte_dadd2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b).8d2
Proof .8d7
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.8df
Proof .8df
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).8f9
Proof .8fc
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.902
Proof .905 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.907
Proof .907
rewrite !dual_addeE lee_opp -lee_opp -(lee_opp y); exact : lee_add. Qed .
Lemma lte_le_dadd a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.910
Proof .910
rewrite !dual_addeE lte_opp -lte_opp; exact : lte_le_sub. Qed .
Lemma lee_lt_dadd a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.91b
Proof .91e by move => afin xa yb; rewrite (daddeC a) (daddeC x) lte_le_dadd. Qed .
Lemma lee_dsub x y z t : x <= y -> t <= z -> x - z <= y - t.cd 1b8 t : dual_extended R
x <= y -> t <= z -> x - z <= y - t
Proof .10b0
rewrite !dual_addeE lee_oppl oppeK -lee_opp !oppeK; exact : lee_add. Qed .
Lemma lte_le_dsub z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u.92d
Proof .932
rewrite !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.98c
Proof .98c
move => Pfg; rewrite !dual_sumeE lee_opp.cd 19a 98f 19b 1df Pfg : forall i : I, P i -> f i <= g i
(\sum_(i <- s | P i) - g i <=
\sum_(i <- s | P i) - f i)%E
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.993
Proof .998
move => QP PQf; rewrite !dual_sumeE lee_opp.cd 19a 19b 996 1e0 99d 99e
(\sum_(i <- s | P i) - f i <=
\sum_(i <- s | Q i) - f i)%E
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.9a1
Proof .9a4
move => QP PQf; rewrite !dual_sumeE lee_opp.cd 19a 19b 996 1e0 99d 9a9
(\sum_(i <- s | Q i) - f i <=
\sum_(i <- s | P i) - f i)%E
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.9ac
Proof .9b2
move => PQf; rewrite !dual_sumeE lee_opp.9b6 (\sum_(i <- s | P i) - f i <=
\sum_(i <- s | P i && Q i) - f i)%E
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.9ba
Proof .9bd
move => PQf; rewrite !dual_sumeE lee_opp.9c1 (\sum_(i <- s | P i && Q i) - f i <=
\sum_(i <- s | P i) - f i)%E
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}.9c7 (forall n : nat, P n -> (0 <= f n)%E) ->
{homo (fun n : nat => \sum_(i < n | P i) f i) : i j /
(i <= j)%N >-> i <= j}
Proof .10d6
move => f0 m n mlen; rewrite !dual_sumeE lee_opp.cd 35a 9c8 f0 : forall n : nat, P n -> (0 <= f n)%E9dd mlen : (m <= n)%N
(\sum_(i | P i) - f i <= \sum_(i | P i) - f i)%E
apply : (lee_sum_npos_ord (fun i => - f i)%E) => [i Pi|//].cd 35a 9c8 10de 9dd 10df i : nat 3ae
(- f i <= 0 )%E
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}.9c7 (forall n : nat, P n -> (f n <= 0 )%E) ->
{homo (fun n : nat => \sum_(i < n | P i) f i) : i j /
(i <= j)%N >-> j <= i}
Proof .10e8
move => f0 m n mlen; rewrite !dual_sumeE lee_opp.cd 35a 9c8 f0 : forall n : nat, P n -> (f n <= 0 )%E9dd 10df
10e0
apply : (lee_sum_nneg_ord (fun i => - f i)%E) => [i Pi|//].cd 35a 9c8 10f0 9dd 10df 10e5 3ae
(0 <= - f i)%E
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}.9e1
Proof .9e6
move => f0 i j le_ij; rewrite !dual_sumeE lee_opp.9ea (\sum_(m <= i < j | P i) - f i <=
\sum_(m <= i < i | P i) - f i)%E
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}.9ee
Proof .9f1
move => f0 i j le_ij; rewrite !dual_sumeE lee_opp.9f5 (\sum_(m <= i < i | P i) - f i <=
\sum_(m <= i < j | P i) - f i)%E
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}.9f9
Proof .9fd
move => f0 i j le_ij; rewrite !dual_sumeE lee_opp.a01 (\sum_(i <= i < n | P i) - f i <=
\sum_(j <= i < n | P i) - f i)%E
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}.a0b
Proof .a0e
move => f0 i j le_ij; rewrite !dual_sumeE lee_opp.a12 (\sum_(j <= i < n | P i) - f i <=
\sum_(i <= i < n | P i) - f i)%E
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.a1a
Proof .a20
move => AB f0; rewrite !dual_sumeE lee_opp.a24 (\sum_(i <- B | P i) - f i <=
\sum_(i <- A | P i) - f i)%E
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.a3e
Proof .a41
move => AB f0; rewrite !dual_sumeE lee_opp.a45 (\sum_(i <- A | P i) - f i <=
\sum_(i <- B | P i) - f i)%E
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).a5b
Proof .a5f
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr oppeK lte_subl_addr.
Qed .
Lemma lte_dsubl_addl x y z : y \is a fin_num -> (x - y < z) = (x < y + z).a67
Proof .a67
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subr_addl ?fin_numN .
Qed .
Lemma lte_dsubr_addr x y z : z \is a fin_num -> (x < y - z) = (x + z < y).a6c
Proof .a6f
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subl_addr ?fin_numN .
Qed .
Lemma lte_dsubr_addl x y z : z \is a fin_num -> (x < y - z) = (z + x < y).a75
Proof .a75
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subl_addl ?fin_numN .
Qed .
Lemma lte_dsuber_addr x y z : y \is a fin_num -> (x < y - z) = (x + z < y).a5d y \is a fin_num -> (x < y - z) = (x + z < y)
Proof .111b
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subel_addr ?fin_numN .
Qed .
Lemma lte_dsuber_addl x y z : y \is a fin_num -> (x < y - z) = (z + x < y).a5d y \is a fin_num -> (x < y - z) = (z + x < y)
Proof .1120
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subel_addl ?fin_numN .
Qed .
Lemma lte_dsubel_addr x y z : z \is a fin_num -> (x - y < z) = (x < z + y).a5d z \is a fin_num -> (x - y < z) = (x < z + y)
Proof .1125
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr lte_suber_addr ?fin_numN .
Qed .
Lemma lte_dsubel_addl x y z : z \is a fin_num -> (x - y < z) = (x < y + z).a5d z \is a fin_num -> (x - y < z) = (x < y + z)
Proof .112a
by move => ?; rewrite !dual_addeE lte_oppl lte_oppr lte_suber_addl ?fin_numN .
Qed .
Lemma lee_dsubl_addr x y z : y \is a fin_num -> (x - y <= z) = (x <= z + y).a8f
Proof .a92
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subr_addr ?fin_numN .
Qed .
Lemma lee_dsubl_addl x y z : y \is a fin_num -> (x - y <= z) = (x <= y + z).a98
Proof .a98
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subr_addl ?fin_numN .
Qed .
Lemma lee_dsubr_addr x y z : z \is a fin_num -> (x <= y - z) = (x + z <= y).a9d
Proof .aa0
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subl_addr ?fin_numN .
Qed .
Lemma lee_dsubr_addl x y z : z \is a fin_num -> (x <= y - z) = (z + x <= y).aa8
Proof .aa8
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subl_addl ?fin_numN .
Qed .
Lemma lee_dsubel_addr x y z : x \is a fin_num -> (x - y <= z) = (x <= z + y).a5d x \is a fin_num -> (x - y <= z) = (x <= z + y)
Proof .1135
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_suber_addr ?fin_numN .
Qed .
Lemma lee_dsubel_addl x y z : x \is a fin_num -> (x - y <= z) = (x <= y + z).a5d x \is a fin_num -> (x - y <= z) = (x <= y + z)
Proof .113a
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_suber_addl ?fin_numN .
Qed .
Lemma lee_dsuber_addr x y z : x \is a fin_num -> (x <= y - z) = (x + z <= y).a5d x \is a fin_num -> (x <= y - z) = (x + z <= y)
Proof .113f
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subel_addr ?fin_numN .
Qed .
Lemma lee_dsuber_addl x y z : x \is a fin_num -> (x <= y - z) = (z + x <= y).a5d x \is a fin_num -> (x <= y - z) = (z + x <= y)
Proof .1144
by move => ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subel_addl ?fin_numN .
Qed .
Lemma dsuber_gt0 x y : x \is a fin_num -> (0 < y - x) = (x < y).732 x \is a fin_num -> (0 < y - x) = (x < y)
Proof .1149
by move => ?; rewrite lte_dsubr_addl// dadde0. Qed .
Lemma dsubre_gt0 x y : y \is a fin_num -> (0 < y - x) = (x < y).732 y \is a fin_num -> (0 < y - x) = (x < y)
Proof .114e
by move => ?; rewrite lte_dsuber_addl// dadde0. Qed .
Lemma dsube_gt0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(0 < y - x) = (x < y).732 (x \is a fin_num) || (y \is a fin_num) ->
(0 < y - x) = (x < y)
Proof .1153
by move => /orP[?|?]; [rewrite dsuber_gt0|rewrite dsubre_gt0]. Qed .
Lemma dmuleDr x y z : x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z.a5d x \is a fin_num ->
(y +? z)%E -> x * (y + z) = x * y + x * z
Proof .1158
by move => *; rewrite !dual_addeE muleN muleDr ?adde_defNN // !muleN. Qed .
Lemma dmuleDl x y z : x \is a fin_num -> y +? z -> (y + z) * x = y * x + z * x.a5d x \is a fin_num ->
(y +? z)%E -> (y + z) * x = y * x + z * x
Proof .115d
by move => *; rewrite -!(muleC x) dmuleDr. Qed .
Lemma dge0_muleDl x y z : 0 <= y -> 0 <= z -> (y + z) * x = y * x + z * x.bae
Proof .bae
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.c43
Proof .c46 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.c48
Proof .c48
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.cca
Proof .ccd 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).d53
Proof .d57
move => F0; rewrite !dual_sumeE !mulNe le0_sume_distrl => [|i Pi].cd 19a 19b 6b 1df 339 6b6
(- (\sum_(i <- s | P i) - F i * x))%E =
(- (\sum_(i <- s | P i) - (F i * x)))%E
- 1169
by under eq_bigr => i _ do rewrite mulNe.
- 1173
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).d65
Proof .d68
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).d6a
Proof .d6d
move => F0; rewrite !dual_sumeE mulNe ge0_sume_distrl => [|i Pi].
- 1179
by under eq_bigr => i _ do rewrite mulNe.
- 1182
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).d79
Proof .d7c
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|.dbd
Proof .dc0
by move : x y => [x| |] [y| |] //; rewrite /abse -dEFinD 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|.dc2
Proof .dc6
elim /big_ind2 : _ => //; first by rewrite abse0.dc4 forall x1 x2 y1 y2 : \bar R,
(`|x2| <= x1)%E ->
(`|y2| <= y1)%E -> (`|(x2 + y2)%dE| <= (x1 + y1)%dE)%E
by move => *; exact /(le_trans (lee_abs_dadd _ _) (lee_dadd _ _)).
Qed .
Lemma lee_abs_dsub x y : `|x - y| <= `|x| + `|y|.dcc
Proof .dcf
by move : x y => [x| |] [y| |] //; rewrite /abse -dEFinD lee_fin ler_norm_sub.
Qed .
Lemma dadde_minl : left_distributive (@dual_adde R) mine.ed left_distributive +%dE mine
Proof .118e
by move => x y z; rewrite !dual_addeE oppe_min adde_maxl oppe_max. Qed .
Lemma dadde_minr : right_distributive (@dual_adde R) mine.ed right_distributive +%dE mine
Proof .1193
by move => x y z; rewrite !dual_addeE oppe_min adde_maxr oppe_max. Qed .
Lemma dmule_natl x n : n%:R%:E * x = x *+ n.f1a
Proof .f1a
by rewrite mule_natl ednatmulE. Qed .
Lemma lee_pdaddl y x z : 0 <= x -> y <= z -> y <= x + z.1055
Proof .105a by move => *; rewrite -[y]dadd0e lee_dadd. Qed .
Lemma lte_pdaddl y x z : 0 <= x -> y < z -> y < x + z.105c
Proof .105f by move => x0 /lt_le_trans; apply ; rewrite lee_pdaddl. Qed .
Lemma lee_pdaddr y x z : 0 <= x -> y <= z -> y <= z + x.1061
Proof .1064 by move => *; rewrite daddeC lee_pdaddl. Qed .
Lemma lte_pdaddr y x z : 0 <= x -> y < z -> y < z + x.1066
Proof .1069 by move => *; rewrite daddeC lte_pdaddl. Qed .
Lemma lte_spdaddre z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.106b
Proof .106e
move : z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry,ltNyr)//.1072 (0 < y)%R -> (z%:E <= x%:E)%E -> (z < x + y)%R
exact : ltr_spaddr.
Qed .
Lemma lte_spdadder z x y : x \is a fin_num -> 0 < y -> z <= x -> z < x + y.1076
Proof .1079
move : z y x => [z| |] [y| |] [x| |] _ //=; rewrite ?(lte_fin,ltry,ltNyr)//.119e
exact : ltr_spaddr.
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 : numDomainType} : {mono @oppe R : x y /~ x <= y}.29 {mono -%E : y x / x <= y >-> y <= x}
Proof .11a4
move => x y; case : x y => [?||] [?||] //; first by rewrite !lee_fin !ler_opp2.22 _r_ : R
(- _r_%:E <= - -oo) = (-oo <= _r_%:E)
by rewrite /Order.le/= realN.
by rewrite /Order.le/= realN.
Qed .
Lemma lte_opp2 {R : numDomainType} : {mono @oppe R : x y /~ x < y}.29 {mono -%E : y x / x < y >-> y < x}
Proof .11b5
move => x y; case : x y => [?||] [?||] //; first by rewrite !lte_fin !ltr_opp2.11ab (- _r_%:E < - -oo) = (-oo < _r_%:E)
by rewrite /Order.lt/= realN.
by rewrite /Order.lt/= realN.
Qed .
Section realFieldType_lemmas .
Variable R : realFieldType.
Implicit Types x y : \bar R.
Implicit Types r : R.
Lemma lee_adde x y : (forall e : {posnum R}, x <= y + e%:num%:E) -> x <= y.R : realFieldType 23
(forall e : {posnum R}, x <= y + (e%:num)%:E) ->
x <= y
Proof .11c4
move : x y => [x||] [y||] // xleye; rewrite ?leNye ?leey //; last first .11c7 xleye : forall e : {posnum R},
+oo <= -oo + (e%:num)%:E
+oo <= -oo
- 11cb
exact : (le_trans (xleye 1 %:pos%R)).
- 11df
by move : (!! xleye 1 %:pos%R).
- 11e4
by move : (!! xleye 1 %:pos%R).
rewrite leNgt; apply /negP => yltx.11c7 95 11db yltx : y%:E < x%:E
6a0
have xmy_gt0 : (0 < (x - y) / 2 )%R by rewrite ltr_pdivl_mulr// mul0r subr_gt0.11c7 95 11db 11ef xmy_gt0 : (0 < (x - y) / 2 )%R
6a0
move : (xleye (PosNum xmy_gt0)); apply /negP; rewrite -ltNge /= -EFinD lte_fin.11f3 (y + (x - y) / 2 < x)%R
rewrite [Y in (Y + _)%R]splitr [X in (_ < X)%R]splitr.11f3 (y / 2 + y / 2 + (x - y) / 2 < x / 2 + x / 2 )%R
by rewrite -!mulrDl ltr_pmul2r// addrCA addrK ltr_add2l.
Qed .
Lemma lee_mul01Pr x y : 0 <= x ->
reflect (forall r , (0 < r < 1 )%R -> r%:E * x <= y) (x <= y).11c6 0 <= x ->
reflect (forall r , (0 < r < 1 )%R -> r%:E * x <= y)
(x <= y)
Proof .11fe
move => x0; apply /(iffP idP) => [xy r /andP[r0 r1]|h].11c7 23 x0 : 0 <= xe35 ae r0 : (0 < r)%R r1 : (r < 1 )%R
r%:E * x <= y
move : x0 xy; rewrite le_eqVlt => /predU1P[<-|x0 xy]; first by rewrite mule0.11c7 23 ae 1207 1208 b49 e35
1209 120a
by rewrite (le_trans _ xy) // gee_pmull // ltW.
have h01 : (0 < (2 ^-1 : R) < 1 )%R by rewrite invr_gt0 ?invf_lt1 ?ltr0n ?ltr1n .11c7 23 1206 120d h01 : (0 < 2 ^-1 < 1 )%R
120e
move : x y => [x||] [y||] // in x0 h *.11c7 121a 95 7cc h : forall r , (0 < r < 1 )%R -> r%:E * x%:E <= y%:E
11dc
- 121c
move : (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0].
by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin.
have y0 : (0 < y)%R.
by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin.
rewrite lee_fin leNgt; apply /negP => yx.11c7 121a 95 121f 4ca 4d4 yx : (y < x)%R
6a0 1220
have /h : (0 < (y + x) / (2 * x) < 1 )%R.1247 (0 < (y + x) / (2 * x) < 1 )%R
apply /andP; split ; first by rewrite divr_gt0 // ?addr_gt0 // ?mulr_gt0 .1247 ((y + x) / (2 * x) < 1 )%R
124d
by rewrite ltr_pdivr_mulr ?mulr_gt0 // mul1r mulr_natl mulr2n ltr_add2r.
rewrite -(EFinM _ x) lee_fin invrM ?unitfE // ?gt_eqF // -mulrA mulrAC.1247 ((y + x) * (x^-1 * x / 2 ) <= y)%R -> False
1220
by rewrite mulVr ?unitfE ?gt_eqF // mul1r; apply /negP; rewrite -ltNge midf_lt.
- 125c
by rewrite leey.
- 1261
by have := h _ h01.
- 1266
by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
- 126b
by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
Qed .
Lemma lte_pdivr_mull r x y : (0 < r)%R -> (r^-1 %:E * y < x) = (y < r%:E * x).11c7 ae 23
(0 < r)%R -> ((r^-1 )%:E * y < x) = (y < r%:E * x)
Proof .126f
move => r0; move : x y => [x| |] [y| |] //=.11c7 ae 1207 95
((r^-1 )%:E * y%:E < x%:E) = (y%:E < r%:E * x%:E)
- 1275
by rewrite 2 !lte_fin ltr_pdivr_mull.
- 128f
by rewrite mulr_infty sgrV gtr0_sg// mul1e 2 !ltNge 2 !leey.
- 1294
by rewrite mulr_infty sgrV gtr0_sg// mul1e -EFinM 2 !ltNyr.
- 1299
by rewrite mulr_infty gtr0_sg// mul1e 2 !ltry.
- 129e
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e ltxx.
- 12a3
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2 !mul1e.
- 12a8
by rewrite mulr_infty gtr0_sg// mul1e.
- 12ad
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2 !mul1e.
- 12b2
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
Qed .
Lemma lte_pdivr_mulr r x y : (0 < r)%R -> (y * r^-1 %:E < x) = (y < x * r%:E).1271 (0 < r)%R -> (y * (r^-1 )%:E < x) = (y < x * r%:E)
Proof .12b6
by move => r0; rewrite muleC lte_pdivr_mull// muleC. Qed .
Lemma lte_pdivl_mull r y x : (0 < r)%R -> (x < r^-1 %:E * y) = (r%:E * x < y).11c7 ae 751
(0 < r)%R -> (x < (r^-1 )%:E * y) = (r%:E * x < y)
Proof .12bb
move => r0; move : x y => [x| |] [y| |] //=.1277 (x%:E < (r^-1 )%:E * y%:E) = (r%:E * x%:E < y%:E)
- 12c1
by rewrite 2 !lte_fin ltr_pdivl_mull.
- 12d7
by rewrite mulr_infty sgrV gtr0_sg// mul1e 2 !ltry.
- 12dc
by rewrite mulr_infty sgrV gtr0_sg// mul1e.
- 12e1
by rewrite mulr_infty gtr0_sg// mul1e.
- 12e6
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
- 12eb
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2 !mul1e.
- 12f0
by rewrite mulr_infty gtr0_sg// mul1e 2 !ltNyr.
- 12f5
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2 !mul1e.
- 12fa
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
Qed .
Lemma lte_pdivl_mulr r x y : (0 < r)%R -> (x < y * r^-1 %:E) = (x * r%:E < y).1271 (0 < r)%R -> (x < y * (r^-1 )%:E) = (x * r%:E < y)
Proof .12fe
by move => r0; rewrite muleC lte_pdivl_mull// muleC. Qed .
Lemma lte_ndivl_mulr r x y : (r < 0 )%R -> (x < y * r^-1 %:E) = (y < x * r%:E).1271 (r < 0 )%R -> (x < y * (r^-1 )%:E) = (y < x * r%:E)
Proof .1303
rewrite -oppr0 ltr_oppr => r0; rewrite -{1 }(opprK r) invrN.11c7 ae 23 r0 : (0 < - r)%R
(x < y * (- (- r)^-1 )%:E) = (y < x * r%:E)
by rewrite EFinN muleN lte_oppr lte_pdivr_mulr// EFinN muleNN.
Qed .
Lemma lte_ndivl_mull r x y : (r < 0 )%R -> (x < r^-1 %:E * y) = (y < r%:E * x).1271 (r < 0 )%R -> (x < (r^-1 )%:E * y) = (y < r%:E * x)
Proof .130e
by move => r0; rewrite muleC lte_ndivl_mulr// muleC. Qed .
Lemma lte_ndivr_mull r x y : (r < 0 )%R -> (r^-1 %:E * y < x) = (r%:E * x < y).1271 (r < 0 )%R -> ((r^-1 )%:E * y < x) = (r%:E * x < y)
Proof .1313
rewrite -oppr0 ltr_oppr => r0; rewrite -{1 }(opprK r) invrN.130a ((- (- r)^-1 )%:E * y < x) = (r%:E * x < y)
by rewrite EFinN mulNe lte_oppl lte_pdivl_mull// EFinN muleNN.
Qed .
Lemma lte_ndivr_mulr r x y : (r < 0 )%R -> (y * r^-1 %:E < x) = (x * r%:E < y).1271 (r < 0 )%R -> (y * (r^-1 )%:E < x) = (x * r%:E < y)
Proof .131c
by move => r0; rewrite muleC lte_ndivr_mull// muleC. Qed .
Lemma lee_pdivr_mull r x y : (0 < r)%R -> (r^-1 %:E * y <= x) = (y <= r%:E * x).1271 (0 < r)%R -> ((r^-1 )%:E * y <= x) = (y <= r%:E * x)
Proof .1321
move => r0; apply /idP/idP.11c7 ae 23 1207
(r^-1 )%:E * y <= x -> y <= r%:E * x
- 1326
rewrite le_eqVlt => /predU1P[<-|]; last by rewrite lte_pdivr_mull// => /ltW.1328 y <= r%:E * ((r^-1 )%:E * y)
132a
by rewrite muleA -EFinM divrr ?mul1e // unitfE gt_eqF.
- 1333
rewrite le_eqVlt => /predU1P[->|]; last by rewrite -lte_pdivr_mull// => /ltW.1328 (r^-1 )%:E * (r%:E * x) <= x
by rewrite muleA -EFinM mulVr ?mul1e // unitfE gt_eqF.
Qed .
Lemma lee_pdivr_mulr r x y : (0 < r)%R -> (y * r^-1 %:E <= x) = (y <= x * r%:E).1271 (0 < r)%R -> (y * (r^-1 )%:E <= x) = (y <= x * r%:E)
Proof .133b
by move => r0; rewrite muleC lee_pdivr_mull// muleC. Qed .
Lemma lee_pdivl_mull r y x : (0 < r)%R -> (x <= r^-1 %:E * y) = (r%:E * x <= y).12bd (0 < r)%R -> (x <= (r^-1 )%:E * y) = (r%:E * x <= y)
Proof .1340
move => r0; apply /idP/idP.11c7 ae 751 1207
x <= (r^-1 )%:E * y -> r%:E * x <= y
- 1345
rewrite le_eqVlt => /predU1P[->|]; last by rewrite lte_pdivl_mull// => /ltW.1347 r%:E * ((r^-1 )%:E * y) <= y
1349
by rewrite muleA -EFinM divrr ?mul1e // unitfE gt_eqF.
- 1352
rewrite le_eqVlt => /predU1P[<-|]; last by rewrite -lte_pdivl_mull// => /ltW.1347 x <= (r^-1 )%:E * (r%:E * x)
by rewrite muleA -EFinM mulVr ?mul1e // unitfE gt_eqF.
Qed .
Lemma lee_pdivl_mulr r x y : (0 < r)%R -> (x <= y * r^-1 %:E) = (x * r%:E <= y).1271 (0 < r)%R -> (x <= y * (r^-1 )%:E) = (x * r%:E <= y)
Proof .135a
by move => r0; rewrite muleC lee_pdivl_mull// muleC. Qed .
Lemma lee_ndivl_mulr r x y : (r < 0 )%R -> (x <= y * r^-1 %:E) = (y <= x * r%:E).1271 (r < 0 )%R -> (x <= y * (r^-1 )%:E) = (y <= x * r%:E)
Proof .135f
rewrite -oppr0 ltr_oppr => r0; rewrite -{1 }(opprK r) invrN.130a (x <= y * (- (- r)^-1 )%:E) = (y <= x * r%:E)
by rewrite EFinN muleN lee_oppr lee_pdivr_mulr// EFinN muleNN.
Qed .
Lemma lee_ndivl_mull r x y : (r < 0 )%R -> (x <= r^-1 %:E * y) = (y <= r%:E * x).1271 (r < 0 )%R -> (x <= (r^-1 )%:E * y) = (y <= r%:E * x)
Proof .1368
by move => r0; rewrite muleC lee_ndivl_mulr// muleC. Qed .
Lemma lee_ndivr_mull r x y : (r < 0 )%R -> (r^-1 %:E * y <= x) = (r%:E * x <= y).1271 (r < 0 )%R -> ((r^-1 )%:E * y <= x) = (r%:E * x <= y)
Proof .136d
rewrite -oppr0 ltr_oppr => r0; rewrite -{1 }(opprK r) invrN.130a ((- (- r)^-1 )%:E * y <= x) = (r%:E * x <= y)
by rewrite EFinN mulNe lee_oppl lee_pdivl_mull// EFinN muleNN.
Qed .
Lemma lee_ndivr_mulr r x y : (r < 0 )%R -> (y * r^-1 %:E <= x) = (x * r%:E <= y).1271 (r < 0 )%R -> (y * (r^-1 )%:E <= x) = (x * r%:E <= y)
Proof .1376
by move => r0; rewrite muleC lee_ndivr_mull// muleC. Qed .
End realFieldType_lemmas .
Module DualAddTheoryRealField .
Import DualAddTheoryNumDomain DualAddTheoryRealDomain.
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.11c4
Proof .11c4
by move => xye; apply : lee_adde => e; case : x {xye} (xye e). Qed .
End DualRealFieldType_lemmas .
End DualAddTheoryRealField .
Module DualAddTheory .
Export DualAddTheoryNumDomain.
Export DualAddTheoryRealDomain.
Export DualAddTheoryRealField.
End DualAddTheory .
Module ConstructiveDualAddTheory .
Export DualAddTheory.
End ConstructiveDualAddTheory .
Definition posnume (R : numDomainType) of phant R := {> 0 : \bar R}.
Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
Definition nonnege (R : numDomainType) of phant R := {>= 0 : \bar R}.
Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing )
: ereal_dual_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing )
: ereal_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing )
: ereal_dual_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing )
: ereal_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0 )) _ _)
(only printing ) : ereal_dual_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0 )) _ _)
(only printing ) : ereal_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0 )) _ _)
(only printing ) : ereal_dual_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0 )) _ _)
(only printing ) : ereal_scope.
#[global ] Hint Extern 0 (is_true (0 %E < _)%O) => solve [apply : gt0] : core.
#[global ] Hint Extern 0 (is_true (_ < 0 %E)%O) => solve [apply : lt0] : core.
#[global ] Hint Extern 0 (is_true (0 %E <= _)%O) => solve [apply : ge0] : core.
#[global ] Hint Extern 0 (is_true (_ <= 0 %E)%O) => solve [apply : le0] : core.
#[global ] Hint Extern 0 (is_true (0 %E >=< _)%O) => solve [apply : cmp0] : core.
#[global ] Hint Extern 0 (is_true (_ != 0 %E)%O) => solve [apply : neq0] : core.
Section SignedNumDomainStability .
Context {R : numDomainType}.
Lemma pinfty_snum_subproof : Signed.spec 0 !=0 >=0 (+oo : \bar R).29 Signed.spec 0 !=0 >=0 (+oo : \bar R)
Proof .137d
by rewrite /= le0y. Qed .
Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof).
Lemma ninfty_snum_subproof : Signed.spec 0 !=0 <=0 (-oo : \bar R).29 Signed.spec 0 !=0 <=0 (-oo : \bar R)
Proof .1382
by rewrite /= leNy0. Qed .
Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof).
Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) :
Signed.spec 0 nz cond x%:num%:E.22 nz : KnownSign.nullity cond : KnownSign.reality x : {num R & nz & cond}
(KnownSign.nullity_bool nz ==> ((x%:num)%:E != 0 )) &&
Signed.reality_cond 0 cond (x%:num)%:E
Proof .1387
apply /andP; split .1389 KnownSign.nullity_bool nz ==> ((x%:num)%:E != 0 )
case : cond nz x => [[[]|]|] [] x //=;
do ?[by case : (bottom x)|by rewrite eqe eq0F].
case : cond nz x => [[[]|]|] [] x //=;
do ?[by case : (bottom x)|by rewrite ?lee_fin ?(eq0, ge0, le0) ?[_ || _]cmp0].
Qed .
Canonical EFin_snum nz cond (x : {num R & nz & cond}) :=
Signed.mk (EFin_snum_subproof x).
Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :
Signed.spec 0 %R ?=0 xr (fine x%:num).22 xnz : KnownSign.nullity xr : KnownSign.reality x : {compare 0 : \bar R & xnz & xr}
(KnownSign.nullity_bool ?=0 ==> (fine x%:num != 0 %R)) &&
Signed.reality_cond 0 %R xr (fine x%:num)
Proof .139a
case : xr x => [[[]|]|]//= [x /andP[_]]/=.22 139d x : ereal_porderType
x == 0 -> fine x == 0 %R
- 13a3
by move => /eqP ->.
- 13af
by case : x.
- 13b4
by case : x.
- 13b9
by move => /orP[]; case : x => [x||]//=; rewrite lee_fin => ->; rewrite ?orbT .
Qed .
Canonical fine_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (fine_snum_subproof x).
Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := opp_reality_subdef xnz xr) :
Signed.spec 0 xnz r (- x%:num).22 139d 139e 139f r := opp_reality_subdef xnz xr : KnownSign.reality
Signed.spec 0 xnz r (- x%:num)
Proof .13bd
rewrite {}/r; case : xr xnz x => [[[]|]|] [] x //=;
do ?[by case : (bottom x)
|by rewrite ?eqe_oppLR ?oppe0 1 ?eq0 //;
rewrite ?oppe_le0 ?oppe_ge0 ?(eq0, eq0F, ge0, le0)//;
rewrite orbC [_ || _]cmp0].
Qed .
Canonical oppe_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (oppe_snum_subproof x).
Lemma adde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num + y%:num).22 xnz, ynz : KnownSign.nullity xr, yr : KnownSign.reality 139f y : {compare 0 : \bar R & ynz & yr} rnz := add_nonzero_subdef xnz ynz xr yr : KnownSign.nullity rrl := add_reality_subdef xnz ynz xr yr : KnownSign.reality
Signed.spec 0 rnz rrl (x%:num + y%:num)
Proof .13c4
rewrite {}/rnz {}/rrl; apply /andP; split .22 13c7 13c8 139f 13c9
KnownSign.nullity_bool
(add_nonzero_subdef xnz ynz xr yr) ==>
(x%:num + y%:num != 0 )
move : xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
by rewrite 1 ?adde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
move : xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
do ?[by case : (bottom x)|by case : (bottom y)
|by rewrite adde_ge0|by rewrite adde_le0
|exact : realDe|by rewrite 2 !eq0 add0e].
Qed .
Canonical adde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (adde_snum_subproof x y).
Import DualAddTheory.
Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num + y%:num)%dE.13c6 Signed.spec 0 rnz rrl (x%:num + y%:num)%dE
Proof .13da
rewrite {}/rnz {}/rrl; apply /andP; split .13d1 KnownSign.nullity_bool
(add_nonzero_subdef xnz ynz xr yr) ==>
((x%:num + y%:num)%dE != 0 )
move : xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
by rewrite 1 ?dadde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
move : xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
do ?[by case : (bottom x)|by case : (bottom y)
|by rewrite dadde_ge0|by rewrite dadde_le0
|exact : realDed|by rewrite 2 !eq0 dadd0e].
Qed .
Canonical dadde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (dadde_snum_subproof x y).
Lemma mule_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := mul_nonzero_subdef xnz ynz xr yr)
(rrl := mul_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num * y%:num).22 13c7 13c8 139f 13c9 rnz := mul_nonzero_subdef xnz ynz xr yr : KnownSign.nullity rrl := mul_reality_subdef xnz ynz xr yr : KnownSign.reality
(KnownSign.nullity_bool rnz ==> (x%:num * y%:num != 0 )) &&
Signed.reality_cond 0 rrl (x%:num * y%:num)
Proof .13e9
rewrite {}/rnz {}/rrl; apply /andP; split .13d1 KnownSign.nullity_bool
(mul_nonzero_subdef xnz ynz xr yr) ==>
(x%:num * y%:num != 0 )
by move : xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y;
rewrite mule_neq0.
by move : xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //;
do ?[by case : (bottom x)|by case : (bottom y)
|by rewrite mule_ge0|by rewrite mule_le0_ge0
|by rewrite mule_ge0_le0|by rewrite mule_le0|exact : realMe
|by rewrite eq0 ?mule0 // mul0e].
Qed .
Canonical mule_snum (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (mule_snum_subproof x y).
Definition abse_reality_subdef (xnz : KnownSign.nullity)
(xr : KnownSign.reality) := (if xr is =0 then =0 else >=0 )%snum_sign.
Arguments abse_reality_subdef /.
Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) :
Signed.spec 0 xnz r `|x%:num|.22 139d 139e 139f r := abse_reality_subdef xnz xr : KnownSign.sign
Signed.spec 0 xnz r `|x%:num|
Proof .13fb
rewrite {}/r; case : xr xnz x => [[[]|]|] [] x //=;
do ?[by case : (bottom x)|by rewrite eq0 abse0
|by rewrite abse_ge0// andbT gee0_abs
|by rewrite abse_ge0// andbT lee0_abs
|by rewrite abse_ge0// andbT abse_eq0].
Qed .
Canonical abse_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (abse_snum_subproof x).
End SignedNumDomainStability .
Section MorphNum .
Context {R : numDomainType} {nz : KnownSign.nullity} {cond : KnownSign.reality}.
Local Notation nR := {compare (0 : \bar R) & nz & cond}.
Implicit Types (a : \bar R).
Lemma num_abse_eq0 a : (`|a|%:nng == 0 %:nng) = (a == 0 ).22 138a 138b a : \bar R
(`|a|%:nng == 0 %:nng :> {nonneg \bar R}) = (a == 0 )
Proof .1402
by rewrite -abse_eq0. Qed .
End MorphNum .
Section MorphReal .
Context {R : numDomainType} {nz : KnownSign.nullity} {r : KnownSign.real}.
Local Notation nR := {compare (0 : \bar R) & nz & r}.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : R) nz r).
Lemma num_lee_maxr a x y :
a <= maxe x%:num y%:num = (a <= x%:num) || (a <= y%:num).22 138a r : KnownSign.real 1405 x, y : {compare 0 : \bar R & nz & r}
(a <= maxe x%:num y%:num) =
(a <= x%:num) || (a <= y%:num)
Proof .1409
by rewrite -comparable_le_maxr// ereal_comparable. Qed .
Lemma num_lee_maxl a x y :
maxe x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a).140b (maxe x%:num y%:num <= a) =
(x%:num <= a) && (y%:num <= a)
Proof .1411
by rewrite -comparable_le_maxl// ereal_comparable. Qed .
Lemma num_lee_minr a x y :
a <= mine x%:num y%:num = (a <= x%:num) && (a <= y%:num).140b (a <= mine x%:num y%:num) =
(a <= x%:num) && (a <= y%:num)
Proof .1416
by rewrite -comparable_le_minr// ereal_comparable. Qed .
Lemma num_lee_minl a x y :
mine x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a).140b (mine x%:num y%:num <= a) =
(x%:num <= a) || (y%:num <= a)
Proof .141b
by rewrite -comparable_le_minl// ereal_comparable. Qed .
Lemma num_lte_maxr a x y :
a < maxe x%:num y%:num = (a < x%:num) || (a < y%:num).140b (a < maxe x%:num y%:num) =
(a < x%:num) || (a < y%:num)
Proof .1420
by rewrite -comparable_lt_maxr// ereal_comparable. Qed .
Lemma num_lte_maxl a x y :
maxe x%:num y%:num < a = (x%:num < a) && (y%:num < a).140b (maxe x%:num y%:num < a) =
(x%:num < a) && (y%:num < a)
Proof .1425
by rewrite -comparable_lt_maxl// ereal_comparable. Qed .
Lemma num_lte_minr a x y :
a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).140b (a < mine x%:num y%:num) =
(a < x%:num) && (a < y%:num)
Proof .142a
by rewrite -comparable_lt_minr// ereal_comparable. Qed .
Lemma num_lte_minl a x y :
mine x%:num y%:num < a = (x%:num < a) || (y%:num < a).140b (mine x%:num y%:num < a) =
(x%:num < a) || (y%:num < a)
Proof .142f
by rewrite -comparable_lt_minl// ereal_comparable. Qed .
End MorphReal .
Section MorphGe0 .
Context {R : numDomainType} {nz : KnownSign.nullity}.
Local Notation nR := {compare (0 : \bar R) & ?=0 & >=0 }.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : \bar R) ?=0 >=0 ).
Lemma num_abse_le a x : 0 <= a -> (`|a|%:nng <= x)%O = (a <= x%:num).22 138a 1405 x : {compare 0 : \bar R & ?=0 & >=0 }
0 <= a ->
((`|a|%:nng : {nonneg \bar R}) <= x) = (a <= x%:num)
Proof .1434
by move => a0; rewrite -num_le//= gee0_abs. Qed .
Lemma num_abse_lt a x : 0 <= a -> (`|a|%:nng < x)%O = (a < x%:num).1436 0 <= a ->
((`|a|%:nng : {nonneg \bar R}) < x) = (a < x%:num)
Proof .143b
by move => a0; rewrite -num_lt/= gee0_abs. Qed .
End MorphGe0 .
Variant posnume_spec (R : numDomainType) (x : \bar R) :
\bar R -> bool -> bool -> bool -> Type :=
| IsPinftyPosnume :
posnume_spec x +oo false true true
| IsRealPosnume (p : {posnum R}) :
posnume_spec x (p%:num%:E) false true true.
Lemma posnumeP (R : numDomainType) (x : \bar R) : 0 < x ->
posnume_spec x x (x == 0 ) (0 <= x) (0 < x).6a 0 < x -> posnume_spec x x (x == 0 ) (0 <= x) (0 < x)
Proof .1440
case : x => [x|_|//]; last by rewrite le0y lt0y; exact : IsPinftyPosnume.99 0 < x%:E ->
posnume_spec x%:E x%:E (x%:E == 0 ) (0 <= x%:E)
(0 < x%:E)
rewrite lte_fin lee_fin eqe => x_gt0.22 9a x_gt0 : (0 < x)%R
posnume_spec x%:E x%:E (x == 0 %R) (0 <= x)%R (0 < x)%R
rewrite x_gt0 (ltW x_gt0) (negbTE (lt0r_neq0 x_gt0)).144b posnume_spec x%:E x%:E false true true
exact : IsRealPosnume (PosNum x_gt0).
Qed .
Variant nonnege_spec (R : numDomainType) (x : \bar R) :
\bar R -> bool -> Type :=
| IsPinftyNonnege : nonnege_spec x +oo true
| IsRealNonnege (p : {nonneg R}) : nonnege_spec x (p%:num%:E) true.
Lemma nonnegeP (R : numDomainType) (x : \bar R) : 0 <= x ->
nonnege_spec x x (0 <= x).6a 0 <= x -> nonnege_spec x x (0 <= x)
Proof .1453
case : x => [x|_|//]; last by rewrite le0y; exact : IsPinftyNonnege.99 0 <= x%:E -> nonnege_spec x%:E x%:E (0 <= x%:E)
by rewrite lee_fin => /[dup] x_ge0 ->; exact : IsRealNonnege (NngNum x_ge0).
Qed .
Section contract_expand .
Variable R : realFieldType.
Implicit Types (x : \bar R) (r : R).
Local Open Scope ereal_scope.
Definition contract x : R :=
match x with
| r%:E => r / (1 + `|r|) | +oo => 1 | -oo => -1
end .
Lemma contract_lt1 r : (`|contract r%:E| < 1 )%R.11c7 ae
(`|contract r%:E| < 1 )%R
Proof .145c
rewrite normrM normrV ?unitfE //.145e (`|r| / `|1 + `|r|| < 1 )%R
rewrite ltr_pdivr_mulr // ?mul1r //; last by rewrite gtr0_norm.145e (`|r| < `|1 + `|r||)%R
by rewrite [ltRHS]gtr0_norm ?ltr_addr // ltr_spaddl.
Qed .
Lemma contract_le1 x : (`|contract x| <= 1 )%R.11c7 6b
(`|contract x| <= 1 )%R
Proof .146a
by case : x => [r| |] /=; rewrite ?normrN1 ?normr1 // (ltW (contract_lt1 _)).
Qed .
Lemma contract0 : contract 0 = 0 %R.
Proof .1470
by rewrite /contract mul0r. Qed .
Lemma contractN x : contract (- x) = (- contract x)%R.146c contract (- x) = (- contract x)%R
Proof .1476
by case : x => //= [r|]; [ rewrite normrN mulNr | rewrite opprK]. Qed .
(* TODO: not exploited yet: expand is nondecreasing everywhere so it should be
possible to use some of the homoRL/homoLR lemma where monoRL/monoLR do not
apply *)
Definition expand r : \bar R :=
if (r >= 1 )%R then +oo else if (r <= -1 )%R then -oo else (r / (1 - `|r|))%:E.
Lemma expand1 r : (1 <= r)%R -> expand r = +oo.145e (1 <= r)%R -> expand r = +oo
Proof .147b
by move => r1; rewrite /expand r1. Qed .
Lemma expandN r : expand (- r)%R = - expand r.145e expand (- r) = - expand r
Proof .1480
rewrite /expand; case : ifPn => [r1|].11c7 ae r1 : (1 <= - r)%R
+oo =
-
(if (1 <= r)%R
then +oo
else if (r <= -1 )%R then -oo else (r / (1 - `|r|))%:E)
rewrite ifF; [by rewrite ifT // -ler_oppr|apply /negbTE].
by rewrite -ltNge -(opprK r) -ltr_oppl (lt_le_trans _ r1) // -subr_gt0 opprK.
rewrite -ltNge => r1; case : ifPn; rewrite ler_oppl opprK; [by move => ->|].11c7 ae r1 : (- r < 1 )%R
~~ (1 <= r)%R ->
(- r / (1 - `|- r|))%:E =
-
(if (1 <= r)%R
then +oo
else if (r <= -1 )%R then -oo else (r / (1 - `|r|))%:E)
by rewrite -ltNge leNgt => ->; rewrite leNgt -ltr_oppl r1 /= mulNr normrN.
Qed .
Lemma expandN1 r : (r <= -1 )%R -> expand r = -oo.145e (r <= -1 )%R -> expand r = -oo
Proof .149b
by rewrite ler_oppr => /expand1/eqP; rewrite expandN eqe_oppLR => /eqP.
Qed .
Lemma expand0 : expand 0 %R = 0 .
Proof .14a0
by rewrite /expand leNgt ltr01 /= oppr_ge0 leNgt ltr01 /= mul0r. Qed .
Lemma expandK : {in [pred r | `|r| <= 1 ]%R, cancel expand contract}.1472 {in [pred r | (`|r| <= 1 )%R], cancel expand contract}
Proof .14a5
move => r; rewrite inE le_eqVlt => /orP[|r1].145e `|r|%R == 1 %R -> contract (expand r) = r
rewrite eqr_norml => /andP[/orP[]/eqP->{r}] _;
by [rewrite expand1|rewrite expandN1].
rewrite /expand 2 !leNgt ltr_oppl; case /ltr_normlP : (r1) => -> -> /=.14af r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|) = r
have r_pneq0 : (1 + r / (1 - r) != 0 )%R.14af (1 + r / (1 - r))%R != 0 %R
rewrite -[X in (X + _)%R](@divrr _ (1 - r)%R) -?mulrDl ; last first .14af (1 - r)%R \is a GRing.unit
by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt_eqF // ltr_normlW.
have r_nneq0 : (1 - r / (1 + r) != 0 )%R.14bf (1 - r / (1 + r))%R != 0 %R
rewrite -[X in (X + _)%R](@divrr _ (1 + r)%R) -?mulrBl ; last first .14bf (1 + r)%R \is a GRing.unit
by rewrite unitfE addrC addr_eq0 gt_eqF // ltrNnormlW.
rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym gt_eqF //.
exact : ltrNnormlW.
wlog : r r1 r_pneq0 r_nneq0 / (0 <= r)%R => wlog_r0.11c7 ae 14b0 14c0 14d5 wlog_r0 : forall r : R,
(`|r| < 1 )%R ->
(1 + r / (1 - r))%R != 0 %R ->
(1 - r / (1 + r))%R != 0 %R ->
(0 <= r)%R ->
r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|) = r
14b8
have [r0|r0] := lerP 0 r; first by rewrite wlog_r0.11c7 ae 14b0 14c0 14d5 14eb de5
14b8 14ec
move : (wlog_r0 (- r)%R).14f3 ((`|- r| < 1 )%R ->
(1 + - r / (1 - - r))%R != 0 %R ->
(1 - - r / (1 - r))%R != 0 %R ->
(0 <= - r)%R ->
- r / (1 - `|(- r)%R|) /
(1 + `|- r / (1 - `|(- r)%R|)|) = (- r)%R) ->
r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|) = r
14ec
rewrite !(normrN, opprK, mulNr) oppr_ge0 => /(_ r1 r_nneq0 r_pneq0 (ltW r0)).14f3 (- (r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|)))%R =
(- r)%R ->
r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|) = r
14ec
by move /eqP; rewrite eqr_opp => /eqP.
rewrite /contract !ger0_norm //; last first .
by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW r1)) // ler_norm.
apply : (@mulIr _ (1 + r / (1 - r))%R); first by rewrite unitfE.14ee (r / (1 - r) / (1 + r / (1 - r)) * (1 + r / (1 - r)))%R =
(r * (1 + r / (1 - r)))%R
rewrite -(mulrA (r / _)) mulVr ?unitfE // mulr1.14ee r / (1 - r) = (r * (1 + r / (1 - r)))%R
rewrite -[X in (X + _ / _)%R](@divrr _ (1 - r)%R) -?mulrDl ?subrK ?div1r //.
by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
Qed .
Lemma le_contract : {mono contract : x y / (x <= y)%O}.1472 {mono contract : x y / x <= y >-> (x <= y)%R}
Proof .1515
apply : le_mono; move => -[r0 | | ] [r1 | _ | _] //=.11c7 11c
r0%:E < r1%:E ->
(r0 / (1 + `|r0|) < r1 / (1 + `|r1|))%R
- 151a
rewrite lte_fin => r0r1; rewrite ltr_pdivr_mulr ?ltr_paddr //.11c7 11c r0r1 : (r0 < r1)%R
(r0 < r1 / (1 + `|r1|) * (1 + `|r0|))%R
151e
rewrite mulrAC ltr_pdivl_mulr ?ltr_paddr // 2 ?mulrDr 2 ?mulr1 .152d (r0 + r0 * `|r1| < r1 + r1 * `|r0|)%R
151e
have [r10|?] := ler0P r1; last first .11c7 11c 152e _i_ : (0 < r1)%R
(r0 + r0 * r1 < r1 + r1 * `|r0|)%R
rewrite ltr_le_add // mulrC; have [r00|//] := ler0P r0.11c7 11c 152e 1538 r00 : (r0 <= 0 )%R
(r0 * r1 <= - r0 * r1)%R
153a
by rewrite (@le_trans _ _ 0 %R) // ?pmulr_lle0 // mulr_ge0// ?oppr_ge0 // ltW.
have [?|r00] := ler0P r0; first by rewrite ltr_le_add // 2 !mulrN mulrC.11c7 11c 152e 153d r00 : (0 < r0)%R
(r0 + r0 * - r1 < r1 + r1 * r0)%R
151e
by move : (le_lt_trans r10 (lt_trans r00 r0r1)); rewrite ltxx.
- 154f
by rewrite ltr_pdivr_mulr ?ltr_paddr // mul1r ltr_spaddl // ler_norm.
- 1554
rewrite ltr_pdivl_mulr ?mulN1r ?ltr_paddr // => _.1524 (- (1 + `|r1|) < r1)%R
1556
by rewrite ltr_oppl ltr_spaddl // ler_normr lexx orbT.
- 155d
by rewrite -subr_gt0 opprK.
Qed .
Definition lt_contract := leW_mono le_contract.
Definition contract_inj := mono_inj lexx le_anti le_contract.
Lemma le_expand_in : {in [pred r | `|r| <= 1 ]%R &,
{mono expand : x y / (x <= y)%O}}.1472 {in [pred r | (`|r| <= 1 )%R] &,
{mono expand : x y / (x <= y)%R >-> x <= y}}
Proof .1561
exact : can_mono_in (onW_can_in predT expandK) _ (in2W le_contract). Qed .
Definition lt_expand := leW_mono_in le_expand_in.
Definition expand_inj := mono_inj_in lexx le_anti le_expand_in.
Lemma fine_expand r : (`|r| < 1 )%R ->
(fine (expand r))%:E = expand r.145e (`|r| < 1 )%R -> (fine (expand r))%:E = expand r
Proof .1566
by move => r1; rewrite /expand 2 !leNgt ltr_oppl; case /ltr_normlP : r1 => -> ->.
Qed .
Lemma le_expand : {homo expand : x y / (x <= y)%O}.1472 {homo expand : x y / (x <= y)%R >-> x <= y}
Proof .156b
move => x y xy; have [x1|] := lerP `|x| 1 .11c7 95 xy : (x <= y)%R x1 : (`|x| <= 1 )%R
expand x <= expand y
have [y_le1|/ltW /expand1->] := leP y 1 %R; last by rewrite leey.11c7 95 1573 1574 y_le1 : (y <= 1 )%R
1575 1576
rewrite le_expand_in ?inE // ler_norml y_le1 (le_trans _ xy)//.
by rewrite ler_oppl (ler_normlP _ _ _).
rewrite ltr_normr => /orP[|] x1; last first .11c7 95 1573 x1 : (1 < - x)%R
1575
by rewrite expandN1 // ?leNye // ler_oppr ltW.
by rewrite expand1; [rewrite expand1 // (le_trans _ xy) // ltW | exact : ltW].
Qed .
Lemma expand_eqoo r : (expand r == +oo) = (1 <= r)%R.145e (expand r == +oo) = (1 <= r)%R
Proof .1593
by rewrite /expand; case : ifP => //; case : ifP. Qed .
Lemma expand_eqNoo r : (expand r == -oo) = (r <= -1 )%R.145e (expand r == -oo) = (r <= -1 )%R
Proof .1598
rewrite /expand; case : ifP => /= r1; last by case : ifP.11c7 ae r1 : (1 <= r)%R
(+oo == -oo) = (r <= -1 )%R
by apply /esym/negbTE; rewrite -ltNge (lt_le_trans _ r1) // -subr_gt0 opprK.
Qed .
End contract_expand .
Section ereal_PseudoMetric .
Variable R : realFieldType.
Implicit Types (x y : \bar R) (r : R).
Definition ereal_ball x r y := (`|contract x - contract y| < r)%R.
Lemma ereal_ball_center x r : (0 < r)%R -> ereal_ball x r x.11c7 6b ae
(0 < r)%R -> ereal_ball x r x
Proof .15a3
by move => e0; rewrite /ereal_ball subrr normr0. Qed .
Lemma ereal_ball_sym x y r : ereal_ball x r y -> ereal_ball y r x.11c7 23 ae
ereal_ball x r y -> ereal_ball y r x
Proof .15a9
by rewrite /ereal_ball distrC. Qed .
Lemma ereal_ball_triangle x y z r1 r2 :
ereal_ball x r1 y -> ereal_ball y r2 z -> ereal_ball x (r1 + r2) z.11c7 1b8 14
ereal_ball x r1 y ->
ereal_ball y r2 z -> ereal_ball x (r1 + r2) z
Proof .15af
rewrite /ereal_ball => h1 h2; rewrite -[X in (X - _)%R](subrK (contract y)).11c7 1b8 14 h1 : (`|contract x - contract y| < r1)%R h2 : (`|contract y - contract z| < r2)%R
(`|contract x - contract y + contract y - contract z| <
r1 + r2)%R
by rewrite -addrA (le_lt_trans (ler_norm_add _ _)) // ltr_add.
Qed .
Lemma ereal_ballN x y (e : {posnum R}) :
ereal_ball (- x) e%:num (- y) -> ereal_ball x e%:num y.11c7 23 e : {posnum R}
ereal_ball (- x) e%:num (- y) -> ereal_ball x e%:num y
Proof .15bc
by rewrite /ereal_ball 2 !contractN opprK -opprB normrN addrC. Qed .
Lemma ereal_ball_ninfty_oversize (e : {posnum R}) x :
(2 < e%:num)%R -> ereal_ball -oo e%:num x.11c7 15bf 6b
(2 < e%:num)%R -> ereal_ball -oo e%:num x
Proof .15c3
move => e2; rewrite /ereal_ball /= (le_lt_trans _ e2) // -opprB normrN opprK.11c7 15bf 6b e2 : (2 < e%:num)%R
(`|contract x + 1 | <= 2 )%R
rewrite (le_trans (ler_norm_add _ _)) // normr1 -ler_subr_addr.15cb (`|contract x| <= 2 - 1 )%R
by rewrite (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1 )%R // addrK.
Qed .
Lemma contract_ereal_ball_pinfty r (e : {posnum R}) :
(1 < contract r%:E + e%:num)%R -> ereal_ball r%:E e%:num +oo.11c7 ae 15bf
(1 < contract r%:E + e%:num)%R ->
ereal_ball r%:E e%:num +oo
Proof .15d3
move => re1; rewrite /ereal_ball; rewrite [contract +oo]/= ler0_norm; last first .11c7 ae 15bf re1 : (1 < contract r%:E + e%:num)%R
(contract r%:E - 1 <= 0 )%R
by rewrite subr_le0; case /ler_normlP: (contract_le1 r%:E).
by rewrite opprB ltr_subl_addl.
Qed .
End ereal_PseudoMetric .
(* TODO: generalize to numFieldType? *)
Lemma lt_ereal_nbhs (R : realFieldType) (a b : \bar R) (r : R) :
a < r%:E -> r%:E < b ->
exists delta : {posnum R},
forall y , (`|y - r| < delta%:num)%R -> (a < y%:E) && (y%:E < b).11c7 a, b : \bar R ae
a < r%:E ->
r%:E < b ->
exists delta : {posnum R},
forall y : R,
(`|y - r| < delta%:num)%R -> a < y%:E < b
Proof .15e5
move => [:wlog ]; case : a b => [a||] [b||] //= ltax ltxb.11c7 ae wlog : <hidden 1 > a, b : R ltax : a%:E < r%:E ltxb : r%:E < b%:E
exists delta : {posnum R},
forall y : R,
(`|y - r| < delta%:num)%R -> a%:E < y%:E < b%:E
- 15ec
move : a b ltax ltxb; abstract : wlog . (*BUG*) 15e7 forall a b : R,
a%:E < r%:E ->
r%:E < b%:E ->
exists delta : {posnum R},
forall y : R,
(`|y - r| < delta%:num)%R -> a%:E < y%:E < b%:E
move => {}a {}b ltxa ltxb.11c7 r, a, b : R ltxa : a%:E < r%:E 15f2
15f3 1606
have m_gt0 : (Num.min ((r - a) / 2 ) ((b - r) / 2 ) > 0 )%R.1611 (0 < Num.min ((r - a) / 2 ) ((b - r) / 2 ))%R
by rewrite lt_minr !divr_gt0 // ?subr_gt0 .
exists (PosNum m_gt0 ) => y //=; rewrite lt_minr !ltr_distl.11c7 1612 1613 15f2 161b 9e
[&& (r - (r - a) / 2 < y < r + (r - a) / 2 )%R,
(r - (b - r) / 2 < y)%R
& (y < r + (b - r) / 2 )%R] ->
a%:E < y%:E < b%:E
1606
move => /andP[/andP[ay _] /andP[_ yb]].11c7 1612 1613 15f2 161b 9e ay : (r - (r - a) / 2 < y)%R yb : (y < r + (b - r) / 2 )%R
a%:E < y%:E < b%:E
1606
rewrite 2 !lte_fin (lt_trans _ ay) ?(lt_trans yb) //=.1627 (r + (b - r) / 2 < b)%R
rewrite -subr_gt0 opprD addrA {1 }[(b - r)%R]splitr addrK.1627 (0 < (b - r) / 2 )%R
162f
by rewrite divr_gt0 ?subr_gt0 .
by rewrite -subr_gt0 addrAC {1 }[(r - a)%R]splitr addrK divr_gt0 ?subr_gt0 .
- 163a
have [//||d dP] := wlog a (r + 1 )%R; rewrite ?lte_fin ?ltr_addl //.11c7 ae 1609 8ea 15f1 15f7 d : {posnum R} dP : forall y : R,
(`|y - r| < d%:num)%R -> a%:E < y%:E < (r + 1 )%:E
15f8 163c
by exists d => y /dP /andP[->] /= /lt_le_trans; apply ; rewrite leey.
- 1645
have [//||d dP] := wlog (r - 1 )%R b; rewrite ?lte_fin ?gtr_addl ?ltrN10 //.11c7 ae 1609 15fb 15fc 15f2 1642 dP : forall y : R,
(`|y - r| < d%:num)%R -> (r - 1 )%:E < y%:E < b%:E
15fd 1647
by exists d => y /dP /andP[_ ->] /=; rewrite ltNyr.
- 164f
by exists 1 %:pos%R => ? ?; rewrite ltNyr ltry.
Qed .