Library mathcomp.analysis.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
-------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import finmap.
Require Import boolp classical_sets reals posnum topology.
--------------------------------------------------------------------
Copyright (c) - 2015--2016 - IMDEA Software Institute
Copyright (c) - 2015--2018 - Inria
Copyright (c) - 2016--2018 - Polytechnique
-------------------------------------------------------------------- *)
From mathcomp Require Import all_ssreflect all_algebra.
From mathcomp Require Import finmap.
Require Import boolp classical_sets reals posnum 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.
\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
+%dE == dual addition for extended reals
(-oo + +oo = +oo instead of -oo)
Import DualAddTheory for related lemmas
x +? y == the addition of the extended real numbers x and
and y is defined, i.e., it is neither +oo - oo
nor -oo + oo
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
ereal_sup E == supremum of E
ereal_inf E == infimum of E
ereal_supremums_neq0 S == S has a supremum
Topology of extended real numbers:
ereal_topologicalType R == topology for extended real numbers over
R, a realFieldType
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]
ereal_pseudoMetricType R == pseudometric space for extended reals
over R where is a realFieldType; the
distance between x and y is defined by
`|contract x - contract y|
Filters:
ereal_dnbhs x == filter on extended real numbers that
corresponds to the deleted neighborhood
x^' if x is a real number and to
predicates that are eventually true if x
is +oo/-oo.
ereal_nbhs x == same as ereal_dnbhs where dnbhs is
replaced with nbhs.
ereal_loc_seq x == sequence that converges to x in the set
of extended real numbers.
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").
NB: in bigop.v since mathcomp 1.13.0
Lemma big_nat_widenl (R : Type) (idx : R) (op : Monoid.law idx) (m1 m2 n : nat)
(P : pred nat) (F : nat → R) :
m2 ≤ m1 →
\big[op/idx]_(m1 ≤ i < n | P i) F i =
\big[op/idx]_(m2 ≤ i < n | P i && (m1 ≤ i)) F i.
Arguments big_nat_widenl [R idx op].
(P : pred nat) (F : nat → R) :
m2 ≤ m1 →
\big[op/idx]_(m1 ≤ i < n | P i) F i =
\big[op/idx]_(m2 ≤ i < n | P i && (m1 ≤ i)) F i.
Arguments big_nat_widenl [R idx op].
NB: in bigop.v since mathcomp 1.13.0
Lemma big_geq_mkord (R : Type) (idx : R) (op : Monoid.law idx) (m n : nat)
(P : pred nat) (F : nat → R) :
\big[op/idx]_(m ≤ i < n | P i) F i =
\big[op/idx]_(i < n | P i && (m ≤ i)) F i.
Reserved Notation "'\bar' x" (at level 2, format "'\bar' x").
Declare Scope ereal_dual_scope.
Declare Scope ereal_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope ring_scope.
Variant extended (R : Type) := EFin of R | EPInf | ENInf.
Arguments EFin {R}.
Definition dual_extended := extended.
Notation "+oo" := (@EPInf _ : dual_extended _) : ereal_dual_scope.
Notation "+oo" := (@EPInf _) : ereal_scope.
Notation "-oo" := (@ENInf _ : dual_extended _) : ereal_dual_scope.
Notation "-oo" := (@ENInf _) : ereal_scope.
Notation "r %:E" := (@EFin _ r%R).
Notation "'\bar' R" := (extended R) : type_scope.
Notation "0" := (0%R%:E) : ereal_scope.
Notation "1" := (1%R%:E) : ereal_scope.
Bind Scope ereal_dual_scope with dual_extended.
Bind Scope ereal_scope with extended.
Delimit Scope ereal_dual_scope with dE.
Delimit Scope ereal_scope with E.
Local Open Scope ereal_scope.
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.
Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E ≤ y%:E) = (x ≤ y)%R.
Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E) = (x < y)%R.
Lemma lee_ninfty_eq (R : numDomainType) (x : \bar R) : (x ≤ -oo) = (x == -oo).
Lemma lee_pinfty_eq (R : numDomainType) (x : \bar R) : (+oo ≤ x) = (x == +oo).
Section ERealOrder_numDomainType.
Context {R : numDomainType}.
Lemma lte_0_pinfty : (0 : \bar R) < +oo.
Lemma lte_ninfty_0 : -oo < (0 : \bar R).
Lemma lee_0_pinfty : (0 : \bar R) ≤ +oo.
Lemma lee_ninfty_0 : -oo ≤ (0 : \bar R).
End ERealOrder_numDomainType.
Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma lte_pinfty r : r%:E < +oo.
Lemma lte_ninfty r : -oo < r%:E.
Lemma lee_pinfty x : x ≤ +oo.
Lemma lee_ninfty 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.
End ERealArith.
Notation "+%dE" := dual_adde.
Notation "+%E" := adde.
Notation "-%E" := oppe.
Notation "x + y" := (dual_adde x%dE y%dE) : ereal_dual_scope.
Notation "x + y" := (adde x y) : ereal_scope.
Notation "x - y" := (dual_adde x%dE (oppe y%dE)) : ereal_dual_scope.
Notation "x - y" := (adde x (oppe y)) : ereal_scope.
Notation "- x" := (oppe (x%dE : dual_extended _)) : ereal_dual_scope.
Notation "- x" := (oppe x) : ereal_scope.
Notation "*%E" := mule.
Notation "x * y" := (mule (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope.
Notation "x * y" := (mule x y) : ereal_scope.
Notation "`| x |" := (abse (x%dE : dual_extended _)) : ereal_dual_scope.
Notation "`| x |" := (abse x) : ereal_scope.
Arguments abse {R}.
Notation "f \+ g" := (fun x ⇒ f x + g x)%dE : ereal_dual_scope.
Notation "f \+ g" := (fun x ⇒ f x + g x)%E : ereal_scope.
Notation "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 le0R (x : \bar R) : 0 ≤ x → (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.
End ERealOrderTheory.
Section finNumPred.
Context {R : numDomainType}.
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 \in 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 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 oppe0 : - 0 = 0 :> \bar R.
Lemma oppeK : involutive (A := \bar R) -%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.
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 abse_eq0 x : (`|x| == 0) = (x == 0).
Lemma abse0 : `|0| = 0 :> \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 oppe_subset (A B : set (\bar R)) :
((A `<=` B) ↔ (-%E @` A `<=` -%E @` B))%classic.
Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).
Lemma fin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \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 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 addooe x : x != -oo → +oo + x = +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 esum_fset_ninfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) :
(\sum_(i < n) f i == -oo) = [∃ i, f i == -oo].
Lemma esum_fset_pinfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) : (∀ i, f i != -oo) →
(\sum_(i < n) f i == +oo) = [∃ i, 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 mule_ninfty_pinfty : -oo × +oo = -oo :> \bar R.
Lemma mule_pinfty_ninfty : +oo × -oo = -oo :> \bar R.
Lemma mule_pinfty_pinfty : +oo × +oo = +oo :> \bar R.
Lemma mule_ninfty_ninfty : -oo × -oo = +oo :> \bar R.
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.
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 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 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 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 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 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 desum_fset_pinfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) :
(\sum_(i < n) f i == +oo) = [∃ i, f i == +oo].
Lemma desum_fset_ninfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) : (∀ i, f i != +oo) →
(\sum_(i < n) f i == -oo) = [∃ i, 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.
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_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 mulN1e x : - 1%E × x = - x.
Lemma muleN1 x : x × - 1%E = - x.
Lemma mulrpinfty r : r%:E × +oo%E = (Num.sg r)%:E × +oo%E.
Lemma mulpinftyr r : +oo%E × r%:E = (Num.sg r)%:E × +oo%E.
Lemma mulrninfty r : r%:E × -oo%E = (Num.sg r)%:E × -oo%E.
Lemma mulninftyr r : -oo%E × r%:E = (Num.sg r)%:E × -oo%E.
Definition mulrinfty := (mulrpinfty, mulpinftyr, mulrninfty, mulninftyr).
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 : a \is a fin_num → b \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 : z \is a fin_num → 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 : x \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_subr_addr x y z : x \is a fin_num → (x < y - z) = (x + z < y).
Lemma lee_subr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_subl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + 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.
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 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 lee_opp x y : (- x ≤ - y) = (y ≤ x).
Lemma lee_abs x : x ≤ `|x|.
Lemma abse_ge0 x : 0 ≤ `|x|.
Lemma abse_id x : `| `|x| | = `|x|.
Lemma lte_absl (x y : \bar R) : (`|x| < y)%E = (- y < x < y)%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 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.
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 maxe_pinftyl : left_zero (+oo : \bar R) maxe.
Lemma maxe_pinftyr : right_zero (+oo : \bar R) maxe.
Lemma maxe_ninftyl : left_id (-oo : \bar R) maxe.
Lemma maxe_ninftyr : right_id (-oo : \bar R) maxe.
Lemma mine_ninftyl : left_zero (-oo : \bar R) mine.
Lemma mine_ninftyr : right_zero (-oo : \bar R) mine.
Lemma mine_pinftyl : left_id (+oo : \bar R) mine.
Lemma mine_pinftyr : 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.
End ERealArithTh_realDomainType.
Arguments lee_sum_nneg_ord {R}.
Arguments lee_sum_npos_ord {R}.
Arguments lee_sum_nneg_natr {R}.
Arguments lee_sum_npos_natr {R}.
Arguments lee_sum_nneg_natl {R}.
Arguments lee_sum_npos_natl {R}.
Module DualAddTheoryRealDomain.
Section DualERealArithTh_realDomainType.
Import DualAddTheoryNumDomain.
Local Open Scope ereal_dual_scope.
Context {R : realDomainType}.
Implicit Types x y z a b : \bar R.
Lemma dsube_lt0 x y : (x - y < 0) = (x < y).
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 : a \is a fin_num → b \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 : z \is a fin_num → 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 : z \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_dsubr_addr x y z : y \is a fin_num → (x < y - z) = (x + z < y).
Lemma lee_dsubr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_dsubl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + 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.
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 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_pmul x1 y1 x2 y2 : 0 ≤ x1 → 0 ≤ x2 → x1 ≤ y1 → x2 ≤ y2 →
x1 × x2 ≤ y1 × y2.
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.
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 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.
Section ereal_supremum.
Variable R : realFieldType.
Local Open Scope classical_set_scope.
Implicit Types S : set (\bar R).
Implicit Types x y : \bar R.
Lemma ereal_ub_pinfty S : ubound S +oo.
Lemma ereal_ub_ninfty S : ubound S -oo → S = set0 ∨ S = [set -oo].
Lemma ereal_supremums_set0_ninfty : supremums (@set0 (\bar R)) -oo.
Lemma supremum_pinfty S x0 : S +oo → supremum x0 S = +oo.
Definition ereal_sup S := supremum -oo S.
Definition ereal_inf S := - ereal_sup (-%E @` S).
Lemma ereal_sup0 : ereal_sup set0 = -oo.
Lemma ereal_sup1 x : ereal_sup [set x] = x.
Lemma ereal_inf0 : ereal_inf set0 = +oo.
Lemma ereal_inf1 x : ereal_inf [set x] = x.
Lemma ub_ereal_sup S M : ubound S M → ereal_sup S ≤ M.
Lemma lb_ereal_inf S M : lbound S M → M ≤ ereal_inf S.
Lemma ub_ereal_sup_adherent S (e : {posnum R}) :
ereal_sup S \is a fin_num → ∃ x, S x ∧ (ereal_sup S - e%:num%:E < x).
Lemma lb_ereal_inf_adherent S (e : {posnum R}) :
ereal_inf S \is a fin_num → ∃ x, S x ∧ (x < ereal_inf S + e%:num%:E).
Lemma ereal_sup_gt S x : x < ereal_sup S → exists2 y, S y & x < y.
Lemma ereal_inf_lt S x : ereal_inf S < x → exists2 y, S y & y < x.
End ereal_supremum.
Section ereal_supremum_realType.
Variable R : realType.
Local Open Scope classical_set_scope.
Implicit Types S : set (\bar R).
Implicit Types x : \bar R.
Let fine_def r0 x : R := if x is r%:E then r else r0.
(P : pred nat) (F : nat → R) :
\big[op/idx]_(m ≤ i < n | P i) F i =
\big[op/idx]_(i < n | P i && (m ≤ i)) F i.
Reserved Notation "'\bar' x" (at level 2, format "'\bar' x").
Declare Scope ereal_dual_scope.
Declare Scope ereal_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope ring_scope.
Variant extended (R : Type) := EFin of R | EPInf | ENInf.
Arguments EFin {R}.
Definition dual_extended := extended.
Notation "+oo" := (@EPInf _ : dual_extended _) : ereal_dual_scope.
Notation "+oo" := (@EPInf _) : ereal_scope.
Notation "-oo" := (@ENInf _ : dual_extended _) : ereal_dual_scope.
Notation "-oo" := (@ENInf _) : ereal_scope.
Notation "r %:E" := (@EFin _ r%R).
Notation "'\bar' R" := (extended R) : type_scope.
Notation "0" := (0%R%:E) : ereal_scope.
Notation "1" := (1%R%:E) : ereal_scope.
Bind Scope ereal_dual_scope with dual_extended.
Bind Scope ereal_scope with extended.
Delimit Scope ereal_dual_scope with dE.
Delimit Scope ereal_scope with E.
Local Open Scope ereal_scope.
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.
Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E ≤ y%:E) = (x ≤ y)%R.
Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E) = (x < y)%R.
Lemma lee_ninfty_eq (R : numDomainType) (x : \bar R) : (x ≤ -oo) = (x == -oo).
Lemma lee_pinfty_eq (R : numDomainType) (x : \bar R) : (+oo ≤ x) = (x == +oo).
Section ERealOrder_numDomainType.
Context {R : numDomainType}.
Lemma lte_0_pinfty : (0 : \bar R) < +oo.
Lemma lte_ninfty_0 : -oo < (0 : \bar R).
Lemma lee_0_pinfty : (0 : \bar R) ≤ +oo.
Lemma lee_ninfty_0 : -oo ≤ (0 : \bar R).
End ERealOrder_numDomainType.
Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma lte_pinfty r : r%:E < +oo.
Lemma lte_ninfty r : -oo < r%:E.
Lemma lee_pinfty x : x ≤ +oo.
Lemma lee_ninfty 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.
End ERealArith.
Notation "+%dE" := dual_adde.
Notation "+%E" := adde.
Notation "-%E" := oppe.
Notation "x + y" := (dual_adde x%dE y%dE) : ereal_dual_scope.
Notation "x + y" := (adde x y) : ereal_scope.
Notation "x - y" := (dual_adde x%dE (oppe y%dE)) : ereal_dual_scope.
Notation "x - y" := (adde x (oppe y)) : ereal_scope.
Notation "- x" := (oppe (x%dE : dual_extended _)) : ereal_dual_scope.
Notation "- x" := (oppe x) : ereal_scope.
Notation "*%E" := mule.
Notation "x * y" := (mule (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope.
Notation "x * y" := (mule x y) : ereal_scope.
Notation "`| x |" := (abse (x%dE : dual_extended _)) : ereal_dual_scope.
Notation "`| x |" := (abse x) : ereal_scope.
Arguments abse {R}.
Notation "f \+ g" := (fun x ⇒ f x + g x)%dE : ereal_dual_scope.
Notation "f \+ g" := (fun x ⇒ f x + g x)%E : ereal_scope.
Notation "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 le0R (x : \bar R) : 0 ≤ x → (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.
End ERealOrderTheory.
Section finNumPred.
Context {R : numDomainType}.
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 \in 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 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 oppe0 : - 0 = 0 :> \bar R.
Lemma oppeK : involutive (A := \bar R) -%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.
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 abse_eq0 x : (`|x| == 0) = (x == 0).
Lemma abse0 : `|0| = 0 :> \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 oppe_subset (A B : set (\bar R)) :
((A `<=` B) ↔ (-%E @` A `<=` -%E @` B))%classic.
Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).
Lemma fin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \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 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 addooe x : x != -oo → +oo + x = +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 esum_fset_ninfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) :
(\sum_(i < n) f i == -oo) = [∃ i, f i == -oo].
Lemma esum_fset_pinfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) : (∀ i, f i != -oo) →
(\sum_(i < n) f i == +oo) = [∃ i, 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 mule_ninfty_pinfty : -oo × +oo = -oo :> \bar R.
Lemma mule_pinfty_ninfty : +oo × -oo = -oo :> \bar R.
Lemma mule_pinfty_pinfty : +oo × +oo = +oo :> \bar R.
Lemma mule_ninfty_ninfty : -oo × -oo = +oo :> \bar R.
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.
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 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 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 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 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 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 desum_fset_pinfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) :
(\sum_(i < n) f i == +oo) = [∃ i, f i == +oo].
Lemma desum_fset_ninfty
(T : choiceType) (s : {fset 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 n (f : 'I_n → \bar R) : (∀ i, f i != +oo) →
(\sum_(i < n) f i == -oo) = [∃ i, 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.
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_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 mulN1e x : - 1%E × x = - x.
Lemma muleN1 x : x × - 1%E = - x.
Lemma mulrpinfty r : r%:E × +oo%E = (Num.sg r)%:E × +oo%E.
Lemma mulpinftyr r : +oo%E × r%:E = (Num.sg r)%:E × +oo%E.
Lemma mulrninfty r : r%:E × -oo%E = (Num.sg r)%:E × -oo%E.
Lemma mulninftyr r : -oo%E × r%:E = (Num.sg r)%:E × -oo%E.
Definition mulrinfty := (mulrpinfty, mulpinftyr, mulrninfty, mulninftyr).
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 : a \is a fin_num → b \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 : z \is a fin_num → 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 : x \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_subr_addr x y z : x \is a fin_num → (x < y - z) = (x + z < y).
Lemma lee_subr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_subl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + 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.
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 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 lee_opp x y : (- x ≤ - y) = (y ≤ x).
Lemma lee_abs x : x ≤ `|x|.
Lemma abse_ge0 x : 0 ≤ `|x|.
Lemma abse_id x : `| `|x| | = `|x|.
Lemma lte_absl (x y : \bar R) : (`|x| < y)%E = (- y < x < y)%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 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.
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 maxe_pinftyl : left_zero (+oo : \bar R) maxe.
Lemma maxe_pinftyr : right_zero (+oo : \bar R) maxe.
Lemma maxe_ninftyl : left_id (-oo : \bar R) maxe.
Lemma maxe_ninftyr : right_id (-oo : \bar R) maxe.
Lemma mine_ninftyl : left_zero (-oo : \bar R) mine.
Lemma mine_ninftyr : right_zero (-oo : \bar R) mine.
Lemma mine_pinftyl : left_id (+oo : \bar R) mine.
Lemma mine_pinftyr : 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.
End ERealArithTh_realDomainType.
Arguments lee_sum_nneg_ord {R}.
Arguments lee_sum_npos_ord {R}.
Arguments lee_sum_nneg_natr {R}.
Arguments lee_sum_npos_natr {R}.
Arguments lee_sum_nneg_natl {R}.
Arguments lee_sum_npos_natl {R}.
Module DualAddTheoryRealDomain.
Section DualERealArithTh_realDomainType.
Import DualAddTheoryNumDomain.
Local Open Scope ereal_dual_scope.
Context {R : realDomainType}.
Implicit Types x y z a b : \bar R.
Lemma dsube_lt0 x y : (x - y < 0) = (x < y).
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 : a \is a fin_num → b \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 : z \is a fin_num → 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 : z \is a fin_num → (x - y < z) = (x < y + z).
Lemma lte_dsubr_addr x y z : y \is a fin_num → (x < y - z) = (x + z < y).
Lemma lee_dsubr_addr x y z : z \is a fin_num → (x ≤ y - z) = (x + z ≤ y).
Lemma lee_dsubl_addr x y z : y \is a fin_num → (x - y ≤ z) = (x ≤ z + 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.
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 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_pmul x1 y1 x2 y2 : 0 ≤ x1 → 0 ≤ x2 → x1 ≤ y1 → x2 ≤ y2 →
x1 × x2 ≤ y1 × y2.
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.
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 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.
Section ereal_supremum.
Variable R : realFieldType.
Local Open Scope classical_set_scope.
Implicit Types S : set (\bar R).
Implicit Types x y : \bar R.
Lemma ereal_ub_pinfty S : ubound S +oo.
Lemma ereal_ub_ninfty S : ubound S -oo → S = set0 ∨ S = [set -oo].
Lemma ereal_supremums_set0_ninfty : supremums (@set0 (\bar R)) -oo.
Lemma supremum_pinfty S x0 : S +oo → supremum x0 S = +oo.
Definition ereal_sup S := supremum -oo S.
Definition ereal_inf S := - ereal_sup (-%E @` S).
Lemma ereal_sup0 : ereal_sup set0 = -oo.
Lemma ereal_sup1 x : ereal_sup [set x] = x.
Lemma ereal_inf0 : ereal_inf set0 = +oo.
Lemma ereal_inf1 x : ereal_inf [set x] = x.
Lemma ub_ereal_sup S M : ubound S M → ereal_sup S ≤ M.
Lemma lb_ereal_inf S M : lbound S M → M ≤ ereal_inf S.
Lemma ub_ereal_sup_adherent S (e : {posnum R}) :
ereal_sup S \is a fin_num → ∃ x, S x ∧ (ereal_sup S - e%:num%:E < x).
Lemma lb_ereal_inf_adherent S (e : {posnum R}) :
ereal_inf S \is a fin_num → ∃ x, S x ∧ (x < ereal_inf S + e%:num%:E).
Lemma ereal_sup_gt S x : x < ereal_sup S → exists2 y, S y & x < y.
Lemma ereal_inf_lt S x : ereal_inf S < x → exists2 y, S y & y < x.
End ereal_supremum.
Section ereal_supremum_realType.
Variable R : realType.
Local Open Scope classical_set_scope.
Implicit Types S : set (\bar R).
Implicit Types x : \bar R.
Let fine_def r0 x : R := if x is r%:E then r else r0.
NB: see also fine above
Lemma ereal_supremums_neq0 S : supremums S !=set0.
Lemma ereal_sup_ub S : ubound S (ereal_sup S).
Lemma ereal_sup_ninfty S : ereal_sup S = -oo ↔ S `<=` [set -oo].
Lemma ereal_inf_lb S : lbound S (ereal_inf S).
Lemma ereal_inf_pinfty S : ereal_inf S = +oo ↔ S `<=` [set +oo].
Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A ≤ B}.
Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B ≤ A}.
End ereal_supremum_realType.
Canonical ereal_pointed (R : numDomainType) := PointedType (extended R) +oo.
Section ereal_nbhs.
Context {R : numFieldType}.
Local Open Scope ereal_scope.
Local Open Scope classical_set_scope.
Definition ereal_dnbhs (x : \bar R) (P : \bar R → Prop) : Prop :=
match x with
| r%:E ⇒ r^' (fun r ⇒ P r%:E)
| +oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, M%:E < y → P y
| -oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, y < M%:E → P y
end.
Definition ereal_nbhs (x : \bar R) (P : \bar R → Prop) : Prop :=
match x with
| x%:E ⇒ nbhs x (fun r ⇒ P r%:E)
| +oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, M%:E < y → P y
| -oo ⇒ ∃ M, M \is Num.real ∧ ∀ y, y < M%:E → P y
end.
Canonical ereal_ereal_filter :=
FilteredType (extended R) (extended R) (ereal_nbhs).
End ereal_nbhs.
Lemma ereal_nbhs_pinfty_ge (R : numFieldType) (e : {posnum R}) :
\∀ x \near +oo, e%:num%:E ≤ x.
Lemma ereal_nbhs_ninfty_le (R : numFieldType) (r : R) : (r < 0)%R →
\∀ x \near -oo, x ≤ r%:E.
Section ereal_nbhs_instances.
Context {R : numFieldType}.
Global Instance ereal_dnbhs_filter :
∀ x : \bar R, ProperFilter (ereal_dnbhs x).
Typeclasses Opaque ereal_dnbhs.
Global Instance ereal_nbhs_filter : ∀ x, ProperFilter (@ereal_nbhs R x).
Typeclasses Opaque ereal_nbhs.
End ereal_nbhs_instances.
Section ereal_topologicalType.
Variable R : realFieldType.
Lemma ereal_nbhs_singleton (p : \bar R) (A : set (\bar R)) :
ereal_nbhs p A → A p.
Lemma ereal_nbhs_nbhs (p : \bar R) (A : set (\bar R)) :
ereal_nbhs p A → ereal_nbhs p (ereal_nbhs^~ A).
Definition ereal_topologicalMixin : Topological.mixin_of (@ereal_nbhs R) :=
topologyOfFilterMixin _ ereal_nbhs_singleton ereal_nbhs_nbhs.
Canonical ereal_topologicalType := TopologicalType _ ereal_topologicalMixin.
End ereal_topologicalType.
Local Open Scope classical_set_scope.
Lemma nbhsNe (R : realFieldType) (x : \bar R) :
nbhs (- x) = [set (-%E @` A) | A in nbhs x].
Lemma nbhsNKe (R : realFieldType) (z : \bar R) (A : set (\bar R)) :
nbhs (- z) (-%E @` A) → nbhs z A.
Lemma oppe_continuous (R : realFieldType) : continuous (@oppe R).
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.
Lemma contract_imageN (S : set (\bar R)) :
contract @` (-%E @` S) = -%R @` (contract @` S).
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 contractK : cancel contract expand.
Lemma bijective_contract : {on [pred r | `|r| ≤ 1]%R, bijective contract}.
Definition le_expandLR := monoLR_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) le_expand_in.
Definition lt_expandLR := monoLR_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) lt_expand.
Definition le_expandRL := monoRL_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) le_expand_in.
Definition lt_expandRL := monoRL_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) lt_expand.
Lemma le_expand : {homo expand : x y / (x ≤ y)%O}.
Lemma contract_eq0 x : (contract x == 0%R) = (x == 0).
Lemma contract_eqN1 x : (contract x == -1) = (x == -oo).
Lemma contract_eq1 x : (contract x == 1%R) = (x == +oo).
Lemma expand_eqoo r : (expand r == +oo) = (1 ≤ r)%R.
Lemma expand_eqNoo r : (expand r == -oo) = (r ≤ -1)%R.
End contract_expand.
Section contract_expand_realType.
Variable R : realType.
Let contract := @contract R.
Lemma sup_contract_le1 S : S !=set0 → (`|sup (contract @` S)| ≤ 1)%R.
Lemma contract_sup S : S !=set0 → contract (ereal_sup S) = sup (contract @` S).
Lemma contract_inf S : S !=set0 → contract (ereal_inf S) = inf (contract @` S).
End contract_expand_realType.
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 le_ereal_ball x : {homo ereal_ball x : e e' / (e ≤ e')%R >-> e `<=` e'}.
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.
Lemma expand_ereal_ball_pinfty {e : {posnum R}} r : (e%:num ≤ 1)%R →
expand (1 - e%:num)%R < r%:E → ereal_ball +oo e%:num r%:E.
Lemma contract_ereal_ball_fin_le r r' (e : {posnum R}) : (r ≤ r')%R →
(1 ≤ contract r%:E + e%:num)%R → ereal_ball r%:E e%:num r'%:E.
Lemma contract_ereal_ball_fin_lt r r' (e : {posnum R}) : (r' < r)%R →
(contract r%:E - e%:num ≤ -1)%R → ereal_ball r%:E e%:num r'%:E.
Lemma expand_ereal_ball_fin_lt r' r (e : {posnum R}) : (r' < r)%R →
expand (contract r%:E - e%:num)%R < r'%:E →
(`|contract r%:E - e%:num| < 1)%R → ereal_ball r%:E e%:num r'%:E.
Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) :
let e' := (r - fine (expand (contract r%:E - e%:num)))%R in
ball r e' r' → (r' < r)%R →
(`|contract r%:E - (e)%:num| < 1)%R →
ereal_ball r%:E (e)%:num r'%:E.
Lemma ball_ereal_ball_fin_le r r' (e : {posnum R}) :
let e' : R := (fine (expand (contract r%:E + e%:num)) - r)%R in
ball r e' r' → (r ≤ r')%R →
(`| contract r%:E + e%:num | < 1)%R →
(ereal_ball r%:E e%:num r'%:E).
Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num ≤ 1)%R →
ereal_ball +oo e%:num `<=` A → nbhs +oo A.
Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num ≤ 1)%R →
ereal_ball -oo e%:num `<=` A → nbhs -oo A.
Lemma nbhs_oo_up_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R →
ereal_ball +oo e%:num `<=` A → nbhs +oo A.
Lemma nbhs_oo_down_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R →
ereal_ball -oo e%:num `<=` A → nbhs -oo A.
Lemma nbhs_fin_out_above r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A →
(- 1 < contract r%:E - e%:num)%R →
(1 ≤ contract r%:E + e%:num)%R →
nbhs r%:E A.
Lemma nbhs_fin_out_below r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A →
(contract r%:E - e%:num ≤ - 1)%R →
(contract r%:E + e%:num < 1)%R →
nbhs r%:E A.
Lemma nbhs_fin_out_above_below r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A →
(contract r%:E - e%:num < -1)%R →
(1 < contract r%:E + e%:num)%R →
nbhs r%:E A.
Lemma nbhs_fin_inbound r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A → nbhs r%:E A.
Lemma ereal_nbhsE : nbhs = nbhs_ (entourage_ ereal_ball).
Definition ereal_pseudoMetricType_mixin :=
PseudoMetric.Mixin ereal_ball_center ereal_ball_sym ereal_ball_triangle
erefl.
Definition ereal_uniformType_mixin : @Uniform.mixin_of (\bar R) nbhs :=
uniformityOfBallMixin ereal_nbhsE ereal_pseudoMetricType_mixin.
Canonical ereal_uniformType :=
UniformType (extended R) ereal_uniformType_mixin.
Canonical ereal_pseudoMetricType :=
PseudoMetricType (extended R) ereal_pseudoMetricType_mixin.
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 contractK : cancel contract expand.
Lemma bijective_contract : {on [pred r | `|r| ≤ 1]%R, bijective contract}.
Definition le_expandLR := monoLR_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) le_expand_in.
Definition lt_expandLR := monoLR_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) lt_expand.
Definition le_expandRL := monoRL_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) le_expand_in.
Definition lt_expandRL := monoRL_in
(in_onW_can _ predT contractK) (fun x _ ⇒ contract_le1 x) lt_expand.
Lemma le_expand : {homo expand : x y / (x ≤ y)%O}.
Lemma contract_eq0 x : (contract x == 0%R) = (x == 0).
Lemma contract_eqN1 x : (contract x == -1) = (x == -oo).
Lemma contract_eq1 x : (contract x == 1%R) = (x == +oo).
Lemma expand_eqoo r : (expand r == +oo) = (1 ≤ r)%R.
Lemma expand_eqNoo r : (expand r == -oo) = (r ≤ -1)%R.
End contract_expand.
Section contract_expand_realType.
Variable R : realType.
Let contract := @contract R.
Lemma sup_contract_le1 S : S !=set0 → (`|sup (contract @` S)| ≤ 1)%R.
Lemma contract_sup S : S !=set0 → contract (ereal_sup S) = sup (contract @` S).
Lemma contract_inf S : S !=set0 → contract (ereal_inf S) = inf (contract @` S).
End contract_expand_realType.
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 le_ereal_ball x : {homo ereal_ball x : e e' / (e ≤ e')%R >-> e `<=` e'}.
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.
Lemma expand_ereal_ball_pinfty {e : {posnum R}} r : (e%:num ≤ 1)%R →
expand (1 - e%:num)%R < r%:E → ereal_ball +oo e%:num r%:E.
Lemma contract_ereal_ball_fin_le r r' (e : {posnum R}) : (r ≤ r')%R →
(1 ≤ contract r%:E + e%:num)%R → ereal_ball r%:E e%:num r'%:E.
Lemma contract_ereal_ball_fin_lt r r' (e : {posnum R}) : (r' < r)%R →
(contract r%:E - e%:num ≤ -1)%R → ereal_ball r%:E e%:num r'%:E.
Lemma expand_ereal_ball_fin_lt r' r (e : {posnum R}) : (r' < r)%R →
expand (contract r%:E - e%:num)%R < r'%:E →
(`|contract r%:E - e%:num| < 1)%R → ereal_ball r%:E e%:num r'%:E.
Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) :
let e' := (r - fine (expand (contract r%:E - e%:num)))%R in
ball r e' r' → (r' < r)%R →
(`|contract r%:E - (e)%:num| < 1)%R →
ereal_ball r%:E (e)%:num r'%:E.
Lemma ball_ereal_ball_fin_le r r' (e : {posnum R}) :
let e' : R := (fine (expand (contract r%:E + e%:num)) - r)%R in
ball r e' r' → (r ≤ r')%R →
(`| contract r%:E + e%:num | < 1)%R →
(ereal_ball r%:E e%:num r'%:E).
Lemma nbhs_oo_up_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num ≤ 1)%R →
ereal_ball +oo e%:num `<=` A → nbhs +oo A.
Lemma nbhs_oo_down_e1 (A : set (\bar R)) (e : {posnum R}) : (e%:num ≤ 1)%R →
ereal_ball -oo e%:num `<=` A → nbhs -oo A.
Lemma nbhs_oo_up_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R →
ereal_ball +oo e%:num `<=` A → nbhs +oo A.
Lemma nbhs_oo_down_1e (A : set (\bar R)) (e : {posnum R}) : (1 < e%:num)%R →
ereal_ball -oo e%:num `<=` A → nbhs -oo A.
Lemma nbhs_fin_out_above r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A →
(- 1 < contract r%:E - e%:num)%R →
(1 ≤ contract r%:E + e%:num)%R →
nbhs r%:E A.
Lemma nbhs_fin_out_below r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A →
(contract r%:E - e%:num ≤ - 1)%R →
(contract r%:E + e%:num < 1)%R →
nbhs r%:E A.
Lemma nbhs_fin_out_above_below r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A →
(contract r%:E - e%:num < -1)%R →
(1 < contract r%:E + e%:num)%R →
nbhs r%:E A.
Lemma nbhs_fin_inbound r (e : {posnum R}) (A : set (\bar R)) :
ereal_ball r%:E e%:num `<=` A → nbhs r%:E A.
Lemma ereal_nbhsE : nbhs = nbhs_ (entourage_ ereal_ball).
Definition ereal_pseudoMetricType_mixin :=
PseudoMetric.Mixin ereal_ball_center ereal_ball_sym ereal_ball_triangle
erefl.
Definition ereal_uniformType_mixin : @Uniform.mixin_of (\bar R) nbhs :=
uniformityOfBallMixin ereal_nbhsE ereal_pseudoMetricType_mixin.
Canonical ereal_uniformType :=
UniformType (extended R) ereal_uniformType_mixin.
Canonical ereal_pseudoMetricType :=
PseudoMetricType (extended R) ereal_pseudoMetricType_mixin.
End ereal_PseudoMetric.
TODO: generalize to numFieldType?
Lemma lt_ereal_nbhs (R : realFieldType) (a b : \bar R) (r : R) :
a < r%:E → r%:E < b →
∃ delta : {posnum R},
∀ y, (`|y - r| < delta%:num)%R → (a < y%:E) && (y%:E < b).
a < r%:E → r%:E < b →
∃ delta : {posnum R},
∀ y, (`|y - r| < delta%:num)%R → (a < y%:E) && (y%:E < b).
TODO: generalize to numFieldType?
Lemma nbhs_interval (R : realFieldType) (P : R → Prop) (r : R) (a b : \bar R) :
a < r%:E → r%:E < b →
(∀ y, a < y%:E → y%:E < b → P y) →
nbhs r P.
Lemma ereal_dnbhs_le (R : numFieldType) (x : \bar R) :
ereal_dnbhs x --> ereal_nbhs x.
Lemma ereal_dnbhs_le_finite (R : numFieldType) (r : R) :
ereal_dnbhs r%:E --> nbhs r%:E.
Definition ereal_loc_seq (R : numDomainType) (x : \bar R) (n : nat) :=
match x with
| x%:E ⇒ (x + (n%:R + 1)^-1)%:E
| +oo ⇒ n%:R%:E
| -oo ⇒ - n%:R%:E
end.
Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) :
ereal_loc_seq x --> ereal_dnbhs x.
a < r%:E → r%:E < b →
(∀ y, a < y%:E → y%:E < b → P y) →
nbhs r P.
Lemma ereal_dnbhs_le (R : numFieldType) (x : \bar R) :
ereal_dnbhs x --> ereal_nbhs x.
Lemma ereal_dnbhs_le_finite (R : numFieldType) (r : R) :
ereal_dnbhs r%:E --> nbhs r%:E.
Definition ereal_loc_seq (R : numDomainType) (x : \bar R) (n : nat) :=
match x with
| x%:E ⇒ (x + (n%:R + 1)^-1)%:E
| +oo ⇒ n%:R%:E
| -oo ⇒ - n%:R%:E
end.
Lemma cvg_ereal_loc_seq (R : realType) (x : \bar R) :
ereal_loc_seq x --> ereal_dnbhs x.