Library mathcomp.analysis.constructive_ereal
(* 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
-------------------------------------------------------------------- *)
--------------------------------------------------------------------
Copyright (c) - 2015--2016 - IMDEA Software Institute
Copyright (c) - 2015--2018 - Inria
Copyright (c) - 2016--2018 - Polytechnique
-------------------------------------------------------------------- *)
TODO: merge this with table.v in real-closed
(c.f. https://github.com/math-comp/real-closed/pull/29 ) and
incorporate it into mathcomp proper where it could then be used for
bounds of intervals
From mathcomp Require Import all_ssreflect all_algebra finmap.
Require Import boolp mathcomp_extra classical_sets functions reals signed.
Require Import topology.
Require Import boolp mathcomp_extra classical_sets functions reals signed.
Require Import topology.
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.
Reserved Notation "x %:E" (at level 2, format "x %:E").
Reserved Notation "x +? y" (at level 50, format "x +? y").
Reserved Notation "x *? y" (at level 50, format "x *? y").
Reserved Notation "'\bar' x" (at level 2, format "'\bar' x").
Reserved Notation "{ 'posnum' '\bar' R }" (at level 0,
format "{ 'posnum' '\bar' R }").
Reserved Notation "{ 'nonneg' '\bar' R }" (at level 0,
format "{ 'nonneg' '\bar' R }").
Declare Scope ereal_dual_scope.
Declare Scope ereal_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Variant extended (R : Type) := EFin of R | EPInf | ENInf.
Arguments EFin {R}.
Lemma EFin_inj T : injective (@EFin T).
Definition dual_extended := extended.
Notations in ereal_dual_scope should be kept *before* the
corresponding notation in ereal_scope, otherwise when none of the
scope is open (lte x y) would be displayed as (x < y)%dE, instead
of (x < y)%E, for instance.
Notation "+oo" := (@EPInf _ : dual_extended _) : ereal_dual_scope.
Notation "+oo" := (@EPInf _) : ereal_scope.
Notation "-oo" := (@ENInf _ : dual_extended _) : ereal_dual_scope.
Notation "-oo" := (@ENInf _) : ereal_scope.
Notation "r %:E" := (@EFin _ r%R).
Notation "'\bar' R" := (extended R) : type_scope.
Notation "0" := (0%R%:E : dual_extended _) : ereal_dual_scope.
Notation "0" := (0%R%:E) : ereal_scope.
Notation "1" := (1%R%:E : dual_extended _) : ereal_dual_scope.
Notation "1" := (1%R%:E) : ereal_scope.
Bind Scope ereal_dual_scope with dual_extended.
Bind Scope ereal_scope with extended.
Delimit Scope ereal_dual_scope with dE.
Delimit Scope ereal_scope with E.
Local Open Scope ereal_scope.
Definition er_map T T' (f : T → T') (x : \bar T) : \bar T' :=
match x with
| r%:E ⇒ (f r)%:E
| +oo ⇒ +oo
| -oo ⇒ -oo
end.
Definition fine {R : zmodType} x : R := if x is EFin v then v else 0.
Section EqEReal.
Variable (R : eqType).
Definition eq_ereal (x y : \bar R) :=
match x, y with
| x%:E, y%:E ⇒ x == y
| +oo, +oo ⇒ true
| -oo, -oo ⇒ true
| _, _ ⇒ false
end.
Lemma ereal_eqP : Equality.axiom eq_ereal.
Definition ereal_eqMixin := Equality.Mixin ereal_eqP.
Canonical ereal_eqType := Equality.Pack ereal_eqMixin.
Lemma eqe (r1 r2 : R) : (r1%:E == r2%:E) = (r1 == r2).
End EqEReal.
Section ERealChoice.
Variable (R : choiceType).
Definition code (x : \bar R) :=
match x with
| r%:E ⇒ GenTree.Node 0 [:: GenTree.Leaf r]
| +oo ⇒ GenTree.Node 1 [::]
| -oo ⇒ GenTree.Node 2 [::]
end.
Definition decode (x : GenTree.tree R) : option (\bar R) :=
match x with
| GenTree.Node 0 [:: GenTree.Leaf r] ⇒ Some r%:E
| GenTree.Node 1 [::] ⇒ Some +oo
| GenTree.Node 2 [::] ⇒ Some -oo
| _ ⇒ None
end.
Lemma codeK : pcancel code decode.
Definition ereal_choiceMixin := PcanChoiceMixin codeK.
Canonical ereal_choiceType := ChoiceType (extended R) ereal_choiceMixin.
End ERealChoice.
Section ERealCount.
Variable (R : countType).
Definition ereal_countMixin := PcanCountMixin (@codeK R).
Canonical ereal_countType := CountType (extended R) ereal_countMixin.
End ERealCount.
Section ERealOrder.
Context {R : numDomainType}.
Implicit Types x y : \bar R.
Definition le_ereal x1 x2 :=
match x1, x2 with
| -oo, r%:E | r%:E, +oo ⇒ r \is Num.real
| r1%:E, r2%:E ⇒ r1 ≤ r2
| -oo, _ | _, +oo ⇒ true
| +oo, _ | _, -oo ⇒ false
end.
Definition lt_ereal x1 x2 :=
match x1, x2 with
| -oo, r%:E | r%:E, +oo ⇒ r \is Num.real
| r1%:E, r2%:E ⇒ r1 < r2
| -oo, -oo | +oo, +oo ⇒ false
| +oo, _ | _ , -oo ⇒ false
| -oo, _ ⇒ true
end.
Lemma lt_def_ereal x y : lt_ereal x y = (y != x) && le_ereal x y.
Lemma le_refl_ereal : reflexive le_ereal.
Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
Lemma le_trans_ereal : ssrbool.transitive le_ereal.
Fact ereal_display : unit.
Definition ereal_porderMixin :=
LePOrderMixin lt_def_ereal le_refl_ereal le_anti_ereal le_trans_ereal.
Canonical ereal_porderType :=
POrderType ereal_display (extended R) ereal_porderMixin.
Lemma leEereal x y : (x ≤ y)%O = le_ereal x y.
Lemma ltEereal x y : (x < y)%O = lt_ereal x y.
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.
Lemma lee_fin (r s : R) : (r%:E ≤ s%:E) = (r ≤ s)%R.
Lemma lte_fin (r s : R) : (r%:E < s%:E) = (r < s)%R.
Lemma lee01 : 0 ≤ 1 :> \bar R.
Lemma lte01 : 0 < 1 :> \bar R.
Lemma leeNy_eq x : (x ≤ -oo) = (x == -oo).
Lemma leye_eq x : (+oo ≤ x) = (x == +oo).
Lemma lt0y : (0 : \bar R) < +oo.
Lemma ltNy0 : -oo < (0 : \bar R).
Lemma le0y : (0 : \bar R) ≤ +oo.
Lemma leNy0 : -oo ≤ (0 : \bar R).
Lemma ereal_comparable x y : (0%E >=< x)%O → (0%E >=< y)%O → (x >=< y)%O.
End ERealOrder_numDomainType.
#[global] Hint Resolve lee01 lte01 : core.
Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma ltey r : r%:E < +oo.
Lemma ltNye r : -oo < r%:E.
Lemma leey x : x ≤ +oo.
Lemma leNye x : -oo ≤ x.
Lemma gee0P x : 0 ≤ x ↔ x = +oo ∨ exists2 r, (r ≥ 0)%R & x = r%:E.
Lemma le_total_ereal : totalPOrderMixin [porderType of \bar R].
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.
Lemma lee0N1 : 0 ≤ (-1)%:E :> \bar R = false.
Lemma lte0N1 : 0 < (-1)%:E :> \bar R = false.
Lemma le0R x : 0 ≤ x → (0 ≤ fine x)%R.
Lemma lt0R x : 0 < x < +oo → (0 < fine x)%R.
Lemma lee_tofin (r0 r1 : R) : (r0 ≤ r1)%R → r0%:E ≤ r1%:E.
Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%R → r0%:E < r1%:E.
Lemma enatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.
Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
Lemma EFin_natmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.
Lemma mule2n x : x *+ 2 = x + x.
Lemma expe2 x : x ^+ 2 = x × x.
End ERealOrderTheory.
Section finNumPred.
Context {R : numDomainType}.
Implicit Type (x : \bar R).
Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
Fact fin_num_key : pred_key fin_num.
Canonical fin_num_keyd := KeyedQualifier fin_num_key.
Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).
Lemma fin_numP x : reflect ((x != -oo) ∧ (x != +oo)) (x \is a fin_num).
Lemma fin_numEn x : (x \isn't a fin_num) = (x == -oo) || (x == +oo).
Lemma fin_numPn x : reflect (x = -oo ∨ x = +oo) (x \isn't a fin_num).
End finNumPred.
Section ERealArithTh_numDomainType.
Context {R : numDomainType}.
Implicit Types (x y z : \bar R) (r : R).
Lemma fine_eq0 x : x \is a fin_num → (fine x == 0%R) = (x == 0).
Lemma EFinN r : (- r)%:E = (- r%:E).
Lemma fineN x : fine (- x) = (- fine x)%R.
Lemma EFinD r r' : (r + r')%:E = r%:E + r'%:E.
Lemma EFinB r r' : (r - r')%:E = r%:E - r'%:E.
Lemma EFinM r r' : (r × r')%:E = r%:E × r'%:E.
Lemma sumEFin I s P (F : I → R) :
\sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.
Definition adde_def x y :=
~~ ((x == +oo) && (y == -oo)) && ~~ ((x == -oo) && (y == +oo)).
Lemma adde_defC x y : x +? y = y +? x.
Lemma adde_defNN x y : - x +? - y = x +? y.
Lemma adde_defEninfty x : (x +? -oo) = (x != +oo).
Lemma ge0_adde_def : {in [pred x | x ≥ 0] &, ∀ x y, x +? y}.
Lemma addeC : commutative (S := \bar R) +%E.
Lemma adde0 : right_id (0 : \bar R) +%E.
Lemma add0e : left_id (0 : \bar R) +%E.
Lemma addeA : associative (S := \bar R) +%E.
Canonical adde_monoid := Monoid.Law addeA add0e adde0.
Canonical adde_comoid := Monoid.ComLaw addeC.
Lemma addeAC : @right_commutative (\bar R) _ +%E.
Lemma addeCA : @left_commutative (\bar R) _ +%E.
Lemma addeACA : @interchange (\bar R) +%E +%E.
Lemma adde_gt0 x y : 0 < x → 0 < y → 0 < x + y.
Lemma padde_eq0 x y : 0 ≤ x → 0 ≤ y → (x + y == 0) = (x == 0) && (y == 0).
Lemma nadde_eq0 x y : x ≤ 0 → y ≤ 0 → (x + y == 0) = (x == 0) && (y == 0).
Lemma realDe x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x + y)%O.
Lemma oppe0 : - 0 = 0 :> \bar R.
Lemma oppeK : involutive (A := \bar R) -%E.
Lemma oppe_eq0 x : (- x == 0)%E = (x == 0)%E.
Lemma oppeD x y : y \is a fin_num → - (x + y) = - x - y.
Lemma sube0 x : x - 0 = x.
Lemma sub0e x : 0 - x = - x.
Lemma muleC x y : x × y = y × x.
Lemma onee_neq0 : 1 != 0 :> \bar R.
Lemma onee_eq0 : 1 == 0 :> \bar R = false.
Lemma mule1 x : x × 1 = x.
Lemma mul1e x : 1 × x = x.
Lemma mule0 x : x × 0 = 0.
Lemma mul0e x : 0 × x = 0.
Canonical mule_mulmonoid := @Monoid.MulLaw _ _ mule mul0e mule0.
Definition mule_def x y :=
~~ (((x == 0) && (`| y | == +oo)) || ((y == 0) && (`| x | == +oo))).
Lemma mule_defC x y : x *? y = y *? x.
Lemma mule_def_fin x y : x \is a fin_num → y \is a fin_num → x *? y.
Lemma mule_def_neq0_infty x y : x != 0 → y \isn't a fin_num → x *? y.
Lemma mule_def_infty_neq0 x y : x \isn't a fin_num → y!= 0 → x *? y.
Lemma neq0_mule_def x y : x × y != 0 → x *? y.
Lemma ltpinfty_adde_def : {in [pred x | x < +oo] &, ∀ x y, x +? y}.
Lemma ltninfty_adde_def : {in [pred x | -oo < x] &, ∀ x y, x +? y}.
Lemma abse_eq0 x : (`|x| == 0) = (x == 0).
Lemma abse0 : `|0| = 0 :> \bar R.
Lemma abse1 : `|1| = 1 :> \bar R.
Lemma abseN x : `|- x| = `|x|.
Lemma eqe_opp x y : (- x == - y) = (x == y).
Lemma eqe_oppP x y : (- x = - y) ↔ (x = y).
Lemma eqe_oppLR x y : (- x == y) = (x == - y).
Lemma eqe_oppLRP x y : (- x = y) ↔ (x = - y).
Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).
Lemma oppeB x y : y \is a fin_num → - (x - y) = - x + y.
Lemma fin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Lemma sum_fin_num (T : Type) (s : seq T) (P : pred T) (f : T → \bar R) :
\sum_(i <- s | P i) f i \is a fin_num =
all [pred x | x \is a fin_num] [seq f i | i <- s & P i].
Lemma sum_fin_numP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
reflect (∀ i, i \in s → P i → f i \is a fin_num)
(\sum_(i <- s | P i) f i \is a fin_num).
Lemma fin_numB x y :
(x - y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Lemma fin_numM x y : x \is a fin_num → y \is a fin_num →
x × y \is a fin_num.
Lemma fineD : {in @fin_num R &, {morph fine : x y / x + y >-> (x + y)%R}}.
Lemma fineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.
Lemma fineM : {in @fin_num R &, {morph fine : x y / x × y >-> (x × y)%R}}.
Lemma fin_num_adde_def x y : y \is a fin_num → x +? y.
Lemma fineK x : x \is a fin_num → (fine x)%:E = x.
Lemma telescope_sume n m (f : nat → \bar R) :
(∀ i, (n ≤ i ≤ m)%N → f i \is a fin_num) → (n ≤ m)%N →
\sum_(n ≤ k < m) (f k.+1 - f k) = f m - f n.
Lemma addeK x y : x \is a fin_num → y + x - x = y.
Lemma subeK x y : y \is a fin_num → x - y + y = x.
Lemma subee x : x \is a fin_num → x - x = 0.
Lemma sube_eq x y z : x \is a fin_num → (y +? z) →
(x - z == y) = (x == y + z).
Lemma adde_eq_ninfty x y : (x + y == -oo) = ((x == -oo) || (y == -oo)).
Lemma addye x : x != -oo → +oo + x = +oo.
Lemma addey x : x != -oo → x + +oo = +oo.
Lemma adde_Neq_pinfty x y : x != -oo → y != -oo →
(x + y != +oo) = (x != +oo) && (y != +oo).
Lemma adde_Neq_ninfty x y : x != +oo → y != +oo →
(x + y != -oo) = (x != -oo) && (y != -oo).
Lemma adde_ss_eq0 x y : (0 ≤ x) && (0 ≤ y) || (x ≤ 0) && (y ≤ 0) →
x + y == 0 = (x == 0) && (y == 0).
Lemma esum_ninftyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
\sum_(i <- s | P i) f i = -oo ↔ ∃ i, [/\ i \in s, P i & f i = -oo].
Lemma esum_ninfty (I : finType) (f : I → \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == -oo) = [∃ i in P, f i == -oo].
Lemma esum_pinftyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
(∀ i, P i → f i != -oo) →
\sum_(i <- s | P i) f i = +oo ↔ ∃ i, [/\ i \in s, P i & f i = +oo].
Lemma esum_pinfty (I : finType) (P : {pred I}) (f : I → \bar R) :
(∀ i, P i → f i != -oo) →
(\sum_(i | P i) f i == +oo) = [∃ i in P, f i == +oo].
Lemma adde_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
Lemma adde_le0 x y : x ≤ 0 → y ≤ 0 → x + y ≤ 0.
Lemma oppe_gt0 x : (0 < - x) = (x < 0).
Lemma oppe_lt0 x : (- x < 0) = (0 < x).
Lemma oppe_ge0 x : (0 ≤ - x) = (x ≤ 0).
Lemma oppe_le0 x : (- x ≤ 0) = (0 ≤ x).
Lemma sume_ge0 T (f : T → \bar R) (P : pred T) :
(∀ t, P t → 0 ≤ f t) → ∀ l, 0 ≤ \sum_(i <- l | P i) f i.
Lemma sume_le0 T (f : T → \bar R) (P : pred T) :
(∀ t, P t → f t ≤ 0) → ∀ l, \sum_(i <- l | P i) f i ≤ 0.
Lemma mulNyy : -oo × +oo = -oo :> \bar R.
Lemma mulyNy : +oo × -oo = -oo :> \bar R.
Lemma mulyy : +oo × +oo = +oo :> \bar R.
Lemma mulNyNy : -oo × -oo = +oo :> \bar R.
Lemma real_mulry r : r \is Num.real → r%:E × +oo = (Num.sg r)%:E × +oo.
Lemma real_mulyr r : r \is Num.real → +oo × r%:E = (Num.sg r)%:E × +oo.
Lemma real_mulrNy r : r \is Num.real → r%:E × -oo = (Num.sg r)%:E × -oo.
Lemma real_mulNyr r : r \is Num.real → -oo × r%:E = (Num.sg r)%:E × -oo.
Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).
Lemma mulN1e x : - 1%E × x = - x.
Lemma muleN1 x : x × - 1%E = - x.
Lemma mule_neq0 x y : x != 0 → y != 0 → x × y != 0.
Lemma mule_eq0 x y : (x × y == 0) = (x == 0) || (y == 0).
Lemma mule_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
Lemma mule_gt0 x y : 0 < x → 0 < y → 0 < x × y.
Lemma mule_le0 x y : x ≤ 0 → y ≤ 0 → 0 ≤ x × y.
Lemma mule_le0_ge0 x y : x ≤ 0 → 0 ≤ y → x × y ≤ 0.
Lemma mule_ge0_le0 x y : 0 ≤ x → y ≤ 0 → x × y ≤ 0.
Lemma mule_lt0_lt0 x y : x < 0 → y < 0 → 0 < x × y.
Lemma mule_gt0_lt0 x y : 0 < x → y < 0 → x × y < 0.
Lemma mule_lt0_gt0 x y : x < 0 → 0 < y → x × y < 0.
Lemma gte_opp x : 0 < x → - x < x.
Lemma realMe x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x × y)%O.
Lemma abse_ge0 x : 0 ≤ `|x|.
Lemma gee0_abs x : 0 ≤ x → `|x| = x.
Lemma gte0_abs x : 0 < x → `|x| = x.
Lemma lee0_abs x : x ≤ 0 → `|x| = - x.
Lemma lte0_abs x : x < 0 → `|x| = - x.
End ERealArithTh_numDomainType.
Notation "x +? y" := (adde_def x%dE y%dE) : ereal_dual_scope.
Notation "x +? y" := (adde_def x y) : ereal_scope.
Notation "x *? y" := (mule_def x%dE y%dE) : ereal_dual_scope.
Notation "x *? y" := (mule_def x y) : ereal_scope.
Notation maxe := (@Order.max ereal_display _).
Notation "@ 'maxe' R" := (@Order.max ereal_display R)
(at level 10, R at level 8, only parsing) : fun_scope.
Notation mine := (@Order.min ereal_display _).
Notation "@ 'mine' R" := (@Order.min ereal_display R)
(at level 10, R at level 8, only parsing) : fun_scope.
Module DualAddTheoryNumDomain.
Section DualERealArithTh_numDomainType.
Local Open Scope ereal_dual_scope.
Context {R : numDomainType}.
Implicit Types x y z : \bar R.
Lemma dual_addeE x y : (x + y)%dE = - ((- x) + (- y))%E.
Lemma dual_sumeE I (r : seq I) (P : pred I) (F : I → \bar R) :
(\sum_(i <- r | P i) F i)%dE = - (\sum_(i <- r | P i) (- F i)%E)%E.
Lemma dual_addeE_def x y : x +? y → (x + y)%dE = (x + y)%E.
Lemma dEFinD (r r' : R) : (r + r')%R%:E = r%:E + r'%:E.
Lemma dEFinB (r r' : R) : (r - r')%R%:E = r%:E - r'%:E.
Lemma dsumEFin I r P (F : I → R) :
\sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%R%:E.
Lemma daddeC : commutative (S := \bar R) +%dE.
Lemma dadde0 : right_id (0 : \bar R) +%dE.
Lemma dadd0e : left_id (0 : \bar R) +%dE.
Lemma daddeA : associative (S := \bar R) +%dE.
Canonical dadde_monoid := Monoid.Law daddeA dadd0e dadde0.
Canonical dadde_comoid := Monoid.ComLaw daddeC.
Lemma daddeAC : right_commutative (S := \bar R) +%dE.
Lemma daddeCA : left_commutative (S := \bar R) +%dE.
Lemma daddeACA : @interchange (\bar R) +%dE +%dE.
Lemma realDed x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x + y)%O.
Lemma doppeD x y : y \is a fin_num → - (x + y) = - x - y.
Lemma dsube0 x : x - 0 = x.
Lemma dsub0e x : 0 - x = - x.
Lemma doppeB x y : y \is a fin_num → - (x - y) = - x + y.
Lemma dfin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Lemma dfineD :
{in (@fin_num R) &, {morph fine : x y / x + y >-> (x + y)%R}}.
Lemma dfineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.
Lemma daddeK x y : x \is a fin_num → y + x - x = y.
Lemma dsubeK x y : y \is a fin_num → x - y + y = x.
Lemma dsubee x : x \is a fin_num → x - x = 0.
Lemma dsube_eq x y z : x \is a fin_num → (y +? z) →
(x - z == y) = (x == y + z).
Lemma dadde_eq_pinfty x y : (x + y == +oo) = ((x == +oo) || (y == +oo)).
Lemma daddooe x : x != -oo → +oo + x = +oo.
Lemma daddeoo x : x != -oo → x + +oo = +oo.
Lemma dadde_Neq_pinfty x y : x != -oo → y != -oo →
(x + y != +oo) = (x != +oo) && (y != +oo).
Lemma dadde_Neq_ninfty x y : x != +oo → y != +oo →
(x + y != -oo) = (x != -oo) && (y != -oo).
Lemma ndadde_eq0 x y : x ≤ 0 → y ≤ 0 → x + y == 0 = (x == 0) && (y == 0).
Lemma pdadde_eq0 x y : 0 ≤ x → 0 ≤ y → x + y == 0 = (x == 0) && (y == 0).
Lemma dadde_ss_eq0 x y : (0 ≤ x) && (0 ≤ y) || (x ≤ 0) && (y ≤ 0) →
x + y == 0 = (x == 0) && (y == 0).
Lemma desum_pinftyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
\sum_(i <- s | P i) f i = +oo ↔ ∃ i, [/\ i \in s, P i & f i = +oo].
Lemma desum_pinfty (I : finType) (f : I → \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == +oo) = [∃ i in P, f i == +oo].
Lemma desum_ninftyP
(T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
(∀ i, P i → f i != +oo) →
\sum_(i <- s | P i) f i = -oo ↔ ∃ i, [/\ i \in s, P i & f i = -oo].
Lemma desum_ninfty (I : finType) (f : I → \bar R) (P : {pred I}) :
(∀ i, f i != +oo) →
(\sum_(i | P i) f i == -oo) = [∃ i in P, f i == -oo].
Lemma dadde_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
Lemma dadde_le0 x y : x ≤ 0 → y ≤ 0 → x + y ≤ 0.
Lemma dsume_ge0 T (f : T → \bar R) (P : pred T) :
(∀ n, P n → 0 ≤ f n) → ∀ l, 0 ≤ \sum_(i <- l | P i) f i.
Lemma dsume_le0 T (f : T → \bar R) (P : pred T) :
(∀ n, P n → f n ≤ 0) → ∀ l, \sum_(i <- l | P i) f i ≤ 0.
Lemma gte_dopp (r : \bar R) : (0 < r)%E → (- r < r)%E.
Lemma ednatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.
Lemma ednatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
Lemma EFin_dnatmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.
Lemma ednatmulE x n : x *+ n = (x *+ n)%E.
Lemma dmule2n x : x *+ 2 = x + x.
End DualERealArithTh_numDomainType.
End DualAddTheoryNumDomain.
Section ERealArithTh_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y z u a b : \bar R) (r : R).
Lemma fin_numElt x : (x \is a fin_num) = (-oo < x < +oo).
Lemma fin_numPlt x : reflect (-oo < x < +oo) (x \is a fin_num).
Lemma lte_pinfty_eq x : (x < +oo) = (x \is a fin_num) || (x == -oo).
Lemma ge0_fin_numE x : 0 ≤ x → (x \is a fin_num) = (x < +oo).
Lemma eq_pinftyP x : x = +oo ↔ (∀ A, (0 < A)%R → A%:E ≤ x).
Lemma seq_psume_eq0 (I : choiceType) (r : seq I)
(P : pred I) (F : I → \bar R) : (∀ i, P i → 0 ≤ F i)%E →
(\sum_(i <- r | P i) F i == 0)%E = all (fun i ⇒ P i ==> (F i == 0%E)) r.
Lemma lte_add_pinfty x y : x < +oo → y < +oo → x + y < +oo.
Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I → \bar R) :
(∀ i, P i → f i < +oo) → \sum_(i <- s | P i) f i < +oo.
Lemma sube_gt0 x y : (0 < y - x) = (x < y).
Lemma sube_le0 x y : (y - x ≤ 0) = (y ≤ x).
Lemma suber_ge0 y x : y \is a fin_num → (0 ≤ x - y) = (y ≤ x).
Lemma subre_ge0 x y : y \is a fin_num → (0 ≤ y - x) = (x ≤ y).
Lemma lte_oppl x y : (- x < y) = (- y < x).
Lemma lte_oppr x y : (x < - y) = (y < - x).
Lemma lee_oppr x y : (x ≤ - y) = (y ≤ - x).
Lemma lee_oppl x y : (- x ≤ y) = (- y ≤ x).
Lemma muleN x y : x × - y = - (x × y).
Lemma mulNe x y : - x × y = - (x × y).
Lemma muleNN x y : - x × - y = x × y.
Lemma mulry r : r%:E × +oo%E = (Num.sg r)%:E × +oo%E.
Lemma mulyr r : +oo%E × r%:E = (Num.sg r)%:E × +oo%E.
Lemma mulrNy r : r%:E × -oo%E = (Num.sg r)%:E × -oo%E.
Lemma mulNyr r : -oo%E × r%:E = (Num.sg r)%:E × -oo%E.
Definition mulr_infty := (mulry, mulyr, mulrNy, mulNyr).
Lemma lte_mul_pinfty x y : 0 ≤ x → x \is a fin_num → y < +oo → x × y < +oo.
Lemma mule_ge0_gt0 x y : 0 ≤ x → 0 ≤ y → (0 < x × y) = (0 < x) && (0 < y).
Lemma gt0_mulye x : (0 < x → +oo × x = +oo)%E.
Lemma lt0_mulye x : (x < 0 → +oo × x = -oo)%E.
Lemma gt0_mulNye x : (0 < x → -oo × x = -oo)%E.
Lemma lt0_mulNye x : (x < 0 → -oo × x = +oo)%E.
Lemma mule_eq_pinfty x y : (x × y == +oo) =
[|| (x > 0) && (y == +oo), (x < 0) && (y == -oo),
(x == +oo) && (y > 0) | (x == -oo) && (y < 0)].
Lemma mule_eq_ninfty x y : (x × y == -oo) =
[|| (x > 0) && (y == -oo), (x < 0) && (y == +oo),
(x == -oo) && (y > 0) | (x == +oo) && (y < 0)].
Lemma lte_opp x y : (- x < - y) = (y < x).
Lemma lte_add a b x y : a < b → x < y → a + x < b + y.
Lemma lee_addl x y : 0 ≤ y → x ≤ x + y.
Lemma lee_addr x y : 0 ≤ y → x ≤ y + x.
Lemma gee_addl x y : y ≤ 0 → x + y ≤ x.
Lemma gee_addr x y : y ≤ 0 → y + x ≤ x.
Lemma lte_addl y x : y \is a fin_num → 0 < x → y < y + x.
Lemma lte_addr y x : y \is a fin_num → 0 < x → y < x + y.
Lemma gte_subl y x : y \is a fin_num → 0 < x → y - x < y.
Lemma gte_subr y x : y \is a fin_num → 0 < x → - x + y < y.
Lemma lte_add2lE x a b : x \is a fin_num → (x + a < x + b) = (a < b).
Lemma lee_add2l x a b : a ≤ b → x + a ≤ x + b.
Lemma lee_add2lE x a b : x \is a fin_num → (x + a ≤ x + b) = (a ≤ b).
Lemma lee_add2r x a b : a ≤ b → a + x ≤ b + x.
Lemma lee_add a b x y : a ≤ b → x ≤ y → a + x ≤ b + y.
Lemma lte_le_add a b x y : b \is a fin_num → a < x → b ≤ y → a + b < x + y.
Lemma lee_lt_add a b x y : a \is a fin_num → a ≤ x → b < y → a + b < x + y.
Lemma lee_sub x y z u : x ≤ y → u ≤ z → x - z ≤ y - u.
Lemma lte_le_sub z u x y : u \is a fin_num →
x < z → u ≤ y → x - y < z - u.
Lemma lte_pmul2r z : z \is a fin_num → 0 < z → {mono *%E^~ z : x y / x < y}.
Lemma lte_pmul2l z : z \is a fin_num → 0 < z → {mono *%E z : x y / x < y}.
Lemma lte_nmul2l z : z \is a fin_num → z < 0 → {mono *%E z : x y /~ x < y}.
Lemma lte_nmul2r z : z \is a fin_num → z < 0 → {mono *%E^~ z : x y /~ x < y}.
Lemma lee_sum I (f g : I → \bar R) s (P : pred I) :
(∀ i, P i → f i ≤ g i) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i) g i.
Lemma lee_sum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, 0 ≤ f i} →
\sum_(i <- s | Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_sum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, f i ≤ 0} →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | Q i) f i.
Lemma lee_sum_nneg (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → 0 ≤ f i) →
\sum_(i <- s | P i && Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_sum_npos (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → f i ≤ 0) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i && Q i) f i.
Lemma lee_sum_nneg_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → 0 ≤ f n) →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_sum_npos_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → f n ≤ 0)%E →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_sum_nneg_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → 0 ≤ f n) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_sum_npos_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → f n ≤ 0) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_sum_nneg_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → 0 ≤ f m) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_sum_npos_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → f m ≤ 0) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_sum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → 0 ≤ f t} →
\sum_(t <- A | P t) f t ≤ \sum_(t <- B | P t) f t.
Lemma lee_sum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → f t ≤ 0} →
\sum_(t <- B | P t) f t ≤ \sum_(t <- A | P t) f t.
Lemma lte_subl_addr x y z : y \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_subl_addl x y z : y \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_subr_addr x y z : z \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_subr_addl x y z : z \is a fin_num → (x < y - z) = (z + x < y).
Lemma lte_subel_addr x y z : x \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_subel_addl x y z : x \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_suber_addr x y z : x \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_suber_addl x y z : x \is a fin_num → (x < y - z) = (z + x < y).
Lemma lee_subl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_subl_addl x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_subr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_subr_addl x y z : z \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma lee_subel_addr x y z : z \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_subel_addl x y z : z \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_suber_addr x y z : y \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_suber_addl x y z : y \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma pmule_rge0 x y : 0 < x → (x × y ≥ 0) = (y ≥ 0).
Lemma pmule_lge0 x y : 0 < x → (y × x ≥ 0) = (y ≥ 0).
Lemma pmule_rlt0 x y : 0 < x → (x × y < 0) = (y < 0).
Lemma pmule_llt0 x y : 0 < x → (y × x < 0) = (y < 0).
Lemma pmule_rle0 x y : 0 < x → (x × y ≤ 0) = (y ≤ 0).
Lemma pmule_lle0 x y : 0 < x → (y × x ≤ 0) = (y ≤ 0).
Lemma pmule_rgt0 x y : 0 < x → (x × y > 0) = (y > 0).
Lemma pmule_lgt0 x y : 0 < x → (y × x > 0) = (y > 0).
Lemma nmule_rge0 x y : x < 0 → (x × y ≥ 0) = (y ≤ 0).
Lemma nmule_lge0 x y : x < 0 → (y × x ≥ 0) = (y ≤ 0).
Lemma nmule_rle0 x y : x < 0 → (x × y ≤ 0) = (y ≥ 0).
Lemma nmule_lle0 x y : x < 0 → (y × x ≤ 0) = (y ≥ 0).
Lemma nmule_rgt0 x y : x < 0 → (x × y > 0) = (y < 0).
Lemma nmule_lgt0 x y : x < 0 → (y × x > 0) = (y < 0).
Lemma nmule_rlt0 x y : x < 0 → (x × y < 0) = (y > 0).
Lemma nmule_llt0 x y : x < 0 → (y × x < 0) = (y > 0).
Lemma mule_lt0 x y : (x × y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)].
Lemma muleA : associative ( *%E : \bar R → \bar R → \bar R ).
Local Open Scope ereal_scope.
Canonical mule_monoid := Monoid.Law muleA mul1e mule1.
Canonical mule_comoid := Monoid.ComLaw muleC.
Lemma muleCA : left_commutative ( *%E : \bar R → \bar R → \bar R ).
Lemma muleAC : right_commutative ( *%E : \bar R → \bar R → \bar R ).
Lemma muleACA : interchange (@mule R) (@mule R).
Lemma muleDr x y z : x \is a fin_num → y +? z → x × (y + z) = x × y + x × z.
Lemma muleDl x y z : x \is a fin_num → y +? z → (y + z) × x = y × x + z × x.
Lemma muleBr x y z : x \is a fin_num → y +? - z → x × (y - z) = x × y - x × z.
Lemma muleBl x y z : x \is a fin_num → y +? - z → (y - z) × x = y × x - z × x.
Lemma ge0_muleDl x y z : 0 ≤ y → 0 ≤ z → (y + z) × x = y × x + z × x.
Lemma ge0_muleDr x y z : 0 ≤ y → 0 ≤ z → x × (y + z) = x × y + x × z.
Lemma le0_muleDl x y z : y ≤ 0 → z ≤ 0 → (y + z) × x = y × x + z × x.
Lemma le0_muleDr x y z : y ≤ 0 → z ≤ 0 → x × (y + z) = x × y + x × z.
Lemma gee_pmull y x : y \is a fin_num → 0 < x → y ≤ 1 → y × x ≤ x.
Lemma lee_wpmul2r x : 0 ≤ x → {homo *%E^~ x : y z / y ≤ z}.
Lemma lee_wpmul2l x : 0 ≤ x → {homo *%E x : y z / y ≤ z}.
Lemma ge0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma ge0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma le0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma le0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma eq_infty x : (∀ r, r%:E ≤ x) → x = +oo.
Lemma eq_ninfty x : (∀ r, x ≤ r%:E) → x = -oo.
Lemma lee_opp x y : (- x ≤ - y) = (y ≤ x).
Lemma lee_abs x : x ≤ `|x|.
Lemma abse_id x : `| `|x| | = `|x|.
Lemma lte_absl (x y : \bar R) : (`|x| < y)%E = (- y < x < y)%E.
Lemma fin_num_abs x : (x \is a fin_num) = (`| x | < +oo)%E.
Lemma eqe_absl x y : (`|x| == y) = ((x == y) || (x == - y)) && (0 ≤ y).
Lemma lee_abs_add x y : `|x + y| ≤ `|x| + `|y|.
Lemma lee_abs_sum (I : Type) (s : seq I) (F : I → \bar R) (P : pred I) :
`|\sum_(i <- s | P i) F i| ≤ \sum_(i <- s | P i) `|F i|.
Lemma lee_abs_sub x y : `|x - y| ≤ `|x| + `|y|.
Lemma abseM : {morph @abse R : x y / x × y}.
Lemma maxEFin r1 r2 : maxe r1%:E r2%:E = (Num.max r1 r2)%:E.
Lemma minEFin r1 r2 : mine r1%:E r2%:E = (Num.min r1 r2)%:E.
Lemma adde_maxl : left_distributive (@adde R) maxe.
Lemma adde_maxr : right_distributive (@adde R) maxe.
Lemma maxye : left_zero (+oo : \bar R) maxe.
Lemma maxey : right_zero (+oo : \bar R) maxe.
Lemma maxNye : left_id (-oo : \bar R) maxe.
Lemma maxeNy : right_id (-oo : \bar R) maxe.
Lemma minNye : left_zero (-oo : \bar R) mine.
Lemma mineNy : right_zero (-oo : \bar R) mine.
Lemma minye : left_id (+oo : \bar R) mine.
Lemma miney : right_id (+oo : \bar R) mine.
Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.
Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.
Lemma maxeMr z x y : z \is a fin_num → 0 < z →
z × maxe x y = maxe (z × x) (z × y).
Lemma maxeMl z x y : z \is a fin_num → 0 < z →
maxe x y × z = maxe (x × z) (y × z).
Lemma mineMr z x y : z \is a fin_num → 0 < z →
z × mine x y = mine (z × x) (z × y).
Lemma mineMl z x y : z \is a fin_num → 0 < z →
mine x y × z = mine (x × z) (y × z).
Lemma lee_pemull x y : 0 ≤ y → 1 ≤ x → y ≤ x × y.
Lemma lee_nemull x y : y ≤ 0 → 1 ≤ x → x × y ≤ y.
Lemma lee_pemulr x y : 0 ≤ y → 1 ≤ x → y ≤ y × x.
Lemma lee_nemulr x y : y ≤ 0 → 1 ≤ x → y × x ≤ y.
Lemma mule_natl x n : n%:R%:E × x = x *+ n.
Lemma lte_pmul x1 y1 x2 y2 :
0 ≤ x1 → 0 ≤ x2 → x1 < y1 → x2 < y2 → x1 × x2 < y1 × y2.
Lemma lee_pmul x1 y1 x2 y2 : 0 ≤ x1 → 0 ≤ x2 → x1 ≤ y1 → x2 ≤ y2 →
x1 × x2 ≤ y1 × y2.
Lemma lee_pmul2l x : x \is a fin_num → 0 < x → {mono *%E x : x y / x ≤ y}.
Lemma lee_pmul2r x : x \is a fin_num → 0 < x → {mono *%E^~ x : x y / x ≤ y}.
End ERealArithTh_realDomainType.
Arguments lee_sum_nneg_ord {R}.
Arguments lee_sum_npos_ord {R}.
Arguments lee_sum_nneg_natr {R}.
Arguments lee_sum_npos_natr {R}.
Arguments lee_sum_nneg_natl {R}.
Arguments lee_sum_npos_natl {R}.
#[global] Hint Extern 0 (is_true (0 ≤ `| _ |)%E) ⇒ solve [apply: abse_ge0] : core.
Module DualAddTheoryRealDomain.
Section DualERealArithTh_realDomainType.
Import DualAddTheoryNumDomain.
Local Open Scope ereal_dual_scope.
Context {R : realDomainType}.
Implicit Types x y z a b : \bar R.
Lemma dsube_lt0 x y : (x - y < 0) = (x < y).
Lemma dsube_ge0 x y : (0 ≤ y - x) = (x ≤ y).
Lemma dsuber_le0 x y : y \is a fin_num → (x - y ≤ 0) = (x ≤ y).
Lemma dsubre_le0 y x : y \is a fin_num → (y - x ≤ 0) = (y ≤ x).
Lemma lte_dadd a b x y : a < b → x < y → a + x < b + y.
Lemma lee_daddl x y : 0 ≤ y → x ≤ x + y.
Lemma lee_daddr x y : 0 ≤ y → x ≤ y + x.
Lemma gee_daddl x y : y ≤ 0 → x + y ≤ x.
Lemma gee_daddr x y : y ≤ 0 → y + x ≤ x.
Lemma lte_daddl y x : y \is a fin_num → 0 < x → y < y + x.
Lemma lte_daddr y x : y \is a fin_num → 0 < x → y < x + y.
Lemma gte_dsubl y x : y \is a fin_num → 0 < x → y - x < y.
Lemma gte_dsubr y x : y \is a fin_num → 0 < x → - x + y < y.
Lemma lte_dadd2lE x a b : x \is a fin_num → (x + a < x + b) = (a < b).
Lemma lee_dadd2l x a b : a ≤ b → x + a ≤ x + b.
Lemma lee_dadd2lE x a b : x \is a fin_num → (x + a ≤ x + b) = (a ≤ b).
Lemma lee_dadd2r x a b : a ≤ b → a + x ≤ b + x.
Lemma lee_dadd a b x y : a ≤ b → x ≤ y → a + x ≤ b + y.
Lemma lte_le_dadd a b x y : b \is a fin_num → a < x → b ≤ y → a + b < x + y.
Lemma lee_lt_dadd a b x y : a \is a fin_num → a ≤ x → b < y → a + b < x + y.
Lemma lee_dsub x y z t : x ≤ y → t ≤ z → x - z ≤ y - t.
Lemma lte_le_dsub z u x y : u \is a fin_num → x < z → u ≤ y → x - y < z - u.
Lemma lee_dsum I (f g : I → \bar R) s (P : pred I) :
(∀ i, P i → f i ≤ g i) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i) g i.
Lemma lee_dsum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, 0 ≤ f i} →
\sum_(i <- s | Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_dsum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, f i ≤ 0} →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | Q i) f i.
Lemma lee_dsum_nneg (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → 0 ≤ f i) →
\sum_(i <- s | P i && Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_dsum_npos (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → f i ≤ 0) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i && Q i) f i.
Lemma lee_dsum_nneg_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → 0 ≤ f n)%E →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_dsum_npos_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → f n ≤ 0)%E →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_dsum_nneg_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → 0 ≤ f n) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_dsum_npos_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → f n ≤ 0) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_dsum_nneg_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → 0 ≤ f m) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_dsum_npos_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → f m ≤ 0) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_dsum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → 0 ≤ f t} →
\sum_(t <- A | P t) f t ≤ \sum_(t <- B | P t) f t.
Lemma lee_dsum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → f t ≤ 0} →
\sum_(t <- B | P t) f t ≤ \sum_(t <- A | P t) f t.
Lemma lte_dsubl_addr x y z : y \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_dsubl_addl x y z : y \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_dsubr_addr x y z : z \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_dsubr_addl x y z : z \is a fin_num → (x < y - z) = (z + x < y).
Lemma lte_dsuber_addr x y z : y \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_dsuber_addl x y z : y \is a fin_num → (x < y - z) = (z + x < y).
Lemma lte_dsubel_addr x y z : z \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_dsubel_addl x y z : z \is a fin_num → (x - y < z) = (x < y + z).
Lemma lee_dsubl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_dsubl_addl x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_dsubr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_dsubr_addl x y z : z \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma lee_dsubel_addr x y z : x \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_dsubel_addl x y z : x \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_dsuber_addr x y z : x \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_dsuber_addl x y z : x \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma dmuleDr x y z : x \is a fin_num → y +? z → x × (y + z) = x × y + x × z.
Lemma dmuleDl x y z : x \is a fin_num → y +? z → (y + z) × x = y × x + z × x.
Lemma dge0_muleDl x y z : 0 ≤ y → 0 ≤ z → (y + z) × x = y × x + z × x.
Lemma dge0_muleDr x y z : 0 ≤ y → 0 ≤ z → x × (y + z) = x × y + x × z.
Lemma dle0_muleDl x y z : y ≤ 0 → z ≤ 0 → (y + z) × x = y × x + z × x.
Lemma dle0_muleDr x y z : y ≤ 0 → z ≤ 0 → x × (y + z) = x × y + x × z.
Lemma ge0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma ge0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma le0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma le0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma lee_abs_dadd x y : `|x + y| ≤ `|x| + `|y|.
Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I → \bar R) (P : pred I) :
`|\sum_(i <- s | P i) F i| ≤ \sum_(i <- s | P i) `|F i|.
Lemma lee_abs_dsub x y : `|x - y| ≤ `|x| + `|y|.
Lemma dadde_minl : left_distributive (@dual_adde R) mine.
Lemma dadde_minr : right_distributive (@dual_adde R) mine.
Lemma dmule_natl x n : n%:R%:E × x = x *+ n.
End DualERealArithTh_realDomainType.
Arguments lee_dsum_nneg_ord {R}.
Arguments lee_dsum_npos_ord {R}.
Arguments lee_dsum_nneg_natr {R}.
Arguments lee_dsum_npos_natr {R}.
Arguments lee_dsum_nneg_natl {R}.
Arguments lee_dsum_npos_natl {R}.
End DualAddTheoryRealDomain.
Lemma lee_opp2 {R : realDomainType} : {mono @oppe R : x y /~ x ≤ y}.
Lemma lte_opp2 {R : realDomainType} : {mono @oppe R : x y /~ x < y}.
Section realFieldType_lemmas.
Variable R : realFieldType.
Implicit Types x y : \bar R.
Implicit Types r : R.
Lemma lee_adde x y : (∀ e : {posnum R}, x ≤ y + e%:num%:E) → x ≤ y.
Lemma lee_paddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.
Lemma lte_paddl y x z : 0 ≤ x → y < z → y < x + z.
Lemma lee_paddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.
Lemma lte_paddr y x z : 0 ≤ x → y < z → y < z + x.
Lemma lte_spaddr z x y : z \is a fin_num → 0 < y → z ≤ x → z < x + y.
Lemma lee_mul01Pr x y : 0 ≤ x →
reflect (∀ r, (0 < r < 1)%R → r%:E × x ≤ y) (x ≤ y).
Lemma lte_pdivr_mull r x y : (0 < r)%R → (r^-1%:E × y < x) = (y < r%:E × x).
Lemma lte_pdivr_mulr r x y : (0 < r)%R → (y × r^-1%:E < x) = (y < x × r%:E).
Lemma lte_pdivl_mull r y x : (0 < r)%R → (x < r^-1%:E × y) = (r%:E × x < y).
Lemma lte_pdivl_mulr r x y : (0 < r)%R → (x < y × r^-1%:E) = (x × r%:E < y).
Lemma lte_ndivl_mulr r x y : (r < 0)%R → (x < y × r^-1%:E) = (y < x × r%:E).
Lemma lte_ndivl_mull r x y : (r < 0)%R → (x < r^-1%:E × y) = (y < r%:E × x).
Lemma lte_ndivr_mull r x y : (r < 0)%R → (r^-1%:E × y < x) = (r%:E × x < y).
Lemma lte_ndivr_mulr r x y : (r < 0)%R → (y × r^-1%:E < x) = (x × r%:E < y).
Lemma lee_pdivr_mull r x y : (0 < r)%R → (r^-1%:E × y ≤ x) = (y ≤ r%:E × x).
Lemma lee_pdivr_mulr r x y : (0 < r)%R → (y × r^-1%:E ≤ x) = (y ≤ x × r%:E).
Lemma lee_pdivl_mull r y x : (0 < r)%R → (x ≤ r^-1%:E × y) = (r%:E × x ≤ y).
Lemma lee_pdivl_mulr r x y : (0 < r)%R → (x ≤ y × r^-1%:E) = (x × r%:E ≤ y).
Lemma lee_ndivl_mulr r x y : (r < 0)%R → (x ≤ y × r^-1%:E) = (y ≤ x × r%:E).
Lemma lee_ndivl_mull r x y : (r < 0)%R → (x ≤ r^-1%:E × y) = (y ≤ r%:E × x).
Lemma lee_ndivr_mull r x y : (r < 0)%R → (r^-1%:E × y ≤ x) = (r%:E × x ≤ y).
Lemma lee_ndivr_mulr r x y : (r < 0)%R → (y × r^-1%:E ≤ x) = (x × r%:E ≤ y).
End realFieldType_lemmas.
Module DualAddTheoryRealField.
Import DualAddTheoryNumDomain DualAddTheoryRealDomain.
Section DualRealFieldType_lemmas.
Local Open Scope ereal_dual_scope.
Variable R : realFieldType.
Implicit Types x y : \bar R.
Lemma lee_dadde x y : (∀ e : {posnum R}, x ≤ y + e%:num%:E) → x ≤ y.
Lemma lee_pdaddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.
Lemma lte_pdaddl y x z : 0 ≤ x → y < z → y < x + z.
Lemma lee_pdaddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.
Lemma lte_pdaddr y x z : 0 ≤ x → y < z → y < z + x.
Lemma lte_spdaddr (r : R) x y : 0 < y → r%:E ≤ x → r%:E < x + y.
End DualRealFieldType_lemmas.
End DualAddTheoryRealField.
Module DualAddTheory.
Export DualAddTheoryNumDomain.
Export DualAddTheoryRealDomain.
Export DualAddTheoryRealField.
End DualAddTheory.
Definition posnume (R : numDomainType) of phant R := {> 0 : \bar R}.
Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
Definition nonnege (R : numDomainType) of phant R := {>= 0 : \bar R}.
Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
: ereal_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
: ereal_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_dual_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_dual_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_scope.
#[global] Hint Extern 0 (is_true (0%E < _)%O) ⇒ solve [apply: gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%E)%O) ⇒ solve [apply: lt0] : core.
#[global] Hint Extern 0 (is_true (0%E ≤ _)%O) ⇒ solve [apply: ge0] : core.
#[global] Hint Extern 0 (is_true (_ ≤ 0%E)%O) ⇒ solve [apply: le0] : core.
#[global] Hint Extern 0 (is_true (0%E >=< _)%O) ⇒ solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (_ != 0%E)%O) ⇒ solve [apply: neq0] : core.
Section SignedNumDomainStability.
Context {R : numDomainType}.
Lemma pinfty_snum_subproof : Signed.spec 0 !=0 >=0 (+oo : \bar R).
Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof).
Lemma ninfty_snum_subproof : Signed.spec 0 !=0 <=0 (-oo : \bar R).
Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof).
Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) :
Signed.spec 0 nz cond x%:num%:E.
Canonical EFin_snum nz cond (x : {num R & nz & cond}) :=
Signed.mk (EFin_snum_subproof x).
Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :
Signed.spec 0%R ?=0 xr (fine x%:num).
Canonical fine_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (fine_snum_subproof x).
Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := opp_reality_subdef xnz xr) :
Signed.spec 0 xnz r (- x%:num).
Canonical oppe_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (oppe_snum_subproof x).
Lemma adde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num + y%:num).
Canonical adde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (adde_snum_subproof x y).
Import DualAddTheory.
Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num + y%:num)%dE.
Canonical dadde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (dadde_snum_subproof x y).
Lemma mule_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := mul_nonzero_subdef xnz ynz xr yr)
(rrl := mul_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num × y%:num).
Canonical mule_snum (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (mule_snum_subproof x y).
Definition abse_reality_subdef (xnz : KnownSign.nullity)
(xr : KnownSign.reality) := (if xr is =0 then =0 else >=0)%snum_sign.
Arguments abse_reality_subdef /.
Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) :
Signed.spec 0 xnz r `|x%:num|.
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}.
Implicit Types (a : \bar R).
Lemma num_abse_eq0 a : (`|a|%:nng == 0%:nng) = (a == 0).
End MorphNum.
Section MorphReal.
Context {R : numDomainType} {nz : KnownSign.nullity} {r : KnownSign.real}.
Implicit Type x y : nR.
Lemma num_lee_maxr a x y :
a ≤ maxe x%:num y%:num = (a ≤ x%:num) || (a ≤ y%:num).
Lemma num_lee_maxl a x y :
maxe x%:num y%:num ≤ a = (x%:num ≤ a) && (y%:num ≤ a).
Lemma num_lee_minr a x y :
a ≤ mine x%:num y%:num = (a ≤ x%:num) && (a ≤ y%:num).
Lemma num_lee_minl a x y :
mine x%:num y%:num ≤ a = (x%:num ≤ a) || (y%:num ≤ a).
Lemma num_lte_maxr a x y :
a < maxe x%:num y%:num = (a < x%:num) || (a < y%:num).
Lemma num_lte_maxl a x y :
maxe x%:num y%:num < a = (x%:num < a) && (y%:num < a).
Lemma num_lte_minr a x y :
a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).
Lemma num_lte_minl a x y :
mine x%:num y%:num < a = (x%:num < a) || (y%:num < a).
End MorphReal.
Section MorphGe0.
Context {R : numDomainType} {nz : KnownSign.nullity}.
Implicit Type x y : nR.
Lemma num_abse_le a x : 0 ≤ a → (`|a|%:nng ≤ x)%O = (a ≤ x%:num).
Lemma num_abse_lt a x : 0 ≤ a → (`|a|%:nng < x)%O = (a < x%:num).
End MorphGe0.
Variant posnume_spec (R : numDomainType) (x : \bar R) :
\bar R → bool → bool → bool → Type :=
| IsPinftyPosnume :
posnume_spec x +oo false true true
| IsRealPosnume (p : {posnum R}) :
posnume_spec x (p%:num%:E) false true true.
Lemma posnumeP (R : numDomainType) (x : \bar R) : 0 < x →
posnume_spec x x (x == 0) (0 ≤ x) (0 < x).
Variant nonnege_spec (R : numDomainType) (x : \bar R) :
\bar R → bool → Type :=
| IsPinftyNonnege : nonnege_spec x +oo true
| IsRealNonnege (p : {nonneg R}) : nonnege_spec x (p%:num%:E) true.
Lemma nonnegeP (R : numDomainType) (x : \bar R) : 0 ≤ x →
nonnege_spec x x (0 ≤ x).
Section contract_expand.
Variable R : realFieldType.
Implicit Types (x : \bar R) (r : R).
Local Open Scope ereal_scope.
Definition contract x : R :=
match x with
| r%:E ⇒ r / (1 + `|r|) | +oo ⇒ 1 | -oo ⇒ -1
end.
Lemma contract_lt1 r : (`|contract r%:E| < 1)%R.
Lemma contract_le1 x : (`|contract x| ≤ 1)%R.
Lemma contract0 : contract 0 = 0%R.
Lemma contractN x : contract (- x) = (- contract x)%R.
Notation "+oo" := (@EPInf _) : ereal_scope.
Notation "-oo" := (@ENInf _ : dual_extended _) : ereal_dual_scope.
Notation "-oo" := (@ENInf _) : ereal_scope.
Notation "r %:E" := (@EFin _ r%R).
Notation "'\bar' R" := (extended R) : type_scope.
Notation "0" := (0%R%:E : dual_extended _) : ereal_dual_scope.
Notation "0" := (0%R%:E) : ereal_scope.
Notation "1" := (1%R%:E : dual_extended _) : ereal_dual_scope.
Notation "1" := (1%R%:E) : ereal_scope.
Bind Scope ereal_dual_scope with dual_extended.
Bind Scope ereal_scope with extended.
Delimit Scope ereal_dual_scope with dE.
Delimit Scope ereal_scope with E.
Local Open Scope ereal_scope.
Definition er_map T T' (f : T → T') (x : \bar T) : \bar T' :=
match x with
| r%:E ⇒ (f r)%:E
| +oo ⇒ +oo
| -oo ⇒ -oo
end.
Definition fine {R : zmodType} x : R := if x is EFin v then v else 0.
Section EqEReal.
Variable (R : eqType).
Definition eq_ereal (x y : \bar R) :=
match x, y with
| x%:E, y%:E ⇒ x == y
| +oo, +oo ⇒ true
| -oo, -oo ⇒ true
| _, _ ⇒ false
end.
Lemma ereal_eqP : Equality.axiom eq_ereal.
Definition ereal_eqMixin := Equality.Mixin ereal_eqP.
Canonical ereal_eqType := Equality.Pack ereal_eqMixin.
Lemma eqe (r1 r2 : R) : (r1%:E == r2%:E) = (r1 == r2).
End EqEReal.
Section ERealChoice.
Variable (R : choiceType).
Definition code (x : \bar R) :=
match x with
| r%:E ⇒ GenTree.Node 0 [:: GenTree.Leaf r]
| +oo ⇒ GenTree.Node 1 [::]
| -oo ⇒ GenTree.Node 2 [::]
end.
Definition decode (x : GenTree.tree R) : option (\bar R) :=
match x with
| GenTree.Node 0 [:: GenTree.Leaf r] ⇒ Some r%:E
| GenTree.Node 1 [::] ⇒ Some +oo
| GenTree.Node 2 [::] ⇒ Some -oo
| _ ⇒ None
end.
Lemma codeK : pcancel code decode.
Definition ereal_choiceMixin := PcanChoiceMixin codeK.
Canonical ereal_choiceType := ChoiceType (extended R) ereal_choiceMixin.
End ERealChoice.
Section ERealCount.
Variable (R : countType).
Definition ereal_countMixin := PcanCountMixin (@codeK R).
Canonical ereal_countType := CountType (extended R) ereal_countMixin.
End ERealCount.
Section ERealOrder.
Context {R : numDomainType}.
Implicit Types x y : \bar R.
Definition le_ereal x1 x2 :=
match x1, x2 with
| -oo, r%:E | r%:E, +oo ⇒ r \is Num.real
| r1%:E, r2%:E ⇒ r1 ≤ r2
| -oo, _ | _, +oo ⇒ true
| +oo, _ | _, -oo ⇒ false
end.
Definition lt_ereal x1 x2 :=
match x1, x2 with
| -oo, r%:E | r%:E, +oo ⇒ r \is Num.real
| r1%:E, r2%:E ⇒ r1 < r2
| -oo, -oo | +oo, +oo ⇒ false
| +oo, _ | _ , -oo ⇒ false
| -oo, _ ⇒ true
end.
Lemma lt_def_ereal x y : lt_ereal x y = (y != x) && le_ereal x y.
Lemma le_refl_ereal : reflexive le_ereal.
Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
Lemma le_trans_ereal : ssrbool.transitive le_ereal.
Fact ereal_display : unit.
Definition ereal_porderMixin :=
LePOrderMixin lt_def_ereal le_refl_ereal le_anti_ereal le_trans_ereal.
Canonical ereal_porderType :=
POrderType ereal_display (extended R) ereal_porderMixin.
Lemma leEereal x y : (x ≤ y)%O = le_ereal x y.
Lemma ltEereal x y : (x < y)%O = lt_ereal x y.
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.
Lemma lee_fin (r s : R) : (r%:E ≤ s%:E) = (r ≤ s)%R.
Lemma lte_fin (r s : R) : (r%:E < s%:E) = (r < s)%R.
Lemma lee01 : 0 ≤ 1 :> \bar R.
Lemma lte01 : 0 < 1 :> \bar R.
Lemma leeNy_eq x : (x ≤ -oo) = (x == -oo).
Lemma leye_eq x : (+oo ≤ x) = (x == +oo).
Lemma lt0y : (0 : \bar R) < +oo.
Lemma ltNy0 : -oo < (0 : \bar R).
Lemma le0y : (0 : \bar R) ≤ +oo.
Lemma leNy0 : -oo ≤ (0 : \bar R).
Lemma ereal_comparable x y : (0%E >=< x)%O → (0%E >=< y)%O → (x >=< y)%O.
End ERealOrder_numDomainType.
#[global] Hint Resolve lee01 lte01 : core.
Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma ltey r : r%:E < +oo.
Lemma ltNye r : -oo < r%:E.
Lemma leey x : x ≤ +oo.
Lemma leNye x : -oo ≤ x.
Lemma gee0P x : 0 ≤ x ↔ x = +oo ∨ exists2 r, (r ≥ 0)%R & x = r%:E.
Lemma le_total_ereal : totalPOrderMixin [porderType of \bar R].
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.
Lemma lee0N1 : 0 ≤ (-1)%:E :> \bar R = false.
Lemma lte0N1 : 0 < (-1)%:E :> \bar R = false.
Lemma le0R x : 0 ≤ x → (0 ≤ fine x)%R.
Lemma lt0R x : 0 < x < +oo → (0 < fine x)%R.
Lemma lee_tofin (r0 r1 : R) : (r0 ≤ r1)%R → r0%:E ≤ r1%:E.
Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%R → r0%:E < r1%:E.
Lemma enatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.
Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
Lemma EFin_natmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.
Lemma mule2n x : x *+ 2 = x + x.
Lemma expe2 x : x ^+ 2 = x × x.
End ERealOrderTheory.
Section finNumPred.
Context {R : numDomainType}.
Implicit Type (x : \bar R).
Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
Fact fin_num_key : pred_key fin_num.
Canonical fin_num_keyd := KeyedQualifier fin_num_key.
Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).
Lemma fin_numP x : reflect ((x != -oo) ∧ (x != +oo)) (x \is a fin_num).
Lemma fin_numEn x : (x \isn't a fin_num) = (x == -oo) || (x == +oo).
Lemma fin_numPn x : reflect (x = -oo ∨ x = +oo) (x \isn't a fin_num).
End finNumPred.
Section ERealArithTh_numDomainType.
Context {R : numDomainType}.
Implicit Types (x y z : \bar R) (r : R).
Lemma fine_eq0 x : x \is a fin_num → (fine x == 0%R) = (x == 0).
Lemma EFinN r : (- r)%:E = (- r%:E).
Lemma fineN x : fine (- x) = (- fine x)%R.
Lemma EFinD r r' : (r + r')%:E = r%:E + r'%:E.
Lemma EFinB r r' : (r - r')%:E = r%:E - r'%:E.
Lemma EFinM r r' : (r × r')%:E = r%:E × r'%:E.
Lemma sumEFin I s P (F : I → R) :
\sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.
Definition adde_def x y :=
~~ ((x == +oo) && (y == -oo)) && ~~ ((x == -oo) && (y == +oo)).
Lemma adde_defC x y : x +? y = y +? x.
Lemma adde_defNN x y : - x +? - y = x +? y.
Lemma adde_defEninfty x : (x +? -oo) = (x != +oo).
Lemma ge0_adde_def : {in [pred x | x ≥ 0] &, ∀ x y, x +? y}.
Lemma addeC : commutative (S := \bar R) +%E.
Lemma adde0 : right_id (0 : \bar R) +%E.
Lemma add0e : left_id (0 : \bar R) +%E.
Lemma addeA : associative (S := \bar R) +%E.
Canonical adde_monoid := Monoid.Law addeA add0e adde0.
Canonical adde_comoid := Monoid.ComLaw addeC.
Lemma addeAC : @right_commutative (\bar R) _ +%E.
Lemma addeCA : @left_commutative (\bar R) _ +%E.
Lemma addeACA : @interchange (\bar R) +%E +%E.
Lemma adde_gt0 x y : 0 < x → 0 < y → 0 < x + y.
Lemma padde_eq0 x y : 0 ≤ x → 0 ≤ y → (x + y == 0) = (x == 0) && (y == 0).
Lemma nadde_eq0 x y : x ≤ 0 → y ≤ 0 → (x + y == 0) = (x == 0) && (y == 0).
Lemma realDe x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x + y)%O.
Lemma oppe0 : - 0 = 0 :> \bar R.
Lemma oppeK : involutive (A := \bar R) -%E.
Lemma oppe_eq0 x : (- x == 0)%E = (x == 0)%E.
Lemma oppeD x y : y \is a fin_num → - (x + y) = - x - y.
Lemma sube0 x : x - 0 = x.
Lemma sub0e x : 0 - x = - x.
Lemma muleC x y : x × y = y × x.
Lemma onee_neq0 : 1 != 0 :> \bar R.
Lemma onee_eq0 : 1 == 0 :> \bar R = false.
Lemma mule1 x : x × 1 = x.
Lemma mul1e x : 1 × x = x.
Lemma mule0 x : x × 0 = 0.
Lemma mul0e x : 0 × x = 0.
Canonical mule_mulmonoid := @Monoid.MulLaw _ _ mule mul0e mule0.
Definition mule_def x y :=
~~ (((x == 0) && (`| y | == +oo)) || ((y == 0) && (`| x | == +oo))).
Lemma mule_defC x y : x *? y = y *? x.
Lemma mule_def_fin x y : x \is a fin_num → y \is a fin_num → x *? y.
Lemma mule_def_neq0_infty x y : x != 0 → y \isn't a fin_num → x *? y.
Lemma mule_def_infty_neq0 x y : x \isn't a fin_num → y!= 0 → x *? y.
Lemma neq0_mule_def x y : x × y != 0 → x *? y.
Lemma ltpinfty_adde_def : {in [pred x | x < +oo] &, ∀ x y, x +? y}.
Lemma ltninfty_adde_def : {in [pred x | -oo < x] &, ∀ x y, x +? y}.
Lemma abse_eq0 x : (`|x| == 0) = (x == 0).
Lemma abse0 : `|0| = 0 :> \bar R.
Lemma abse1 : `|1| = 1 :> \bar R.
Lemma abseN x : `|- x| = `|x|.
Lemma eqe_opp x y : (- x == - y) = (x == y).
Lemma eqe_oppP x y : (- x = - y) ↔ (x = y).
Lemma eqe_oppLR x y : (- x == y) = (x == - y).
Lemma eqe_oppLRP x y : (- x = y) ↔ (x = - y).
Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).
Lemma oppeB x y : y \is a fin_num → - (x - y) = - x + y.
Lemma fin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Lemma sum_fin_num (T : Type) (s : seq T) (P : pred T) (f : T → \bar R) :
\sum_(i <- s | P i) f i \is a fin_num =
all [pred x | x \is a fin_num] [seq f i | i <- s & P i].
Lemma sum_fin_numP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
reflect (∀ i, i \in s → P i → f i \is a fin_num)
(\sum_(i <- s | P i) f i \is a fin_num).
Lemma fin_numB x y :
(x - y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Lemma fin_numM x y : x \is a fin_num → y \is a fin_num →
x × y \is a fin_num.
Lemma fineD : {in @fin_num R &, {morph fine : x y / x + y >-> (x + y)%R}}.
Lemma fineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.
Lemma fineM : {in @fin_num R &, {morph fine : x y / x × y >-> (x × y)%R}}.
Lemma fin_num_adde_def x y : y \is a fin_num → x +? y.
Lemma fineK x : x \is a fin_num → (fine x)%:E = x.
Lemma telescope_sume n m (f : nat → \bar R) :
(∀ i, (n ≤ i ≤ m)%N → f i \is a fin_num) → (n ≤ m)%N →
\sum_(n ≤ k < m) (f k.+1 - f k) = f m - f n.
Lemma addeK x y : x \is a fin_num → y + x - x = y.
Lemma subeK x y : y \is a fin_num → x - y + y = x.
Lemma subee x : x \is a fin_num → x - x = 0.
Lemma sube_eq x y z : x \is a fin_num → (y +? z) →
(x - z == y) = (x == y + z).
Lemma adde_eq_ninfty x y : (x + y == -oo) = ((x == -oo) || (y == -oo)).
Lemma addye x : x != -oo → +oo + x = +oo.
Lemma addey x : x != -oo → x + +oo = +oo.
Lemma adde_Neq_pinfty x y : x != -oo → y != -oo →
(x + y != +oo) = (x != +oo) && (y != +oo).
Lemma adde_Neq_ninfty x y : x != +oo → y != +oo →
(x + y != -oo) = (x != -oo) && (y != -oo).
Lemma adde_ss_eq0 x y : (0 ≤ x) && (0 ≤ y) || (x ≤ 0) && (y ≤ 0) →
x + y == 0 = (x == 0) && (y == 0).
Lemma esum_ninftyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
\sum_(i <- s | P i) f i = -oo ↔ ∃ i, [/\ i \in s, P i & f i = -oo].
Lemma esum_ninfty (I : finType) (f : I → \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == -oo) = [∃ i in P, f i == -oo].
Lemma esum_pinftyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
(∀ i, P i → f i != -oo) →
\sum_(i <- s | P i) f i = +oo ↔ ∃ i, [/\ i \in s, P i & f i = +oo].
Lemma esum_pinfty (I : finType) (P : {pred I}) (f : I → \bar R) :
(∀ i, P i → f i != -oo) →
(\sum_(i | P i) f i == +oo) = [∃ i in P, f i == +oo].
Lemma adde_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
Lemma adde_le0 x y : x ≤ 0 → y ≤ 0 → x + y ≤ 0.
Lemma oppe_gt0 x : (0 < - x) = (x < 0).
Lemma oppe_lt0 x : (- x < 0) = (0 < x).
Lemma oppe_ge0 x : (0 ≤ - x) = (x ≤ 0).
Lemma oppe_le0 x : (- x ≤ 0) = (0 ≤ x).
Lemma sume_ge0 T (f : T → \bar R) (P : pred T) :
(∀ t, P t → 0 ≤ f t) → ∀ l, 0 ≤ \sum_(i <- l | P i) f i.
Lemma sume_le0 T (f : T → \bar R) (P : pred T) :
(∀ t, P t → f t ≤ 0) → ∀ l, \sum_(i <- l | P i) f i ≤ 0.
Lemma mulNyy : -oo × +oo = -oo :> \bar R.
Lemma mulyNy : +oo × -oo = -oo :> \bar R.
Lemma mulyy : +oo × +oo = +oo :> \bar R.
Lemma mulNyNy : -oo × -oo = +oo :> \bar R.
Lemma real_mulry r : r \is Num.real → r%:E × +oo = (Num.sg r)%:E × +oo.
Lemma real_mulyr r : r \is Num.real → +oo × r%:E = (Num.sg r)%:E × +oo.
Lemma real_mulrNy r : r \is Num.real → r%:E × -oo = (Num.sg r)%:E × -oo.
Lemma real_mulNyr r : r \is Num.real → -oo × r%:E = (Num.sg r)%:E × -oo.
Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).
Lemma mulN1e x : - 1%E × x = - x.
Lemma muleN1 x : x × - 1%E = - x.
Lemma mule_neq0 x y : x != 0 → y != 0 → x × y != 0.
Lemma mule_eq0 x y : (x × y == 0) = (x == 0) || (y == 0).
Lemma mule_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x × y.
Lemma mule_gt0 x y : 0 < x → 0 < y → 0 < x × y.
Lemma mule_le0 x y : x ≤ 0 → y ≤ 0 → 0 ≤ x × y.
Lemma mule_le0_ge0 x y : x ≤ 0 → 0 ≤ y → x × y ≤ 0.
Lemma mule_ge0_le0 x y : 0 ≤ x → y ≤ 0 → x × y ≤ 0.
Lemma mule_lt0_lt0 x y : x < 0 → y < 0 → 0 < x × y.
Lemma mule_gt0_lt0 x y : 0 < x → y < 0 → x × y < 0.
Lemma mule_lt0_gt0 x y : x < 0 → 0 < y → x × y < 0.
Lemma gte_opp x : 0 < x → - x < x.
Lemma realMe x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x × y)%O.
Lemma abse_ge0 x : 0 ≤ `|x|.
Lemma gee0_abs x : 0 ≤ x → `|x| = x.
Lemma gte0_abs x : 0 < x → `|x| = x.
Lemma lee0_abs x : x ≤ 0 → `|x| = - x.
Lemma lte0_abs x : x < 0 → `|x| = - x.
End ERealArithTh_numDomainType.
Notation "x +? y" := (adde_def x%dE y%dE) : ereal_dual_scope.
Notation "x +? y" := (adde_def x y) : ereal_scope.
Notation "x *? y" := (mule_def x%dE y%dE) : ereal_dual_scope.
Notation "x *? y" := (mule_def x y) : ereal_scope.
Notation maxe := (@Order.max ereal_display _).
Notation "@ 'maxe' R" := (@Order.max ereal_display R)
(at level 10, R at level 8, only parsing) : fun_scope.
Notation mine := (@Order.min ereal_display _).
Notation "@ 'mine' R" := (@Order.min ereal_display R)
(at level 10, R at level 8, only parsing) : fun_scope.
Module DualAddTheoryNumDomain.
Section DualERealArithTh_numDomainType.
Local Open Scope ereal_dual_scope.
Context {R : numDomainType}.
Implicit Types x y z : \bar R.
Lemma dual_addeE x y : (x + y)%dE = - ((- x) + (- y))%E.
Lemma dual_sumeE I (r : seq I) (P : pred I) (F : I → \bar R) :
(\sum_(i <- r | P i) F i)%dE = - (\sum_(i <- r | P i) (- F i)%E)%E.
Lemma dual_addeE_def x y : x +? y → (x + y)%dE = (x + y)%E.
Lemma dEFinD (r r' : R) : (r + r')%R%:E = r%:E + r'%:E.
Lemma dEFinB (r r' : R) : (r - r')%R%:E = r%:E - r'%:E.
Lemma dsumEFin I r P (F : I → R) :
\sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%R%:E.
Lemma daddeC : commutative (S := \bar R) +%dE.
Lemma dadde0 : right_id (0 : \bar R) +%dE.
Lemma dadd0e : left_id (0 : \bar R) +%dE.
Lemma daddeA : associative (S := \bar R) +%dE.
Canonical dadde_monoid := Monoid.Law daddeA dadd0e dadde0.
Canonical dadde_comoid := Monoid.ComLaw daddeC.
Lemma daddeAC : right_commutative (S := \bar R) +%dE.
Lemma daddeCA : left_commutative (S := \bar R) +%dE.
Lemma daddeACA : @interchange (\bar R) +%dE +%dE.
Lemma realDed x y : (0%E >=< x)%O → (0%E >=< y)%O → (0%E >=< x + y)%O.
Lemma doppeD x y : y \is a fin_num → - (x + y) = - x - y.
Lemma dsube0 x : x - 0 = x.
Lemma dsub0e x : 0 - x = - x.
Lemma doppeB x y : y \is a fin_num → - (x - y) = - x + y.
Lemma dfin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Lemma dfineD :
{in (@fin_num R) &, {morph fine : x y / x + y >-> (x + y)%R}}.
Lemma dfineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.
Lemma daddeK x y : x \is a fin_num → y + x - x = y.
Lemma dsubeK x y : y \is a fin_num → x - y + y = x.
Lemma dsubee x : x \is a fin_num → x - x = 0.
Lemma dsube_eq x y z : x \is a fin_num → (y +? z) →
(x - z == y) = (x == y + z).
Lemma dadde_eq_pinfty x y : (x + y == +oo) = ((x == +oo) || (y == +oo)).
Lemma daddooe x : x != -oo → +oo + x = +oo.
Lemma daddeoo x : x != -oo → x + +oo = +oo.
Lemma dadde_Neq_pinfty x y : x != -oo → y != -oo →
(x + y != +oo) = (x != +oo) && (y != +oo).
Lemma dadde_Neq_ninfty x y : x != +oo → y != +oo →
(x + y != -oo) = (x != -oo) && (y != -oo).
Lemma ndadde_eq0 x y : x ≤ 0 → y ≤ 0 → x + y == 0 = (x == 0) && (y == 0).
Lemma pdadde_eq0 x y : 0 ≤ x → 0 ≤ y → x + y == 0 = (x == 0) && (y == 0).
Lemma dadde_ss_eq0 x y : (0 ≤ x) && (0 ≤ y) || (x ≤ 0) && (y ≤ 0) →
x + y == 0 = (x == 0) && (y == 0).
Lemma desum_pinftyP (T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
\sum_(i <- s | P i) f i = +oo ↔ ∃ i, [/\ i \in s, P i & f i = +oo].
Lemma desum_pinfty (I : finType) (f : I → \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == +oo) = [∃ i in P, f i == +oo].
Lemma desum_ninftyP
(T : eqType) (s : seq T) (P : pred T) (f : T → \bar R) :
(∀ i, P i → f i != +oo) →
\sum_(i <- s | P i) f i = -oo ↔ ∃ i, [/\ i \in s, P i & f i = -oo].
Lemma desum_ninfty (I : finType) (f : I → \bar R) (P : {pred I}) :
(∀ i, f i != +oo) →
(\sum_(i | P i) f i == -oo) = [∃ i in P, f i == -oo].
Lemma dadde_ge0 x y : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
Lemma dadde_le0 x y : x ≤ 0 → y ≤ 0 → x + y ≤ 0.
Lemma dsume_ge0 T (f : T → \bar R) (P : pred T) :
(∀ n, P n → 0 ≤ f n) → ∀ l, 0 ≤ \sum_(i <- l | P i) f i.
Lemma dsume_le0 T (f : T → \bar R) (P : pred T) :
(∀ n, P n → f n ≤ 0) → ∀ l, \sum_(i <- l | P i) f i ≤ 0.
Lemma gte_dopp (r : \bar R) : (0 < r)%E → (- r < r)%E.
Lemma ednatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.
Lemma ednatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
Lemma EFin_dnatmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.
Lemma ednatmulE x n : x *+ n = (x *+ n)%E.
Lemma dmule2n x : x *+ 2 = x + x.
End DualERealArithTh_numDomainType.
End DualAddTheoryNumDomain.
Section ERealArithTh_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y z u a b : \bar R) (r : R).
Lemma fin_numElt x : (x \is a fin_num) = (-oo < x < +oo).
Lemma fin_numPlt x : reflect (-oo < x < +oo) (x \is a fin_num).
Lemma lte_pinfty_eq x : (x < +oo) = (x \is a fin_num) || (x == -oo).
Lemma ge0_fin_numE x : 0 ≤ x → (x \is a fin_num) = (x < +oo).
Lemma eq_pinftyP x : x = +oo ↔ (∀ A, (0 < A)%R → A%:E ≤ x).
Lemma seq_psume_eq0 (I : choiceType) (r : seq I)
(P : pred I) (F : I → \bar R) : (∀ i, P i → 0 ≤ F i)%E →
(\sum_(i <- r | P i) F i == 0)%E = all (fun i ⇒ P i ==> (F i == 0%E)) r.
Lemma lte_add_pinfty x y : x < +oo → y < +oo → x + y < +oo.
Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I → \bar R) :
(∀ i, P i → f i < +oo) → \sum_(i <- s | P i) f i < +oo.
Lemma sube_gt0 x y : (0 < y - x) = (x < y).
Lemma sube_le0 x y : (y - x ≤ 0) = (y ≤ x).
Lemma suber_ge0 y x : y \is a fin_num → (0 ≤ x - y) = (y ≤ x).
Lemma subre_ge0 x y : y \is a fin_num → (0 ≤ y - x) = (x ≤ y).
Lemma lte_oppl x y : (- x < y) = (- y < x).
Lemma lte_oppr x y : (x < - y) = (y < - x).
Lemma lee_oppr x y : (x ≤ - y) = (y ≤ - x).
Lemma lee_oppl x y : (- x ≤ y) = (- y ≤ x).
Lemma muleN x y : x × - y = - (x × y).
Lemma mulNe x y : - x × y = - (x × y).
Lemma muleNN x y : - x × - y = x × y.
Lemma mulry r : r%:E × +oo%E = (Num.sg r)%:E × +oo%E.
Lemma mulyr r : +oo%E × r%:E = (Num.sg r)%:E × +oo%E.
Lemma mulrNy r : r%:E × -oo%E = (Num.sg r)%:E × -oo%E.
Lemma mulNyr r : -oo%E × r%:E = (Num.sg r)%:E × -oo%E.
Definition mulr_infty := (mulry, mulyr, mulrNy, mulNyr).
Lemma lte_mul_pinfty x y : 0 ≤ x → x \is a fin_num → y < +oo → x × y < +oo.
Lemma mule_ge0_gt0 x y : 0 ≤ x → 0 ≤ y → (0 < x × y) = (0 < x) && (0 < y).
Lemma gt0_mulye x : (0 < x → +oo × x = +oo)%E.
Lemma lt0_mulye x : (x < 0 → +oo × x = -oo)%E.
Lemma gt0_mulNye x : (0 < x → -oo × x = -oo)%E.
Lemma lt0_mulNye x : (x < 0 → -oo × x = +oo)%E.
Lemma mule_eq_pinfty x y : (x × y == +oo) =
[|| (x > 0) && (y == +oo), (x < 0) && (y == -oo),
(x == +oo) && (y > 0) | (x == -oo) && (y < 0)].
Lemma mule_eq_ninfty x y : (x × y == -oo) =
[|| (x > 0) && (y == -oo), (x < 0) && (y == +oo),
(x == -oo) && (y > 0) | (x == +oo) && (y < 0)].
Lemma lte_opp x y : (- x < - y) = (y < x).
Lemma lte_add a b x y : a < b → x < y → a + x < b + y.
Lemma lee_addl x y : 0 ≤ y → x ≤ x + y.
Lemma lee_addr x y : 0 ≤ y → x ≤ y + x.
Lemma gee_addl x y : y ≤ 0 → x + y ≤ x.
Lemma gee_addr x y : y ≤ 0 → y + x ≤ x.
Lemma lte_addl y x : y \is a fin_num → 0 < x → y < y + x.
Lemma lte_addr y x : y \is a fin_num → 0 < x → y < x + y.
Lemma gte_subl y x : y \is a fin_num → 0 < x → y - x < y.
Lemma gte_subr y x : y \is a fin_num → 0 < x → - x + y < y.
Lemma lte_add2lE x a b : x \is a fin_num → (x + a < x + b) = (a < b).
Lemma lee_add2l x a b : a ≤ b → x + a ≤ x + b.
Lemma lee_add2lE x a b : x \is a fin_num → (x + a ≤ x + b) = (a ≤ b).
Lemma lee_add2r x a b : a ≤ b → a + x ≤ b + x.
Lemma lee_add a b x y : a ≤ b → x ≤ y → a + x ≤ b + y.
Lemma lte_le_add a b x y : b \is a fin_num → a < x → b ≤ y → a + b < x + y.
Lemma lee_lt_add a b x y : a \is a fin_num → a ≤ x → b < y → a + b < x + y.
Lemma lee_sub x y z u : x ≤ y → u ≤ z → x - z ≤ y - u.
Lemma lte_le_sub z u x y : u \is a fin_num →
x < z → u ≤ y → x - y < z - u.
Lemma lte_pmul2r z : z \is a fin_num → 0 < z → {mono *%E^~ z : x y / x < y}.
Lemma lte_pmul2l z : z \is a fin_num → 0 < z → {mono *%E z : x y / x < y}.
Lemma lte_nmul2l z : z \is a fin_num → z < 0 → {mono *%E z : x y /~ x < y}.
Lemma lte_nmul2r z : z \is a fin_num → z < 0 → {mono *%E^~ z : x y /~ x < y}.
Lemma lee_sum I (f g : I → \bar R) s (P : pred I) :
(∀ i, P i → f i ≤ g i) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i) g i.
Lemma lee_sum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, 0 ≤ f i} →
\sum_(i <- s | Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_sum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, f i ≤ 0} →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | Q i) f i.
Lemma lee_sum_nneg (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → 0 ≤ f i) →
\sum_(i <- s | P i && Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_sum_npos (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → f i ≤ 0) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i && Q i) f i.
Lemma lee_sum_nneg_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → 0 ≤ f n) →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_sum_npos_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → f n ≤ 0)%E →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_sum_nneg_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → 0 ≤ f n) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_sum_npos_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → f n ≤ 0) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_sum_nneg_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → 0 ≤ f m) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_sum_npos_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → f m ≤ 0) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_sum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → 0 ≤ f t} →
\sum_(t <- A | P t) f t ≤ \sum_(t <- B | P t) f t.
Lemma lee_sum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → f t ≤ 0} →
\sum_(t <- B | P t) f t ≤ \sum_(t <- A | P t) f t.
Lemma lte_subl_addr x y z : y \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_subl_addl x y z : y \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_subr_addr x y z : z \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_subr_addl x y z : z \is a fin_num → (x < y - z) = (z + x < y).
Lemma lte_subel_addr x y z : x \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_subel_addl x y z : x \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_suber_addr x y z : x \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_suber_addl x y z : x \is a fin_num → (x < y - z) = (z + x < y).
Lemma lee_subl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_subl_addl x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_subr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_subr_addl x y z : z \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma lee_subel_addr x y z : z \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_subel_addl x y z : z \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_suber_addr x y z : y \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_suber_addl x y z : y \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma pmule_rge0 x y : 0 < x → (x × y ≥ 0) = (y ≥ 0).
Lemma pmule_lge0 x y : 0 < x → (y × x ≥ 0) = (y ≥ 0).
Lemma pmule_rlt0 x y : 0 < x → (x × y < 0) = (y < 0).
Lemma pmule_llt0 x y : 0 < x → (y × x < 0) = (y < 0).
Lemma pmule_rle0 x y : 0 < x → (x × y ≤ 0) = (y ≤ 0).
Lemma pmule_lle0 x y : 0 < x → (y × x ≤ 0) = (y ≤ 0).
Lemma pmule_rgt0 x y : 0 < x → (x × y > 0) = (y > 0).
Lemma pmule_lgt0 x y : 0 < x → (y × x > 0) = (y > 0).
Lemma nmule_rge0 x y : x < 0 → (x × y ≥ 0) = (y ≤ 0).
Lemma nmule_lge0 x y : x < 0 → (y × x ≥ 0) = (y ≤ 0).
Lemma nmule_rle0 x y : x < 0 → (x × y ≤ 0) = (y ≥ 0).
Lemma nmule_lle0 x y : x < 0 → (y × x ≤ 0) = (y ≥ 0).
Lemma nmule_rgt0 x y : x < 0 → (x × y > 0) = (y < 0).
Lemma nmule_lgt0 x y : x < 0 → (y × x > 0) = (y < 0).
Lemma nmule_rlt0 x y : x < 0 → (x × y < 0) = (y > 0).
Lemma nmule_llt0 x y : x < 0 → (y × x < 0) = (y > 0).
Lemma mule_lt0 x y : (x × y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)].
Lemma muleA : associative ( *%E : \bar R → \bar R → \bar R ).
Local Open Scope ereal_scope.
Canonical mule_monoid := Monoid.Law muleA mul1e mule1.
Canonical mule_comoid := Monoid.ComLaw muleC.
Lemma muleCA : left_commutative ( *%E : \bar R → \bar R → \bar R ).
Lemma muleAC : right_commutative ( *%E : \bar R → \bar R → \bar R ).
Lemma muleACA : interchange (@mule R) (@mule R).
Lemma muleDr x y z : x \is a fin_num → y +? z → x × (y + z) = x × y + x × z.
Lemma muleDl x y z : x \is a fin_num → y +? z → (y + z) × x = y × x + z × x.
Lemma muleBr x y z : x \is a fin_num → y +? - z → x × (y - z) = x × y - x × z.
Lemma muleBl x y z : x \is a fin_num → y +? - z → (y - z) × x = y × x - z × x.
Lemma ge0_muleDl x y z : 0 ≤ y → 0 ≤ z → (y + z) × x = y × x + z × x.
Lemma ge0_muleDr x y z : 0 ≤ y → 0 ≤ z → x × (y + z) = x × y + x × z.
Lemma le0_muleDl x y z : y ≤ 0 → z ≤ 0 → (y + z) × x = y × x + z × x.
Lemma le0_muleDr x y z : y ≤ 0 → z ≤ 0 → x × (y + z) = x × y + x × z.
Lemma gee_pmull y x : y \is a fin_num → 0 < x → y ≤ 1 → y × x ≤ x.
Lemma lee_wpmul2r x : 0 ≤ x → {homo *%E^~ x : y z / y ≤ z}.
Lemma lee_wpmul2l x : 0 ≤ x → {homo *%E x : y z / y ≤ z}.
Lemma ge0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma ge0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma le0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma le0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma eq_infty x : (∀ r, r%:E ≤ x) → x = +oo.
Lemma eq_ninfty x : (∀ r, x ≤ r%:E) → x = -oo.
Lemma lee_opp x y : (- x ≤ - y) = (y ≤ x).
Lemma lee_abs x : x ≤ `|x|.
Lemma abse_id x : `| `|x| | = `|x|.
Lemma lte_absl (x y : \bar R) : (`|x| < y)%E = (- y < x < y)%E.
Lemma fin_num_abs x : (x \is a fin_num) = (`| x | < +oo)%E.
Lemma eqe_absl x y : (`|x| == y) = ((x == y) || (x == - y)) && (0 ≤ y).
Lemma lee_abs_add x y : `|x + y| ≤ `|x| + `|y|.
Lemma lee_abs_sum (I : Type) (s : seq I) (F : I → \bar R) (P : pred I) :
`|\sum_(i <- s | P i) F i| ≤ \sum_(i <- s | P i) `|F i|.
Lemma lee_abs_sub x y : `|x - y| ≤ `|x| + `|y|.
Lemma abseM : {morph @abse R : x y / x × y}.
Lemma maxEFin r1 r2 : maxe r1%:E r2%:E = (Num.max r1 r2)%:E.
Lemma minEFin r1 r2 : mine r1%:E r2%:E = (Num.min r1 r2)%:E.
Lemma adde_maxl : left_distributive (@adde R) maxe.
Lemma adde_maxr : right_distributive (@adde R) maxe.
Lemma maxye : left_zero (+oo : \bar R) maxe.
Lemma maxey : right_zero (+oo : \bar R) maxe.
Lemma maxNye : left_id (-oo : \bar R) maxe.
Lemma maxeNy : right_id (-oo : \bar R) maxe.
Lemma minNye : left_zero (-oo : \bar R) mine.
Lemma mineNy : right_zero (-oo : \bar R) mine.
Lemma minye : left_id (+oo : \bar R) mine.
Lemma miney : right_id (+oo : \bar R) mine.
Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.
Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.
Lemma maxeMr z x y : z \is a fin_num → 0 < z →
z × maxe x y = maxe (z × x) (z × y).
Lemma maxeMl z x y : z \is a fin_num → 0 < z →
maxe x y × z = maxe (x × z) (y × z).
Lemma mineMr z x y : z \is a fin_num → 0 < z →
z × mine x y = mine (z × x) (z × y).
Lemma mineMl z x y : z \is a fin_num → 0 < z →
mine x y × z = mine (x × z) (y × z).
Lemma lee_pemull x y : 0 ≤ y → 1 ≤ x → y ≤ x × y.
Lemma lee_nemull x y : y ≤ 0 → 1 ≤ x → x × y ≤ y.
Lemma lee_pemulr x y : 0 ≤ y → 1 ≤ x → y ≤ y × x.
Lemma lee_nemulr x y : y ≤ 0 → 1 ≤ x → y × x ≤ y.
Lemma mule_natl x n : n%:R%:E × x = x *+ n.
Lemma lte_pmul x1 y1 x2 y2 :
0 ≤ x1 → 0 ≤ x2 → x1 < y1 → x2 < y2 → x1 × x2 < y1 × y2.
Lemma lee_pmul x1 y1 x2 y2 : 0 ≤ x1 → 0 ≤ x2 → x1 ≤ y1 → x2 ≤ y2 →
x1 × x2 ≤ y1 × y2.
Lemma lee_pmul2l x : x \is a fin_num → 0 < x → {mono *%E x : x y / x ≤ y}.
Lemma lee_pmul2r x : x \is a fin_num → 0 < x → {mono *%E^~ x : x y / x ≤ y}.
End ERealArithTh_realDomainType.
Arguments lee_sum_nneg_ord {R}.
Arguments lee_sum_npos_ord {R}.
Arguments lee_sum_nneg_natr {R}.
Arguments lee_sum_npos_natr {R}.
Arguments lee_sum_nneg_natl {R}.
Arguments lee_sum_npos_natl {R}.
#[global] Hint Extern 0 (is_true (0 ≤ `| _ |)%E) ⇒ solve [apply: abse_ge0] : core.
Module DualAddTheoryRealDomain.
Section DualERealArithTh_realDomainType.
Import DualAddTheoryNumDomain.
Local Open Scope ereal_dual_scope.
Context {R : realDomainType}.
Implicit Types x y z a b : \bar R.
Lemma dsube_lt0 x y : (x - y < 0) = (x < y).
Lemma dsube_ge0 x y : (0 ≤ y - x) = (x ≤ y).
Lemma dsuber_le0 x y : y \is a fin_num → (x - y ≤ 0) = (x ≤ y).
Lemma dsubre_le0 y x : y \is a fin_num → (y - x ≤ 0) = (y ≤ x).
Lemma lte_dadd a b x y : a < b → x < y → a + x < b + y.
Lemma lee_daddl x y : 0 ≤ y → x ≤ x + y.
Lemma lee_daddr x y : 0 ≤ y → x ≤ y + x.
Lemma gee_daddl x y : y ≤ 0 → x + y ≤ x.
Lemma gee_daddr x y : y ≤ 0 → y + x ≤ x.
Lemma lte_daddl y x : y \is a fin_num → 0 < x → y < y + x.
Lemma lte_daddr y x : y \is a fin_num → 0 < x → y < x + y.
Lemma gte_dsubl y x : y \is a fin_num → 0 < x → y - x < y.
Lemma gte_dsubr y x : y \is a fin_num → 0 < x → - x + y < y.
Lemma lte_dadd2lE x a b : x \is a fin_num → (x + a < x + b) = (a < b).
Lemma lee_dadd2l x a b : a ≤ b → x + a ≤ x + b.
Lemma lee_dadd2lE x a b : x \is a fin_num → (x + a ≤ x + b) = (a ≤ b).
Lemma lee_dadd2r x a b : a ≤ b → a + x ≤ b + x.
Lemma lee_dadd a b x y : a ≤ b → x ≤ y → a + x ≤ b + y.
Lemma lte_le_dadd a b x y : b \is a fin_num → a < x → b ≤ y → a + b < x + y.
Lemma lee_lt_dadd a b x y : a \is a fin_num → a ≤ x → b < y → a + b < x + y.
Lemma lee_dsub x y z t : x ≤ y → t ≤ z → x - z ≤ y - t.
Lemma lte_le_dsub z u x y : u \is a fin_num → x < z → u ≤ y → x - y < z - u.
Lemma lee_dsum I (f g : I → \bar R) s (P : pred I) :
(∀ i, P i → f i ≤ g i) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i) g i.
Lemma lee_dsum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, 0 ≤ f i} →
\sum_(i <- s | Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_dsum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I → \bar R) :
{subset Q ≤ P} → {in [predD P & Q], ∀ i, f i ≤ 0} →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | Q i) f i.
Lemma lee_dsum_nneg (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → 0 ≤ f i) →
\sum_(i <- s | P i && Q i) f i ≤ \sum_(i <- s | P i) f i.
Lemma lee_dsum_npos (I : eqType) (s : seq I) (P Q : pred I)
(f : I → \bar R) : (∀ i, P i → ~~ Q i → f i ≤ 0) →
\sum_(i <- s | P i) f i ≤ \sum_(i <- s | P i && Q i) f i.
Lemma lee_dsum_nneg_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → 0 ≤ f n)%E →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_dsum_npos_ord (f : nat → \bar R) (P : pred nat) :
(∀ n, P n → f n ≤ 0)%E →
{homo (fun n ⇒ \sum_(i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_dsum_nneg_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → 0 ≤ f n) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_dsum_npos_natr (f : nat → \bar R) (P : pred nat) m :
(∀ n, (m ≤ n)%N → P n → f n ≤ 0) →
{homo (fun n ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_dsum_nneg_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → 0 ≤ f m) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> j ≤ i}.
Lemma lee_dsum_npos_natl (f : nat → \bar R) (P : pred nat) n :
(∀ m, (m < n)%N → P m → f m ≤ 0) →
{homo (fun m ⇒ \sum_(m ≤ i < n | P i) (f i)) : i j / (i ≤ j)%N >-> i ≤ j}.
Lemma lee_dsum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → 0 ≤ f t} →
\sum_(t <- A | P t) f t ≤ \sum_(t <- B | P t) f t.
Lemma lee_dsum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T → \bar R) : {subset A ≤ B} →
{in [predD B & A], ∀ t, P t → f t ≤ 0} →
\sum_(t <- B | P t) f t ≤ \sum_(t <- A | P t) f t.
Lemma lte_dsubl_addr x y z : y \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_dsubl_addl x y z : y \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_dsubr_addr x y z : z \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_dsubr_addl x y z : z \is a fin_num → (x < y - z) = (z + x < y).
Lemma lte_dsuber_addr x y z : y \is a fin_num → (x < y - z) = (x + z < y).
Lemma lte_dsuber_addl x y z : y \is a fin_num → (x < y - z) = (z + x < y).
Lemma lte_dsubel_addr x y z : z \is a fin_num → (x - y < z) = (x < z + y).
Lemma lte_dsubel_addl x y z : z \is a fin_num → (x - y < z) = (x < y + z).
Lemma lee_dsubl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_dsubl_addl x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_dsubr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_dsubr_addl x y z : z \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma lee_dsubel_addr x y z : x \is a fin_num → (x - y ≤ z) = (x ≤ z + y).
Lemma lee_dsubel_addl x y z : x \is a fin_num → (x - y ≤ z) = (x ≤ y + z).
Lemma lee_dsuber_addr x y z : x \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_dsuber_addl x y z : x \is a fin_num → (x ≤ y - z) = (z + x ≤ y).
Lemma dmuleDr x y z : x \is a fin_num → y +? z → x × (y + z) = x × y + x × z.
Lemma dmuleDl x y z : x \is a fin_num → y +? z → (y + z) × x = y × x + z × x.
Lemma dge0_muleDl x y z : 0 ≤ y → 0 ≤ z → (y + z) × x = y × x + z × x.
Lemma dge0_muleDr x y z : 0 ≤ y → 0 ≤ z → x × (y + z) = x × y + x × z.
Lemma dle0_muleDl x y z : y ≤ 0 → z ≤ 0 → (y + z) × x = y × x + z × x.
Lemma dle0_muleDr x y z : y ≤ 0 → z ≤ 0 → x × (y + z) = x × y + x × z.
Lemma ge0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma ge0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → 0 ≤ F i) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma le0_dsume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
(\sum_(i <- s | P i) F i) × x = \sum_(i <- s | P i) (F i × x).
Lemma le0_dsume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I → \bar R) :
(∀ i, P i → F i ≤ 0) →
x × (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x × F i).
Lemma lee_abs_dadd x y : `|x + y| ≤ `|x| + `|y|.
Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I → \bar R) (P : pred I) :
`|\sum_(i <- s | P i) F i| ≤ \sum_(i <- s | P i) `|F i|.
Lemma lee_abs_dsub x y : `|x - y| ≤ `|x| + `|y|.
Lemma dadde_minl : left_distributive (@dual_adde R) mine.
Lemma dadde_minr : right_distributive (@dual_adde R) mine.
Lemma dmule_natl x n : n%:R%:E × x = x *+ n.
End DualERealArithTh_realDomainType.
Arguments lee_dsum_nneg_ord {R}.
Arguments lee_dsum_npos_ord {R}.
Arguments lee_dsum_nneg_natr {R}.
Arguments lee_dsum_npos_natr {R}.
Arguments lee_dsum_nneg_natl {R}.
Arguments lee_dsum_npos_natl {R}.
End DualAddTheoryRealDomain.
Lemma lee_opp2 {R : realDomainType} : {mono @oppe R : x y /~ x ≤ y}.
Lemma lte_opp2 {R : realDomainType} : {mono @oppe R : x y /~ x < y}.
Section realFieldType_lemmas.
Variable R : realFieldType.
Implicit Types x y : \bar R.
Implicit Types r : R.
Lemma lee_adde x y : (∀ e : {posnum R}, x ≤ y + e%:num%:E) → x ≤ y.
Lemma lee_paddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.
Lemma lte_paddl y x z : 0 ≤ x → y < z → y < x + z.
Lemma lee_paddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.
Lemma lte_paddr y x z : 0 ≤ x → y < z → y < z + x.
Lemma lte_spaddr z x y : z \is a fin_num → 0 < y → z ≤ x → z < x + y.
Lemma lee_mul01Pr x y : 0 ≤ x →
reflect (∀ r, (0 < r < 1)%R → r%:E × x ≤ y) (x ≤ y).
Lemma lte_pdivr_mull r x y : (0 < r)%R → (r^-1%:E × y < x) = (y < r%:E × x).
Lemma lte_pdivr_mulr r x y : (0 < r)%R → (y × r^-1%:E < x) = (y < x × r%:E).
Lemma lte_pdivl_mull r y x : (0 < r)%R → (x < r^-1%:E × y) = (r%:E × x < y).
Lemma lte_pdivl_mulr r x y : (0 < r)%R → (x < y × r^-1%:E) = (x × r%:E < y).
Lemma lte_ndivl_mulr r x y : (r < 0)%R → (x < y × r^-1%:E) = (y < x × r%:E).
Lemma lte_ndivl_mull r x y : (r < 0)%R → (x < r^-1%:E × y) = (y < r%:E × x).
Lemma lte_ndivr_mull r x y : (r < 0)%R → (r^-1%:E × y < x) = (r%:E × x < y).
Lemma lte_ndivr_mulr r x y : (r < 0)%R → (y × r^-1%:E < x) = (x × r%:E < y).
Lemma lee_pdivr_mull r x y : (0 < r)%R → (r^-1%:E × y ≤ x) = (y ≤ r%:E × x).
Lemma lee_pdivr_mulr r x y : (0 < r)%R → (y × r^-1%:E ≤ x) = (y ≤ x × r%:E).
Lemma lee_pdivl_mull r y x : (0 < r)%R → (x ≤ r^-1%:E × y) = (r%:E × x ≤ y).
Lemma lee_pdivl_mulr r x y : (0 < r)%R → (x ≤ y × r^-1%:E) = (x × r%:E ≤ y).
Lemma lee_ndivl_mulr r x y : (r < 0)%R → (x ≤ y × r^-1%:E) = (y ≤ x × r%:E).
Lemma lee_ndivl_mull r x y : (r < 0)%R → (x ≤ r^-1%:E × y) = (y ≤ r%:E × x).
Lemma lee_ndivr_mull r x y : (r < 0)%R → (r^-1%:E × y ≤ x) = (r%:E × x ≤ y).
Lemma lee_ndivr_mulr r x y : (r < 0)%R → (y × r^-1%:E ≤ x) = (x × r%:E ≤ y).
End realFieldType_lemmas.
Module DualAddTheoryRealField.
Import DualAddTheoryNumDomain DualAddTheoryRealDomain.
Section DualRealFieldType_lemmas.
Local Open Scope ereal_dual_scope.
Variable R : realFieldType.
Implicit Types x y : \bar R.
Lemma lee_dadde x y : (∀ e : {posnum R}, x ≤ y + e%:num%:E) → x ≤ y.
Lemma lee_pdaddl y x z : 0 ≤ x → y ≤ z → y ≤ x + z.
Lemma lte_pdaddl y x z : 0 ≤ x → y < z → y < x + z.
Lemma lee_pdaddr y x z : 0 ≤ x → y ≤ z → y ≤ z + x.
Lemma lte_pdaddr y x z : 0 ≤ x → y < z → y < z + x.
Lemma lte_spdaddr (r : R) x y : 0 < y → r%:E ≤ x → r%:E < x + y.
End DualRealFieldType_lemmas.
End DualAddTheoryRealField.
Module DualAddTheory.
Export DualAddTheoryNumDomain.
Export DualAddTheoryRealDomain.
Export DualAddTheoryRealField.
End DualAddTheory.
Definition posnume (R : numDomainType) of phant R := {> 0 : \bar R}.
Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
Definition nonnege (R : numDomainType) of phant R := {>= 0 : \bar R}.
Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
: ereal_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
: ereal_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_dual_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_dual_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_scope.
#[global] Hint Extern 0 (is_true (0%E < _)%O) ⇒ solve [apply: gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%E)%O) ⇒ solve [apply: lt0] : core.
#[global] Hint Extern 0 (is_true (0%E ≤ _)%O) ⇒ solve [apply: ge0] : core.
#[global] Hint Extern 0 (is_true (_ ≤ 0%E)%O) ⇒ solve [apply: le0] : core.
#[global] Hint Extern 0 (is_true (0%E >=< _)%O) ⇒ solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (_ != 0%E)%O) ⇒ solve [apply: neq0] : core.
Section SignedNumDomainStability.
Context {R : numDomainType}.
Lemma pinfty_snum_subproof : Signed.spec 0 !=0 >=0 (+oo : \bar R).
Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof).
Lemma ninfty_snum_subproof : Signed.spec 0 !=0 <=0 (-oo : \bar R).
Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof).
Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) :
Signed.spec 0 nz cond x%:num%:E.
Canonical EFin_snum nz cond (x : {num R & nz & cond}) :=
Signed.mk (EFin_snum_subproof x).
Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :
Signed.spec 0%R ?=0 xr (fine x%:num).
Canonical fine_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (fine_snum_subproof x).
Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := opp_reality_subdef xnz xr) :
Signed.spec 0 xnz r (- x%:num).
Canonical oppe_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (oppe_snum_subproof x).
Lemma adde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num + y%:num).
Canonical adde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (adde_snum_subproof x y).
Import DualAddTheory.
Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num + y%:num)%dE.
Canonical dadde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (dadde_snum_subproof x y).
Lemma mule_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := mul_nonzero_subdef xnz ynz xr yr)
(rrl := mul_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num × y%:num).
Canonical mule_snum (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (mule_snum_subproof x y).
Definition abse_reality_subdef (xnz : KnownSign.nullity)
(xr : KnownSign.reality) := (if xr is =0 then =0 else >=0)%snum_sign.
Arguments abse_reality_subdef /.
Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) :
Signed.spec 0 xnz r `|x%:num|.
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}.
Implicit Types (a : \bar R).
Lemma num_abse_eq0 a : (`|a|%:nng == 0%:nng) = (a == 0).
End MorphNum.
Section MorphReal.
Context {R : numDomainType} {nz : KnownSign.nullity} {r : KnownSign.real}.
Implicit Type x y : nR.
Lemma num_lee_maxr a x y :
a ≤ maxe x%:num y%:num = (a ≤ x%:num) || (a ≤ y%:num).
Lemma num_lee_maxl a x y :
maxe x%:num y%:num ≤ a = (x%:num ≤ a) && (y%:num ≤ a).
Lemma num_lee_minr a x y :
a ≤ mine x%:num y%:num = (a ≤ x%:num) && (a ≤ y%:num).
Lemma num_lee_minl a x y :
mine x%:num y%:num ≤ a = (x%:num ≤ a) || (y%:num ≤ a).
Lemma num_lte_maxr a x y :
a < maxe x%:num y%:num = (a < x%:num) || (a < y%:num).
Lemma num_lte_maxl a x y :
maxe x%:num y%:num < a = (x%:num < a) && (y%:num < a).
Lemma num_lte_minr a x y :
a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).
Lemma num_lte_minl a x y :
mine x%:num y%:num < a = (x%:num < a) || (y%:num < a).
End MorphReal.
Section MorphGe0.
Context {R : numDomainType} {nz : KnownSign.nullity}.
Implicit Type x y : nR.
Lemma num_abse_le a x : 0 ≤ a → (`|a|%:nng ≤ x)%O = (a ≤ x%:num).
Lemma num_abse_lt a x : 0 ≤ a → (`|a|%:nng < x)%O = (a < x%:num).
End MorphGe0.
Variant posnume_spec (R : numDomainType) (x : \bar R) :
\bar R → bool → bool → bool → Type :=
| IsPinftyPosnume :
posnume_spec x +oo false true true
| IsRealPosnume (p : {posnum R}) :
posnume_spec x (p%:num%:E) false true true.
Lemma posnumeP (R : numDomainType) (x : \bar R) : 0 < x →
posnume_spec x x (x == 0) (0 ≤ x) (0 < x).
Variant nonnege_spec (R : numDomainType) (x : \bar R) :
\bar R → bool → Type :=
| IsPinftyNonnege : nonnege_spec x +oo true
| IsRealNonnege (p : {nonneg R}) : nonnege_spec x (p%:num%:E) true.
Lemma nonnegeP (R : numDomainType) (x : \bar R) : 0 ≤ x →
nonnege_spec x x (0 ≤ x).
Section contract_expand.
Variable R : realFieldType.
Implicit Types (x : \bar R) (r : R).
Local Open Scope ereal_scope.
Definition contract x : R :=
match x with
| r%:E ⇒ r / (1 + `|r|) | +oo ⇒ 1 | -oo ⇒ -1
end.
Lemma contract_lt1 r : (`|contract r%:E| < 1)%R.
Lemma contract_le1 x : (`|contract x| ≤ 1)%R.
Lemma contract0 : contract 0 = 0%R.
Lemma contractN x : contract (- x) = (- contract x)%R.
TODO: not exploited yet: expand is nondecreasing everywhere so it should be
possible to use some of the homoRL/homoLR lemma where monoRL/monoLR do not
apply
Definition expand r : \bar R :=
if (r ≥ 1)%R then +oo else if (r ≤ -1)%R then -oo else (r / (1 - `|r|))%:E.
Lemma expand1 r : (1 ≤ r)%R → expand r = +oo.
Lemma expandN r : expand (- r)%R = - expand r.
Lemma expandN1 r : (r ≤ -1)%R → expand r = -oo.
Lemma expand0 : expand 0%R = 0.
Lemma expandK : {in [pred r | `|r| ≤ 1]%R, cancel expand contract}.
Lemma le_contract : {mono contract : x y / (x ≤ y)%O}.
Definition lt_contract := leW_mono le_contract.
Definition contract_inj := mono_inj lexx le_anti le_contract.
Lemma le_expand_in : {in [pred r | `|r| ≤ 1]%R &,
{mono expand : x y / (x ≤ y)%O}}.
Definition lt_expand := leW_mono_in le_expand_in.
Definition expand_inj := mono_inj_in lexx le_anti le_expand_in.
Lemma fine_expand r : (`|r| < 1)%R →
(fine (expand r))%:E = expand r.
Lemma le_expand : {homo expand : x y / (x ≤ y)%O}.
Lemma expand_eqoo r : (expand r == +oo) = (1 ≤ r)%R.
Lemma expand_eqNoo r : (expand r == -oo) = (r ≤ -1)%R.
End contract_expand.
Section ereal_PseudoMetric.
Variable R : realFieldType.
Implicit Types (x y : \bar R) (r : R).
Definition ereal_ball x r y := (`|contract x - contract y| < r)%R.
Lemma ereal_ball_center x r : (0 < r)%R → ereal_ball x r x.
Lemma ereal_ball_sym x y r : ereal_ball x r y → ereal_ball y r x.
Lemma ereal_ball_triangle x y z r1 r2 :
ereal_ball x r1 y → ereal_ball y r2 z → ereal_ball x (r1 + r2) z.
Lemma ereal_ballN x y (e : {posnum R}) :
ereal_ball (- x) e%:num (- y) → ereal_ball x e%:num y.
Lemma ereal_ball_ninfty_oversize (e : {posnum R}) x :
(2 < e%:num)%R → ereal_ball -oo e%:num x.
Lemma contract_ereal_ball_pinfty r (e : {posnum R}) :
(1 < contract r%:E + e%:num)%R → ereal_ball r%:E e%:num +oo.
End ereal_PseudoMetric.
if (r ≥ 1)%R then +oo else if (r ≤ -1)%R then -oo else (r / (1 - `|r|))%:E.
Lemma expand1 r : (1 ≤ r)%R → expand r = +oo.
Lemma expandN r : expand (- r)%R = - expand r.
Lemma expandN1 r : (r ≤ -1)%R → expand r = -oo.
Lemma expand0 : expand 0%R = 0.
Lemma expandK : {in [pred r | `|r| ≤ 1]%R, cancel expand contract}.
Lemma le_contract : {mono contract : x y / (x ≤ y)%O}.
Definition lt_contract := leW_mono le_contract.
Definition contract_inj := mono_inj lexx le_anti le_contract.
Lemma le_expand_in : {in [pred r | `|r| ≤ 1]%R &,
{mono expand : x y / (x ≤ y)%O}}.
Definition lt_expand := leW_mono_in le_expand_in.
Definition expand_inj := mono_inj_in lexx le_anti le_expand_in.
Lemma fine_expand r : (`|r| < 1)%R →
(fine (expand r))%:E = expand r.
Lemma le_expand : {homo expand : x y / (x ≤ y)%O}.
Lemma expand_eqoo r : (expand r == +oo) = (1 ≤ r)%R.
Lemma expand_eqNoo r : (expand r == -oo) = (r ≤ -1)%R.
End contract_expand.
Section ereal_PseudoMetric.
Variable R : realFieldType.
Implicit Types (x y : \bar R) (r : R).
Definition ereal_ball x r y := (`|contract x - contract y| < r)%R.
Lemma ereal_ball_center x r : (0 < r)%R → ereal_ball x r x.
Lemma ereal_ball_sym x y r : ereal_ball x r y → ereal_ball y r x.
Lemma ereal_ball_triangle x y z r1 r2 :
ereal_ball x r1 y → ereal_ball y r2 z → ereal_ball x (r1 + r2) z.
Lemma ereal_ballN x y (e : {posnum R}) :
ereal_ball (- x) e%:num (- y) → ereal_ball x e%:num y.
Lemma ereal_ball_ninfty_oversize (e : {posnum R}) x :
(2 < e%:num)%R → ereal_ball -oo e%:num x.
Lemma contract_ereal_ball_pinfty r (e : {posnum R}) :
(1 < contract r%:E + e%:num)%R → ereal_ball r%:E e%:num +oo.
End ereal_PseudoMetric.
TODO: generalize to numFieldType?