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*)
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]
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}.
T: Type

injective EFin
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.
R: eqType

Equality.axiom eq_ereal
a
by case=> [?||][?||]; apply: (iffP idP) => //= [/eqP|[]] ->. Qed. Definition ereal_eqMixin := Equality.Mixin ereal_eqP. Canonical ereal_eqType := Equality.Pack ereal_eqMixin.
d
r1, r2: R

(r1%:E == r2%:E) = (r1 == r2)
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.
R: choiceType

pcancel code decode
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.
R: numDomainType
x, y: \bar R

lt_ereal x y = (y != x) && le_ereal x y
1f
by case: x y => [?||][?||] //=; rewrite lt_def eqe. Qed.
22

reflexive le_ereal
27
by case => /=. Qed.
29
antisymmetric le_ereal
2d
by case=> [?||][?||]/=; rewrite ?andbF => // /le_anti ->. Qed.
29
transitive le_ereal
32
22
_r_, _r1_: R

_r1_ <= _r_ -> _r_ >=< 0%R -> _r1_ >=< 0%R
39
_r_ >=< 0%R -> _r_ <= _r1_ -> _r1_ >=< 0%R
39
3e
by move=> cmp /ge_comparable /comparabler_trans; apply. Qed.
29
unit
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.
21
(x <= y)%O = le_ereal x y
48
by []. Qed.
21
(x < y)%O = lt_ereal x y
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).
22
r, s: R

(r%:E <= s%:E) = (r <= s)%R
52
by []. Qed.
54
(r%:E < s%:E) = (r < s)%R
59
by []. Qed.
29
(0 : \bar R) <= (1 : \bar R)
5e
by rewrite lee_fin. Qed.
29
(0 : \bar R) < (1 : \bar R)
63
by rewrite lte_fin. Qed.
22
x: \bar R

(x <= -oo) = (x == -oo)
68
by case: x. Qed.
6a
(+oo <= x) = (x == +oo)
6f
by case: x. Qed.
29
(0 : \bar R) < +oo
74
exact: real0. Qed.
29
-oo < (0 : \bar R)
79
exact: real0. Qed.
29
(0 : \bar R) <= +oo
7e
exact: real0. Qed.
29
-oo <= (0 : \bar R)
83
exact: real0. Qed.
6a
(0 < x) = (x != 0) && (0 <= x)
88
by case: x => [r| |]//; rewrite lte_fin lee_fin lt0r. Qed.
21
(0%E >=< x)%O -> (0%E >=< y)%O -> (x >=< y)%O
8d
22
x, y: R

x \is Num.real -> y \is Num.real -> (x <= y)%R || (y <= x)%R
22
x: R
x \is Num.real -> (0 <= +oo) || (+oo <= 0) -> (x%:E <= +oo) || (+oo <= x%:E)
22
y: R
(0 <= -oo) || (-oo <= 0) -> y \is Num.real -> (-oo <= y%:E) || (y%:E <= -oo)
92
99
9b
9c
a2
9d
9f
a7
by rewrite /lee/= => _ ->. Qed.
22
r: R

(r%:E < +oo) = (r \is Num.real)
ab
by []. Qed.
ad
(-oo < r%:E) = (r \is Num.real)
b2
by []. Qed.
6a
(x <= +oo) = (fine x \is Num.real)
b7
by case: x => //=; rewrite real0. Qed.
6a
(-oo <= x) = (fine x \is Num.real)
bc
by case: x => //=; rewrite real0. Qed.
6a
0 <= x <-> x = +oo \/ (exists2 r : R, (0 <= r)%R & x = r%:E)
c1
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).
R: realDomainType
ae

r%:E < +oo
ca
exact: num_real. Qed.
cd
6b

(x < +oo) = (x != +oo)
d1
by case: x => // r; rewrite ltry. Qed.
cc
-oo < r%:E
d7
exact: num_real. Qed.
d3
(-oo < x) = (x != -oo)
dc
by case: x => // r; rewrite ltNyr. Qed.
d3
x <= +oo
e1
by case: x => //= r; exact: num_real. Qed.
d3
-oo <= x
e6
by case: x => //= r; exact: num_real. Qed. Definition lteey := (ltey, leey). Definition lteNye := (ltNye, leNye).
cd

totalPOrderMixin [porderType of \bar R]
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.
29
((0 : \bar R) <= ((-1)%:E : \bar R)) = false
f1
by rewrite lee_fin ler0N1. Qed.
29
((0 : \bar R) < ((-1)%:E : \bar R)) = false
f6
by rewrite lte_fin ltr0N1. Qed.
29
(- (1) : \bar R) < (0 : \bar R)
fb
by rewrite lte_fin ltrN10. Qed.
29
(- (1) : \bar R) <= (0 : \bar R)
100
by rewrite lee_fin lerN10. Qed.
6a
0 <= x -> (0 <= fine x)%R
105
by case: x. Qed.
6a
0 < x < +oo -> (0 < fine x)%R
10a
by move: x => [x| |] //=; rewrite ?ltxx ?andbF// lte_fin => /andP[]. Qed.
6a
-oo < x < 0 -> (fine x < 0)%R
10f
by move: x => [x| |] //= /andP[_]; rewrite lte_fin. Qed.
6a
x <= 0 -> (fine x <= 0)%R
114
by case: x. Qed.
22
r0, r1: R

(r0 <= r1)%R -> r0%:E <= r1%:E
119
by []. Qed.
11b
(r0 < r1)%R -> r0%:E < r1%:E
120
by []. Qed.
22
n: nat

+oo *+ n.+1 = +oo
125
by elim: n => //= n ->. Qed.
127
-oo *+ n.+1 = -oo
12c
by elim: n => //= n ->. Qed.
22
ae
128

(r *+ n.+1)%:E = r%:E *+ n.+1
131
by elim: n => //= n <-. Qed.
6a
x *+ 2 = x + x
137
by []. Qed.
6a
x ^+ 2 = x * x
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)].
29
pred_key fin_num
by []. Qed. Canonical fin_num_keyd := KeyedQualifier fin_num_key.
6a
(x \is a fin_num) = (x != -oo) && (x != +oo)
145
by []. Qed.
6a
reflect (x != -oo /\ x != +oo) (x \is a fin_num)
14a
by apply/(iffP idP) => [/andP//|/andP]. Qed.
6a
(x \isn't a fin_num) = (x == -oo) || (x == +oo)
14f
by rewrite fin_numE negb_and ?negbK. Qed.
6a
reflect (x = -oo \/ x = +oo) (x \isn't a fin_num)
154
by rewrite fin_numEn; apply: (iffP orP) => -[]/eqP; by [left|right]. Qed.
6a
-oo < x < +oo -> x \is a fin_num
159
by move=> /andP[oox xoo]; rewrite fin_numE gt_eqF ?lt_eqF. Qed.
6a
(x \is a fin_num) = (`|x| < +oo)
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).
29
{in fin_num &, {homo fine : x y / x <= y >-> (x <= y)%R}}
163
by move=> [? [?| |]| |]. Qed.
29
{in fin_num &, {homo fine : x y / x < y >-> (x < y)%R}}
168
by move=> [? [?| |]| |]. Qed.
29
{in fin_num, {morph fine : x / `|x| >-> `|x|%R}}
16d
by case. Qed.
6a
(`|x| \is a fin_num) = (x \is a fin_num)
172
by case: x. Qed.
6a
x \is a fin_num -> (fine x == 0%R) = (x == 0)
177
by move: x => [//| |] /=; rewrite fin_numE. Qed.
ad
(- r)%:E = - r%:E
17c
by []. Qed.
6a
fine (- x) = (- fine x)%R
181
by case: x => //=; rewrite oppr0. Qed.
22
r, r': R

(r + r')%:E = r%:E + r'%:E
186
by []. Qed.
188
(r - r')%:E = r%:E - r'%:E
18d
by []. Qed.
188
(r * r')%:E = r%:E * r'%:E
192
by []. Qed.
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
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).
21
x +? y = y +? x
1a1
by rewrite /adde_def andbC (andbC (x == -oo)) (andbC (x == +oo)). Qed.
21
x \is a fin_num -> x +? y
1a6
by move: x y => [x| |] [y | |]. Qed.
21
y \is a fin_num -> x +? y
1ab
by rewrite adde_defC; exact: fin_num_adde_defr. Qed.
21
x +? - y = - x +? y
1b0
by move: x y => [x| |] [y| |]. Qed.
22
x, y, z: \bar R

x +? y -> x +? z -> x +? (y + z)
1b5
by move: x y z => [x||] [y||] [z||]. Qed.
6a
x +? -oo = (x != +oo)
1bc
by case: x. Qed.
29
{in [pred x | 0 <= x] &, forall x y, x +? y}
1c1
by move=> [x| |] [y| |]. Qed.
29
commutative +%E
1c6
by case=> [x||] [y||] //; rewrite /adde /= addrC. Qed.
29
right_id (0 : \bar R) +%E
1cb
by case=> // r; rewrite /adde /= addr0. Qed.
29
left_id (0 : \bar R) +%E
1d0
by move=> x; rewrite addeC adde0. Qed.
29
associative +%E
1d5
by case=> [x||] [y||] [z||] //; rewrite /adde /= addrA. Qed. Canonical adde_monoid := Monoid.Law addeA add0e adde0. Canonical adde_comoid := Monoid.ComLaw addeC.
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
1da
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.
29
right_commutative +%E
1ea
exact: Monoid.mulmAC. Qed.
29
left_commutative +%E
1ef
exact: Monoid.mulmCA. Qed.
29
interchange +%E +%E
1f4
exact: Monoid.mulmACA. Qed.
21
0 < x -> 0 < y -> 0 < x + y
1f9
by move: x y => [x| |] [y| |] //; rewrite !lte_fin; exact: addr_gt0. Qed.
21
0 <= x -> 0 <= y -> (x + y == 0) = (x == 0) && (y == 0)
1fe
99
(0 <= x)%R -> 0 <= +oo -> (x%:E + +oo == 0) = (x%:E == 0) && (+oo == 0)
by move=> x0 _ /=; rewrite andbF. Qed.
21
x <= 0 -> y <= 0 -> (x + y == 0) = (x == 0) && (y == 0)
207
99
(x <= 0)%R -> -oo <= 0 -> (x%:E + -oo == 0) = (x%:E == 0) && (-oo == 0)
by move=> x0 _ /=; rewrite andbF. Qed.
21
(0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x + y)%O
210
case: x y => [x||] [y||] //; exact: realD. Qed.
29
- 0 = 0
215
by rewrite /= oppr0. Qed.
29
involutive -%E
21a
by case=> [x||] //=; rewrite opprK. Qed.
29
injective -%E
21f
exact: inv_inj oppeK. Qed.
21
- x +? - y = x +? y
224
by rewrite adde_defN oppeK. Qed.
6a
(- x == 0) = (x == 0)
229
by rewrite -(can_eq oppeK) oppe0. Qed.
21
x +? y -> - (x + y) = - x - y
22e
by move: x y => [x| |] [y| |] //= _; rewrite opprD. Qed.
21
y \is a fin_num -> - (x + y) = - x - y
233
by move=> finy; rewrite oppeD// fin_num_adde_defl. Qed.
6a
x - 0 = x
238
by move: x => [x| |] //; rewrite -EFinB subr0. Qed.
6a
0 - x = - x
23d
by move: x => [x| |] //; rewrite -EFinB sub0r. Qed.
21
x * y = y * x
242
by move: x y => [r||] [s||]//=; rewrite -EFinM mulrC. Qed.
29
1 != 0 :> \bar R
247
exact: oner_neq0. Qed.
29
(1 == 0 :> \bar R) = false
24c
exact: oner_eq0. Qed.
6a
x * 1 = x
251
by move: x=> [r||]/=; rewrite /mule/= ?mulr1 ?(negbTE onee_neq0) ?lte_tofin. Qed.
6a
1 * x = x
256
by rewrite muleC mule1. Qed.
6a
x * 0 = 0
25b
by move: x => [r| |] //=; rewrite /mule/= ?mulr0// eqxx. Qed.
6a
0 * x = 0
260
by move: x => [r| |]/=; rewrite /mule/= ?mul0r// eqxx. Qed. Canonical mule_mulmonoid := @Monoid.MulLaw _ _ mule mul0e mule0.
22
6b
128

x ^+ n.+1 = x * x ^+ n
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).
21
x *? y = y *? x
26b
by rewrite [in LHS]/mule_def orbC. Qed.
21
x \is a fin_num -> y \is a fin_num -> x *? y
270
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.
21
x != 0 -> y \isn't a fin_num -> x *? y
27c
by move: x y => [x| |] [y| |]// x0 _; rewrite /mule_def (negbTE x0). Qed.
21
x \isn't a fin_num -> y != 0 -> x *? y
281
by move: x y => [x| |] [y| |]// _ y0; rewrite /mule_def (negbTE y0). Qed.
21
x * y != 0 -> x *? y
286
99
x%:E * +oo != 0 -> x%:E *? +oo
99
x%:E * -oo != 0 -> x%:E *? -oo
9d
+oo * y%:E != 0 -> +oo *? y%:E
9d
-oo * y%:E != 0 -> -oo *? y%:E
28b
99
290
291293
297
9d
292
293
29c
9d
294
2a1
by have [->|?] := eqVneq y 0%R; rewrite ?mule0 ?eqxx// mule_def_infty_neq0. Qed.
29
{in [pred x | x < +oo] &, forall x y, x +? y}
2a5
by move=> [x| |] [y| |]. Qed.
29
{in [pred x | -oo < x] &, forall x y, x +? y}
2aa
by move=> [x| |] [y| |]. Qed.
6a
(`|x| == 0) = (x == 0)
2af
by move: x => [| |] //= r; rewrite !eqe normr_eq0. Qed.
29
`|0| = 0
2b4
by rewrite /abse normr0. Qed.
29
`|1| = 1
2b9
by rewrite /abse normr1. Qed.
6a
`|- x| = `|x|
2be
by case: x => [r||]; rewrite //= normrN. Qed.
21
(- x == - y) = (x == y)
2c3
188
(- r)%:E == (- r')%:E -> r%:E == r'%:E
by move/eqP => -[] /eqP; rewrite eqr_opp => /eqP ->. Qed.
21
- x = - y <-> x = y
2cc
by split=> [/eqP | -> //]; rewrite eqe_opp => /eqP. Qed.
21
(- x == y) = (x == - y)
2d1
by move: x y => [r0| |] [r1| |] //=; rewrite !eqe eqr_oppLR. Qed.
21
- x = y <-> x = - y
2d6
21
x == - y -> - x = y
by rewrite -eqe_oppLR => /eqP. Qed.
6a
(- x \is a fin_num) = (x \is a fin_num)
2df
by rewrite !fin_num_abs abseN. Qed.
21
x +? - y -> - (x - y) = - x + y
2e4
by move=> xy; rewrite oppeD// oppeK. Qed.
21
y \is a fin_num -> - (x - y) = - x + y
2e9
by move=> ?; rewrite oppeB// adde_defN fin_num_adde_defl. Qed.
21
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num)
2ee
by move: x y => [x| |] [y| |]. Qed.
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]
2f3
by rewrite -big_all big_map big_filter; exact: (big_morph _ fin_numD). Qed.
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)
2fc
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
2fe
(forall i : T, i \in s -> P i -> f i \is a fin_num) -> {in [seq f i | i <- s & P i], forall x, x \is a fin_num}
2fe
308
by move=> + _ /mapP[x /[!mem_filter]/andP[Px xs] ->]; apply. Qed.
21
(x - y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num)
30d
by move: x y => [x| |] [y| |]. Qed.
21
x \is a fin_num -> y \is a fin_num -> x * y \is a fin_num
312
by move: x y => [x| |] [y| |]. Qed.
267
x \is a fin_num -> x ^+ n \is a fin_num
317
by elim: n x => // n ih x finx; rewrite expeS fin_numM// ih. Qed.
29
{in fin_num &, {morph fine : x y / x + y >-> (x + y)%R}}
31c
by move=> [r| |] [s| |]. Qed.
29
{in fin_num &, {morph fine : x y / x - y >-> (x - y)%R}}
321
by move=> [r| |] [s| |]. Qed.
29
{in fin_num &, {morph fine : x y / x * y >-> (x * y)%R}}
326
by move=> [x| |] [y| |]. Qed.
6a
x \is a fin_num -> (fine x)%:E = x
32b
by case: x. Qed.
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
330
by move=> h; rewrite -sumEFin; apply: eq_bigr => i Pi; rewrite fineK// h. Qed.
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)
336
by move=> h; rewrite -EFin_sum_fine. Qed.
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)
33d
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)
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.
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)
351
by move=> h; rewrite sumeN// => i j Pi Pj; rewrite fin_num_adde_defl// h. Qed.
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
356
22
359
35a
nmf: forall i : nat, (n <= i <= m)%N -> f i \is a fin_num
nm: (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.
21
x \is a fin_num -> y + x - x = y
365
by move: x y => [x| |] [y| |] //; rewrite -EFinD -EFinB addrK. Qed.
21
y \is a fin_num -> x - y + y = x
36a
by move: x y => [x| |] [y| |] //; rewrite -EFinD subrK. Qed.
6a
x \is a fin_num -> x - x = 0
36f
by move: x => [r _| |] //; rewrite -EFinB subrr. Qed.
1b7
x \is a fin_num -> y +? z -> (x - z == y) = (x == y + z)
374
by move: x y z => [x| |] [y| |] [z| |] // _ _; rewrite !eqe subr_eq. Qed.
21
(x + y == -oo) = (x == -oo) || (y == -oo)
379
by move: x y => [?| |] [?| |]. Qed.
6a
x != -oo -> +oo + x = +oo
37e
by case: x. Qed.
6a
x != -oo -> x + +oo = +oo
383
by case: x. Qed.
6a
-oo + x = -oo
388
by []. Qed.
6a
x + -oo = -oo
38d
by case: x. Qed.
21
x != -oo -> y != -oo -> (x + y != +oo) = (x != +oo) && (y != +oo)
392
by move: x y => [x| |] [y| |]. Qed.
21
x != +oo -> y != +oo -> (x + y != -oo) = (x != -oo) && (y != -oo)
397
by move: x y => [x| |] [y| |]. Qed.
21
(0 <= x) && (0 <= y) || (x <= 0) && (y <= 0) -> (x + y == 0) = (x == 0) && (y == 0)
39c
by move=> /orP[|] /andP[]; [exact: padde_eq0|exact: nadde_eq0]. Qed.
2fe
\sum_(i <- s | P i) f i = -oo <-> (exists i : T, [/\ i \in s, P i & f i = -oo])
3a1
2fe
\sum_(i <- s | P i) f i = -oo -> exists i : T, [/\ i \in s, P i & f i = -oo]
22
2ff
2f6
2f7
2f8
i: T
si: i \in s
Pi: P i
fi: f i = -oo
\sum_(i <- s | P i) f i = -oo
2fe
forall i : T, (i \in s) && P i -> f i = -oo -> exists i0 : T, [/\ i0 \in s, P i0 & f i0 = -oo]
3a9
3ab
3b0
3ab
forall i0 : T, i0 == i -> (if P i0 then f i0 else 0) = -oo
3ab
\sum_(i0 <- s | i0 == i) -oo + \sum_(i0 <- s | i0 != i) (if P i0 then f i0 else 0) = -oo
3ab
3be
3ab
iter (count (eq_op^~ i) s) (+%E -oo) 0 = -oo
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 = -oo
3ac
3ae
3af

i \in h :: t -> iter (count (eq_op^~ i) (h :: t)) (+%E -oo) 0 = -oo
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.
22
I: finType
1e0
P: {pred I}

(\sum_(i | P i) f i == -oo) = [exists i in P, f i == -oo]
3d5
3d7
(exists i : I, [/\ i \in index_enum I, P i & f i = -oo]) -> [exists i in P, f i == -oo]
22
3d8
1e0
3d9
i: I
Pi: i \in P
3af
\sum_(i | P i) f i == -oo
3e2
3e5
by apply/eqP/esum_eqNyP; exists i. Qed.
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])
3ea
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]
22
2ff
2f6
2f7
2f8
3f2
3ac
3ad
3ae
fi: f i = +oo
\sum_(i <- s | P i) f i = +oo
3f1
forall i : T, (i \in s) && P i -> f i = +oo -> exists i0 : T, [/\ i0 \in s, P i0 & f i0 = +oo]
3f4
3f6
3f8
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 = +oo
3ac
3ae
3f7

i \in h :: t -> \sum_(i <- (h :: t) | P i) f i = +oo
403
\sum_(i <- (i :: t) | P i) f i = +oo
22
2ff
2f7
2f8
3f2
3ca
3cb
404
3ac
3ae
3f7
3d2
\sum_(i <- (h :: t) | P i) f i = +oo
403
\sum_(j <- t | P j) f j != -oo
40a
40c
40d
by rewrite big_cons; case: ifPn => Ph; rewrite (ih i)// addey// finoo. Qed.
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]
416
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)
22
3d8
3d9
1e0
41f
3e3
3e4
3f7
\sum_(i | P i) f i == +oo
41c
423
424
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.
21
0 <= x -> 0 <= y -> 0 <= x + y
42a
by move: x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed.
21
x <= 0 -> y <= 0 -> x + y <= 0
42f
move: x y => [r0||] [r1||]// ? ?; rewrite !lee_fin -(addr0 0%R); exact: ler_add. Qed.
6a
(0 < - x) = (x < 0)
434
move: x => [x||] //; exact: oppr_gt0. Qed.
6a
(- x < 0) = (0 < x)
439
move: x => [x||] //; exact: oppr_lt0. Qed.
6a
(0 <= - x) = (x <= 0)
43e
move: x => [x||] //; exact: oppr_ge0. Qed.
6a
(- x <= 0) = (0 <= x)
443
move: x => [x||] //; exact: oppr_le0. Qed.
22
6
2f8
2f7

(forall t : T, P t -> 0 <= f t) -> forall l : seq T, 0 <= \sum_(i <- l | P i) f i
448
by move=> f0 l; elim/big_rec : _ => // t x Pt; apply/adde_ge0/f0. Qed.
44a
(forall t : T, P t -> f t <= 0) -> forall l : seq T, \sum_(i <- l | P i) f i <= 0
44e
by move=> f0 l; elim/big_rec : _ => // t x Pt; apply/adde_le0/f0. Qed.
29
-oo * +oo = -oo
453
by rewrite /mule /= lt0y. Qed.
29
+oo * -oo = -oo
458
by rewrite muleC mulNyy. Qed.
29
+oo * +oo = +oo
45d
by rewrite /mule /= lt0y. Qed.
29
-oo * -oo = +oo
462
by []. Qed.
ad
r \is Num.real -> r%:E * +oo = (Num.sg r)%:E * +oo
467
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)
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)
475
(r == 0%R) || (r < 0)%R -> (if 0 < r%:E then +oo else -oo) = (if 0 < (Num.sg r)%:E then +oo else -oo)
475
479
by rewrite rn0/= => rlt0; rewrite lt_def lt_geF// andbF ltr0_sg// lte0N1. Qed.
ad
r \is Num.real -> +oo * r%:E = (Num.sg r)%:E * +oo
47e
by move=> rreal; rewrite muleC real_mulry. Qed.
ad
r \is Num.real -> r%:E * -oo = (Num.sg r)%:E * -oo
483
46e
(if 0 < r%:E then -oo else +oo) = (if 0 < (Num.sg r)%:E then -oo else +oo)
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)
475
(r == 0%R) || (r < 0)%R -> (if 0 < r%:E then -oo else +oo) = (if 0 < (Num.sg r)%:E then -oo else +oo)
475
491
by rewrite rn0/= => rlt0; rewrite lt_def lt_geF// andbF ltr0_sg// lte0N1. Qed.
ad
r \is Num.real -> -oo * r%:E = (Num.sg r)%:E * -oo
496
by move=> rreal; rewrite muleC real_mulrNy. Qed. Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).
6a
- (1) * x = - x
49b
rewrite -EFinN /mule/=; case: x => [x||]; do ?[by rewrite mulN1r|by rewrite eqe oppr_eq0 oner_eq0 lte_fin ltr0N1]. Qed.
6a
x * - (1) = - x
4a0
by rewrite muleC mulN1e. Qed.
21
x != 0 -> y != 0 -> x * y != 0
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.
21
(x * y == 0) = (x == 0) || (y == 0)
4aa
21
x * y == 0 -> (x == 0) || (y == 0)
by apply: contraTT => /norP[]; apply: mule_neq0. Qed.
21
0 <= x -> 0 <= y -> 0 <= x * y
4b3
94
(0 <= x)%R -> (0 <= y)%R -> (0 <= x * y)%R
99
(0 <= x)%R -> 0 <= +oo -> 0 <= (if x == 0%R then 0 else if (0 < x)%R then +oo else -oo)
9d
0 <= +oo -> (0 <= y)%R -> 0 <= (if y == 0%R then 0 else if (0 < y)%R then +oo else -oo)
4b8
99
4bd
4be
4c2
22
9a
x0: (0 < x)%R

0 <= (if x == 0%R then 0 else if (0 < x)%R then +oo else -oo)
4c4
9d
4bf
4cd
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.
21
0 < x -> 0 < y -> 0 < x * y
4d7
by rewrite !lt_def => /andP[? ?] /andP[? ?]; rewrite mule_neq0 ?mule_ge0. Qed.
21
x <= 0 -> y <= 0 -> 0 <= x * y
4dc
94
(x <= 0)%R -> (y <= 0)%R -> (0 <= x * y)%R
99
(x <= 0)%R -> -oo <= 0 -> 0 <= (if x == 0%R then 0 else if (0 < x)%R then -oo else +oo)
9d
-oo <= 0 -> (y <= 0)%R -> 0 <= (if y == 0%R then 0 else if (0 < y)%R then -oo else +oo)
4e1
99
4e6
4e7
4eb
9d
4e8
4f0
by rewrite lt_leAnge => _ ->; case: ifP => _ //; rewrite andbF le0y. Qed.
21
x <= 0 -> 0 <= y -> x * y <= 0
4f4
94
(x <= 0)%R -> (0 <= y)%R -> (x * y <= 0)%R
99
(x <= 0)%R -> 0 <= +oo -> (if x%:E == 0 then 0 else if (0 < x)%R then +oo else -oo) <= 0
9d
-oo <= 0 -> (0 <= y)%R -> (if y%:E == 0 then 0 else if (0 < y)%R then -oo else +oo) <= 0
29
-oo <= 0 -> 0 <= +oo -> (if 0 < +oo then -oo else +oo) <= 0
4f9
99
4fe
4ff501
505
9d
500
501
50a
9d
(if y%:E == 0 then 0 else -oo) <= 0
50c
29
502
513
by rewrite lt0y leNy0. Qed.
21
0 <= x -> y <= 0 -> x * y <= 0
517
by move=> x0 y0; rewrite muleC mule_le0_ge0. Qed.
21
x < 0 -> y < 0 -> 0 < x * y
51c
by rewrite !lt_neqAle => /andP[? ?]/andP[*]; rewrite eq_sym mule_neq0 ?mule_le0. Qed.
21
0 < x -> y < 0 -> x * y < 0
521
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.
21
x < 0 -> 0 < y -> x * y < 0
52f
by move=> x0 y0; rewrite muleC mule_gt0_lt0. Qed.
6a
0 < x -> - x < x
534
by case: x => //= r; rewrite !lte_fin; apply: gtr_opp. Qed.
21
(0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x * y)%O
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.
6a
0 <= `|x|
53e
by move: x => [x| |] /=; rewrite ?le0y ?lee_fin. Qed.
6a
0 <= x -> `|x| = x
543
by move: x => [x| |]//; rewrite lee_fin => x0; apply/eqP; rewrite eqe ger0_norm. Qed.
6a
0 < x -> `|x| = x
548
by move=> /ltW/gee0_abs. Qed.
6a
x <= 0 -> `|x| = - x
54d
by move: x => [x| |]//; rewrite lee_fin => x0; apply/eqP; rewrite eqe ler0_norm. Qed.
6a
x < 0 -> `|x| = - x
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.
21
x + y = - (- x - y)%E
557
by case: x => [x| |]; case: y => [y| |] //=; rewrite opprD !opprK. Qed.
22
19a
r: seq I
1df
339

\sum_(i <- r | P i) F i = - (\sum_(i <- r | P i) - F i)%E
55c
55e
0%E = (- 0)%E
22
19a
55f
1df
339
23
(- x)%E - y = (- (x + y))%E
22
19a
55f
1df
339
3e3
F i = (- - F i)%E
563
568
569
56a
56f
56b
56c
574
by rewrite oppeK. Qed.
21
(x +? y)%E -> x + y = (x + y)%E
578
by case: x => [x| |]; case: y. Qed.
186
18b by []. Qed.
18d
190 by []. Qed.
22
19a
55f
19c
19d

\sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%:E
57f
by rewrite dual_sumeE fin_num_sumeN// oppeK sumEFin. Qed.
29
commutative +%dE
585
by move=> x y; rewrite !dual_addeE addeC. Qed.
29
right_id (0 : \bar R) +%dE
58a
by move=> x; rewrite dual_addeE eqe_oppLRP oppe0 adde0. Qed.
29
left_id (0 : \bar R) +%dE
58f
by move=> x;rewrite dual_addeE eqe_oppLRP oppe0 add0e. Qed.
29
associative +%dE
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.
29
right_commutative +%dE
599
exact: Monoid.mulmAC. Qed.
29
left_commutative +%dE
59e
exact: Monoid.mulmCA. Qed.
29
interchange +%dE +%dE
5a3
exact: Monoid.mulmACA. Qed.
210
213 case: x y => [x||] [y||] //; exact: realD. Qed.
21
(x +? y)%E -> - (x + y) = - x - y
5a9
by move: x y => [x| |] [y| |] //= _; rewrite opprD. Qed.
233
236 by move=> finy; rewrite doppeD// fin_num_adde_defl. Qed.
238
23b by move: x => [x| |] //; rewrite -dEFinB subr0. Qed.
23d
240 by move: x => [x| |] //; rewrite -dEFinB sub0r. Qed.
21
(x +? (- y)%dE)%E -> - (x - y) = - x + y
5b1
by move=> xy; rewrite doppeD// oppeK. Qed.
2e9
2ec by move=> ?; rewrite doppeB// fin_num_adde_defl// fin_numN. Qed.
2ee
2f1 by move: x y => [x| |] [y| |]. Qed.
31c
31f by move=> [r| |] [s| |]. Qed.
321
324 by move=> [r| |] [s| |]. Qed.
365
368 by move=> fx; rewrite !dual_addeE oppeK addeK ?oppeK; case: x fx. Qed.
36a
36d by move=> fy; rewrite !dual_addeE oppeK subeK ?oppeK; case: y fy. Qed.
36f
372 by move=> fx; rewrite dual_addeE subee ?oppe0; case: x fx. Qed.
1b7
x \is a fin_num -> (y +? z)%E -> (x - z == y) = (x == y + z)
5bd
by move: x y z => [x| |] [y| |] [z| |] // _ _; rewrite !eqe subr_eq. Qed.
21
(x + y == +oo) = (x == +oo) || (y == +oo)
5c2
by move: x y => [?| |] [?| |]. Qed.
6a
+oo + x = +oo
5c7
by []. Qed.
6a
x + +oo = +oo
5cc
by case: x. Qed.
6a
x != +oo -> -oo + x = -oo
5d1
by case: x. Qed.
6a
x != +oo -> x + -oo = -oo
5d6
by case: x. Qed.
37e
381 by rewrite daddye. Qed.
383
386 by rewrite daddey. Qed.
392
395 by move: x y => [x| |] [y| |]. Qed.
397
39a by move: x y => [x| |] [y| |]. Qed.
207
20a
94
(x%:E <= 0)%E -> (y%:E <= 0)%E -> (x%:E + y%:E == 0%E) = (x%:E == 0%E) && (y%:E == 0%E)
99
(x%:E <= 0)%E -> (-oo <= 0)%E -> (x%:E + -oo%E == 0%E) = (x%:E == 0%E) && (-oo%E == 0%E)
5e0
99
5e5
5e8
by rewrite /adde/= (_ : -oo == 0 = false)// andbF. Qed.
1fe
201
94
(0 <= x%:E)%E -> (0 <= y%:E)%E -> (x%:E + y%:E == 0%E) = (x%:E == 0%E) && (y%:E == 0%E)
99
(0 <= x%:E)%E -> (0 <= +oo)%E -> (x%:E + +oo%E == 0%E) = (x%:E == 0%E) && (+oo%E == 0%E)
5ed
99
5f2
5f5
by rewrite /adde/= (_ : +oo == 0 = false)// andbF. Qed.
39c
39f move=> /orP[|] /andP[]; [exact: pdadde_eq0|exact: ndadde_eq0]. Qed.
2fe
\sum_(i <- s | P i) f i = +oo <-> (exists i : T, [/\ i \in s, P i & f i = +oo])
5fa
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.
3d7
(\sum_(i | P i) f i == +oo) = [exists i in P, f i == +oo]
603
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.
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])
60c
22
2ff
2f6
2f7
2f8
fioo: forall i : T, P i -> f i != +oo

3a3
22
2ff
2f6
2f7
2f8
614
3ac
3ae

(- f i)%E != -oo%E
613
(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])
613
61c
by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP. Qed.
3d7
(forall i : I, f i != +oo) -> (\sum_(i | P i) f i == -oo) = [exists i in P, f i == -oo]
621
22
3d8
1e0
3d9
finoo: forall i : I, f i != +oo

3da
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.
42a
42d rewrite dual_addeE oppe_ge0 -!oppe_le0; exact: adde_le0. Qed.
42f
42f
rewrite dual_addeE oppe_le0 -!oppe_ge0; exact: adde_ge0. Qed.
44a
(forall n : T, P n -> 0 <= f n) -> forall l : seq T, 0 <= \sum_(i <- l | P i) f i
632
22
6
2f8
2f7
u0: forall n : T, P n -> 0 <= f n
l: seq T
t: T
Pt: P t

(- f t <= 0)%E
rewrite oppe_le0; exact: u0. Qed.
44a
(forall n : T, P n -> f n <= 0) -> forall l : seq T, \sum_(i <- l | P i) f i <= 0
640
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.
22
r: \bar R

(0 < r)%E -> (- r < r)%E
64b
by case: r => //= r; rewrite !lte_fin; apply: gtr_opp. Qed.
125
12a by elim: n => //= n ->. Qed.
12c
12f by elim: n => //= n ->. Qed.
131
135 by elim: n => //= n <-. Qed.
267
x *+ n = (x *+ n)%E
655
22
9a
128

x%:E *+ n.+1 = (x%:E *+ n.+1)%E
127
+oo%E *+ n.+1 = (+oo *+ n.+1)%E
127
-oo%E *+ n.+1 = (-oo *+ n.+1)%E
65a
127
660
661
665
127
662
66a
by rewrite enatmul_ninfty ednatmul_ninfty. Qed.
137
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).
d3
(x \is a fin_num) = (-oo < x < +oo)
66f
by rewrite fin_numE -leye_eq -leeNy_eq -2!ltNge. Qed.
d3
reflect (-oo < x < +oo) (x \is a fin_num)
674
by rewrite fin_numElt; exact: idP. Qed.
d3
(x < +oo) = (x \is a fin_num) || (x == -oo)
679
by case: x => // x //=; exact: ltry. Qed.
d3
(-oo < x) = (x \is a fin_num) || (x == +oo)
67e
by case: x => // x //=; exact: ltNyr. Qed.
d3
0 <= x -> (x \is a fin_num) = (x < +oo)
683
by move: x => [x| |] => // x0; rewrite fin_numElt ltNyr. Qed.
d3
x <= 0 -> (x \is a fin_num) = (-oo < x)
688
by move: x => [x| |]//=; rewrite lee_fin => x0; rewrite ltNyr. Qed.
d3
x = +oo <-> (forall A : R, (0 < A)%R -> A%:E <= x)
68d
cd
6b
Ax: forall A : R, (0 < A)%R -> A%:E <= x

x = +oo
694
~ x < +oo
cd
9a
Ax: forall A : R, (0 < A)%R -> A%:E <= x%:E

False
69e
~ x%:E < (Num.max 0 x + 1)%:E -> False
69e
~ x%:E < (Num.max 0 x + 1)%:E
69e
6a7
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.
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
6ac
cd
6af
55f
1df
339
F0: forall i : I, P i -> 0 <= F i
PF0: {in r, forall x : I, P x ==> (F x == 0)}

\sum_(i <- r | P i) F i = 0
cd
6af
55f
1df
339
6b6
PF0: \sum_(i <- r | P i) F i = 0
{in r, forall x : I, P x ==> (F x == 0)}
cd
6af
55f
1df
339
6b6
6b7
3e3
ir: i \in r
3ae

F i = 0
6b9
6bb
6bd
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae

6c3
6ca
{in r, forall i : I, P i ==> (F i \is a fin_num)}
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
rPF: {in r, forall i : I, P i ==> (F i \is a fin_num)}
6c3
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
j: I
jr: j \in r
Pj: P j

-oo < F j
6d6
F j < +oo
6d0
6d6
6dd
6cf
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
6d7
6d8
6d9
Fjoo: F j = +oo

6a0
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
rPF: {in r, forall i : I, P i ==> (F i \is a fin_num)}
6c3
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
6d7
6d8
6d9
6e5
k: I

P k -> F k != -oo
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
6d7
6d8
6d9
6e5
PFninfty: forall k : I, P k -> F k != -oo
6a0
6e7
6f2
6a0
6e6
6f2
((forall i : I, P i -> F i != -oo) -> \sum_(i0 <- r | P i0) F i0 = +oo) -> False
6e6
6d1
6c3
6d1
(\sum_(i <- r | P i) (fine \o F) i)%R == 0%R
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
6d2
_x_: (\sum_(i <- r | P i) (fine \o F) i)%R == 0%R
6c3
6d1
\sum_(i <- r | (i \in r) && P i) ((fine \o F) i)%:E = 0
702
6d1
forall i : I, (i \in r) && P i -> ((fine \o F) i)%:E = F i
6d1
\sum_(i <- r | (i \in r) && P i) F i = 0
703
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
6d2
6d7
6d8
6d9

F j \is a fin_num
70e
6d1
710
702
704
6c3
704
all (fun i : I => P i ==> ((fine \o F) i == 0%R)) r
704
P i ==> ((fine \o F) i == 0%R) -> F i = 0
704
722
cd
6af
55f
1df
339
6b6
6bc
3e3
6c2
3ae
6d2
705
Fi0: fine (F i) = 0%R

6c3
729
(fine (F i))%:E = 0
by rewrite Fi0. Qed.
cd
23

x < +oo -> y < +oo -> x + y < +oo
730
by move: x y => -[r [r'| |]| |] // ? ?; rewrite -EFinD ltry. Qed.
cd
19a
19b
1df
1e0

(forall i : I, P i -> f i < +oo) -> \sum_(i <- s | P i) f i < +oo
736
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.
732
(0 < y - x) = (x < y)
744
by move: x y => [r | |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin subr_gt0. Qed.
732
(y - x <= 0) = (y <= x)
749
by rewrite !leNgt sube_gt0. Qed.
cd
y, x: \bar R

y \is a fin_num -> (0 <= x - y) = (y <= x)
74e
by move: x y => [x| |] [y| |] //= _; rewrite ?(leey, lee_fin, subr_ge0). Qed.
732
y \is a fin_num -> (0 <= y - x) = (x <= y)
755
by move: x y => [x| |] [y| |] //=; rewrite ?(leey, leNye, lee_fin) //= subr_ge0. Qed.
732
(x \is a fin_num) || (y \is a fin_num) -> (0 <= y - x) = (x <= y)
75a
by move=> /orP[?|?]; [rewrite suber_ge0|rewrite subre_ge0]. Qed.
732
(- x < y) = (- y < x)
75f
by move: x y => [r| |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin ltr_oppl. Qed.
732
(x < - y) = (y < - x)
764
by move: x y => [r| |] [r'| |] //=; rewrite ?(ltry, ltNyr)// !lte_fin ltr_oppr. Qed.
732
(x <= - y) = (y <= - x)
769
by move: x y => [r0| |] [r1| |] //=; rewrite ?(leey, leNye)// !lee_fin ler_oppr. Qed.
732
(- x <= y) = (- y <= x)
76e
by move: x y => [r0| |] [r1| |] //=; rewrite ?(leey, leNye)// !lee_fin ler_oppl. Qed.
732
x * - y = - (x * y)
773
cd
95

(x * - y)%:E = (- (x * y))%:E
cd
9a
(if x%:E == 0 then 0 else if 0 < x%:E then -oo else +oo) = - (if x%:E == 0 then 0 else if 0 < x%:E then +oo else -oo)
77e
(if x%:E == 0 then 0 else if 0 < x%:E then +oo else -oo) = - (if x%:E == 0 then 0 else if 0 < x%:E then -oo else +oo)
cd
9e
(if (- y)%:E == 0 then 0 else if 0 < (- y)%:E then +oo else -oo) = - (if y%:E == 0 then 0 else if 0 < y%:E then +oo else -oo)
783
(if (- y)%:E == 0 then 0 else if 0 < (- y)%:E then -oo else +oo) = - (if y%:E == 0 then 0 else if 0 < y%:E then -oo else +oo)
778
77e
77f
780782785
789
77e
781
782785
78e
783
784
785
793
cd
9e
y0: (0%R == y) = false

(if 0 < (- y)%:E then +oo else -oo) = - (if 0 < y%:E then +oo else -oo)
795
783
786
79e
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.
732
- x * y = - (x * y)
7a6
by rewrite muleC muleN muleC. Qed.
732
- x * - y = x * y
7ab
by rewrite mulNe muleN oppeK. Qed.
cc
r%:E * +oo = (Num.sg r)%:E * +oo
7b0
by rewrite [LHS]real_mulry// num_real. Qed.
cc
+oo * r%:E = (Num.sg r)%:E * +oo
7b5
by rewrite muleC mulry. Qed.
cc
r%:E * -oo = (Num.sg r)%:E * -oo
7ba
by rewrite [LHS]real_mulrNy// num_real. Qed.
cc
-oo * r%:E = (Num.sg r)%:E * -oo
7bf
by rewrite muleC mulrNy. Qed. Definition mulr_infty := (mulry, mulyr, mulrNy, mulNyr).
732
0 <= x -> x \is a fin_num -> y < +oo -> x * y < +oo
7c4
cd
9a
x0: 0 <= x%:E
xfin: x%:E \is a fin_num

x%:E * -oo < +oo
cd
9a
7cd

(Num.sg 0)%:E * -oo < +oo
cd
9a
7cd
4ca
(Num.sg x)%:E * -oo < +oo
7d0
7d6
7d7
7da
by rewrite gtr0_sg // mul1e. Qed.
732
0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y)
7de
77a
(0 <= x)%R -> (0 <= y)%R -> (0 < x%:E * y%:E) = (0 < x%:E) && (0 < y%:E)
77e
(0 <= x)%R -> 0 <= +oo -> (0 < x%:E * +oo) = (0 < x%:E) && (0 < +oo)
783
0 <= +oo -> (0 <= y)%R -> (0 < +oo * y%:E) = (0 < +oo) && (0 < y%:E)
ed
0 <= +oo -> 0 <= +oo -> (0 < +oo * +oo) = (0 < +oo) && (0 < +oo)
7e3
77e
7e8
7e97eb
7ef
cd
9a
4ca

(0 < x%:E * +oo) = (0 < x%:E) && (0 < +oo)
7f1
783
7ea
7eb
7f9
783
(0 < +oo * 0) = (0 < +oo) && (0 < 0)
cd
9e
x0: (0 < y)%R
(0 < +oo * y%:E) = (0 < +oo) && (0 < y%:E)
7eb
803
805
7fb
ed
7ec
80a
by move=> _ _; rewrite mulyy ltry. Qed.
d3
0 < x -> +oo * x = +oo
80e
77e
0 < x%:E -> +oo * x%:E = +oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty gtr0_sg// mul1e. Qed.
d3
x < 0 -> +oo * x = -oo
817
77e
x%:E < 0 -> +oo * x%:E = -oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty ltr0_sg// mulN1e. Qed.
d3
0 < x -> -oo * x = -oo
820
77e
0 < x%:E -> -oo * x%:E = -oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty gtr0_sg// mul1e. Qed.
d3
x < 0 -> -oo * x = +oo
829
77e
x%:E < 0 -> -oo * x%:E = +oo
by rewrite lte_fin => x0; rewrite muleC mulr_infty ltr0_sg// mulN1e. Qed.
d3
0 < x -> x * +oo = +oo
832
by move=> /gt0_mulye; rewrite muleC; apply. Qed.
d3
x < 0 -> x * +oo = -oo
837
by move=> /lt0_mulye; rewrite muleC; apply. Qed.
d3
0 < x -> x * -oo = -oo
83c
by move=> /gt0_mulNye; rewrite muleC; apply. Qed.
d3
x < 0 -> x * -oo = +oo
841
by move=> /lt0_mulNye; rewrite muleC; apply. Qed.
732
(x * y == +oo) = [|| (0 < x) && (y == +oo), (x < 0) && (y == -oo), (x == +oo) && (0 < y) | (x == -oo) && (y < 0)]
846
77e
(x%:E * +oo == +oo) = (0 < x)%R
77e
(x%:E * -oo == +oo) = (x < 0)%R
783
(+oo * y%:E == +oo) = (0 < y)%R
ed
(+oo * +oo == +oo) = (0 < +oo) || (0 < +oo)
ed
(+oo * -oo == +oo) = false
783
(-oo * y%:E == +oo) = (y < 0)%R
ed
(-oo * +oo == +oo) = (0 < -oo)
ed
true = (-oo < 0) || (-oo < 0)
84b
77e
850
85185385585785985b
85f
783
852
85385585785985b
864
ed
854
85585785985b
869
ed
856
85785985b
86e
783
858
85985b
873
ed
85a
85b
878
ed
85c
87d
by rewrite ltNyr. Qed.
732
(x * y == -oo) = [|| (0 < x) && (y == -oo), (x < 0) && (y == +oo), (x == -oo) && (0 < y) | (x == +oo) && (y < 0)]
881
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.
732
(- x < - y) = (y < x)
88a
by rewrite lte_oppl oppeK. Qed.
cd
a, b, x, y: \bar R

a < b -> x < y -> a + x < b + y
88f
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.
732
0 <= y -> x <= x + y
89c
move: x y => -[ x [y| |]//= | [| |]// | [| | ]//]; by [rewrite !lee_fin ler_addl | move=> _; exact: leey]. Qed.
732
0 <= y -> x <= y + x
8a1
by rewrite addeC; exact: lee_addl. Qed.
732
y <= 0 -> x + y <= x
8a6
move: x y => -[ x [y| |]//= | [| |]// | [| | ]//]; by [rewrite !lee_fin ger_addl | move=> _; exact: leNye]. Qed.
732
y <= 0 -> y + x <= x
8ab
rewrite addeC; exact: gee_addl. Qed.
750
y \is a fin_num -> (y < y + x) = (0 < x)
8b0
by move: x y => [x| |] [y| |] _ //; rewrite ?ltry ?ltNyr // !lte_fin ltr_addl. Qed.
750
y \is a fin_num -> (y < x + y) = (0 < x)
8b5
rewrite addeC; exact: lte_addl. Qed.
750
y \is a fin_num -> (y - x < y) = (0 < x)
8ba
77a
((- y)%:E + x%:E < x%:E) = (0 < y%:E)
by rewrite !lte_fin gtr_addr ltr_oppl oppr0. Qed.
750
y \is a fin_num -> (- x + y < y) = (0 < x)
8c3
by rewrite addeC; exact: gte_subl. Qed.
732
x \is a fin_num -> (x + y < x) = (y < 0)
8c8
by move: x y => [r| |] [s| |]// _; [rewrite !lte_fin gtr_addl|rewrite !ltNyr]. Qed.
732
x \is a fin_num -> (y + x < x) = (y < 0)
8cd
by rewrite addeC; exact: gte_addl. Qed.
cd
x, a, b: \bar R

x \is a fin_num -> (x + a < x + b) = (a < b)
8d2
cd
a, b, x: R

(x%:E + a%:E < x%:E + b%:E) = (a%:E < b%:E)
by rewrite !lte_fin ltr_add2l. Qed.
8d4
a <= b -> x + a <= x + b
8df
8db
a%:E <= b%:E -> x%:E + a%:E <= x%:E + b%:E
cd
a: R
forall r, a%:E <= +oo -> r%:E + a%:E <= r%:E + +oo
ed
forall b x, -oo <= b -> x + -oo <= x + b
8e4
8e9
8eb
8ec
8f0
ed
8ed
8f5
by move=> -[b [| |]// | []// | //] r oob; exact: leNye. Qed.
8d4
x \is a fin_num -> (x + a <= x + b) = (a <= b)
8f9
8db
(x%:E + a%:E <= x%:E + b%:E) = (a%:E <= b%:E)
by rewrite !lee_fin ler_add2l. Qed.
8d4
a <= b -> a + x <= b + x
902
rewrite addeC (addeC b); exact: lee_add2l. Qed.
891
a <= b -> x <= y -> a + x <= b + y
907
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.
891
b \is a fin_num -> a < x -> b <= y -> a + b < x + y
910
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.
891
a \is a fin_num -> a <= x -> b < y -> a + b < x + y
91b
by move=> afin xa yb; rewrite (addeC a) (addeC x) lte_le_add. Qed.
cd
x, y, z, u: \bar R

x <= y -> u <= z -> x - z <= y - u
920
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.
cd
z, u, x, y: \bar R

u \is a fin_num -> x < z -> u <= y -> x - y < z - u
92d
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.
cd
z: \bar R

z \is a fin_num -> 0 < z -> {mono *%E^~ z : x y / x < y >-> x < y}
93a
cd
z: R
z0: 0 < z%:E
95

(x%:E * z%:E < y%:E * z%:E) = (x%:E < y%:E)
cd
944
945
9a
(x%:E * z%:E < +oo * z%:E) = (x%:E < +oo)
949
(x%:E * z%:E < -oo * z%:E) = (x%:E < -oo)
cd
944
945
9e
(+oo * z%:E < y%:E * z%:E) = (+oo < y%:E)
cd
944
945
(+oo * z%:E < -oo * z%:E) = (+oo < -oo)
94e
(-oo * z%:E < y%:E * z%:E) = (-oo < y%:E)
951
(-oo * z%:E < +oo * z%:E) = (-oo < +oo)
941
949
94a
94b94d950953955
959
949
94c
94d950953955
95e
94e
94f
950953955
963
951
952
953955
968
94e
954
955
96d
951
956
972
by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e. Qed.
93c
z \is a fin_num -> 0 < z -> {mono *%E z : x y / x < y >-> x < y}
976
by move=> zfin z0 x y; rewrite 2!(muleC z) lte_pmul2r. Qed.
93c
z \is a fin_num -> z < 0 -> {mono *%E z : y x / x < y >-> y < x}
97b
cd
93d
zfin: z \is a fin_num
z0: 0 < - z
23

(z * x < z * y) = (y < x)
by rewrite -(oppeK z) !mulNe lte_oppl oppeK -2!mulNe lte_pmul2l ?fin_numN. Qed.
93c
z \is a fin_num -> z < 0 -> {mono *%E^~ z : y x / x < y >-> y < x}
987
by move=> zfin z0 x y; rewrite -!(muleC z) lte_nmul2l. Qed.
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
98c
by move=> Pfg; elim/big_ind2 : _ => // *; apply lee_add. Qed.
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
993
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.
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
9a1
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.
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
9ac
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.
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
9ba
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.
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}
9c5
cd
35a
9c8
f0: forall n : nat, P n -> 0 <= f n
i, 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.
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}
9d4
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.
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}
9e1
cd
35a
9c8
9e4
f0: forall n : nat, (m <= n)%N -> P n -> 0 <= f n
9d0
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.
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}
9ee
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.
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}
9f9
cd
35a
9c8
128
f0: forall m : nat, (m < n)%N -> P m -> 0 <= f m
9d0
9d1

\sum_(i < n | P i && (j <= i)%N) f i <= \sum_(i0 < n | P i0 && (i <= i0)%N) f i0
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.
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}
a0b
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
cd
35a
9c8
128
a13
9d0
9d1
a08

a09
by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->]. Qed.
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
a1a
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)
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)
a24
0 <= \sum_(i <- [fset x | x in B & x \notin A]%fset) (if P i then f i else 0)
a24
A = [fset x | x in B & x \in A]%fset
a2c
a24
a2e
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.
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
a3e
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
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
a45
\sum_(i <- [fset x | x in B & x \notin A]%fset) (if P i then f i else 0) <= 0
a45
a32
a4c
a45
a4e
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.
cd
1b8

y \is a fin_num -> (x - y < z) = (x < z + y)
a5b
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.
a5d
y \is a fin_num -> (x - y < z) = (x < y + z)
a67
by move=> ?; rewrite lte_subl_addr// addeC. Qed.
a5d
z \is a fin_num -> (x < y - z) = (x + z < y)
a6c
a63
(x%:E < y%:E + (- z)%:E) = (x%:E + z%:E < y%:E)
by rewrite !lte_fin ltr_subr_addr. Qed.
a5d
z \is a fin_num -> (x < y - z) = (z + x < y)
a75
by move=> ?; rewrite lte_subr_addr// addeC. Qed.
a5d
x \is a fin_num -> (x - y < z) = (x < z + y)
a7a
a61
by rewrite !lte_fin ltr_subl_addr. Qed.
a5d
x \is a fin_num -> (x - y < z) = (x < y + z)
a80
by move=> ?; rewrite lte_subel_addr// addeC. Qed.
a5d
x \is a fin_num -> (x < y - z) = (x + z < y)
a85
a70 by rewrite !lte_fin ltr_subr_addr. Qed.
a5d
x \is a fin_num -> (x < y - z) = (z + x < y)
a8a
by move=> ?; rewrite lte_suber_addr// addeC. Qed.
a5d
y \is a fin_num -> (x - y <= z) = (x <= z + y)
a8f
a63
(x%:E + (- y)%:E <= z%:E) = (x%:E <= z%:E + y%:E)
by rewrite !lee_fin ler_subl_addr. Qed.
a5d
y \is a fin_num -> (x - y <= z) = (x <= y + z)
a98
by move=> ?; rewrite lee_subl_addr// addeC. Qed.
a5d
z \is a fin_num -> (x <= y - z) = (x + z <= y)
a9d
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.
a5d
z \is a fin_num -> (x <= y - z) = (z + x <= y)
aa8
by move=> ?; rewrite lee_subr_addr// addeC. Qed.
a5d
z \is a fin_num -> (x - y <= z) = (x <= z + y)
aad
a93 by rewrite !lee_fin ler_subl_addr. Qed.
a5d
z \is a fin_num -> (x - y <= z) = (x <= y + z)
ab2
by move=> ?; rewrite lee_subel_addr// addeC. Qed.
a5d
y \is a fin_num -> (x <= y - z) = (x + z <= y)
ab7
aa1 by rewrite !lee_fin ler_subr_addr. Qed.
a5d
y \is a fin_num -> (x <= y - z) = (z + x <= y)
abc
by move=> ?; rewrite lee_suber_addr// addeC. Qed.
732
x \is a fin_num -> (x - y < 0) = (x < y)
ac1
by move=> ?; rewrite lte_subel_addr// add0e. Qed.
732
y \is a fin_num -> (x - y < 0) = (x < y)
ac6
by move=> ?; rewrite lte_subl_addl// adde0. Qed.
732
(x \is a fin_num) || (y \is a fin_num) -> (x - y < 0) = (x < y)
acb
by move=> /orP[?|?]; [rewrite subre_lt0|rewrite suber_lt0]. Qed.
732
0 < x -> (0 <= x * y) = (0 <= y)
ad0
cd
23
x_gt0: 0 < x

0 <= x * y -> 0 <= y
by apply: contra_le; apply: mule_gt0_lt0. Qed.
732
0 < x -> (0 <= y * x) = (0 <= y)
adb
by rewrite muleC; apply: pmule_rge0. Qed.
732
0 < x -> (x * y < 0) = (y < 0)
ae0
by move=> /pmule_rge0; rewrite !ltNge => ->. Qed.
732
0 < x -> (y * x < 0) = (y < 0)
ae5
by rewrite muleC; apply: pmule_rlt0. Qed.
732
0 < x -> (x * y <= 0) = (y <= 0)
aea
by move=> xgt0; rewrite -oppe_ge0 -muleN pmule_rge0 ?oppe_ge0. Qed.
732
0 < x -> (y * x <= 0) = (y <= 0)
aef
by rewrite muleC; apply: pmule_rle0. Qed.
732
0 < x -> (0 < x * y) = (0 < y)
af4
by move=> xgt0; rewrite -oppe_lt0 -muleN pmule_rlt0 ?oppe_lt0. Qed.
732
0 < x -> (0 < y * x) = (0 < y)
af9
by rewrite muleC; apply: pmule_rgt0. Qed.
732
x < 0 -> (0 <= x * y) = (y <= 0)
afe
by rewrite -oppe_gt0 => /pmule_rle0<-; rewrite mulNe oppe_le0. Qed.
732
x < 0 -> (0 <= y * x) = (y <= 0)
b03
by rewrite muleC; apply: nmule_rge0. Qed.
732
x < 0 -> (x * y <= 0) = (0 <= y)
b08
by rewrite -oppe_gt0 => /pmule_rge0<-; rewrite mulNe oppe_ge0. Qed.
732
x < 0 -> (y * x <= 0) = (0 <= y)
b0d
by rewrite muleC; apply: nmule_rle0. Qed.
732
x < 0 -> (0 < x * y) = (y < 0)
b12
by rewrite -oppe_gt0 => /pmule_rlt0<-; rewrite mulNe oppe_lt0. Qed.
732
x < 0 -> (0 < y * x) = (y < 0)
b17
by rewrite muleC; apply: nmule_rgt0. Qed.
732
x < 0 -> (x * y < 0) = (0 < y)
b1c
by rewrite -oppe_gt0 => /pmule_rgt0<-; rewrite mulNe oppe_gt0. Qed.
732
x < 0 -> (y * x < 0) = (0 < y)
b21
by rewrite muleC; apply: nmule_rlt0. Qed.
732
(x * y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)]
b26
cd
23
xlt0: x < 0

(x * y < 0) = [&& ~~ false, y != 0 & true (+) (y < 0)]
cd
23
xgt0: 0 < x
(x * y < 0) = [&& ~~ false, y != 0 & false (+) (y < 0)]
b32
b34
by rewrite pmule_rlt0//= !lt_neqAle andbA andbb. Qed.
ed
associative (*%E : \bar R -> \bar R -> \bar R)
b39
a5d
x * (y * z) = x * y * z
cd
1b8
hwlog: forall x y z, 0 < x -> x * (y * z) = x * y * z

b40
cd
1b8
x0: 0 < x
b40
cd
1b8
b45
x0: x < 0

b40
b46
b48
b40
cd
1b8
b49
hwlog: forall x y z, 0 < x -> 0 < y -> x * (y * z) = x * y * z

b40
cd
1b8
b49
y0: 0 < y
b40
cd
1b8
b49
b56
y0: y < 0

b40
b57
b59
b40
cd
1b8
b49
b5a
hwlog: forall x y z, 0 < x -> 0 < y -> 0 < z -> x * (y * z) = x * y * z

b40
cd
1b8
b49
b5a
z0: 0 < z
b40
cd
1b8
b49
b5a
b67
z0: z < 0

b40
b68
b6a
b40
cd
y, z: \bar R
b5a
b6b
9a
x0: 0 < x%:E

x%:E * (y * z) = x%:E * y * z
cd
93d
b6b
9a
b79
9e
y0: 0 < y%:E

x%:E * (y%:E * z) = x%:E * y%:E * z
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.
ed
left_commutative (*%E : \bar R -> \bar R -> \bar R)
b87
exact: Monoid.mulmCA. Qed.
ed
right_commutative (*%E : \bar R -> \bar R -> \bar R)
b8c
exact: Monoid.mulmAC. Qed.
ed
interchange *%E *%E
b91
exact: Monoid.mulmACA. Qed.
a5d
x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z
b96
a63
y%:E +? z%:E -> (x * (y + z))%:E = (x * y)%:E + (x * z)%:E
by rewrite mulrDr. Qed.
a5d
x \is a fin_num -> y +? z -> (y + z) * x = y * x + z * x
b9f
by move=> ? ?; rewrite -!(muleC x) muleDr. Qed.
a5d
x \is a fin_num -> y +? - z -> x * (y - z) = x * y - x * z
ba4
by move=> ? yz; rewrite muleDr ?muleN. Qed.
a5d
x \is a fin_num -> y +? - z -> (y - z) * x = y * x - z * x
ba9
by move=> ? yz; rewrite muleDl// mulNe. Qed.
a5d
0 <= y -> 0 <= z -> (y + z) * x = y * x + z * x
bae
cd
r, s, t: R
s0: 0 <= s%:E
t0: 0 <= t%:E

((s + t) * r)%:E = (s * r)%:E + (t * r)%:E
cd
55
bb7
t0: 0 <= +oo
(if r%:E == 0 then 0 else if 0 < r%:E then +oo else -oo) = (s * r)%:E + (if r%:E == 0 then 0 else if 0 < r%:E then +oo else -oo)
cd
r, t: R
s0: 0 <= +oo
bb8
(if r%:E == 0 then 0 else if 0 < r%:E then +oo else -oo) = (if r%:E == 0 then 0 else if 0 < r%:E then +oo else -oo) + (t * r)%:E
cd
ae
s0, t0: 0 <= +oo
(if r%:E == 0 then 0 else if 0 < r%:E then +oo else -oo) = (if r%:E == 0 then 0 else if 0 < r%:E then +oo else -oo) + (if r%:E == 0 then 0 else if 0 < r%:E then +oo else -oo)
cd
s, t: R
bb7
bb8
(if s%:E + t%:E == 0 then 0 else if 0 < s%:E + t%:E then +oo else -oo) = (if s%:E == 0 then 0 else if 0 < s%:E then +oo else -oo) + (if t%:E == 0 then 0 else if 0 < t%:E then +oo else -oo)
cd
s: R
bb7
bbd
(if 0 < +oo then +oo else -oo) = (if s%:E == 0 then 0 else if 0 < s%:E then +oo else -oo) + (if 0 < +oo then +oo else -oo)
cd
t: R
bc2
bb8
(if 0 < +oo then +oo else -oo) = (if 0 < +oo then +oo else -oo) + (if t%:E == 0 then 0 else if 0 < t%:E then +oo else -oo)
cd
bc6
(if 0 < +oo then +oo else -oo) = (if 0 < +oo then +oo else -oo) + (if 0 < +oo then +oo else -oo)
bc9
(if s%:E + t%:E == 0 then 0 else if 0 < s%:E + t%:E then -oo else +oo) = (if s%:E == 0 then 0 else if 0 < s%:E then -oo else +oo) + (if t%:E == 0 then 0 else if 0 < t%:E then -oo else +oo)
bcd
(if 0 < s%:E + +oo then -oo else +oo) = (if s%:E == 0 then 0 else if 0 < s%:E then -oo else +oo) + (if 0 < +oo then -oo else +oo)
bd1
(if 0 < +oo + t%:E then -oo else +oo) = (if 0 < +oo then -oo else +oo) + (if t%:E == 0 then 0 else if 0 < t%:E then -oo else +oo)
bd5
(if 0 < +oo + +oo then -oo else +oo) = (if 0 < +oo then -oo else +oo) + (if 0 < +oo then -oo else +oo)
bb3
bbc
bbe
bbfbc4bc8bccbd0bd4bd7bd9bdbbdd
be1
bc0
bc3
bc4bc8bccbd0bd4bd7bd9bdbbdd
be6
bc5
bc7
bc8bccbd0bd4bd7bd9bdbbdd
beb
bc9
bcb
bccbd0bd4bd7bd9bdbbdd
bf0
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
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)
cd
bd2
bb8
(if t == 0%R then 0 else if 0 < t%:E then +oo else -oo) = (if t == 0%R then 0 else if 0 < t%:E then +oo else -oo)
bccbd0bd4bd7bd9bdbbdd
bfa
bfc
+oo = +oo + (if t == 0%R then 0 else if 0 < t%:E then +oo else -oo)
bff
c01
c02
bf2
c09
bcd
bcf
bd0bd4bd7bd9bdbbdd
c0d
bd1
bd3
bd4bd7bd9bdbbdd
c12
bd5
bd6
bd7bd9bdbbdd
c17
bc9
bd8
bd9bdbbdd
c1c
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
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)
c01
(if t == 0%R then 0 else if 0 < t%:E then -oo else +oo) = (if t == 0%R then 0 else if 0 < t%:E then -oo else +oo)
bd9bdbbdd
c25
bfc
-oo = -oo + (if t == 0%R then 0 else if 0 < t%:E then -oo else +oo)
c28
c01
c2a
c1e
c31
bcd
bda
bdbbdd
c35
bd1
bdc
bdd
c3a
bd5
bde
c3f
by rewrite ltry; case: ltgtP s0. Qed.
a5d
0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z
c43
by move=> y0 z0; rewrite !(muleC x) ge0_muleDl. Qed.
a5d
y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x
c48
cd
bb6
s0: s%:E <= 0
t0: t%:E <= 0

bb9
cd
55
c50
t0: -oo <= 0
(if r%:E == 0 then 0 else if 0 < r%:E then -oo else +oo) = (s * r)%:E + (if r%:E == 0 then 0 else if 0 < r%:E then -oo else +oo)
cd
bc1
s0: -oo <= 0
c51
(if r%:E == 0 then 0 else if 0 < r%:E then -oo else +oo) = (if r%:E == 0 then 0 else if 0 < r%:E then -oo else +oo) + (t * r)%:E
cd
ae
s0, t0: -oo <= 0
(if r%:E == 0 then 0 else if 0 < r%:E then -oo else +oo) = (if r%:E == 0 then 0 else if 0 < r%:E then -oo else +oo) + (if r%:E == 0 then 0 else if 0 < r%:E then -oo else +oo)
cd
bca
c50
c51
bcb
cd
bce
c50
c55
(if 0 < +oo then -oo else +oo) = (if s%:E == 0 then 0 else if 0 < s%:E then +oo else -oo) + (if 0 < +oo then -oo else +oo)
cd
bd2
c59
c51
(if 0 < +oo then -oo else +oo) = (if 0 < +oo then -oo else +oo) + (if t%:E == 0 then 0 else if 0 < t%:E then +oo else -oo)
cd
c5d
(if 0 < +oo then -oo else +oo) = (if 0 < +oo then -oo else +oo) + (if 0 < +oo then -oo else +oo)
c60bd8
c62
+oo = (if s%:E == 0 then 0 else if 0 < s%:E then -oo else +oo) + +oo
c65
+oo = +oo + (if t%:E == 0 then 0 else if 0 < t%:E then -oo else +oo)
c4d
c54
c56
c57c5bc5fc61c64c67c6ac6bc6d
c71
c58
c5a
c5bc5fc61c64c67c6ac6bc6d
c76
c5c
c5e
c5fc61c64c67c6ac6bc6d
c7b
c60
bcb
c61c64c67c6ac6bc6d
c80
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
cd
bca
c51
s0: (s < 0)%R

bfe
cd
bd2
c51
c02
c61c64c67c6ac6bc6d
c8a
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
c90
c02
c82
c97
c62
c63
c64c67c6ac6bc6d
c9b
c65
c66
c67c6ac6bc6d
ca0
c68
c69
c6ac6bc6d
ca5
c60
bd8
c6bc6d
caa
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
c8c
c27
c90c2a
c6bc6d
cb3
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
c90
c2a
cac
cbd
c62
c6c
c6d
cc1
c65
c6e
cc6
by rewrite ltNge t0 /=; case: eqP. Qed.
a5d
y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z
cca
by move=> y0 z0; rewrite !(muleC x) le0_muleDl. Qed.
750
y \is a fin_num -> 0 < x -> y <= 1 -> y * x <= x
ccf
77a
0 < x%:E -> y%:E <= 1 -> y%:E * x%:E <= x%:E
783
0 < +oo -> y%:E <= 1 -> y%:E * +oo <= +oo
cd4
783
cd9
cdc
by move=> _; rewrite /mule/= eqe => r1; rewrite leey. Qed.
d3
0 <= x -> {homo *%E^~ x : y z / y <= z >-> y <= z}
ce0
77e
0 <= x%:E -> {homo *%E^~ x%:E : y z / y <= z}
ed
{homo *%E^~ +oo : y z / y <= z}
7f6
{homo *%E^~ x%:E : y z / y <= z}
ce8
cd
9a
4ca
9e

y%:E <= +oo -> y%:E * x%:E <= +oo * x%:E
cd
9a
4ca
944
-oo <= z%:E -> -oo * x%:E <= z%:E * x%:E
7f6
-oo <= +oo -> -oo * x%:E <= +oo * x%:E
ce9
cf0
cf6
cf7
cf8ce9
cfc
7f6
cf9
ce8
d01
ed
cea
cd
y, z: R

y%:E <= z%:E -> y%:E * +oo <= z%:E * +oo
783
y%:E <= +oo -> y%:E * +oo <= +oo * +oo
cd
944
-oo <= z%:E -> -oo * +oo <= z%:E * +oo
ed
-oo <= +oo -> -oo * +oo <= +oo * +oo
d08
cd
d0b
yz: (y <= z)%R

y%:E * +oo <= z%:E * +oo
d0d
cd
d0b
d1a
z0: (0 < z)%R

d1b
cd
d0b
d1a
z0: (z < 0)%R
d1b
d19
0%R = z -> y%:E * +oo <= z%:E * +oo
d0ed10d13
d1d
d23
d1b
d25d0ed10d13
d29
d19
d26
d0d
d2e
cd
d0b
z0: 0%R = z

0 * +oo <= 0
cd
d0b
d35
y0: (y < 0)%R
y%:E * +oo <= 0
d0ed10d13
d39
d3b
d0d
783
d0f
d10d13
d40
d11
d12
d13
d45
ed
d14
d4a
by move=> _; rewrite mulNyy leNye. Qed.
d3
0 <= x -> {homo *%E x : y z / y <= z >-> y <= z}
d4e
by move=> x0 y z yz; rewrite !(muleC x) lee_wpmul2r. Qed.
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
d53
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 * x
6b
1df
339
6b6

(\sum_(i <- (h :: t) | P i) F i) * x = \sum_(i <- (h :: t) | P i) F i * x
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.
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
d65
by move=> F0; rewrite muleC ge0_sume_distrl//; under eq_bigr do rewrite muleC. Qed.
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
d6a
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 * x
6b
1df
339
F0: forall i : I, P i -> F i <= 0

d5d
cd
19a
1dd
1de
d72
6b
1df
339
d73
d62

d63
by rewrite le0_muleDl ?sume_le0// ?F0// ih// big_cons Ph. Qed.
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
d79
by move=> F0; rewrite muleC le0_sume_distrl//; under eq_bigr do rewrite muleC. Qed.
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
d7e
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
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.
d3
(forall r, r%:E <= x) -> x = +oo
d90
77e
(x + 1)%:E <= x%:E -> x%:E = +oo
by rewrite EFinD addeC -lee_subr_addr// subee// lee_fin ler10. Qed.
d3
(forall r, x <= r%:E) -> x = -oo
d99
cd
6b
_Hyp_: forall r, x <= r%:E
ae

r%:E <= - x
by rewrite lee_oppr -EFinN. Qed.
732
(- x <= - y) = (y <= x)
da4
by rewrite lee_oppl oppeK. Qed.
d3
x <= `|x|
da9
by move: x => [x| |]//=; rewrite lee_fin ler_norm. Qed.
d3
`|`|x|| = `|x|
dae
by move: x => [x| |] //=; rewrite normr_id. Qed.
732
(`|x| < y) = (- y < x < y)
db3
by move: x y => [x| |] [y| |] //=; rewrite ?lte_fin ?ltry ?ltNyr// ltr_norml. Qed.
732
(`|x| == y) = ((x == y) || (x == - y)) && (0 <= y)
db8
by move: x y => [x| |] [y| |] //=; rewrite? leey// !eqe eqr_norml lee_fin. Qed.
732
`|x + y| <= `|x| + `|y|
dbd
by move: x y => [x| |] [y| |] //; rewrite /abse -EFinD lee_fin ler_norm_add. Qed.
cd
19a
19b
339
1df

`|\sum_(i <- s | P i) F i| <= \sum_(i <- s | P i) `|F i|
dc2
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.
732
`|x - y| <= `|x| + `|y|
dcc
by move: x y => [x| |] [y| |] //; rewrite /abse -EFinD lee_fin ler_norm_sub. Qed.
ed
{morph abse : x y / x * y}
dd1
cc
`|r%:E * +oo| = `|r|%:E * +oo
cd
xoo: forall r, `|r%:E * +oo| = `|r|%:E * +oo
dd3
cd
ae
r0: (0 <= r)%R

dd8
cd
ae
r0: (r < 0)%R
dd8
dda
de4
dd8
dd9
de4
r%:E * +oo < 0
dd9
ddb
dd3
cd
ddc
9a

`|x%:E * -oo| = `|x|%:E * +oo
cd
ddc
9e
`|+oo * y%:E| = +oo * `|y|%:E
ddb
`|+oo * +oo| = +oo * +oo
ddb
`|+oo * -oo| = +oo * +oo
df7
`|-oo * y%:E| = +oo * `|y|%:E
ddb
`|-oo * +oo| = +oo * +oo
ddb
+oo = +oo * +oo
df1
df7
df8
df9dfbdfddffe01
e05
ddb
dfa
dfbdfddffe01
e0a
ddb
dfc
dfddffe01
e0f
df7
dfe
dffe01
e14
ddb
e00
e01
e19
ddb
e02
e1e
by rewrite mulyy. Qed.
cd
14

maxe r1%:E r2%:E = (Num.max r1 r2)%:E
e22
by have [ab|ba] := leP r1 r2; [apply/max_idPr; rewrite lee_fin|apply/max_idPl; rewrite lee_fin ltW]. Qed.
e24
mine r1%:E r2%:E = (Num.min r1 r2)%:E
e28
by have [ab|ba] := leP r1 r2; [apply/min_idPl; rewrite lee_fin|apply/min_idPr; rewrite lee_fin ltW]. Qed.
ed
left_distributive +%E maxe
e2d
cd
1b8
xy: x <= y

y + z = maxe (x + z) (y + z)
cd
1b8
yx: y < x
x + z = maxe (x + z) (y + z)
e39
e3b
by apply/esym/max_idPl; rewrite lee_add2r// ltW. Qed.
ed
right_distributive +%E maxe
e40
cd
1b8
yz: y <= z

x + z = maxe (x + y) (x + z)
cd
1b8
zy: z < y
x + y = maxe (x + y) (x + z)
e4c
e4e
by apply/esym/max_idPl; rewrite lee_add2l// ltW. Qed.
ed
left_zero (+oo : \bar R) maxe
e53
by move=> x; have [|//] := leP +oo x; rewrite leye_eq => /eqP. Qed.
ed
right_zero (+oo : \bar R) maxe
e58
by move=> x; rewrite maxC maxye. Qed.
ed
left_id (-oo : \bar R) maxe
e5d
by move=> x; have [//|] := leP -oo x; rewrite ltNge leNye. Qed.
ed
right_id (-oo : \bar R) maxe
e62
by move=> x; rewrite maxC maxNye. Qed. Canonical maxe_monoid := Monoid.Law maxA maxNye maxeNy. Canonical maxe_comoid := Monoid.ComLaw maxC.
ed
left_zero (-oo : \bar R) mine
e67
by move=> x; have [|//] := leP x -oo; rewrite leeNy_eq => /eqP. Qed.
ed
right_zero (-oo : \bar R) mine
e6c
by move=> x; rewrite minC minNye. Qed.
ed
left_id (+oo : \bar R) mine
e71
by move=> x; have [//|] := leP x +oo; rewrite ltNge leey. Qed.
ed
right_id (+oo : \bar R) mine
e76
by move=> x; rewrite minC minye. Qed. Canonical mine_monoid := Monoid.Law minA minye miney. Canonical mine_comoid := Monoid.ComLaw minC.
ed
{morph -%E : x y / maxe x y >-> mine x y : \bar R}
e7b
77a
- maxe x%:E y%:E = mine (- x)%:E (- y)%:E
77e
- maxe x%:E +oo = mine (- x)%:E -oo
77e
(- x)%:E = mine (- x)%:E +oo
783
-oo = mine -oo (- y)%:E
783
- maxe -oo y%:E = mine +oo (- y)%:E
e80
77e
e85
e86e88e8a
e8e
77e
e87
e88e8a
e93
783
e89
e8a
e98
783
e8b
e9d
by rewrite maxNye minye. Qed.
ed
{morph -%E : x y / mine x y >-> maxe x y : \bar R}
ea1
by move=> x y; rewrite -[RHS]oppeK oppe_max !oppeK. Qed.
cd
z, x, y: \bar R

z \is a fin_num -> 0 < z -> z * maxe x y = maxe (z * x) (z * y)
ea6
cd
ea9
r0: 0 < z
xy: x < y

z \is a fin_num -> z * y = maxe (z * x) (z * y)
cd
ea9
eb0
e3a
z \is a fin_num -> z * x = maxe (z * x) (z * y)
ead
eb5
eb6
eb9
by move=> zfin; rewrite maxC /maxe lte_pmul2l// yx. Qed.
ea8
z \is a fin_num -> 0 < z -> maxe x y * z = maxe (x * z) (y * z)
ebd
by move=> zfin z0; rewrite muleC maxeMr// !(muleC z). Qed.
ea8
z \is a fin_num -> 0 < z -> z * mine x y = mine (z * x) (z * y)
ec2
by move=> ? ?; rewrite -eqe_oppP -muleN oppe_min maxeMr// !muleN -oppe_min. Qed.
ea8
z \is a fin_num -> 0 < z -> mine x y * z = mine (x * z) (y * z)
ec7
by move=> zfin z0; rewrite muleC mineMr// !(muleC z). Qed.
732
0 <= y -> 1 <= x -> y <= x * y
ecc
77a
0 <= y%:E -> 1 <= x%:E -> y%:E <= x%:E * y%:E
77e
0 <= +oo -> 1 <= x%:E -> +oo <= x%:E * +oo
783
0 <= y%:E -> 1 <= +oo -> y%:E <= +oo * y%:E
ed1
77e
ed6
ed7
edb
cd
9a
x1: (1 <= x)%R

+oo <= x%:E * +oo
edd
783
ed8
ee6
cd
9e
4d4

y%:E <= +oo * y%:E
by rewrite mulr_infty gtr0_sg// mul1e leey. Qed.
732
y <= 0 -> 1 <= x -> x * y <= y
eef
77a
y%:E <= 0 -> 1 <= x%:E -> x%:E * y%:E <= y%:E
77e
-oo <= 0 -> 1 <= x%:E -> x%:E * -oo <= -oo
783
y%:E <= 0 -> 1 <= +oo -> +oo * y%:E <= y%:E
ef4
77e
ef9
efa
efe
ee2
x%:E * -oo <= -oo
f00
783
efb
f07
cd
9e
d3a

+oo * y%:E <= y%:E
by rewrite mulr_infty ltr0_sg// mulN1e leNye. Qed.
732
0 <= y -> 1 <= x -> y <= y * x
f10
by move=> y0 x1; rewrite muleC lee_pemull. Qed.
732
y <= 0 -> 1 <= x -> y * x <= y
f15
by move=> y0 x1; rewrite muleC lee_nemull. Qed.
cd
6b
128

(n%:R)%:E * x = x *+ n
f1a
f1c
(n%:R)%:E * x = x *+ n -> (n.+1%:R)%:E * x = x *+ n.+1
cd
128
9a
ih: (n%:R)%:E * x%:E = x%:E *+ n

(n.+1%:R)%:E * x%:E = x%:E *+ n.+1
cd
128
ih: (n%:R)%:E * +oo = +oo *+ n
(n.+1%:R)%:E * +oo = +oo *+ n.+1
cd
128
ih: (n%:R)%:E * -oo = -oo *+ n
(n.+1%:R)%:E * -oo = -oo *+ n.+1
f24
f2b
f2d
f2e
f34
f2f
f31
f39
by rewrite mulrNy gtr0_sg// mul1e enatmul_ninfty. Qed.
cd
x1, y1, x2, y2: \bar R

0 <= x1 -> 0 <= x2 -> x1 < y1 -> x2 < y2 -> x1 * x2 < y1 * y2
f3d
cd
x1, y1, x2, y2: R

(0 <= x1)%R -> (0 <= x2)%R -> (x1 < y1)%R -> (x2 < y2)%R -> (x1 * x2 < y1 * y2)%R
cd
x1, y1, x2: R
(0 <= x1)%R -> (0 <= x2)%R -> (x1 < y1)%R -> x2%:E < +oo -> x1%:E * x2%:E < y1%:E * +oo
cd
x1, x2, y2: R
(0 <= x1)%R -> (0 <= x2)%R -> x1%:E < +oo -> (x2 < y2)%R -> x1%:E * x2%:E < +oo * y2%:E
cd
x1, x2: R
(0 <= x1)%R -> (0 <= x2)%R -> x1%:E < +oo -> x2%:E < +oo -> x1%:E * x2%:E < +oo * +oo
f44
f4b
f4d
f4ef52
f58
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
f4f
f51
f52
f66
cd
f50
f60
f61
xy1: x1%:E < +oo
xy2: (x2 < y2)%R

x1%:E * x2%:E < +oo * y2%:E
f68
f53
f55
f72
by move=> *; rewrite mulyy -EFinM ltry. Qed.
f3f
0 <= x1 -> 0 <= x2 -> x1 <= y1 -> x2 <= y2 -> x1 * x2 <= y1 * y2
f76
f46
(0 <= x1)%R -> (0 <= x2)%R -> (x1 <= y1)%R -> (x2 <= y2)%R -> (x1 * x2 <= y1 * y2)%R
f4b
(0 <= x1)%R -> (0 <= x2)%R -> (x1 <= y1)%R -> x2%:E <= +oo -> x1%:E * x2%:E <= y1%:E * +oo
cd
x1, y1: R
(0 <= x1)%R -> 0 <= +oo -> (x1 <= y1)%R -> +oo <= +oo -> x1%:E * +oo <= y1%:E * +oo
f4f
(0 <= x1)%R -> (0 <= x2)%R -> x1%:E <= +oo -> (x2 <= y2)%R -> x1%:E * x2%:E <= +oo * y2%:E
f53
(0 <= x1)%R -> (0 <= x2)%R -> x1%:E <= +oo -> x2%:E <= +oo -> x1%:E * x2%:E <= +oo * +oo
cd
x1: R
(0 <= x1)%R -> 0 <= +oo -> x1%:E <= +oo -> +oo <= +oo -> x1%:E * +oo <= +oo * +oo
cd
x2, y2: R
0 <= +oo -> (0 <= x2)%R -> +oo <= +oo -> (x2 <= y2)%R -> +oo * x2%:E <= +oo * y2%:E
cd
x2: R
0 <= +oo -> (0 <= x2)%R -> +oo <= +oo -> x2%:E <= +oo -> +oo * x2%:E <= +oo * +oo
f7b
f4b
f80
f81f85f87f89f8df91
f97
cd
f4c
f61
y10: (0 <= y1)%R

0 * x2%:E <= y1%:E * +oo
cd
f4c
x10: (0 < x1)%R
f61
xy1: (x1 <= y1)%R
x1%:E * x2%:E <= y1%:E * +oo
f81f85f87f89f8df91
fa3
fa6
f99
f82
f84
f85f87f89f8df91
fab
cd
f83
f9f

0 * +oo <= y1%:E * +oo
cd
f83
fa4
fa5
x1%:E * +oo <= y1%:E * +oo
f85f87f89f8df91
fb6
fb7
fad
fb6
(0 < y1)%R
fad
f4f
f86
f87f89f8df91
fc0
cd
f50
f60
y20: (0 <= y2)%R

x1%:E * 0 <= +oo * y2%:E
cd
f50
f60
x20: (0 < x2)%R
xy2: (x2 <= y2)%R
x1%:E * x2%:E <= +oo * y2%:E
f87f89f8df91
fcc
fcf
fc2
f53
f88
f89f8df91
fd4
f8a
f8c
f8df91
fd9
f8a
0 * +oo <= +oo * +oo
cd
f8b
fa4
x1%:E * +oo <= +oo * +oo
f8df91
fe3
fe4
fdb
f8e
f90
f91
fe9
cd
f8f
fc8

+oo * 0 <= +oo * y2%:E
cd
f8f
fcd
fce
+oo * x2%:E <= +oo * y2%:E
f91
ff4
ff5
feb
ff4
(0 < y2)%R
feb
f92
f94
ffe
f92
+oo * 0 <= +oo * +oo
cd
f93
fcd
+oo * x2%:E <= +oo * +oo
1007
1008
by rewrite mulr_infty gtr0_sg// mul1e// mulyy. Qed.
d3
x \is a fin_num -> 0 < x -> {mono *%E x : x y / x <= y >-> x <= y}
100d
cd
9a
4ca
d0b

(x%:E * y%:E <= x%:E * z%:E) = (y%:E <= z%:E)
cf2
(x%:E * y%:E <= x%:E * +oo) = (y%:E <= +oo)
cf2
(x%:E * y%:E <= x%:E * -oo) = (y%:E <= -oo)
cf6
(x%:E * +oo <= x%:E * z%:E) = (+oo <= z%:E)
7f6
(x%:E * +oo <= x%:E * +oo) = (+oo <= +oo)
7f6
(x%:E * +oo <= x%:E * -oo) = (+oo <= -oo)
cf6
(x%:E * -oo <= x%:E * z%:E) = (-oo <= z%:E)
7f6
(x%:E * -oo <= x%:E * +oo) = (-oo <= +oo)
7f6
(x%:E * -oo <= x%:E * -oo) = (-oo <= -oo)
1012
cf2
1018
1019101b101d101f102110231025
1029
cf2
101a
101b101d101f102110231025
102e
cf6
101c
101d101f102110231025
1033
7f6
101e
101f102110231025
1038
7f6
1020
102110231025
103d
cf6
1022
10231025
1042
7f6
1024
1025
1047
7f6
1026
104c
by rewrite mulrNy gtr0_sg// mul1e. Qed.
d3
x \is a fin_num -> 0 < x -> {mono *%E^~ x : x y / x <= y >-> x <= y}
1050
by move=> xfin x0 y z; rewrite -2!(muleC x) lee_pmul2l. Qed.
cd
y, x, z: \bar R

0 <= x -> y <= z -> y <= x + z
1055
by move=> *; rewrite -[y]add0e lee_add. Qed.
1057
0 <= x -> y < z -> y < x + z
105c
by move=> x0 /lt_le_trans; apply; rewrite lee_paddl. Qed.
1057
0 <= x -> y <= z -> y <= z + x
1061
by move=> *; rewrite addeC lee_paddl. Qed.
1057
0 <= x -> y < z -> y < z + x
1066
by move=> *; rewrite addeC lte_paddl. Qed.
ea8
z \is a fin_num -> 0 < y -> z <= x -> z < x + y
106b
cd
z, y, x: R

(0 < y)%R -> z%:E <= x%:E -> (z < x + y)%R
exact: ltr_spaddr. Qed.
ea8
x \is a fin_num -> 0 < y -> z <= x -> z < x + y
1076
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}.
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.
732
(x - y < 0) = (x < y)
107d
by rewrite dual_addeE oppe_lt0 sube_gt0 lte_opp. Qed.
732
(0 <= y - x) = (x <= y)
1082
by rewrite dual_addeE oppe_ge0 sube_le0 lee_opp. Qed.
732
y \is a fin_num -> (x - y <= 0) = (x <= y)
1087
by move=> ?; rewrite dual_addeE oppe_le0 suber_ge0 ?fin_numN// lee_opp. Qed.
750
y \is a fin_num -> (y - x <= 0) = (y <= x)
108c
by move=> ?; rewrite dual_addeE oppe_le0 subre_ge0 ?fin_numN// lee_opp. Qed.
732
(x \is a fin_num) || (y \is a fin_num) -> (y - x <= 0) = (y <= x)
1091
by move=> /orP[?|?]; [rewrite dsuber_le0|rewrite dsubre_le0]. Qed.
88f
88f
rewrite !dual_addeE lte_opp -lte_opp -(lte_opp y); exact: lte_add. Qed.
89c
89c
rewrite dual_addeE lee_oppr -oppe_le0; exact: gee_addl. Qed.
8a1
8a4 rewrite dual_addeE lee_oppr -oppe_le0; exact: gee_addr. Qed.
8a6
8a6
rewrite dual_addeE lee_oppl -oppe_ge0; exact: lee_addl. Qed.
8ab
8ae rewrite dual_addeE lee_oppl -oppe_ge0; exact: lee_addr. Qed.
8b0
8b0
by rewrite -fin_numN dual_addeE lte_oppr; exact: gte_subl. Qed.
8b5
8b8 by rewrite -fin_numN dual_addeE lte_oppr addeC; exact: gte_subl. Qed.
8ba
8ba
by rewrite -fin_numN dual_addeE lte_oppl oppeK; exact: lte_addl. Qed.
8c3
8c6 by rewrite -fin_numN dual_addeE lte_oppl oppeK; exact: lte_addr. Qed.
8c8
8cb by rewrite -fin_numN dual_addeE lte_oppl -oppe0 lte_oppr; exact: lte_addl. Qed.
8cd
8d0 by rewrite daddeC; exact: gte_daddl. Qed.
8d2
8d7 by move=> ?; rewrite !dual_addeE lte_opp lte_add2lE ?fin_numN// lte_opp. Qed.
8df
8df
rewrite !dual_addeE lee_opp -lee_opp; exact: lee_add2l. Qed.
8f9
8fc by move=> ?; rewrite !dual_addeE lee_opp lee_add2lE ?fin_numN// lee_opp. Qed.
902
905 rewrite !dual_addeE lee_opp -lee_opp; exact: lee_add2r. Qed.
907
907
rewrite !dual_addeE lee_opp -lee_opp -(lee_opp y); exact: lee_add. Qed.
910
910
rewrite !dual_addeE lte_opp -lte_opp; exact: lte_le_sub. Qed.
91b
91e by move=> afin xa yb; rewrite (daddeC a) (daddeC x) lte_le_dadd. Qed.
cd
1b8
t: dual_extended R

x <= y -> t <= z -> x - z <= y - t
10b0
rewrite !dual_addeE lee_oppl oppeK -lee_opp !oppeK; exact: lee_add. Qed.
92d
932 rewrite !dual_addeE lte_opp !oppeK -lte_opp; exact: lte_le_add. Qed.
98c
98c
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.
993
998
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.
9a1
9a4
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.
9ac
9b2
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.
9ba
9bd
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.
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}
10d6
cd
35a
9c8
f0: forall n : nat, P n -> (0 <= f n)%E
9dd
mlen: (m <= n)%N

(\sum_(i | P i) - f i <= \sum_(i | P i) - f i)%E
cd
35a
9c8
10de
9dd
10df
i: nat
3ae

(- f i <= 0)%E
rewrite oppe_le0; exact: f0. Qed.
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}
10e8
cd
35a
9c8
f0: forall n : nat, P n -> (f n <= 0)%E
9dd
10df

10e0
cd
35a
9c8
10f0
9dd
10df
10e5
3ae

(0 <= - f i)%E
rewrite oppe_ge0; exact: f0. Qed.
9e1
9e6
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.
9ee
9f1
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.
9f9
9fd
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.
a0b
a0e
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.
a1a
a20
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.
a3e
a41
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.
a5b
a5f by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr oppeK lte_subl_addr. Qed.
a67
a67
by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subr_addl ?fin_numN. Qed.
a6c
a6f by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subl_addr ?fin_numN. Qed.
a75
a75
by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subl_addl ?fin_numN. Qed.
a5d
y \is a fin_num -> (x < y - z) = (x + z < y)
111b
by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subel_addr ?fin_numN. Qed.
a5d
y \is a fin_num -> (x < y - z) = (z + x < y)
1120
by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr lte_subel_addl ?fin_numN. Qed.
a5d
z \is a fin_num -> (x - y < z) = (x < z + y)
1125
by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr lte_suber_addr ?fin_numN. Qed.
a5d
z \is a fin_num -> (x - y < z) = (x < y + z)
112a
by move=> ?; rewrite !dual_addeE lte_oppl lte_oppr lte_suber_addl ?fin_numN. Qed.
a8f
a92 by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subr_addr ?fin_numN. Qed.
a98
a98
by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subr_addl ?fin_numN. Qed.
a9d
aa0 by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subl_addr ?fin_numN. Qed.
aa8
aa8
by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subl_addl ?fin_numN. Qed.
a5d
x \is a fin_num -> (x - y <= z) = (x <= z + y)
1135
by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_suber_addr ?fin_numN. Qed.
a5d
x \is a fin_num -> (x - y <= z) = (x <= y + z)
113a
by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_suber_addl ?fin_numN. Qed.
a5d
x \is a fin_num -> (x <= y - z) = (x + z <= y)
113f
by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subel_addr ?fin_numN. Qed.
a5d
x \is a fin_num -> (x <= y - z) = (z + x <= y)
1144
by move=> ?; rewrite !dual_addeE lee_oppl lee_oppr lee_subel_addl ?fin_numN. Qed.
732
x \is a fin_num -> (0 < y - x) = (x < y)
1149
by move=> ?; rewrite lte_dsubr_addl// dadde0. Qed.
732
y \is a fin_num -> (0 < y - x) = (x < y)
114e
by move=> ?; rewrite lte_dsuber_addl// dadde0. Qed.
732
(x \is a fin_num) || (y \is a fin_num) -> (0 < y - x) = (x < y)
1153
by move=> /orP[?|?]; [rewrite dsuber_gt0|rewrite dsubre_gt0]. Qed.
a5d
x \is a fin_num -> (y +? z)%E -> x * (y + z) = x * y + x * z
1158
by move=> *; rewrite !dual_addeE muleN muleDr ?adde_defNN// !muleN. Qed.
a5d
x \is a fin_num -> (y +? z)%E -> (y + z) * x = y * x + z * x
115d
by move=> *; rewrite -!(muleC x) dmuleDr. Qed.
bae
bae
by move=> *; rewrite !dual_addeE mulNe le0_muleDl ?oppe_le0 ?mulNe. Qed.
c43
c46 by move=> *; rewrite !dual_addeE muleN le0_muleDr ?oppe_le0 ?muleN. Qed.
c48
c48
by move=> *; rewrite !dual_addeE mulNe ge0_muleDl ?oppe_ge0 ?mulNe. Qed.
cca
ccd by move=> *; rewrite !dual_addeE muleN ge0_muleDr ?oppe_ge0 ?muleN. Qed.
d53
d57
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
cd
19a
19b
6b
1df
339
6b6
3e3
3ae
(- F i <= 0)%E
1169
116f
1170
1173
by rewrite oppe_le0 F0. Qed.
d65
d68 by move=> F0; rewrite muleC ge0_dsume_distrl//; under eq_bigr do rewrite muleC. Qed.
d6a
d6d
cd
19a
19b
6b
1df
339
d73

116c
cd
19a
19b
6b
1df
339
d73
3e3
3ae
(0 <= - F i)%E
1179
117e
117f
1182
by rewrite oppe_ge0 F0. Qed.
d79
d7c by move=> F0; rewrite muleC le0_dsume_distrl//; under eq_bigr do rewrite muleC. Qed.
dbd
dc0 by move: x y => [x| |] [y| |] //; rewrite /abse -dEFinD lee_fin ler_norm_add. Qed.
dc2
dc6
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.
dcc
dcf by move: x y => [x| |] [y| |] //; rewrite /abse -dEFinD lee_fin ler_norm_sub. Qed.
ed
left_distributive +%dE mine
118e
by move=> x y z; rewrite !dual_addeE oppe_min adde_maxl oppe_max. Qed.
ed
right_distributive +%dE mine
1193
by move=> x y z; rewrite !dual_addeE oppe_min adde_maxr oppe_max. Qed.
f1a
f1a
by rewrite mule_natl ednatmulE. Qed.
1055
105a by move=> *; rewrite -[y]dadd0e lee_dadd. Qed.
105c
105f by move=> x0 /lt_le_trans; apply; rewrite lee_pdaddl. Qed.
1061
1064 by move=> *; rewrite daddeC lee_pdaddl. Qed.
1066
1069 by move=> *; rewrite daddeC lte_pdaddl. Qed.
106b
106e
1072
(0 < y)%R -> (z%:E <= x%:E)%E -> (z < x + y)%R
exact: ltr_spaddr. Qed.
1076
1079 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.
29
{mono -%E : y x / x <= y >-> y <= x}
11a4
22
_r_: R

(- _r_%:E <= - -oo) = (-oo <= _r_%:E)
11ab
(- +oo <= - _r_%:E) = (_r_%:E <= +oo)
11ab
11b0
by rewrite /Order.le/= realN. Qed.
29
{mono -%E : y x / x < y >-> y < x}
11b5
11ab
(- _r_%:E < - -oo) = (-oo < _r_%:E)
11ab
(- +oo < - _r_%:E) = (_r_%:E < +oo)
11ab
11bf
by rewrite /Order.lt/= realN. Qed. Section realFieldType_lemmas. Variable R : realFieldType. Implicit Types x y : \bar R. Implicit Types r : R.
R: realFieldType
23

(forall e : {posnum R}, x <= y + (e%:num)%:E) -> x <= y
11c4
11c7
xleye: forall e : {posnum R}, +oo <= -oo + (e%:num)%:E

+oo <= -oo
11c7
9e
xleye: forall e : {posnum R}, +oo <= y%:E + (e%:num)%:E
+oo <= y%:E
11c7
9a
xleye: forall e : {posnum R}, x%:E <= -oo + (e%:num)%:E
x%:E <= -oo
11c7
95
xleye: forall e : {posnum R}, x%:E <= y%:E + (e%:num)%:E
x%:E <= y%:E
11cb
11d2
11d4
11d511d9
11df
11d6
11d8
11d9
11e4
11da
11dc
11c7
95
11db
yltx: y%:E < x%:E

6a0
11c7
95
11db
11ef
xmy_gt0: (0 < (x - y) / 2)%R

6a0
11f3
(y + (x - y) / 2 < x)%R
11f3
(y / 2 + y / 2 + (x - y) / 2 < x / 2 + x / 2)%R
by rewrite -!mulrDl ltr_pmul2r// addrCA addrK ltr_add2l. Qed.
11c6
0 <= x -> reflect (forall r, (0 < r < 1)%R -> r%:E * x <= y) (x <= y)
11fe
11c7
23
x0: 0 <= x
e35
ae
r0: (0 < r)%R
r1: (r < 1)%R

r%:E * x <= y
11c7
23
1206
h: forall r, (0 < r < 1)%R -> r%:E * x <= y
x <= y
11c7
23
ae
1207
1208
b49
e35

1209
120a
120c
120e
11c7
23
1206
120d
h01: (0 < 2^-1 < 1)%R

120e
11c7
121a
95
7cc
h: forall r, (0 < r < 1)%R -> r%:E * x%:E <= y%:E

11dc
11c7
121a
9a
7cc
h: forall r, (0 < r < 1)%R -> r%:E * x%:E <= +oo
x%:E <= +oo
11c7
121a
9a
7cc
h: forall r, (0 < r < 1)%R -> r%:E * x%:E <= -oo
11d8
11c7
121a
9e
x0: 0 <= +oo
h: forall r, (0 < r < 1)%R -> r%:E * +oo <= y%:E
11d4
11c7
121a
122a
h: forall r, (0 < r < 1)%R -> r%:E * +oo <= -oo
11cf
121c
121e
0 <= y%:E
11c7
121a
95
121f
4ca
11dc
122112251228122c
1236
11dc
1220
1236
(0 < y)%R
11c7
121a
95
121f
4ca
4d4
11dc
122112251228122c
1240
11dc
1220
11c7
121a
95
121f
4ca
4d4
yx: (y < x)%R

6a0
1220
1247
(0 < (y + x) / (2 * x) < 1)%R
1247
((y + x) / (2 * x))%:E * x%:E <= y%:E -> False
122112251228122c
1247
((y + x) / (2 * x) < 1)%R
124d
1247
124f
1220
1247
((y + x) * (x^-1 * x / 2) <= y)%R -> False
1220
1222
1224
12251228122c
125c
1226
11d8
1228122c
1261
1229
11d4
122c
1266
122d
11cf
126b
by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e. Qed.
11c7
ae
23

(0 < r)%R -> ((r^-1)%:E * y < x) = (y < r%:E * x)
126f
11c7
ae
1207
95

((r^-1)%:E * y%:E < x%:E) = (y%:E < r%:E * x%:E)
11c7
ae
1207
9a
((r^-1)%:E * +oo < x%:E) = (+oo < r%:E * x%:E)
127b
((r^-1)%:E * -oo < x%:E) = (-oo < r%:E * x%:E)
11c7
ae
1207
9e
((r^-1)%:E * y%:E < +oo) = (y%:E < r%:E * +oo)
11c7
ae
1207
((r^-1)%:E * +oo < +oo) = (+oo < r%:E * +oo)
1283
((r^-1)%:E * -oo < +oo) = (-oo < r%:E * +oo)
1280
((r^-1)%:E * y%:E < -oo) = (y%:E < r%:E * -oo)
1283
((r^-1)%:E * +oo < -oo) = (+oo < r%:E * -oo)
1283
((r^-1)%:E * -oo < -oo) = (-oo < r%:E * -oo)
1275
127b
127c
127d127f1282128512871289128b
128f
127b
127e
127f1282128512871289128b
1294
1280
1281
1282128512871289128b
1299
1283
1284
128512871289128b
129e
1283
1286
12871289128b
12a3
1280
1288
1289128b
12a8
1283
128a
128b
12ad
1283
128c
12b2
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e. Qed.
1271
(0 < r)%R -> (y * (r^-1)%:E < x) = (y < x * r%:E)
12b6
by move=> r0; rewrite muleC lte_pdivr_mull// muleC. Qed.
11c7
ae
751

(0 < r)%R -> (x < (r^-1)%:E * y) = (r%:E * x < y)
12bb
1277
(x%:E < (r^-1)%:E * y%:E) = (r%:E * x%:E < y%:E)
127b
(x%:E < (r^-1)%:E * +oo) = (r%:E * x%:E < +oo)
127b
(x%:E < (r^-1)%:E * -oo) = (r%:E * x%:E < -oo)
1280
(+oo < (r^-1)%:E * y%:E) = (r%:E * +oo < y%:E)
1283
(+oo < (r^-1)%:E * +oo) = (r%:E * +oo < +oo)
1283
(+oo < (r^-1)%:E * -oo) = (r%:E * +oo < -oo)
1280
(-oo < (r^-1)%:E * y%:E) = (r%:E * -oo < y%:E)
1283
(-oo < (r^-1)%:E * +oo) = (r%:E * -oo < +oo)
1283
(-oo < (r^-1)%:E * -oo) = (r%:E * -oo < -oo)
12c1
127b
12c6
12c712c912cb12cd12cf12d112d3
12d7
127b
12c8
12c912cb12cd12cf12d112d3
12dc
1280
12ca
12cb12cd12cf12d112d3
12e1
1283
12cc
12cd12cf12d112d3
12e6
1283
12ce
12cf12d112d3
12eb
1280
12d0
12d112d3
12f0
1283
12d2
12d3
12f5
1283
12d4
12fa
by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e. Qed.
1271
(0 < r)%R -> (x < y * (r^-1)%:E) = (x * r%:E < y)
12fe
by move=> r0; rewrite muleC lte_pdivl_mull// muleC. Qed.
1271
(r < 0)%R -> (x < y * (r^-1)%:E) = (y < x * r%:E)
1303
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.
1271
(r < 0)%R -> (x < (r^-1)%:E * y) = (y < r%:E * x)
130e
by move=> r0; rewrite muleC lte_ndivl_mulr// muleC. Qed.
1271
(r < 0)%R -> ((r^-1)%:E * y < x) = (r%:E * x < y)
1313
130a
((- (- r)^-1)%:E * y < x) = (r%:E * x < y)
by rewrite EFinN mulNe lte_oppl lte_pdivl_mull// EFinN muleNN. Qed.
1271
(r < 0)%R -> (y * (r^-1)%:E < x) = (x * r%:E < y)
131c
by move=> r0; rewrite muleC lte_ndivr_mull// muleC. Qed.
1271
(0 < r)%R -> ((r^-1)%:E * y <= x) = (y <= r%:E * x)
1321
11c7
ae
23
1207

(r^-1)%:E * y <= x -> y <= r%:E * x
1328
y <= r%:E * x -> (r^-1)%:E * y <= x
1326
1328
y <= r%:E * ((r^-1)%:E * y)
132a
1328
132c
1333
1328
(r^-1)%:E * (r%:E * x) <= x
by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF. Qed.
1271
(0 < r)%R -> (y * (r^-1)%:E <= x) = (y <= x * r%:E)
133b
by move=> r0; rewrite muleC lee_pdivr_mull// muleC. Qed.
12bd
(0 < r)%R -> (x <= (r^-1)%:E * y) = (r%:E * x <= y)
1340
11c7
ae
751
1207

x <= (r^-1)%:E * y -> r%:E * x <= y
1347
r%:E * x <= y -> x <= (r^-1)%:E * y
1345
1347
r%:E * ((r^-1)%:E * y) <= y
1349
1347
134b
1352
1347
x <= (r^-1)%:E * (r%:E * x)
by rewrite muleA -EFinM mulVr ?mul1e// unitfE gt_eqF. Qed.
1271
(0 < r)%R -> (x <= y * (r^-1)%:E) = (x * r%:E <= y)
135a
by move=> r0; rewrite muleC lee_pdivl_mull// muleC. Qed.
1271
(r < 0)%R -> (x <= y * (r^-1)%:E) = (y <= x * r%:E)
135f
130a
(x <= y * (- (- r)^-1)%:E) = (y <= x * r%:E)
by rewrite EFinN muleN lee_oppr lee_pdivr_mulr// EFinN muleNN. Qed.
1271
(r < 0)%R -> (x <= (r^-1)%:E * y) = (y <= r%:E * x)
1368
by move=> r0; rewrite muleC lee_ndivl_mulr// muleC. Qed.
1271
(r < 0)%R -> ((r^-1)%:E * y <= x) = (r%:E * x <= y)
136d
130a
((- (- r)^-1)%:E * y <= x) = (r%:E * x <= y)
by rewrite EFinN mulNe lee_oppl lee_pdivl_mull// EFinN muleNN. Qed.
1271
(r < 0)%R -> (y * (r^-1)%:E <= x) = (x * r%:E <= y)
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.
11c4
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}.
29
Signed.spec 0 !=0 >=0 (+oo : \bar R)
137d
by rewrite /= le0y. Qed. Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof).
29
Signed.spec 0 !=0 <=0 (-oo : \bar R)
1382
by rewrite /= leNy0. Qed. Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof).
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
1387
1389
KnownSign.nullity_bool nz ==> ((x%:num)%:E != 0)
1389
Signed.reality_cond 0 cond (x%:num)%:E
1389
1395
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).
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)
139a
22
139d
x: ereal_porderType

x == 0 -> fine x == 0%R
13a5107
13a5116
13a5
(0 <= x) || (x <= 0) -> (0 <= fine x)%R || (fine x <= 0)%R
13a3
13a5
107
13aa13ab
13af
13a5
116
13ab
13b4
13a5
13ac
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).
22
139d
139e
139f
r:= opp_reality_subdef xnz xr: KnownSign.reality

Signed.spec 0 xnz r (- x%:num)
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).
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)
13c4
22
13c7
13c8
139f
13c9

KnownSign.nullity_bool (add_nonzero_subdef xnz ynz xr yr) ==> (x%:num + y%:num != 0)
13d1
Signed.reality_cond 0 (add_reality_subdef xnz ynz xr yr) (x%:num + y%:num)
13d1
13d5
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.
13c6
Signed.spec 0 rnz rrl (x%:num + y%:num)%dE
13da
13d1
KnownSign.nullity_bool (add_nonzero_subdef xnz ynz xr yr) ==> ((x%:num + y%:num)%dE != 0)
13d1
Signed.reality_cond 0 (add_reality_subdef xnz ynz xr yr) (x%:num + y%:num)%dE
13d1
13e4
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).
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)
13e9
13d1
KnownSign.nullity_bool (mul_nonzero_subdef xnz ynz xr yr) ==> (x%:num * y%:num != 0)
13d1
Signed.reality_cond 0 (mul_reality_subdef xnz ynz xr yr) (x%:num * y%:num)
13d1
13f6
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 /.
22
139d
139e
139f
r:= abse_reality_subdef xnz xr: KnownSign.sign

Signed.spec 0 xnz r `|x%:num|
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).
22
138a
138b
a: \bar R

(`|a|%:nng == 0%:nng :> {nonneg \bar R}) = (a == 0)
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).
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)
1409
by rewrite -comparable_le_maxr// ereal_comparable. Qed.
140b
(maxe x%:num y%:num <= a) = (x%:num <= a) && (y%:num <= a)
1411
by rewrite -comparable_le_maxl// ereal_comparable. Qed.
140b
(a <= mine x%:num y%:num) = (a <= x%:num) && (a <= y%:num)
1416
by rewrite -comparable_le_minr// ereal_comparable. Qed.
140b
(mine x%:num y%:num <= a) = (x%:num <= a) || (y%:num <= a)
141b
by rewrite -comparable_le_minl// ereal_comparable. Qed.
140b
(a < maxe x%:num y%:num) = (a < x%:num) || (a < y%:num)
1420
by rewrite -comparable_lt_maxr// ereal_comparable. Qed.
140b
(maxe x%:num y%:num < a) = (x%:num < a) && (y%:num < a)
1425
by rewrite -comparable_lt_maxl// ereal_comparable. Qed.
140b
(a < mine x%:num y%:num) = (a < x%:num) && (a < y%:num)
142a
by rewrite -comparable_lt_minr// ereal_comparable. Qed.
140b
(mine x%:num y%:num < a) = (x%:num < a) || (y%:num < a)
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).
22
138a
1405
x: {compare 0 : \bar R & ?=0 & >=0}

0 <= a -> ((`|a|%:nng : {nonneg \bar R}) <= x) = (a <= x%:num)
1434
by move=> a0; rewrite -num_le//= gee0_abs. Qed.
1436
0 <= a -> ((`|a|%:nng : {nonneg \bar R}) < x) = (a < x%:num)
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.
6a
0 < x -> posnume_spec x x (x == 0) (0 <= x) (0 < x)
1440
99
0 < x%:E -> posnume_spec x%:E x%:E (x%:E == 0) (0 <= x%:E) (0 < x%:E)
22
9a
x_gt0: (0 < x)%R

posnume_spec x%:E x%:E (x == 0%R) (0 <= x)%R (0 < x)%R
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.
6a
0 <= x -> nonnege_spec x x (0 <= x)
1453
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.
11c7
ae

(`|contract r%:E| < 1)%R
145c
145e
(`|r| / `|1 + `|r|| < 1)%R
145e
(`|r| < `|1 + `|r||)%R
by rewrite [ltRHS]gtr0_norm ?ltr_addr// ltr_spaddl. Qed.
11c7
6b

(`|contract x| <= 1)%R
146a
by case: x => [r| |] /=; rewrite ?normrN1 ?normr1 // (ltW (contract_lt1 _)). Qed.
11c7

contract 0 = 0%R
1470
by rewrite /contract mul0r. Qed.
146c
contract (- x) = (- contract x)%R
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.
145e
(1 <= r)%R -> expand r = +oo
147b
by move=> r1; rewrite /expand r1. Qed.
145e
expand (- r) = - expand r
1480
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)
145e
~~ (1 <= - r)%R -> (if (- r <= -1)%R then -oo else (- r / (1 - `|- r|))%:E) = - (if (1 <= r)%R then +oo else if (r <= -1)%R then -oo else (r / (1 - `|r|))%:E)
1487
~~ (1 <= r)%R
148a
145e
148c
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.
145e
(r <= -1)%R -> expand r = -oo
149b
by rewrite ler_oppr => /expand1/eqP; rewrite expandN eqe_oppLR => /eqP. Qed.
1472
expand 0 = 0
14a0
by rewrite /expand leNgt ltr01 /= oppr_ge0 leNgt ltr01 /= mul0r. Qed.
1472
{in [pred r | (`|r| <= 1)%R], cancel expand contract}
14a5
145e
`|r|%R == 1%R -> contract (expand r) = r
11c7
ae
r1: (`|r| < 1)%R
contract (expand r) = r
14af
14b1
14af
r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|) = r
14af
(1 + r / (1 - r))%R != 0%R
11c7
ae
14b0
r_pneq0: (1 + r / (1 - r))%R != 0%R
14b8
14af
(1 - r)%R \is a GRing.unit
14af
(1 - r + r) / (1 - r) != 0%R
14be
14af
14c7
14bd
14bf
14b8
14bf
(1 - r / (1 + r))%R != 0%R
11c7
ae
14b0
14c0
r_nneq0: (1 - r / (1 + r))%R != 0%R
14b8
14bf
(1 + r)%R \is a GRing.unit
14bf
(1 + r - r) / (1 + r) != 0%R
14d3
14bf
14dc
14d2
14bf
(-1 < r)%R
14d2
14d4
14b8
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
11c7
ae
14b0
14c0
14d5
wlog_r0: (0 <= r)%R
14b8
11c7
ae
14b0
14c0
14d5
14eb
de5

14b8
14ec
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
14f3
(- (r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|)))%R = (- r)%R -> r / (1 - `|r|) / (1 + `|r / (1 - `|r|)|) = r
14ec
14ee
14b8
14ee
(0 <= r / (1 - r))%R
14ee
r / (1 - r) / (1 + r / (1 - r)) = r
14ee
1505
14ee
(r / (1 - r) / (1 + r / (1 - r)) * (1 + r / (1 - r)))%R = (r * (1 + r / (1 - r)))%R
14ee
r / (1 - r) = (r * (1 + r / (1 - r)))%R
14ee
14c4
by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW. Qed.
1472
{mono contract : x y / x <= y >-> (x <= y)%R}
1515
11c7
11c

r0%:E < r1%:E -> (r0 / (1 + `|r0|) < r1 / (1 + `|r1|))%R
11c7
r0: R
(r0 / (1 + `|r0|) < 1)%R
11c7
r1: R
-oo < r1%:E -> (-1 < r1 / (1 + `|r1|))%R
1472
(-1 < 1)%R
151a
11c7
11c
r0r1: (r0 < r1)%R

(r0 < r1 / (1 + `|r1|) * (1 + `|r0|))%R
151e
152d
(r0 + r0 * `|r1| < r1 + r1 * `|r0|)%R
151e
11c7
11c
152e
_i_: (0 < r1)%R

(r0 + r0 * r1 < r1 + r1 * `|r0|)%R
11c7
11c
152e
r10: (r1 <= 0)%R
(r0 + r0 * - r1 < r1 + r1 * `|r0|)%R
151f15231527
11c7
11c
152e
1538
r00: (r0 <= 0)%R

(r0 * r1 <= - r0 * r1)%R
153a
153c
153e
151e
11c7
11c
152e
153d
r00: (0 < r0)%R

(r0 + r0 * - r1 < r1 + r1 * r0)%R
151e
1520
1522
15231527
154f
1524
1526
1527
1554
1524
(- (1 + `|r1|) < r1)%R
1556
1472
1528
155d
by rewrite -subr_gt0 opprK. Qed. Definition lt_contract := leW_mono le_contract. Definition contract_inj := mono_inj lexx le_anti le_contract.
1472
{in [pred r | (`|r| <= 1)%R] &, {mono expand : x y / (x <= y)%R >-> x <= y}}
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.
145e
(`|r| < 1)%R -> (fine (expand r))%:E = expand r
1566
by move=> r1; rewrite /expand 2!leNgt ltr_oppl; case/ltr_normlP : r1 => -> ->. Qed.
1472
{homo expand : x y / (x <= y)%R >-> x <= y}
156b
11c7
95
xy: (x <= y)%R
x1: (`|x| <= 1)%R

expand x <= expand y
11c7
95
1573
(1 < `|x|)%R -> expand x <= expand y
11c7
95
1573
1574
y_le1: (y <= 1)%R

1575
1576
157d
(-1 <= x)%R
1576
1578
1579
11c7
95
1573
x1: (1 < - x)%R

1575
11c7
95
1573
x1: (1 < x)%R
1575
158d
1575
by rewrite expand1; [rewrite expand1 // (le_trans _ xy) // ltW | exact: ltW]. Qed.
145e
(expand r == +oo) = (1 <= r)%R
1593
by rewrite /expand; case: ifP => //; case: ifP. Qed.
145e
(expand r == -oo) = (r <= -1)%R
1598
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.
11c7
6b
ae

(0 < r)%R -> ereal_ball x r x
15a3
by move=> e0; rewrite /ereal_ball subrr normr0. Qed.
11c7
23
ae

ereal_ball x r y -> ereal_ball y r x
15a9
by rewrite /ereal_ball distrC. Qed.
11c7
1b8
14

ereal_ball x r1 y -> ereal_ball y r2 z -> ereal_ball x (r1 + r2) z
15af
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.
11c7
23
e: {posnum R}

ereal_ball (- x) e%:num (- y) -> ereal_ball x e%:num y
15bc
by rewrite /ereal_ball 2!contractN opprK -opprB normrN addrC. Qed.
11c7
15bf
6b

(2 < e%:num)%R -> ereal_ball -oo e%:num x
15c3
11c7
15bf
6b
e2: (2 < e%:num)%R

(`|contract x + 1| <= 2)%R
15cb
(`|contract x| <= 2 - 1)%R
by rewrite (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1)%R // addrK. Qed.
11c7
ae
15bf

(1 < contract r%:E + e%:num)%R -> ereal_ball r%:E e%:num +oo
15d3
11c7
ae
15bf
re1: (1 < contract r%:E + e%:num)%R

(contract r%:E - 1 <= 0)%R
15db
(- (contract r%:E - 1) < e%:num)%R
15db
15e0
by rewrite opprB ltr_subl_addl. Qed. End ereal_PseudoMetric. (* TODO: generalize to numFieldType? *)
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
15e5
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
11c7
ae
15ef
8ea
15f1
ltxb: r%:E < +oo
exists delta : {posnum R}, forall y : R, (`|y - r| < delta%:num)%R -> a%:E < y%:E < +oo
11c7
ae
15ef
b: R
ltax: -oo < r%:E
15f2
exists delta : {posnum R}, forall y : R, (`|y - r| < delta%:num)%R -> -oo < y%:E < b%:E
11c7
ae
15ef
15fc
15f7
exists delta : {posnum R}, forall y : R, (`|y - r| < delta%:num)%R -> -oo < y%:E < +oo
15ec
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
11c7
ae
wlog: (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) (*1*)
8ea
15f1
15f7
15f8
11c7
ae
1609
15fb
15fc
15f2
15fd
11c7
ae
1609
15fc
15f7
1600
11c7
r, a, b: R
ltxa: a%:E < r%:E
15f2

15f3
1606
1611
(0 < Num.min ((r - a) / 2) ((b - r) / 2))%R
11c7
1612
1613
15f2
m_gt0: (0 < Num.min ((r - a) / 2) ((b - r) / 2))%R
15f3
1607160a160c
161a
15f3
1606
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
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
1627
(r + (b - r) / 2 < b)%R
1627
(a < r - (r - a) / 2)%R
1607160a160c
1627
(0 < (b - r) / 2)%R
162f
1627
1631
1606
1608
15f8
160a160c
163a
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
160b
15fd
160c
1645
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
160d
1600
164f
by exists 1%:pos%R => ? ?; rewrite ltNyr ltry. Qed.