Module mathcomp.reals.constructive_ereal
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra finmap.
From mathcomp Require Import mathcomp_extra interval_inference.
# Extended real numbers $\overline{R}$
Given a type R for numbers, `\bar R` is the type `R` extended with symbols
`-oo` and `+oo` (notation scope: `%E`), suitable to represent extended
real numbers. When `R` is a `numDomainType`, `\bar R` is equipped with a
canonical `porderType` and operations for addition/opposite. When `R` is a
`realDomainType`, `\bar R` is equipped with a canonical `orderType`.
Naming convention: in definition/lemma identifiers, "e" stands for an
extended number and "y" and "Ny" for `+oo` and `-oo` respectively.
Examples of notations:
| Coq definitions | | Meaning |
|-----------------------:|--|--------------------------------------------|
| `\bar R` |==| coproduct of `R` and $\{+\infty, -\infty\}$|
| | | notation for `extended (R:Type)` |
| `r%:E` |==| injects real numbers into `\bar R` |
| `+%E, -%E, *%E` |==| addition/opposite/multiplication for |
| | | extended reals |
| `er_map (f : T -> T')` |==| the `\bar T -> \bar T'` lifting of `f` |
| `sqrte` |==| square root for extended reals |
| `` `\| x \|%E `` |==| the absolute value of `x` |
| `x ^+ n` |==| iterated multiplication |
| `x *+ n` |==| iterated addition |
| `+%dE, (x *+ n)%dE` |==| dual addition/dual iterated addition |
| | | ($-\infty + +\infty = +\infty$) |
| | | Import DualAddTheory for related lemmas |
| `x +? y` |==| the addition of `x` and `y` is defined |
| | | it is neither $+\infty - \infty$ |
| | | nor $-\infty + \infty$ |
| `x *? y` |==| the multiplication of `x` and `y` is not |
| | | of the form $0 * +\infty$ or $0 * -\infty$ |
| `(_ <= _)%E`, `(_ < _)%E`,|==| comparison relations for extended reals |
| `(_ >= _)%E`, `(_ > _)%E` | | |
| `(\sum_(i in A) f i)%E`|==| bigop-like notation in scope `%E` |
|`(\prod_(i in A) f i)%E`|==| bigop-like notation in scope `%E` |
| `maxe x y, mine x y` |==| notation for the maximum/minimum |
Detailed documentation:
```
\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
er_map (f : T -> T') == the \bar T -> \bar T' lifting of f
sqrte == square root for extended reals
`| x |%E == the absolute value of x
x ^+ n == iterated multiplication
x *+ n == iterated addition
+%dE, (x *+ n)%dE == dual addition/dual iterated addition for
extended reals (-oo + +oo = +oo instead of -oo)
Import DualAddTheory for related lemmas
x +? y == the addition of the extended real numbers x and
and y is defined, i.e., it is neither +oo - oo
nor -oo + oo
x *? y == the multiplication of the extended real numbers
x and y is not of the form 0 * +oo or 0 * -oo
(_ <= _)%E, (_ < _)%E, == comparison relations for extended reals
(_ >= _)%E, (_ > _)%E
(\sum_(i in A) f i)%E == bigop-like notation in scope %E
(\prod_(i in A) f i)%E == bigop-like notation in scope %E
maxe x y, mine x y == notation for the maximum/minimum of two
extended real numbers
```
## Signed extended real numbers
```
{posnum \bar R} == interface type for elements in \bar R that are
positive, c.f., interval_inference.v,
notation in scope %E
{nonneg \bar R} == interface types for elements in \bar R that are
non-negative, c.f. interval_inference.v,
notation in scope %E
x%:pos == explicitly casts x to {posnum \bar R}, in scope %E
x%:nng == explicitly casts x to {nonneg \bar R}, in scope %E
```
## Topology of extended real numbers
```
contract == order-preserving bijective function
from extended real numbers to [-1; 1]
expand == function from real numbers to extended
real numbers that cancels contract in
[-1; 1]
```
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Reserved Notation "x %:E" (at level 2, format "x %:E").
Reserved Notation "x %:dE" (at level 2, format "x %:dE").
Reserved Notation "x +? y" (at level 50, format "x +? y").
Reserved Notation "x *? y" (at level 50, format "x *? y").
Reserved Notation "'\bar' x" (at level 2, format "'\bar' x").
Reserved Notation "'\bar' '^d' x" (at level 2, format "'\bar' '^d' x").
Reserved Notation "{ 'posnum' '\bar' R }" (at level 0,
format "{ 'posnum' '\bar' R }").
Reserved Notation "{ 'nonneg' '\bar' R }" (at level 0,
format "{ 'nonneg' '\bar' R }").
Declare Scope ereal_dual_scope.
Declare Scope ereal_scope.
Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.
Variant extended (R : Type) := EFin of R | EPInf | ENInf.
Arguments EFin {R}.
Lemma EFin_inj T : injective (@EFin T).
Proof.
by move=> a b; case. Qed.
Definition dual_extended := extended.
Definition dEFin : forall {R}, R -> dual_extended R := @EFin.
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 %:dE" := (@EFin _ r%R : dual_extended _) : ereal_dual_scope.
Notation "r %:E" := (@EFin _ r%R : dual_extended _) : ereal_dual_scope.
Notation "r %:E" := (@EFin _ r%R).
Notation "'\bar' R" := (extended R) : type_scope.
Notation "'\bar' '^d' R" := (dual_extended R) : type_scope.
Notation "0" := (@GRing.zero (\bar^d _)) : ereal_dual_scope.
Notation "0" := (@GRing.zero (\bar _)) : ereal_scope.
Notation "1" := (1%R%:E : dual_extended _) : ereal_dual_scope.
Notation "1" := (1%R%:E) : ereal_scope.
Bind Scope ereal_dual_scope with dual_extended.
Bind Scope ereal_scope with extended.
Delimit Scope ereal_dual_scope with dE.
Delimit Scope ereal_scope with E.
Local Open Scope ereal_scope.
Definition er_map T T' (f : T -> T') (x : \bar T) : \bar T' :=
match x with
| r%:E => (f r)%:E
| +oo => +oo
| -oo => -oo
end.
Lemma er_map_idfun T (x : \bar T) : er_map idfun x = x.
Proof.
by case: x. Qed.
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.
HB.instance Definition _ := hasDecEq.Build (\bar R) ereal_eqP.
Lemma eqe (r1 r2 : R) : (r1%:E == r2%:E) = (r1 == r2)
Proof.
by []. Qed.
End EqEReal.
Section ERealChoice.
Variable (R : choiceType).
Definition code (x : \bar R) :=
match x with
| r%:E => GenTree.Node 0 [:: GenTree.Leaf r]
| +oo => GenTree.Node 1 [::]
| -oo => GenTree.Node 2 [::]
end.
Definition decode (x : GenTree.tree R) : option (\bar R) :=
match x with
| GenTree.Node 0 [:: GenTree.Leaf r] => Some r%:E
| GenTree.Node 1 [::] => Some +oo
| GenTree.Node 2 [::] => Some -oo
| _ => None
end.
Lemma codeK : pcancel code decode
Proof.
by case. Qed.
HB.instance Definition _ := Choice.copy (\bar R) (pcan_type codeK).
End ERealChoice.
Section ERealCount.
Variable (R : countType).
HB.instance Definition _ := PCanIsCountable (@codeK R).
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.
Proof.
by case => /=. Qed.
Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
Lemma le_trans_ereal : ssrbool.transitive le_ereal.
Proof.
case=> [?||][?||][?||] //=; rewrite -?comparabler0; first exact: le_trans.
by move=> /le_comparable cmp /(comparabler_trans cmp).
by move=> cmp /ge_comparable /comparabler_trans; apply.
Qed.
by move=> /le_comparable cmp /(comparabler_trans cmp).
by move=> cmp /ge_comparable /comparabler_trans; apply.
Qed.
Fact ereal_display : Order.disp_t
Proof.
by []. Qed.
HB.instance Definition _ := Order.isPOrder.Build ereal_display (\bar R)
lt_def_ereal le_refl_ereal le_anti_ereal le_trans_ereal.
Lemma leEereal x y : (x <= y)%O = le_ereal x y
Proof.
by []. Qed.
Proof.
by []. Qed.
End ERealOrder.
Notation lee := (@Order.le ereal_display _) (only parsing).
Notation "@ 'lee' R" :=
(@Order.le ereal_display R) (at level 10, R at level 8, only parsing).
Notation lte := (@Order.lt ereal_display _) (only parsing).
Notation "@ 'lte' R" :=
(@Order.lt ereal_display R) (at level 10, R at level 8, only parsing).
Notation gee := (@Order.ge ereal_display _) (only parsing).
Notation "@ 'gee' R" :=
(@Order.ge ereal_display R) (at level 10, R at level 8, only parsing).
Notation gte := (@Order.gt ereal_display _) (only parsing).
Notation "@ 'gte' R" :=
(@Order.gt ereal_display R) (at level 10, R at level 8, only parsing).
Notation "x <= y" := (lee x y) (only printing) : ereal_dual_scope.
Notation "x <= y" := (lee x y) (only printing) : ereal_scope.
Notation "x < y" := (lte x y) (only printing) : ereal_dual_scope.
Notation "x < y" := (lte x y) (only printing) : ereal_scope.
Notation "x <= y <= z" := ((lee x y) && (lee y z)) (only printing) : ereal_dual_scope.
Notation "x <= y <= z" := ((lee x y) && (lee y z)) (only printing) : ereal_scope.
Notation "x < y <= z" := ((lte x y) && (lee y z)) (only printing) : ereal_dual_scope.
Notation "x < y <= z" := ((lte x y) && (lee y z)) (only printing) : ereal_scope.
Notation "x <= y < z" := ((lee x y) && (lte y z)) (only printing) : ereal_dual_scope.
Notation "x <= y < z" := ((lee x y) && (lte y z)) (only printing) : ereal_scope.
Notation "x < y < z" := ((lte x y) && (lte y z)) (only printing) : ereal_dual_scope.
Notation "x < y < z" := ((lte x y) && (lte y z)) (only printing) : ereal_scope.
Notation "x <= y" := (lee (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope.
Notation "x <= y" := (lee (x : extended _) (y : extended _)) : ereal_scope.
Notation "x < y" := (lte (x%dE : dual_extended _) (y%dE : dual_extended _)) : ereal_dual_scope.
Notation "x < y" := (lte (x : extended _) (y : extended _)) : ereal_scope.
Notation "x >= y" := (y <= x) (only parsing) : ereal_dual_scope.
Notation "x >= y" := (y <= x) (only parsing) : ereal_scope.
Notation "x > y" := (y < x) (only parsing) : ereal_dual_scope.
Notation "x > y" := (y < x) (only parsing) : ereal_scope.
Notation "x <= y <= z" := ((x <= y) && (y <= z)) : ereal_dual_scope.
Notation "x <= y <= z" := ((x <= y) && (y <= z)) : ereal_scope.
Notation "x < y <= z" := ((x < y) && (y <= z)) : ereal_dual_scope.
Notation "x < y <= z" := ((x < y) && (y <= z)) : ereal_scope.
Notation "x <= y < z" := ((x <= y) && (y < z)) : ereal_dual_scope.
Notation "x <= y < z" := ((x <= y) && (y < z)) : ereal_scope.
Notation "x < y < z" := ((x < y) && (y < z)) : ereal_dual_scope.
Notation "x < y < z" := ((x < y) && (y < z)) : ereal_scope.
Notation "x <= y :> T" := ((x : T) <= (y : T)) (only parsing) : ereal_scope.
Notation "x < y :> T" := ((x : T) < (y : T)) (only parsing) : ereal_scope.
Section ERealZsemimodule.
Context {R : nmodType}.
Implicit Types x y z : \bar R.
Definition adde x y :=
match x, y with
| x%:E , y%:E => (x + y)%:E
| -oo, _ => -oo
| _ , -oo => -oo
| +oo, _ => +oo
| _ , +oo => +oo
end.
Arguments adde : simpl never.
Definition dual_adde x y :=
match x, y with
| x%:E , y%:E => (x + y)%R%:E
| +oo, _ => +oo
| _ , +oo => +oo
| -oo, _ => -oo
| _ , -oo => -oo
end.
Arguments dual_adde : simpl never.
Lemma addeA_subproof : associative (S := \bar R) adde.
Lemma addeC_subproof : commutative (S := \bar R) adde.
Lemma add0e_subproof : left_id (0%:E : \bar R) adde.
HB.instance Definition _ := GRing.isNmodule.Build (\bar R)
addeA_subproof addeC_subproof add0e_subproof.
Lemma daddeA_subproof : associative (S := \bar^d R) dual_adde.
Lemma daddeC_subproof : commutative (S := \bar^d R) dual_adde.
Lemma dadd0e_subproof : left_id (0%:dE%dE : \bar^d R) dual_adde.
HB.instance Definition _ := Choice.on (\bar^d R).
HB.instance Definition _ := GRing.isNmodule.Build (\bar^d R)
daddeA_subproof daddeC_subproof dadd0e_subproof.
Definition enatmul x n : \bar R := iterop n +%R x 0.
Definition ednatmul (x : \bar^d R) n : \bar^d R := iterop n +%R x 0.
End ERealZsemimodule.
Arguments adde : simpl never.
Arguments dual_adde : simpl never.
Section ERealOrder_numDomainType.
Context {R : numDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma lee_fin (r s : R) : (r%:E <= s%:E) = (r <= s)%R
Proof.
by []. Qed.
Lemma lte_fin (r s : R) : (r%:E < s%:E) = (r < s)%R
Proof.
by []. Qed.
Lemma lee01 : 0 <= 1 :> \bar R
Proof.
Lemma lte01 : 0 < 1 :> \bar R
Proof.
Lemma leeNy_eq x : (x <= -oo) = (x == -oo)
Proof.
by case: x. Qed.
Lemma leye_eq x : (+oo <= x) = (x == +oo)
Proof.
by case: x. Qed.
Lemma lt0y : (0 : \bar R) < +oo
Proof.
Lemma ltNy0 : -oo < (0 : \bar R)
Proof.
Lemma le0y : (0 : \bar R) <= +oo
Proof.
Lemma leNy0 : -oo <= (0 : \bar R)
Proof.
Lemma cmp0y : ((0 : \bar R) >=< +oo%E)%O.
Proof.
Lemma cmp0Ny : ((0 : \bar R) >=< -oo%E)%O.
Proof.
Lemma lt0e x : (0 < x) = (x != 0) && (0 <= x).
Lemma ereal_comparable x y : (0%E >=< x)%O -> (0%E >=< y)%O -> (x >=< y)%O.
Proof.
move: x y => [x||] [y||] //; rewrite /Order.comparable !lee_fin -!realE.
- exact: real_comparable.
- by rewrite /lee/= => ->.
- by rewrite /lee/= => _ ->.
Qed.
- exact: real_comparable.
- by rewrite /lee/= => ->.
- by rewrite /lee/= => _ ->.
Qed.
Lemma real_ltry r : r%:E < +oo = (r \is Num.real)
Proof.
by []. Qed.
Proof.
by []. Qed.
Lemma real_leey x : (x <= +oo) = (fine x \is Num.real).
Proof.
Lemma real_leNye x : (-oo <= x) = (fine x \is Num.real).
Proof.
Lemma minye : left_id (+oo : \bar R) Order.min.
Proof.
by case. Qed.
Lemma real_miney (x : \bar R) : (0 >=< x)%O -> Order.min x +oo = x.
Lemma real_minNye (x : \bar R) : (0 >=< x)%O -> Order.min -oo%E x = -oo%E.
Proof.
Lemma mineNy : right_zero (-oo : \bar R) Order.min.
Proof.
Lemma maxye : left_zero (+oo : \bar R) Order.max.
Proof.
by case. Qed.
Lemma real_maxey (x : \bar R) : (0 >=< x)%O -> Order.max x +oo = +oo.
Lemma real_maxNye (x : \bar R) : (0 >=< x)%O -> Order.max -oo%E x = x.
Proof.
Lemma maxeNy : right_id (-oo : \bar R) Order.max.
Proof.
Lemma gee0P x : 0 <= x <-> x = +oo \/ exists2 r, (r >= 0)%R & x = r%:E.
Proof.
split=> [|[->|[r r0 ->//]]]; last by rewrite real_leey/=.
by case: x => [r r0 | _ |//]; [right; exists r|left].
Qed.
by case: x => [r r0 | _ |//]; [right; exists r|left].
Qed.
Lemma fine0 : fine 0 = 0%R :> R
Proof.
by []. Qed.
Proof.
by []. Qed.
End ERealOrder_numDomainType.
#[global] Hint Resolve lee01 lte01 : core.
Section ERealOrder_realDomainType.
Context {R : realDomainType}.
Implicit Types (x y : \bar R) (r : R).
Lemma ltry r : r%:E < +oo
Proof.
Lemma ltey x : (x < +oo) = (x != +oo).
Proof.
Lemma ltNyr r : -oo < r%:E
Proof.
Lemma ltNye x : (-oo < x) = (x != -oo).
Proof.
Lemma leey x : x <= +oo
Proof.
Lemma leNye x : -oo <= x
Proof.
Definition lteey := (ltey, leey).
Definition lteNye := (ltNye, leNye).
Lemma le_er_map (f : R -> R) : {homo f : x y / (x <= y)%R} ->
{homo er_map f : x y / x <= y}.
Lemma le_total_ereal : total (Order.le : rel (\bar R)).
HB.instance Definition _ := Order.POrder_isTotal.Build ereal_display (\bar R)
le_total_ereal.
HB.instance Definition _ := Order.hasBottom.Build ereal_display (\bar R) leNye.
HB.instance Definition _ := Order.hasTop.Build ereal_display (\bar R) leey.
End ERealOrder_realDomainType.
Section ERealZmodule.
Context {R : zmodType}.
Implicit Types x y z : \bar R.
Definition oppe x :=
match x with
| r%:E => (- r)%:E
| -oo => +oo
| +oo => -oo
end.
End ERealZmodule.
Section ERealArith.
Context {R : numDomainType}.
Implicit Types x y z : \bar R.
Definition mule 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.
Arguments mule : simpl never.
Definition abse x : \bar R := if x is r%:E then `|r|%:E else +oo.
Definition expe x n := iterop n mule x 1.
End ERealArith.
Arguments mule : simpl never.
Notation "+%dE" := (@GRing.add (\bar^d _)).
Notation "+%E" := (@GRing.add (\bar _)).
Notation "-%E" := oppe.
Notation "x + y" := (GRing.add (x%dE : \bar^d _) y%dE) : ereal_dual_scope.
Notation "x + y" := (GRing.add x%E y%E) : ereal_scope.
Notation "x - y" := ((x%dE : \bar^d _) + oppe y%dE) : ereal_dual_scope.
Notation "x - y" := (x%E + (oppe y%E)) : ereal_scope.
Notation "- x" := (oppe x%dE : \bar^d _) : ereal_dual_scope.
Notation "- x" := (oppe x%E) : ereal_scope.
Notation "*%E" := mule.
Notation "x * y" := (mule x%dE y%dE : \bar^d _) : ereal_dual_scope.
Notation "x * y" := (mule x%E y%E) : ereal_scope.
Notation "`| x |" := (abse x%dE : \bar^d _) : ereal_dual_scope.
Notation "`| x |" := (abse x%E) : ereal_scope.
Arguments abse {R}.
Notation "x ^+ n" := (expe x%dE n : \bar^d _) : ereal_dual_scope.
Notation "x ^+ n" := (expe x%E n) : ereal_scope.
Notation "x *+ n" := (ednatmul x%dE n) : ereal_dual_scope.
Notation "x *+ n" := (enatmul x%E n) : ereal_scope.
Notation "\- f" := (fun x => - f x)%dE : ereal_dual_scope.
Notation "\- f" := (fun x => - f x)%E : ereal_scope.
Notation "f \+ g" := (fun x => f x + g x)%dE : ereal_dual_scope.
Notation "f \+ g" := (fun x => f x + g x)%E : ereal_scope.
Notation "f \* g" := (fun x => f x * g x)%dE : ereal_dual_scope.
Notation "f \* g" := (fun x => f x * g x)%E : ereal_scope.
Notation "f \- g" := (fun x => f x - g x)%dE : ereal_dual_scope.
Notation "f \- g" := (fun x => f x - g x)%E : ereal_scope.
Notation "\sum_ ( i <- r | P ) F" :=
(\big[+%dE/0%dE]_(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%dE]_(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%dE]_(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%dE]_(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%dE]_(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%dE]_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%dE]_(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%dE]_(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%dE]_(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%dE]_(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%dE]_(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%dE]_(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.
Notation "\prod_ ( i <- r | P ) F" :=
(\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope.
Notation "\prod_ ( i <- r ) F" :=
(\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope.
Notation "\prod_ ( m <= i < n | P ) F" :=
(\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope.
Notation "\prod_ ( m <= i < n ) F" :=
(\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope.
Notation "\prod_ ( i | P ) F" :=
(\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope.
Notation "\prod_ i F" :=
(\big[*%E/1%:E]_i F%E) : ereal_scope.
Notation "\prod_ ( i : t | P ) F" :=
(\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope.
Notation "\prod_ ( i : t ) F" :=
(\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope.
Notation "\prod_ ( i < n | P ) F" :=
(\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope.
Notation "\prod_ ( i < n ) F" :=
(\big[*%E/1%:E]_(i < n) F%E) : ereal_scope.
Notation "\prod_ ( i 'in' A | P ) F" :=
(\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope.
Notation "\prod_ ( i 'in' A ) F" :=
(\big[*%E/1%:E]_(i in A) F%E) : ereal_scope.
Section ERealOrderTheory.
Context {R : numDomainType}.
Implicit Types x y z : \bar R.
Local Tactic Notation "elift" constr(lm) ":" ident(x) :=
by case: x => [||?]; first by rewrite ?eqe; apply: lm.
Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) :=
by case: x y => [?||] [?||]; first by rewrite ?eqe; apply: lm.
Local Tactic Notation "elift" constr(lm) ":" ident(x) ident(y) ident(z) :=
by case: x y z => [?||] [?||] [?||]; first by rewrite ?eqe; apply: lm.
Lemma lee0N1 : 0 <= (-1)%:E :> \bar R = false.
Lemma lte0N1 : 0 < (-1)%:E :> \bar R = false.
Lemma lteN10 : - 1%E < 0 :> \bar R.
Lemma leeN10 : - 1%E <= 0 :> \bar R.
Lemma lte0n n : (0 < n%:R%:E :> \bar R) = (0 < n)%N.
Lemma lee0n n : (0 <= n%:R%:E :> \bar R) = (0 <= n)%N.
Lemma lte1n n : (1 < n%:R%:E :> \bar R) = (1 < n)%N.
Lemma lee1n n : (1 <= n%:R%:E :> \bar R) = (1 <= n)%N.
Lemma fine_ge0 x : 0 <= x -> (0 <= fine x)%R.
Proof.
by case: x. Qed.
Lemma fine_gt0 x : 0 < x < +oo -> (0 < fine x)%R.
Lemma fine_lt0 x : -oo < x < 0 -> (fine x < 0)%R.
Lemma fine_le0 x : x <= 0 -> (fine x <= 0)%R.
Proof.
by case: x. Qed.
Lemma lee_tofin (r0 r1 : R) : (r0 <= r1)%R -> r0%:E <= r1%:E.
Proof.
by []. Qed.
Lemma lte_tofin (r0 r1 : R) : (r0 < r1)%R -> r0%:E < r1%:E.
Proof.
by []. Qed.
Lemma enatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar R.
Proof.
by elim: n => //= n ->. Qed.
Lemma enatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar R.
Proof.
by elim: n => //= n ->. Qed.
Lemma EFin_natmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.
Proof.
by elim: n => //= n <-. Qed.
Lemma mule2n x : x *+ 2 = x + x
Proof.
by []. Qed.
Lemma expe2 x : x ^+ 2 = x * x
Proof.
by []. Qed.
Lemma leeN2 : {mono @oppe R : x y /~ x <= y}.
Proof.
Lemma lteN2 : {mono @oppe R : x y /~ x < y}.
Proof.
End ERealOrderTheory.
#[global] Hint Resolve leeN10 lteN10 : core.
Section finNumPred.
Context {R : numDomainType}.
Implicit Type (x : \bar R).
Definition fin_num := [qualify a x : \bar R | (x != -oo) && (x != +oo)].
Fact fin_num_key : pred_key fin_num
Proof.
by []. Qed.
Lemma fin_numE x : (x \is a fin_num) = (x != -oo) && (x != +oo).
Proof.
by []. Qed.
Lemma fin_numP x : reflect ((x != -oo) /\ (x != +oo)) (x \is a fin_num).
Lemma fin_numEn x : (x \isn't a fin_num) = (x == -oo) || (x == +oo).
Lemma fin_numPn x : reflect (x = -oo \/ x = +oo) (x \isn't a fin_num).
Lemma fin_real x : -oo < x < +oo -> x \is a fin_num.
Lemma fin_num_abs x : (x \is a fin_num) = (`| x | < +oo)%E.
Proof.
End finNumPred.
Section ERealArithTh_numDomainType.
Context {R : numDomainType}.
Implicit Types (x y z : \bar R) (r : R).
Lemma fine_le : {in fin_num &, {homo @fine R : x y / x <= y >-> (x <= y)%R}}.
Proof.
by move=> [? [?| |]| |]. Qed.
Lemma fine_lt : {in fin_num &, {homo @fine R : x y / x < y >-> (x < y)%R}}.
Proof.
by move=> [? [?| |]| |]. Qed.
Lemma abse_EFin r : `|r%:E|%E = `|r|%:E.
Proof.
by []. Qed.
Lemma fine_abse : {in fin_num, {morph @fine R : x / `|x| >-> `|x|%R}}.
Proof.
by case. Qed.
Lemma abse_fin_num x : (`|x| \is a fin_num) = (x \is a fin_num).
Proof.
by case: x. Qed.
Lemma fine_eq0 x : x \is a fin_num -> (fine x == 0%R) = (x == 0).
Proof.
Lemma EFinN r : (- r)%:E = (- r%:E)
Proof.
by []. Qed.
Lemma fineN x : fine (- x) = (- fine x)%R.
Proof.
Lemma EFinD r r' : (r + r')%:E = r%:E + r'%:E
Proof.
by []. Qed.
Lemma EFin_semi_additive : @semi_additive _ (\bar R) EFin
Proof.
by split. Qed.
EFin_semi_additive.
Lemma EFinB r r' : (r - r')%:E = r%:E - r'%:E
Proof.
by []. Qed.
Lemma EFinM r r' : (r * r')%:E = r%:E * r'%:E
Proof.
by []. Qed.
Lemma sumEFin I s P (F : I -> R) :
\sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.
Lemma EFin_min : {morph (@EFin R) : r s / Num.min r s >-> Order.min r s}.
Lemma EFin_max : {morph (@EFin R) : r s / Num.max r s >-> Order.max r s}.
Definition adde_def x y :=
~~ ((x == +oo) && (y == -oo)) && ~~ ((x == -oo) && (y == +oo)).
Local Notation "x +? y" := (adde_def x y).
Lemma adde_defC x y : x +? y = y +? x.
Lemma fin_num_adde_defr x y : x \is a fin_num -> x +? y.
Proof.
by move: x y => [x| |] [y | |]. Qed.
Lemma fin_num_adde_defl x y : y \is a fin_num -> x +? y.
Proof.
Lemma adde_defN x y : x +? - y = - x +? y.
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma adde_defDr x y z : x +? y -> x +? z -> x +? (y + z).
Proof.
by move: x y z => [x||] [y||] [z||]. Qed.
Lemma adde_defEninfty x : (x +? -oo) = (x != +oo).
Proof.
by case: x. Qed.
Lemma ge0_adde_def : {in [pred x | x >= 0] &, forall x y, x +? y}.
Proof.
by move=> [x| |] [y| |]. Qed.
Lemma addeC : commutative (S := \bar R) +%E
Proof.
Lemma adde0 : right_id (0 : \bar R) +%E
Proof.
Lemma add0e : left_id (0 : \bar R) +%E
Proof.
Lemma addeA : associative (S := \bar R) +%E
Proof.
Lemma adde_def_sum I h t (P : pred I) (f : I -> \bar R) :
{in P, forall i : I, f h +? f i} ->
f h +? \sum_(j <- t | P j) f j.
Proof.
move=> fhi; elim/big_rec : _; first by rewrite fin_num_adde_defl.
by move=> i x Pi fhx; rewrite adde_defDr// fhi.
Qed.
by move=> i x Pi fhx; rewrite adde_defDr// fhi.
Qed.
Lemma addeAC : @right_commutative (\bar R) _ +%E.
Lemma addeCA : @left_commutative (\bar R) _ +%E.
Lemma addeACA : @interchange (\bar R) +%E +%E.
Lemma adde_gt0 x y : 0 < x -> 0 < y -> 0 < x + y.
Lemma padde_eq0 x y : 0 <= x -> 0 <= y -> (x + y == 0) = (x == 0) && (y == 0).
Proof.
Lemma nadde_eq0 x y : x <= 0 -> y <= 0 -> (x + y == 0) = (x == 0) && (y == 0).
Proof.
Lemma realDe x y : (0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x + y)%O.
Proof.
Lemma oppe0 : - 0 = 0 :> \bar R.
Proof.
Lemma oppeK : involutive (A := \bar R) -%E.
Proof.
Lemma oppe_inj : @injective (\bar R) _ -%E.
Lemma adde_defNN x y : - x +? - y = x +? y.
Lemma oppe_eq0 x : (- x == 0)%E = (x == 0)%E.
Lemma oppeD x y : x +? y -> - (x + y) = - x - y.
Proof.
Lemma fin_num_oppeD x y : y \is a fin_num -> - (x + y) = - x - y.
Proof.
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
Proof.
Proof.
Lemma mule1 x : x * 1 = x.
Lemma mul1e x : 1 * x = x.
Lemma mule0 x : x * 0 = 0.
Lemma mul0e x : 0 * x = 0.
HB.instance Definition _ := Monoid.isMulLaw.Build (\bar R) 0 mule mul0e mule0.
Lemma expeS x n : x ^+ n.+1 = x * x ^+ n.
Proof.
Lemma EFin_expe r n : (r ^+ n)%:E = r%:E ^+ n.
Definition mule_def x y :=
~~ (((x == 0) && (`| y | == +oo)) || ((y == 0) && (`| x | == +oo))).
Local Notation "x *? y" := (mule_def x y).
Lemma mule_defC x y : x *? y = y *? x.
Lemma mule_def_fin x y : x \is a fin_num -> y \is a fin_num -> x *? y.
Proof.
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.
Proof.
move: x y => [x| |] [y| |] //; first by rewrite mule_def_fin.
- by have [->|?] := eqVneq x 0%R; rewrite ?mul0e ?eqxx// mule_def_neq0_infty.
- by have [->|?] := eqVneq x 0%R; rewrite ?mul0e ?eqxx// mule_def_neq0_infty.
- by have [->|?] := eqVneq y 0%R; rewrite ?mule0 ?eqxx// mule_def_infty_neq0.
- by have [->|?] := eqVneq y 0%R; rewrite ?mule0 ?eqxx// mule_def_infty_neq0.
Qed.
- by have [->|?] := eqVneq x 0%R; rewrite ?mul0e ?eqxx// mule_def_neq0_infty.
- by have [->|?] := eqVneq x 0%R; rewrite ?mul0e ?eqxx// mule_def_neq0_infty.
- by have [->|?] := eqVneq y 0%R; rewrite ?mule0 ?eqxx// mule_def_infty_neq0.
- by have [->|?] := eqVneq y 0%R; rewrite ?mule0 ?eqxx// mule_def_infty_neq0.
Qed.
Lemma ltpinfty_adde_def : {in [pred x | x < +oo] &, forall x y, x +? y}.
Proof.
by move=> [x| |] [y| |]. Qed.
Lemma ltninfty_adde_def : {in [pred x | -oo < x] &, forall x y, x +? y}.
Proof.
by move=> [x| |] [y| |]. Qed.
Lemma abse_eq0 x : (`|x| == 0) = (x == 0).
Lemma abse0 : `|0| = 0 :> \bar R
Lemma abse1 : `|1| = 1 :> \bar R
Lemma abseN x : `|- x| = `|x|.
Proof.
Lemma eqe_opp x y : (- x == - y) = (x == y).
Proof.
Lemma eqe_oppP x y : (- x = - y) <-> (x = y).
Lemma eqe_oppLR x y : (- x == y) = (x == - y).
Lemma eqe_oppLRP x y : (- x = y) <-> (x = - y).
Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).
Proof.
Lemma oppeB x y : x +? - y -> - (x - y) = - x + y.
Lemma fin_num_oppeB x y : y \is a fin_num -> - (x - y) = - x + y.
Proof.
Lemma fin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma sum_fin_num (T : Type) (s : seq T) (P : pred T) (f : T -> \bar R) :
\sum_(i <- s | P i) f i \is a fin_num =
all [pred x | x \is a fin_num] [seq f i | i <- s & P i].
Proof.
Lemma sum_fin_numP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar R) :
reflect (forall i, i \in s -> P i -> f i \is a fin_num)
(\sum_(i <- s | P i) f i \is a fin_num).
Proof.
rewrite sum_fin_num; apply: (iffP allP) => /=.
by move=> + x xs Px; apply; rewrite map_f// mem_filter Px.
by move=> + _ /mapP[x /[!mem_filter]/andP[Px xs] ->]; apply.
Qed.
by move=> + x xs Px; apply; rewrite map_f// mem_filter Px.
by move=> + _ /mapP[x /[!mem_filter]/andP[Px xs] ->]; apply.
Qed.
Lemma fin_numB x y :
(x - y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma fin_numM x y : x \is a fin_num -> y \is a fin_num ->
x * y \is a fin_num.
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma prode_fin_num (I : Type) (s : seq I) (P : pred I) (f : I -> \bar R) :
(forall i, P i -> f i \is a fin_num) ->
\prod_(i <- s | P i) f i \is a fin_num.
Lemma fin_numX x n : x \is a fin_num -> x ^+ n \is a fin_num.
Lemma fineD : {in @fin_num R &, {morph fine : x y / x + y >-> (x + y)%R}}.
Proof.
by move=> [r| |] [s| |]. Qed.
Lemma fineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.
Proof.
by move=> [r| |] [s| |]. Qed.
Lemma fineM : {in @fin_num R &, {morph fine : x y / x * y >-> (x * y)%R}}.
Proof.
by move=> [x| |] [y| |]. Qed.
Lemma fineK x : x \is a fin_num -> (fine x)%:E = x.
Proof.
by case: x. Qed.
Lemma EFin_sum_fine (I : Type) s (P : pred I) (f : I -> \bar R) :
(forall i, P i -> f i \is a fin_num) ->
(\sum_(i <- s | P i) fine (f i))%:E = \sum_(i <- s | P i) f i.
Lemma sum_fine (I : Type) s (P : pred I) (F : I -> \bar R) :
(forall i, P i -> F i \is a fin_num) ->
(\sum_(i <- s | P i) fine (F i) = fine (\sum_(i <- s | P i) F i))%R.
Proof.
Lemma sumeN I s (P : pred I) (f : I -> \bar R) :
{in P &, forall i j, f i +? f j} ->
\sum_(i <- s | P i) - f i = - \sum_(i <- s | P i) f i.
Proof.
Lemma fin_num_sumeN I s (P : pred I) (f : I -> \bar R) :
(forall i, P i -> f i \is a fin_num) ->
\sum_(i <- s | P i) - f i = - \sum_(i <- s | P i) f i.
Proof.
Lemma telescope_sume n m (f : nat -> \bar R) :
(forall i, (n <= i <= m)%N -> f i \is a fin_num) -> (n <= m)%N ->
\sum_(n <= k < m) (f k.+1 - f k) = f m - f n.
Proof.
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)).
Proof.
by move: x y => [?| |] [?| |]. Qed.
Lemma addye x : x != -oo -> +oo + x = +oo
Proof.
by case: x. Qed.
Lemma addey x : x != -oo -> x + +oo = +oo
Proof.
by case: x. Qed.
Lemma addNye x : -oo + x = -oo
Proof.
by []. Qed.
Lemma addeNy x : x + -oo = -oo
Proof.
by case: x. Qed.
Lemma adde_Neq_pinfty x y : x != -oo -> y != -oo ->
(x + y != +oo) = (x != +oo) && (y != +oo).
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma adde_Neq_ninfty x y : x != +oo -> y != +oo ->
(x + y != -oo) = (x != -oo) && (y != -oo).
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma adde_ss_eq0 x y : (0 <= x) && (0 <= y) || (x <= 0) && (y <= 0) ->
x + y == 0 = (x == 0) && (y == 0).
Lemma esum_eqNyP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar R) :
\sum_(i <- s | P i) f i = -oo <-> exists i, [/\ i \in s, P i & f i = -oo].
Proof.
split=> [|[i [si Pi fi]]].
rewrite big_seq_cond; elim/big_ind: _ => // [[?| |] [?| |]//|].
by move=> i /andP[si Pi] fioo; exists i; rewrite si Pi fioo.
rewrite big_mkcond (bigID (xpred1 i))/= (eq_bigr (fun _ => -oo)); last first.
by move=> j /eqP ->; rewrite Pi.
rewrite big_const_seq/= [X in X + _](_ : _ = -oo)//.
elim: s i Pi fi si => // h t ih i Pi fi.
rewrite inE => /predU1P[<-/=|it]; first by rewrite eqxx.
by rewrite /= iterD ih//=; case: (_ == _).
Qed.
rewrite big_seq_cond; elim/big_ind: _ => // [[?| |] [?| |]//|].
by move=> i /andP[si Pi] fioo; exists i; rewrite si Pi fioo.
rewrite big_mkcond (bigID (xpred1 i))/= (eq_bigr (fun _ => -oo)); last first.
by move=> j /eqP ->; rewrite Pi.
rewrite big_const_seq/= [X in X + _](_ : _ = -oo)//.
elim: s i Pi fi si => // h t ih i Pi fi.
rewrite inE => /predU1P[<-/=|it]; first by rewrite eqxx.
by rewrite /= iterD ih//=; case: (_ == _).
Qed.
Lemma esum_eqNy (I : finType) (f : I -> \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == -oo) = [exists i in P, f i == -oo].
Proof.
Lemma esum_eqyP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar R) :
(forall i, P i -> f i != -oo) ->
\sum_(i <- s | P i) f i = +oo <-> exists i, [/\ i \in s, P i & f i = +oo].
Proof.
move=> finoo; split=> [|[i [si Pi fi]]].
rewrite big_seq_cond; elim/big_ind: _ => // [[?| |] [?| |]//|].
by move=> i /andP[si Pi] fioo; exists i; rewrite si Pi fioo.
elim: s i Pi fi si => // h t ih i Pi fi.
rewrite inE => /predU1P[<-/=|it].
rewrite big_cons Pi fi addye//.
by apply/eqP => /esum_eqNyP[j [jt /finoo/negbTE/eqP]].
by rewrite big_cons; case: ifPn => Ph; rewrite (ih i)// addey// finoo.
Qed.
rewrite big_seq_cond; elim/big_ind: _ => // [[?| |] [?| |]//|].
by move=> i /andP[si Pi] fioo; exists i; rewrite si Pi fioo.
elim: s i Pi fi si => // h t ih i Pi fi.
rewrite inE => /predU1P[<-/=|it].
rewrite big_cons Pi fi addye//.
by apply/eqP => /esum_eqNyP[j [jt /finoo/negbTE/eqP]].
by rewrite big_cons; case: ifPn => Ph; rewrite (ih i)// addey// finoo.
Qed.
Lemma esum_eqy (I : finType) (P : {pred I}) (f : I -> \bar R) :
(forall i, P i -> f i != -oo) ->
(\sum_(i | P i) f i == +oo) = [exists i in P, f i == +oo].
Proof.
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNyP`")]
Notation esum_ninftyP := esum_eqNyP (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNy`")]
Notation esum_ninfty := esum_eqNy (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqyP`")]
Notation esum_pinftyP := esum_eqyP (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqy`")]
Notation esum_pinfty := esum_eqy (only parsing).
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).
Proof.
Lemma oppe_lt0 x : (- x < 0) = (0 < x).
Proof.
Lemma oppe_ge0 x : (0 <= - x) = (x <= 0).
Proof.
Lemma oppe_le0 x : (- x <= 0) = (0 <= x).
Proof.
Lemma oppe_cmp0 x : (0 >=< - x)%O = (0 >=< x)%O.
Proof.
Lemma sume_ge0 T (f : T -> \bar R) (P : pred T) :
(forall t, P t -> 0 <= f t) -> forall l, 0 <= \sum_(i <- l | P i) f i.
Lemma sume_le0 T (f : T -> \bar R) (P : pred T) :
(forall t, P t -> f t <= 0) -> forall l, \sum_(i <- l | P i) f i <= 0.
Lemma mulNyy : -oo * +oo = -oo :> \bar R
Lemma mulyNy : +oo * -oo = -oo :> \bar R
Lemma mulyy : +oo * +oo = +oo :> \bar R
Lemma mulNyNy : -oo * -oo = +oo :> \bar R
Proof.
by []. Qed.
Lemma real_mulry r : r \is Num.real -> r%:E * +oo = (Num.sg r)%:E * +oo.
Proof.
Lemma real_mulyr r : r \is Num.real -> +oo * r%:E = (Num.sg r)%:E * +oo.
Proof.
Lemma real_mulrNy r : r \is Num.real -> r%:E * -oo = (Num.sg r)%:E * -oo.
Proof.
Lemma real_mulNyr r : r \is Num.real -> -oo * r%:E = (Num.sg r)%:E * -oo.
Proof.
Definition real_mulr_infty := (real_mulry, real_mulyr, real_mulrNy, real_mulNyr).
Lemma mulN1e x : - 1%E * x = - x.
Proof.
Lemma muleN1 x : x * - 1%E = - x
Lemma mule_neq0 x y : x != 0 -> y != 0 -> x * y != 0.
Proof.
Lemma mule_eq0 x y : (x * y == 0) = (x == 0) || (y == 0).
Proof.
Lemma mule_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x * y.
Proof.
move: x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin, lt0y)//.
- exact: mulr_ge0.
- rewrite le_eqVlt => /predU1P[<- _|x0 _]; first by rewrite eqxx.
by rewrite gt_eqF // x0 le0y.
- move=> _; rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite eqxx.
by rewrite gt_eqF // y0 le0y.
Qed.
- exact: mulr_ge0.
- rewrite le_eqVlt => /predU1P[<- _|x0 _]; first by rewrite eqxx.
by rewrite gt_eqF // x0 le0y.
- move=> _; rewrite le_eqVlt => /predU1P[<-|y0]; first by rewrite eqxx.
by rewrite gt_eqF // y0 le0y.
Qed.
Lemma prode_ge0 (I : Type) (s : seq I) (P : pred I) (f : I -> \bar R) :
(forall i, P i -> 0 <= f i) -> 0 <= \prod_(i <- s | P i) f i.
Lemma mule_gt0 x y : 0 < x -> 0 < y -> 0 < x * y.
Lemma mule_le0 x y : x <= 0 -> y <= 0 -> 0 <= x * y.
Proof.
Lemma mule_le0_ge0 x y : x <= 0 -> 0 <= y -> x * y <= 0.
Proof.
move: x y => [x| |] [y| |] //; rewrite /mule/= ?(lee_fin, lte_fin).
- exact: mulr_le0_ge0.
- by move=> x0 _; case: ifP => _ //; rewrite lt_leAnge /= x0 andbF leNy0.
- move=> _; rewrite le_eqVlt => /predU1P[<-|->]; first by rewrite eqxx.
by case: ifP => _ //; rewrite leNy0.
- by rewrite lt0y leNy0.
Qed.
- exact: mulr_le0_ge0.
- by move=> x0 _; case: ifP => _ //; rewrite lt_leAnge /= x0 andbF leNy0.
- move=> _; rewrite le_eqVlt => /predU1P[<-|->]; first by rewrite eqxx.
by case: ifP => _ //; rewrite leNy0.
- by rewrite lt0y leNy0.
Qed.
Lemma mule_ge0_le0 x y : 0 <= x -> y <= 0 -> x * y <= 0.
Proof.
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.
Proof.
Lemma gteN x : 0 < x -> - x < x.
Lemma realMe x y : (0%E >=< x)%O -> (0%E >=< y)%O -> (0%E >=< x * y)%O.
Proof.
Lemma real_fine (x : \bar R) : (0 >=< x)%O = (fine x \in Num.real).
Proof.
Lemma real_muleN (x y : \bar R) : (0 >=< x)%O -> (0 >=< y)%O ->
x * - y = - (x * y).
Proof.
rewrite !real_fine; case: x y => [x||] [y||] /= xr yr; rewrite /mule/=.
- by rewrite mulrN.
- by case: ifP; rewrite ?oppe0//; case: ifP.
- by case: ifP; rewrite ?oppe0//; case: ifP.
- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin.
by case: (real_ltgtP xr yr) => // <-; rewrite eqxx.
- by case: ifP.
- by case: ifP.
- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin.
by case: (real_ltgtP xr yr) => // <-; rewrite eqxx.
- by rewrite lt0y.
- by rewrite lt0y.
Qed.
- by rewrite mulrN.
- by case: ifP; rewrite ?oppe0//; case: ifP.
- by case: ifP; rewrite ?oppe0//; case: ifP.
- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin.
by case: (real_ltgtP xr yr) => // <-; rewrite eqxx.
- by case: ifP.
- by case: ifP.
- rewrite EFinN oppe_eq0; case: ifP; rewrite ?oppe0// oppe_gt0 !lte_fin.
by case: (real_ltgtP xr yr) => // <-; rewrite eqxx.
- by rewrite lt0y.
- by rewrite lt0y.
Qed.
Lemma real_mulNe (x y : \bar R) : (0 >=< x)%O -> (0 >=< y)%O ->
- x * y = - (x * y).
Proof.
Lemma real_muleNN (x y : \bar R) : (0 >=< x)%O -> (0 >=< y)%O ->
- x * - y = x * y.
Proof.
Lemma sqreD x y : x + y \is a fin_num ->
(x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2.
Proof.
Lemma abse_ge0 x : 0 <= `|x|.
Lemma gee0_abs x : 0 <= x -> `|x| = x.
Lemma gte0_abs x : 0 < x -> `|x| = x
Lemma lee0_abs x : x <= 0 -> `|x| = - x.
Lemma lte0_abs x : x < 0 -> `|x| = - x.
End ERealArithTh_numDomainType.
Notation "x +? y" := (adde_def x%dE y%dE) : ereal_dual_scope.
Notation "x +? y" := (adde_def x y) : ereal_scope.
Notation "x *? y" := (mule_def x%dE y%dE) : ereal_dual_scope.
Notation "x *? y" := (mule_def x y) : ereal_scope.
Notation maxe := (@Order.max ereal_display _).
Notation "@ 'maxe' R" := (@Order.max ereal_display R)
(at level 10, R at level 8, only parsing) : function_scope.
Notation mine := (@Order.min ereal_display _).
Notation "@ 'mine' R" := (@Order.min ereal_display R)
(at level 10, R at level 8, only parsing) : function_scope.
Module DualAddTheoryNumDomain.
Section DualERealArithTh_numDomainType.
Local Open Scope ereal_dual_scope.
Context {R : numDomainType}.
Implicit Types x y z : \bar^d 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^d R) :
(\sum_(i <- r | P i) F i)%dE = - (\sum_(i <- r | P i) (- F i)%E)%E.
Proof.
Lemma dual_addeE_def x y : x +? y -> (x + y)%dE = (x + y)%E.
Proof.
by case: x => [x| |]; case: y. Qed.
Lemma dEFinD (r r' : R) : (r + r')%R%:E = r%:E + r'%:E.
Proof.
by []. Qed.
Lemma dEFinE (r : R) : dEFin r = r%:E
Proof.
by []. Qed.
Lemma dEFin_semi_additive : @semi_additive _ (\bar^d R) dEFin.
Proof.
by split. Qed.
HB.instance Definition _ := GRing.isSemiAdditive.Build R (\bar^d R) dEFin
dEFin_semi_additive.
Lemma dEFinB (r r' : R) : (r - r')%R%:E = r%:E - r'%:E.
Proof.
by []. Qed.
Lemma dsumEFin I r P (F : I -> R) :
\sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%R%:E.
Proof.
Lemma daddeC : commutative (S := \bar^d R) +%dE
Proof.
Lemma dadde0 : right_id (0 : \bar^d R) +%dE
Proof.
Lemma dadd0e : left_id (0 : \bar^d R) +%dE
Proof.
Lemma daddeA : associative (S := \bar^d R) +%dE
Proof.
Lemma daddeAC : right_commutative (S := \bar^d R) +%dE.
Lemma daddeCA : left_commutative (S := \bar^d R) +%dE.
Lemma daddeACA : @interchange (\bar^d R) +%dE +%dE.
Lemma realDed x y : (0%dE >=< x)%O -> (0%dE >=< y)%O -> (0%dE >=< x + y)%O.
Proof.
Lemma doppeD x y : x +? y -> - (x + y) = - x - y.
Proof.
Lemma fin_num_doppeD x y : y \is a fin_num -> - (x + y) = - x - y.
Proof.
Lemma dsube0 x : x - 0 = x.
Lemma dsub0e x : 0 - x = - x.
Lemma doppeB x y : x +? - y -> - (x - y) = - x + y.
Lemma fin_num_doppeB x y : y \is a fin_num -> - (x - y) = - x + y.
Proof.
Lemma dfin_numD x y :
(x + y \is a fin_num) = (x \is a fin_num) && (y \is a fin_num).
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma dfineD :
{in (@fin_num R) &, {morph fine : x y / x + y >-> (x + y)%R}}.
Proof.
by move=> [r| |] [s| |]. Qed.
Lemma dfineB : {in @fin_num R &, {morph fine : x y / x - y >-> (x - y)%R}}.
Proof.
by move=> [r| |] [s| |]. Qed.
Lemma daddeK x y : x \is a fin_num -> y + x - x = y.
Proof.
Lemma dsubeK x y : y \is a fin_num -> x - y + y = x.
Proof.
Lemma dsubee x : x \is a fin_num -> x - x = 0.
Proof.
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)).
Proof.
by move: x y => [?| |] [?| |]. Qed.
Lemma daddye x : +oo + x = +oo
Proof.
by []. Qed.
Lemma daddey x : x + +oo = +oo
Proof.
by case: x. Qed.
Lemma daddNye x : x != +oo -> -oo + x = -oo
Proof.
by case: x. Qed.
Lemma daddeNy x : x != +oo -> x + -oo = -oo
Proof.
by case: x. Qed.
Lemma dadde_Neq_pinfty x y : x != -oo -> y != -oo ->
(x + y != +oo) = (x != +oo) && (y != +oo).
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma dadde_Neq_ninfty x y : x != +oo -> y != +oo ->
(x + y != -oo) = (x != -oo) && (y != -oo).
Proof.
by move: x y => [x| |] [y| |]. Qed.
Lemma ndadde_eq0 x y : x <= 0 -> y <= 0 -> x + y == 0 = (x == 0) && (y == 0).
Proof.
Lemma pdadde_eq0 x y : 0 <= x -> 0 <= y -> x + y == 0 = (x == 0) && (y == 0).
Proof.
Lemma dadde_ss_eq0 x y : (0 <= x) && (0 <= y) || (x <= 0) && (y <= 0) ->
x + y == 0 = (x == 0) && (y == 0).
Proof.
Lemma desum_eqyP (T : eqType) (s : seq T) (P : pred T) (f : T -> \bar^d R) :
\sum_(i <- s | P i) f i = +oo <-> exists i, [/\ i \in s, P i & f i = +oo].
Proof.
rewrite dual_sumeE eqe_oppLRP /= esum_eqNyP.
by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP.
Qed.
by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP.
Qed.
Lemma desum_eqy (I : finType) (f : I -> \bar R) (P : {pred I}) :
(\sum_(i | P i) f i == +oo) = [exists i in P, f i == +oo].
Proof.
Lemma desum_eqNyP
(T : eqType) (s : seq T) (P : pred T) (f : T -> \bar^d R) :
(forall i, P i -> f i != +oo) ->
\sum_(i <- s | P i) f i = -oo <-> exists i, [/\ i \in s, P i & f i = -oo].
Proof.
move=> fioo.
rewrite dual_sumeE eqe_oppLRP /= esum_eqyP => [|i Pi]; last first.
by rewrite eqe_oppLR fioo.
by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP.
Qed.
rewrite dual_sumeE eqe_oppLRP /= esum_eqyP => [|i Pi]; last first.
by rewrite eqe_oppLR fioo.
by split=> -[i + /ltac:(exists i)] => [|] []; [|split]; rewrite // eqe_oppLRP.
Qed.
Lemma desum_eqNy (I : finType) (f : I -> \bar^d R) (P : {pred I}) :
(forall i, f i != +oo) ->
(\sum_(i | P i) f i == -oo) = [exists i in P, f i == -oo].
Proof.
move=> finoo.
rewrite dual_sumeE eqe_oppLR /= esum_eqy => [|i]; rewrite ?eqe_oppLR //.
by under eq_existsb => i do rewrite eqe_oppLR.
Qed.
rewrite dual_sumeE eqe_oppLR /= esum_eqy => [|i]; rewrite ?eqe_oppLR //.
by under eq_existsb => i do rewrite eqe_oppLR.
Qed.
Lemma dadde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
Proof.
Lemma dadde_le0 x y : x <= 0 -> y <= 0 -> x + y <= 0.
Proof.
Lemma dsume_ge0 T (f : T -> \bar^d R) (P : pred T) :
(forall n, P n -> 0 <= f n) -> forall l, 0 <= \sum_(i <- l | P i) f i.
Proof.
Lemma dsume_le0 T (f : T -> \bar^d R) (P : pred T) :
(forall n, P n -> f n <= 0) -> forall l, \sum_(i <- l | P i) f i <= 0.
Proof.
Lemma gte_dN (r : \bar^d R) : (0 < r)%E -> (- r < r)%E.
Lemma ednatmul_pinfty n : +oo *+ n.+1 = +oo :> \bar^d R.
Proof.
by elim: n => //= n ->. Qed.
Lemma ednatmul_ninfty n : -oo *+ n.+1 = -oo :> \bar^d R.
Proof.
by elim: n => //= n ->. Qed.
Lemma EFin_dnatmul (r : R) n : (r *+ n.+1)%:E = r%:E *+ n.+1.
Proof.
by elim: n => //= n <-. Qed.
Lemma ednatmulE x n : x *+ n = (x *+ n)%E.
Proof.
case: x => [x| |]; case: n => [//|n].
- by rewrite -EFin_natmul -EFin_dnatmul.
- by rewrite enatmul_pinfty ednatmul_pinfty.
- by rewrite enatmul_ninfty ednatmul_ninfty.
Qed.
- by rewrite -EFin_natmul -EFin_dnatmul.
- by rewrite enatmul_pinfty ednatmul_pinfty.
- by rewrite enatmul_ninfty ednatmul_ninfty.
Qed.
Lemma dmule2n x : x *+ 2 = x + x
Proof.
by []. Qed.
Lemma sqredD x y : x + y \is a fin_num ->
(x + y) ^+ 2 = x ^+ 2 + x * y *+ 2 + y ^+ 2.
Proof.
End DualERealArithTh_numDomainType.
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dN`")]
Notation gte_dopp := gte_dN (only parsing).
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).
Proof.
Lemma ltey_eq x : (x < +oo) = (x \is a fin_num) || (x == -oo).
Proof.
Lemma ltNye_eq x : (-oo < x) = (x \is a fin_num) || (x == +oo).
Proof.
Lemma ge0_fin_numE x : 0 <= x -> (x \is a fin_num) = (x < +oo).
Proof.
Lemma gt0_fin_numE x : 0 < x -> (x \is a fin_num) = (x < +oo).
Proof.
Lemma le0_fin_numE x : x <= 0 -> (x \is a fin_num) = (-oo < x).
Lemma lt0_fin_numE x : x < 0 -> (x \is a fin_num) = (-oo < x).
Proof.
Lemma eqyP x : x = +oo <-> (forall A, (0 < A)%R -> A%:E <= x).
Proof.
split=> [-> // A A0|Ax]; first by rewrite leey.
apply/eqP; rewrite eq_le leey /= leNgt; apply/negP.
case: x Ax => [x Ax _|//|/(_ _ ltr01)//].
suff: ~ x%:E < (Order.max 0 x + 1)%:E.
by apply; rewrite lte_fin ltr_pwDr// le_max lexx orbT.
by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_max lexx.
Qed.
apply/eqP; rewrite eq_le leey /= leNgt; apply/negP.
case: x Ax => [x Ax _|//|/(_ _ ltr01)//].
suff: ~ x%:E < (Order.max 0 x + 1)%:E.
by apply; rewrite lte_fin ltr_pwDr// le_max lexx orbT.
by apply/negP; rewrite -leNgt; apply/Ax/ltr_pwDr; rewrite // le_max lexx.
Qed.
Lemma seq_psume_eq0 (I : choiceType) (r : seq I)
(P : pred I) (F : I -> \bar R) : (forall i, P i -> 0 <= F i)%E ->
(\sum_(i <- r | P i) F i == 0)%E = all (fun i => P i ==> (F i == 0%E)) r.
Proof.
move=> F0; apply/eqP/allP => PF0; last first.
rewrite big_seq_cond big1// => i /andP[ir Pi].
by have := PF0 _ ir; rewrite Pi implyTb => /eqP.
move=> i ir; apply/implyP => Pi; apply/eqP.
have rPF : {in r, forall i, P i ==> (F i \is a fin_num)}.
move=> j jr; apply/implyP => Pj; rewrite fin_numElt; apply/andP; split.
by rewrite (lt_le_trans _ (F0 _ Pj))// ltNyr.
rewrite ltNge; apply/eqP; rewrite leye_eq; apply/eqP/negP => /eqP Fjoo.
have PFninfty k : P k -> F k != -oo%E.
by move=> Pk; rewrite gt_eqF// (lt_le_trans _ (F0 _ Pk))// ltNyr.
have /esum_eqyP : exists i, [/\ i \in r, P i & F i = +oo%E] by exists j.
by move=> /(_ PFninfty); rewrite PF0.
have ? : (\sum_(i <- r | P i) (fine \o F) i == 0)%R.
apply/eqP/EFin_inj; rewrite big_seq_cond -sumEFin.
rewrite (eq_bigr (fun i0 => F i0)); last first.
move=> j /andP[jr Pj] /=; rewrite fineK//.
by have := rPF _ jr; rewrite Pj implyTb.
by rewrite -big_seq_cond PF0.
have /allP/(_ _ ir) : all (fun i => P i ==> ((fine \o F) i == 0))%R r.
by rewrite -psumr_eq0// => j Pj/=; apply/fine_ge0/F0.
rewrite Pi implyTb => /= => /eqP Fi0.
rewrite -(@fineK _ (F i))//; last by have := rPF _ ir; rewrite Pi implyTb.
by rewrite Fi0.
Qed.
rewrite big_seq_cond big1// => i /andP[ir Pi].
by have := PF0 _ ir; rewrite Pi implyTb => /eqP.
move=> i ir; apply/implyP => Pi; apply/eqP.
have rPF : {in r, forall i, P i ==> (F i \is a fin_num)}.
move=> j jr; apply/implyP => Pj; rewrite fin_numElt; apply/andP; split.
by rewrite (lt_le_trans _ (F0 _ Pj))// ltNyr.
rewrite ltNge; apply/eqP; rewrite leye_eq; apply/eqP/negP => /eqP Fjoo.
have PFninfty k : P k -> F k != -oo%E.
by move=> Pk; rewrite gt_eqF// (lt_le_trans _ (F0 _ Pk))// ltNyr.
have /esum_eqyP : exists i, [/\ i \in r, P i & F i = +oo%E] by exists j.
by move=> /(_ PFninfty); rewrite PF0.
have ? : (\sum_(i <- r | P i) (fine \o F) i == 0)%R.
apply/eqP/EFin_inj; rewrite big_seq_cond -sumEFin.
rewrite (eq_bigr (fun i0 => F i0)); last first.
move=> j /andP[jr Pj] /=; rewrite fineK//.
by have := rPF _ jr; rewrite Pj implyTb.
by rewrite -big_seq_cond PF0.
have /allP/(_ _ ir) : all (fun i => P i ==> ((fine \o F) i == 0))%R r.
by rewrite -psumr_eq0// => j Pj/=; apply/fine_ge0/F0.
rewrite Pi implyTb => /= => /eqP Fi0.
rewrite -(@fineK _ (F i))//; last by have := rPF _ ir; rewrite Pi implyTb.
by rewrite Fi0.
Qed.
Lemma lte_add_pinfty x y : x < +oo -> y < +oo -> x + y < +oo.
Lemma lte_sum_pinfty I (s : seq I) (P : pred I) (f : I -> \bar R) :
(forall i, P i -> f i < +oo) -> \sum_(i <- s | P i) f i < +oo.
Proof.
elim/big_ind : _ => [_|x y xoo yoo foo|i ?]; [exact: ltry| |exact].
by apply: lte_add_pinfty; [exact: xoo| exact: yoo].
Qed.
by apply: lte_add_pinfty; [exact: xoo| exact: yoo].
Qed.
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 sube_ge0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(0 <= y - x) = (x <= y).
Lemma lteNl x y : (- x < y) = (- y < x).
Lemma lteNr x y : (x < - y) = (y < - x).
Lemma leeNr x y : (x <= - y) = (y <= - x).
Lemma leeNl x y : (- x <= y) = (- y <= x).
Lemma muleN x y : x * - y = - (x * y).
Proof.
Lemma mulNe x y : - x * y = - (x * y)
Lemma muleNN x y : - x * - y = x * y
Lemma mulry r : r%:E * +oo%E = (Num.sg r)%:E * +oo%E.
Proof.
Lemma mulyr r : +oo%E * r%:E = (Num.sg r)%:E * +oo%E.
Lemma mulrNy r : r%:E * -oo%E = (Num.sg r)%:E * -oo%E.
Proof.
Lemma mulNyr r : -oo%E * r%:E = (Num.sg r)%:E * -oo%E.
Definition mulr_infty := (mulry, mulyr, mulrNy, mulNyr).
Lemma lte_mul_pinfty x y : 0 <= x -> x \is a fin_num -> y < +oo -> x * y < +oo.
Proof.
Lemma mule_ge0_gt0 x y : 0 <= x -> 0 <= y -> (0 < x * y) = (0 < x) && (0 < y).
Proof.
move: x y => [x| |] [y| |] //; rewrite ?lee_fin.
- by move=> x0 y0; rewrite !lte_fin; exact: mulr_ge0_gt0.
- rewrite le_eqVlt => /predU1P[<-|x0] _; first by rewrite mul0e ltxx.
by rewrite ltry andbT mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- move=> _; rewrite le_eqVlt => /predU1P[<-|x0].
by rewrite mule0 ltxx andbC.
by rewrite ltry/= mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- by move=> _ _; rewrite mulyy ltry.
Qed.
- by move=> x0 y0; rewrite !lte_fin; exact: mulr_ge0_gt0.
- rewrite le_eqVlt => /predU1P[<-|x0] _; first by rewrite mul0e ltxx.
by rewrite ltry andbT mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- move=> _; rewrite le_eqVlt => /predU1P[<-|x0].
by rewrite mule0 ltxx andbC.
by rewrite ltry/= mulr_infty gtr0_sg// mul1e lte_fin x0 ltry.
- by move=> _ _; rewrite mulyy ltry.
Qed.
Lemma gt0_mulye x : (0 < x -> +oo * x = +oo)%E.
Proof.
Lemma lt0_mulye x : (x < 0 -> +oo * x = -oo)%E.
Proof.
Lemma gt0_mulNye x : (0 < x -> -oo * x = -oo)%E.
Proof.
Lemma lt0_mulNye x : (x < 0 -> -oo * x = +oo)%E.
Proof.
Lemma gt0_muley x : (0 < x -> x * +oo = +oo)%E.
Lemma lt0_muley x : (x < 0 -> x * +oo = -oo)%E.
Lemma gt0_muleNy x : (0 < x -> x * -oo = -oo)%E.
Proof.
Lemma lt0_muleNy x : (x < 0 -> x * -oo = +oo)%E.
Proof.
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)].
Proof.
move: x y => [x| |] [y| |]; rewrite ?(lte_fin,andbF,andbT,orbF,eqxx,andbT)//=.
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulyy ltry.
- by rewrite mulyNy.
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulNyy.
- by rewrite ltNyr.
Qed.
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulyy ltry.
- by rewrite mulyNy.
- by rewrite mulr_infty; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
- by rewrite mulNyy.
- by rewrite ltNyr.
Qed.
Lemma mule_eq_ninfty x y : (x * y == -oo) =
[|| (x > 0) && (y == -oo), (x < 0) && (y == +oo),
(x == -oo) && (y > 0) | (x == +oo) && (y < 0)].
Proof.
Lemma lteD a b x y : a < b -> x < y -> a + x < b + y.
Proof.
Lemma leeDl x y : 0 <= y -> x <= x + y.
Proof.
Lemma leeDr x y : 0 <= y -> x <= y + x.
Lemma geeDl x y : y <= 0 -> x + y <= x.
Proof.
Lemma geeDr x y : y <= 0 -> y + x <= x
Lemma lteDl y x : y \is a fin_num -> (y < y + x) = (0 < x).
Lemma lteDr y x : y \is a fin_num -> (y < x + y) = (0 < x).
Lemma gte_subl y x : y \is a fin_num -> (y - x < y) = (0 < x).
Proof.
Lemma gte_subr y x : y \is a fin_num -> (- x + y < y) = (0 < x).
Lemma gteDl x y : x \is a fin_num -> (x + y < x) = (y < 0).
Lemma gteDr x y : x \is a fin_num -> (y + x < x) = (y < 0).
Lemma lteD2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b).
Proof.
Lemma lteD2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b).
Lemma leeD2l x a b : a <= b -> x + a <= x + b.
Proof.
Lemma leeD2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b).
Proof.
Lemma leeD2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b).
Lemma leeD2r x a b : a <= b -> a + x <= b + x.
Lemma leeD a b x y : a <= b -> x <= y -> a + x <= b + y.
Proof.
Lemma lte_leD a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
Proof.
Lemma lee_ltD a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.
Lemma leeB x y z u : x <= y -> u <= z -> x - z <= y - u.
Proof.
Lemma lte_leB z u x y : u \is a fin_num ->
x < z -> u <= y -> x - y < z - u.
Proof.
Lemma lte_pmul2r z : z \is a fin_num -> 0 < z -> {mono *%E^~ z : x y / x < y}.
Proof.
move: z => [z| |] _ // z0 [x| |] [y| |] //.
- by rewrite !lte_fin ltr_pM2r.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltry.
- by rewrite mulr_infty gtr0_sg// mul1e ltNge leNye ltNge leNye.
- by rewrite mulr_infty gtr0_sg// mul1e ltNge leey ltNge leey.
- by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltNyr.
- by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
Qed.
- by rewrite !lte_fin ltr_pM2r.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltry.
- by rewrite mulr_infty gtr0_sg// mul1e ltNge leNye ltNge leNye.
- by rewrite mulr_infty gtr0_sg// mul1e ltNge leey ltNge leey.
- by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltNyr.
- by rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// mul1e.
Qed.
Lemma lte_pmul2l z : z \is a fin_num -> 0 < z -> {mono *%E z : x y / x < y}.
Proof.
Lemma lte_nmul2l z : z \is a fin_num -> z < 0 -> {mono *%E z : x y /~ x < y}.
Proof.
Lemma lte_nmul2r z : z \is a fin_num -> z < 0 -> {mono *%E^~ z : x y /~ x < y}.
Proof.
Lemma lte_pmulr x y : y \is a fin_num -> 0 < y -> (y < y * x) = (1 < x).
Proof.
Lemma lte_pmull x y : y \is a fin_num -> 0 < y -> (y < x * y) = (1 < x).
Lemma lte_nmulr x y : y \is a fin_num -> y < 0 -> (y < y * x) = (x < 1).
Proof.
Lemma lte_nmull x y : y \is a fin_num -> y < 0 -> (y < x * y) = (x < 1).
Lemma lee_sum I (f g : I -> \bar R) s (P : pred I) :
(forall i, P i -> f i <= g i) ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | P i) g i.
Lemma lee_sum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar R) :
{subset Q <= P} -> {in [predD P & Q], forall i, 0 <= f i} ->
\sum_(i <- s | Q i) f i <= \sum_(i <- s | P i) f i.
Proof.
move=> QP PQf; rewrite big_mkcond [leRHS]big_mkcond lee_sum// => i.
by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP.
Qed.
by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP.
Qed.
Lemma lee_sum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar R) :
{subset Q <= P} -> {in [predD P & Q], forall i, f i <= 0} ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | Q i) f i.
Proof.
move=> QP PQf; rewrite big_mkcond [leRHS]big_mkcond lee_sum// => i.
by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP.
Qed.
by move/implyP: (QP i); move: (PQf i); rewrite !inE -!topredE/=; do !case: ifP.
Qed.
Lemma lee_sum_nneg (I : eqType) (s : seq I) (P Q : pred I)
(f : I -> \bar R) : (forall i, P i -> ~~ Q i -> 0 <= f i) ->
\sum_(i <- s | P i && Q i) f i <= \sum_(i <- s | P i) f i.
Proof.
Lemma lee_sum_npos (I : eqType) (s : seq I) (P Q : pred I)
(f : I -> \bar R) : (forall i, P i -> ~~ Q i -> f i <= 0) ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | P i && Q i) f i.
Proof.
Lemma lee_sum_nneg_ord (f : nat -> \bar R) (P : pred nat) :
(forall n, P n -> 0 <= f n) ->
{homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}.
Proof.
move=> f0 i j le_ij; rewrite (big_ord_widen_cond j) // big_mkcondr /=.
by rewrite lee_sum // => k ?; case: ifP => // _; exact: f0.
Qed.
by rewrite lee_sum // => k ?; case: ifP => // _; exact: f0.
Qed.
Lemma lee_sum_npos_ord (f : nat -> \bar R) (P : pred nat) :
(forall n, P n -> f n <= 0) ->
{homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
Proof.
move=> f0 m n ?; rewrite [leRHS](big_ord_widen_cond n) // big_mkcondr /=.
by rewrite lee_sum // => i ?; case: ifP => // _; exact: f0.
Qed.
by rewrite lee_sum // => i ?; case: ifP => // _; exact: f0.
Qed.
Lemma lee_sum_nneg_natr (f : nat -> \bar R) (P : pred nat) m :
(forall n, (m <= n)%N -> P n -> 0 <= f n) ->
{homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}.
Proof.
Lemma lee_sum_npos_natr (f : nat -> \bar R) (P : pred nat) m :
(forall n, (m <= n)%N -> P n -> f n <= 0) ->
{homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
Proof.
Lemma lee_sum_nneg_natl (f : nat -> \bar R) (P : pred nat) n :
(forall m, (m < n)%N -> P m -> 0 <= f m) ->
{homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
Proof.
move=> f0 i j le_ij; rewrite !big_geq_mkord/=.
rewrite lee_sum_nneg_subset// => [k | k /and3P[_ /f0->//]].
by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->].
Qed.
rewrite lee_sum_nneg_subset// => [k | k /and3P[_ /f0->//]].
by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->].
Qed.
Lemma lee_sum_npos_natl (f : nat -> \bar R) (P : pred nat) n :
(forall m, (m < n)%N -> P m -> f m <= 0) ->
{homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}.
Proof.
move=> f0 i j le_ij; rewrite !big_geq_mkord/=.
rewrite lee_sum_npos_subset// => [k | k /and3P[_ /f0->//]].
by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->].
Qed.
rewrite lee_sum_npos_subset// => [k | k /and3P[_ /f0->//]].
by rewrite ?inE -!topredE/= => /andP[-> /(leq_trans le_ij)->].
Qed.
Lemma lee_sum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T -> \bar R) : {subset A <= B} ->
{in [predD B & A], forall t, P t -> 0 <= f t} ->
\sum_(t <- A | P t) f t <= \sum_(t <- B | P t) f t.
Proof.
move=> AB f0; rewrite [leRHS]big_mkcond (big_fsetID _ (mem A) B) /=.
rewrite -[leLHS]adde0 leeD //.
rewrite -big_mkcond /= {1}(_ : A = [fset x in B | x \in A]%fset) //.
by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB.
rewrite big_fset /= big_seq_cond sume_ge0 // => t /andP[tB tA].
by case: ifPn => // Pt; rewrite f0 // !inE tA.
Qed.
rewrite -[leLHS]adde0 leeD //.
rewrite -big_mkcond /= {1}(_ : A = [fset x in B | x \in A]%fset) //.
by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB.
rewrite big_fset /= big_seq_cond sume_ge0 // => t /andP[tB tA].
by case: ifPn => // Pt; rewrite f0 // !inE tA.
Qed.
Lemma lee_sum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T -> \bar R) : {subset A <= B} ->
{in [predD B & A], forall t, P t -> f t <= 0} ->
\sum_(t <- B | P t) f t <= \sum_(t <- A | P t) f t.
Proof.
move=> AB f0; rewrite big_mkcond (big_fsetID _ (mem A) B) /=.
rewrite -[leRHS]adde0 leeD //.
rewrite -big_mkcond /= {3}(_ : A = [fset x in B | x \in A]%fset) //.
by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB.
rewrite big_fset /= big_seq_cond sume_le0 // => t /andP[tB tA].
by case: ifPn => // Pt; rewrite f0 // !inE tA.
Qed.
rewrite -[leRHS]adde0 leeD //.
rewrite -big_mkcond /= {3}(_ : A = [fset x in B | x \in A]%fset) //.
by apply/fsetP=> t; rewrite !inE /= andbC; case: (boolP (_ \in _)) => // /AB.
rewrite big_fset /= big_seq_cond sume_le0 // => t /andP[tB tA].
by case: ifPn => // Pt; rewrite f0 // !inE tA.
Qed.
Lemma lteBlDr x y z : y \is a fin_num -> (x - y < z) = (x < z + y).
Proof.
Lemma lteBlDl x y z : y \is a fin_num -> (x - y < z) = (x < y + z).
Lemma lteBrDr x y z : z \is a fin_num -> (x < y - z) = (x + z < y).
Proof.
Lemma lteBrDl x y z : z \is a fin_num -> (x < y - z) = (z + x < y).
Lemma lte_subel_addr x y z : x \is a fin_num -> (x - y < z) = (x < z + y).
Proof.
Lemma lte_subel_addl x y z : x \is a fin_num -> (x - y < z) = (x < y + z).
Proof.
Lemma lte_suber_addr x y z : x \is a fin_num -> (x < y - z) = (x + z < y).
Proof.
Lemma lte_suber_addl x y z : x \is a fin_num -> (x < y - z) = (z + x < y).
Proof.
Lemma leeBlDr x y z : y \is a fin_num -> (x - y <= z) = (x <= z + y).
Proof.
Lemma leeBlDl x y z : y \is a fin_num -> (x - y <= z) = (x <= y + z).
Lemma leeBrDr x y z : z \is a fin_num -> (x <= y - z) = (x + z <= y).
Proof.
Lemma leeBrDl x y z : z \is a fin_num -> (x <= y - z) = (z + x <= y).
Lemma lee_subel_addr x y z : z \is a fin_num -> (x - y <= z) = (x <= z + y).
Proof.
Lemma lee_subel_addl x y z : z \is a fin_num -> (x - y <= z) = (x <= y + z).
Proof.
Lemma lee_suber_addr x y z : y \is a fin_num -> (x <= y - z) = (x + z <= y).
Proof.
Lemma lee_suber_addl x y z : y \is a fin_num -> (x <= y - z) = (z + x <= y).
Proof.
Lemma subre_lt0 x y : x \is a fin_num -> (x - y < 0) = (x < y).
Proof.
Lemma suber_lt0 x y : y \is a fin_num -> (x - y < 0) = (x < y).
Lemma sube_lt0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(x - y < 0) = (x < y).
Lemma pmule_rge0 x y : 0 < x -> (x * y >= 0) = (y >= 0).
Proof.
Lemma pmule_lge0 x y : 0 < x -> (y * x >= 0) = (y >= 0).
Proof.
Lemma pmule_rlt0 x y : 0 < x -> (x * y < 0) = (y < 0).
Proof.
Lemma pmule_llt0 x y : 0 < x -> (y * x < 0) = (y < 0).
Proof.
Lemma pmule_rle0 x y : 0 < x -> (x * y <= 0) = (y <= 0).
Proof.
Lemma pmule_lle0 x y : 0 < x -> (y * x <= 0) = (y <= 0).
Proof.
Lemma pmule_rgt0 x y : 0 < x -> (x * y > 0) = (y > 0).
Proof.
Lemma pmule_lgt0 x y : 0 < x -> (y * x > 0) = (y > 0).
Proof.
Lemma nmule_rge0 x y : x < 0 -> (x * y >= 0) = (y <= 0).
Proof.
Lemma nmule_lge0 x y : x < 0 -> (y * x >= 0) = (y <= 0).
Proof.
Lemma nmule_rle0 x y : x < 0 -> (x * y <= 0) = (y >= 0).
Proof.
Lemma nmule_lle0 x y : x < 0 -> (y * x <= 0) = (y >= 0).
Proof.
Lemma nmule_rgt0 x y : x < 0 -> (x * y > 0) = (y < 0).
Proof.
Lemma nmule_lgt0 x y : x < 0 -> (y * x > 0) = (y < 0).
Proof.
Lemma nmule_rlt0 x y : x < 0 -> (x * y < 0) = (y > 0).
Proof.
Lemma nmule_llt0 x y : x < 0 -> (y * x < 0) = (y > 0).
Proof.
Lemma mule_lt0 x y : (x * y < 0) = [&& x != 0, y != 0 & (x < 0) (+) (y < 0)].
Proof.
have [xlt0|xgt0|->] := ltgtP x 0; last by rewrite mul0e.
by rewrite nmule_rlt0//= -leNgt lt_def.
by rewrite pmule_rlt0//= !lt_neqAle andbA andbb.
Qed.
by rewrite nmule_rlt0//= -leNgt lt_def.
by rewrite pmule_rlt0//= !lt_neqAle andbA andbb.
Qed.
Lemma muleA : associative ( *%E : \bar R -> \bar R -> \bar R ).
Proof.
move=> x y z.
wlog x0 : x y z / 0 < x => [hwlog|].
have [x0| |->] := ltgtP x 0; [ |exact: hwlog|by rewrite !mul0e].
by apply: oppe_inj; rewrite -!mulNe hwlog ?oppe_gt0.
wlog y0 : x y z x0 / 0 < y => [hwlog|].
have [y0| |->] := ltgtP y 0; [ |exact: hwlog|by rewrite !(mul0e, mule0)].
by apply: oppe_inj; rewrite -muleN -2!mulNe -muleN hwlog ?oppe_gt0.
wlog z0 : x y z x0 y0 / 0 < z => [hwlog|].
have [z0| |->] := ltgtP z 0; [ |exact: hwlog|by rewrite !mule0].
by apply: oppe_inj; rewrite -!muleN hwlog ?oppe_gt0.
case: x x0 => [x x0| |//]; last by rewrite !gt0_mulye ?mule_gt0.
case: y y0 => [y y0| |//]; last by rewrite gt0_mulye // muleC !gt0_mulye.
case: z z0 => [z z0| |//]; last by rewrite !gt0_muley ?mule_gt0.
by rewrite /mule/= mulrA.
Qed.
wlog x0 : x y z / 0 < x => [hwlog|].
have [x0| |->] := ltgtP x 0; [ |exact: hwlog|by rewrite !mul0e].
by apply: oppe_inj; rewrite -!mulNe hwlog ?oppe_gt0.
wlog y0 : x y z x0 / 0 < y => [hwlog|].
have [y0| |->] := ltgtP y 0; [ |exact: hwlog|by rewrite !(mul0e, mule0)].
by apply: oppe_inj; rewrite -muleN -2!mulNe -muleN hwlog ?oppe_gt0.
wlog z0 : x y z x0 y0 / 0 < z => [hwlog|].
have [z0| |->] := ltgtP z 0; [ |exact: hwlog|by rewrite !mule0].
by apply: oppe_inj; rewrite -!muleN hwlog ?oppe_gt0.
case: x x0 => [x x0| |//]; last by rewrite !gt0_mulye ?mule_gt0.
case: y y0 => [y y0| |//]; last by rewrite gt0_mulye // muleC !gt0_mulye.
case: z z0 => [z z0| |//]; last by rewrite !gt0_muley ?mule_gt0.
by rewrite /mule/= mulrA.
Qed.
Local Open Scope ereal_scope.
HB.instance Definition _ := Monoid.isComLaw.Build (\bar R) 1%E mule
muleA muleC mul1e.
Lemma muleCA : left_commutative ( *%E : \bar R -> \bar R -> \bar R ).
Lemma muleAC : right_commutative ( *%E : \bar R -> \bar R -> \bar R ).
Lemma muleACA : interchange (@mule R) (@mule R).
Lemma muleDr x y z : x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z.
Proof.
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.
Proof.
rewrite /mule/=; move: x y z => [r| |] [s| |] [t| |] //= s0 t0.
- by rewrite mulrDl.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => //; rewrite adde0.
- rewrite !eqe paddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0.
by case: ltgtP t0 => // [t0|[<-{t}]] _; [rewrite gt_eqF|rewrite eqxx].
+ by move: t0; rewrite lee_fin; case: (ltgtP t).
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP t0.
- by rewrite ltry.
- rewrite !eqe paddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0.
by case: ltgtP t0 => // [t0|[<-{t}]].
+ by move: t0; rewrite lee_fin; case: (ltgtP t).
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP s0.
Qed.
- by rewrite mulrDl.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => //; rewrite adde0.
- rewrite !eqe paddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0.
by case: ltgtP t0 => // [t0|[<-{t}]] _; [rewrite gt_eqF|rewrite eqxx].
+ by move: t0; rewrite lee_fin; case: (ltgtP t).
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP t0.
- by rewrite ltry.
- rewrite !eqe paddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite lte_fin -[in LHS](addr0 0%R) ltr_leD // lte_fin s0.
by case: ltgtP t0 => // [t0|[<-{t}]].
+ by move: t0; rewrite lee_fin; case: (ltgtP t).
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP s0.
Qed.
Lemma ge0_muleDr x y z : 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z.
Proof.
Lemma le0_muleDl x y z : y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x.
Proof.
rewrite /mule/=; move: x y z => [r| |] [s| |] [t| |] //= s0 t0.
- by rewrite mulrDl.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => //; rewrite adde0.
- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=.
by rewrite !ltNge ltW //.
+ by case: (ltgtP t).
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP t0.
- by rewrite ltry.
- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=.
by rewrite !ltNge ltW // -lee_fin t0; case: eqP.
+ by case: (ltgtP t).
- by rewrite ltNge s0 /=; case: eqP.
- by rewrite ltNge t0 /=; case: eqP.
Qed.
- by rewrite mulrDl.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => // -[] <-; rewrite mulr0 adde0.
- by case: ltgtP => //; rewrite adde0.
- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=.
by rewrite !ltNge ltW //.
+ by case: (ltgtP t).
- by rewrite ltry; case: ltgtP s0.
- by rewrite ltry; case: ltgtP t0.
- by rewrite ltry.
- rewrite !eqe naddr_eq0 //; move: s0; rewrite lee_fin.
case: (ltgtP s) => //= [s0|->{s}] _; rewrite ?add0e.
+ rewrite !lte_fin -[in LHS](addr0 0%R) ltNge lerD // ?ltW //=.
by rewrite !ltNge ltW // -lee_fin t0; case: eqP.
+ by case: (ltgtP t).
- by rewrite ltNge s0 /=; case: eqP.
- by rewrite ltNge t0 /=; case: eqP.
Qed.
Lemma le0_muleDr x y z : y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z.
Proof.
Lemma gee_pMl y x : y \is a fin_num -> 0 <= x -> y <= 1 -> y * x <= x.
Proof.
Lemma lee_wpmul2r x : 0 <= x -> {homo *%E^~ x : y z / y <= z}.
Proof.
move: x => [x|_|//].
rewrite lee_fin le_eqVlt => /predU1P[<- y z|x0]; first by rewrite 2!mule0.
move=> [y| |] [z| |]//; first by rewrite !lee_fin// ler_pM2r.
- by move=> _; rewrite mulr_infty gtr0_sg// mul1e leey.
- by move=> _; rewrite mulr_infty gtr0_sg// mul1e leNye.
- by move=> _; rewrite 2!mulr_infty gtr0_sg// 2!mul1e.
move=> [y| |] [z| |]//.
- rewrite lee_fin => yz.
have [z0|z0|] := ltgtP 0%R z.
+ by rewrite [leRHS]mulr_infty gtr0_sg// mul1e leey.
+ by rewrite mulr_infty ltr0_sg// ?(le_lt_trans yz)// [leRHS]mulr_infty ltr0_sg.
+ move=> z0; move: yz; rewrite -z0 mul0e le_eqVlt => /predU1P[->|y0].
by rewrite mul0e.
by rewrite mulr_infty ltr0_sg// mulN1e leNye.
+ by move=> _; rewrite mulyy leey.
+ by move=> _; rewrite mulNyy leNye.
+ by move=> _; rewrite mulNyy leNye.
Qed.
rewrite lee_fin le_eqVlt => /predU1P[<- y z|x0]; first by rewrite 2!mule0.
move=> [y| |] [z| |]//; first by rewrite !lee_fin// ler_pM2r.
- by move=> _; rewrite mulr_infty gtr0_sg// mul1e leey.
- by move=> _; rewrite mulr_infty gtr0_sg// mul1e leNye.
- by move=> _; rewrite 2!mulr_infty gtr0_sg// 2!mul1e.
move=> [y| |] [z| |]//.
- rewrite lee_fin => yz.
have [z0|z0|] := ltgtP 0%R z.
+ by rewrite [leRHS]mulr_infty gtr0_sg// mul1e leey.
+ by rewrite mulr_infty ltr0_sg// ?(le_lt_trans yz)// [leRHS]mulr_infty ltr0_sg.
+ move=> z0; move: yz; rewrite -z0 mul0e le_eqVlt => /predU1P[->|y0].
by rewrite mul0e.
by rewrite mulr_infty ltr0_sg// mulN1e leNye.
+ by move=> _; rewrite mulyy leey.
+ by move=> _; rewrite mulNyy leNye.
+ by move=> _; rewrite mulNyy leNye.
Qed.
Lemma lee_wpmul2l x : 0 <= x -> {homo *%E x : y z / y <= z}.
Proof.
Lemma ge0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) :
(forall i, P i -> 0 <= F i) ->
(\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x).
Proof.
Lemma ge0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) :
(forall i, P i -> 0 <= F i) ->
x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i).
Proof.
Lemma le0_sume_distrl (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) :
(forall i, P i -> F i <= 0) ->
(\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x).
Proof.
Lemma le0_sume_distrr (I : Type) (s : seq I) x (P : pred I) (F : I -> \bar R) :
(forall i, P i -> F i <= 0) ->
x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i).
Proof.
Lemma fin_num_sume_distrr (I : Type) (s : seq I) x (P : pred I)
(F : I -> \bar R) :
x \is a fin_num -> {in P &, forall i j, F i +? F j} ->
x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) x * F i.
Proof.
Lemma eq_infty x : (forall r, r%:E <= x) -> x = +oo.
Proof.
Lemma eq_ninfty x : (forall r, x <= r%:E) -> x = -oo.
Lemma lee_abs x : x <= `|x|.
Lemma abse_id x : `| `|x| | = `|x|.
Proof.
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|.
Proof.
elim/big_ind2 : _ => //; first by rewrite abse0.
by move=> *; exact/(le_trans (lee_abs_add _ _) (leeD _ _)).
Qed.
by move=> *; exact/(le_trans (lee_abs_add _ _) (leeD _ _)).
Qed.
Lemma lee_abs_sub x y : `|x - y| <= `|x| + `|y|.
Lemma abseM : {morph @abse R : x y / x * y}.
Proof.
have xoo r : `|r%:E * +oo| = `|r|%:E * +oo.
have [r0|r0] := leP 0%R r.
by rewrite (ger0_norm r0)// gee0_abs// mule_ge0// leey.
rewrite (ltr0_norm r0)// lte0_abs// ?EFinN ?mulNe//.
by rewrite mule_lt0 /= eqe lt_eqF//= lte_fin r0.
move=> [x| |] [y| |] //=; first by rewrite normrM.
- by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
- by rewrite muleC xoo muleC.
- by rewrite mulyy.
- by rewrite mulyy mulyNy.
- by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
- by rewrite mulyy mulNyy.
- by rewrite mulyy.
Qed.
have [r0|r0] := leP 0%R r.
by rewrite (ger0_norm r0)// gee0_abs// mule_ge0// leey.
rewrite (ltr0_norm r0)// lte0_abs// ?EFinN ?mulNe//.
by rewrite mule_lt0 /= eqe lt_eqF//= lte_fin r0.
move=> [x| |] [y| |] //=; first by rewrite normrM.
- by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
- by rewrite muleC xoo muleC.
- by rewrite mulyy.
- by rewrite mulyy mulyNy.
- by rewrite -abseN -muleNN abseN -EFinN xoo normrN.
- by rewrite mulyy mulNyy.
- by rewrite mulyy.
Qed.
Lemma fine_max :
{in fin_num &, {mono @fine R : x y / maxe x y >-> (Num.max x y)%:E}}.
Proof.
Lemma fine_min :
{in fin_num &, {mono @fine R : x y / mine x y >-> (Num.min x y)%:E}}.
Proof.
Lemma adde_maxl : left_distributive (@GRing.add (\bar R)) maxe.
Proof.
Lemma adde_maxr : right_distributive (@GRing.add (\bar R)) maxe.
Proof.
Lemma maxey : right_zero (+oo : \bar R) maxe.
Lemma maxNye : left_id (-oo : \bar R) maxe.
HB.instance Definition _ :=
Monoid.isLaw.Build (\bar R) -oo maxe maxA maxNye maxeNy.
Lemma minNye : left_zero (-oo : \bar R) mine.
Lemma miney : right_id (+oo : \bar R) mine.
Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.
Proof.
Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.
Lemma maxe_pMr z x y : z \is a fin_num -> 0 <= z ->
z * maxe x y = maxe (z * x) (z * y).
Proof.
Lemma maxe_pMl z x y : z \is a fin_num -> 0 <= z ->
maxe x y * z = maxe (x * z) (y * z).
Lemma mine_pMr z x y : z \is a fin_num -> 0 <= z ->
z * mine x y = mine (z * x) (z * y).
Proof.
Lemma mine_pMl z x y : z \is a fin_num -> 0 <= z ->
mine x y * z = mine (x * z) (y * z).
Lemma bigmaxe_fin_num (s : seq R) r : r \in s ->
\big[maxe/-oo%E]_(i <- s) i%:E \is a fin_num.
Proof.
Lemma lee_pemull x y : 0 <= y -> 1 <= x -> y <= x * y.
Proof.
move: x y => [x| |] [y| |] //; last by rewrite mulyy.
- by rewrite -EFinM 3!lee_fin; exact: ler_peMl.
- move=> _; rewrite lee_fin => x1.
by rewrite mulr_infty gtr0_sg ?mul1e// (lt_le_trans _ x1).
- rewrite lee_fin le_eqVlt => /predU1P[<- _|y0 _]; first by rewrite mule0.
by rewrite mulr_infty gtr0_sg// mul1e leey.
Qed.
- by rewrite -EFinM 3!lee_fin; exact: ler_peMl.
- move=> _; rewrite lee_fin => x1.
by rewrite mulr_infty gtr0_sg ?mul1e// (lt_le_trans _ x1).
- rewrite lee_fin le_eqVlt => /predU1P[<- _|y0 _]; first by rewrite mule0.
by rewrite mulr_infty gtr0_sg// mul1e leey.
Qed.
Lemma lee_nemull x y : y <= 0 -> 1 <= x -> x * y <= y.
Proof.
move: x y => [x| |] [y| |] //; last by rewrite mulyNy.
- by rewrite -EFinM 3!lee_fin; exact: ler_neMl.
- move=> _; rewrite lee_fin => x1.
by rewrite mulr_infty gtr0_sg ?mul1e// (lt_le_trans _ x1).
- rewrite lee_fin le_eqVlt => /predU1P[-> _|y0 _]; first by rewrite mule0.
by rewrite mulr_infty ltr0_sg// mulN1e leNye.
Qed.
- by rewrite -EFinM 3!lee_fin; exact: ler_neMl.
- move=> _; rewrite lee_fin => x1.
by rewrite mulr_infty gtr0_sg ?mul1e// (lt_le_trans _ x1).
- rewrite lee_fin le_eqVlt => /predU1P[-> _|y0 _]; first by rewrite mule0.
by rewrite mulr_infty ltr0_sg// mulN1e leNye.
Qed.
Lemma lee_pemulr x y : 0 <= y -> 1 <= x -> y <= y * x.
Proof.
Lemma lee_nemulr x y : y <= 0 -> 1 <= x -> y * x <= y.
Proof.
Lemma mule_natl x n : n%:R%:E * x = x *+ n.
Proof.
elim: n => [|n]; first by rewrite mul0e.
move: x => [x| |] ih.
- by rewrite -EFinM mulr_natl EFin_natmul.
- by rewrite mulry gtr0_sg// mul1e enatmul_pinfty.
- by rewrite mulrNy gtr0_sg// mul1e enatmul_ninfty.
Qed.
move: x => [x| |] ih.
- by rewrite -EFinM mulr_natl EFin_natmul.
- by rewrite mulry gtr0_sg// mul1e enatmul_pinfty.
- by rewrite mulrNy gtr0_sg// mul1e enatmul_ninfty.
Qed.
Lemma lte_pmul x1 y1 x2 y2 :
0 <= x1 -> 0 <= x2 -> x1 < y1 -> x2 < y2 -> x1 * x2 < y1 * y2.
Proof.
move: x1 y1 x2 y2 => [x1| |] [y1| |] [x2| |] [y2| |] //;
rewrite !(lte_fin,lee_fin).
- by move=> *; rewrite ltr_pM.
- move=> x10 x20 xy1 xy2.
by rewrite mulry gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy1).
- move=> x10 x20 xy1 xy2.
by rewrite mulyr gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy2).
- by move=> *; rewrite mulyy -EFinM ltry.
Qed.
rewrite !(lte_fin,lee_fin).
- by move=> *; rewrite ltr_pM.
- move=> x10 x20 xy1 xy2.
by rewrite mulry gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy1).
- move=> x10 x20 xy1 xy2.
by rewrite mulyr gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy2).
- by move=> *; rewrite mulyy -EFinM ltry.
Qed.
Lemma lee_pmul x1 y1 x2 y2 : 0 <= x1 -> 0 <= x2 -> x1 <= y1 -> x2 <= y2 ->
x1 * x2 <= y1 * y2.
Proof.
move: x1 y1 x2 y2 => [x1| |] [y1| |] [x2| |] [y2| |] //; rewrite !lee_fin.
- exact: ler_pM.
- rewrite le_eqVlt => /predU1P[<- x20 y10 _|x10 x20 xy1 _].
by rewrite mul0e mule_ge0// leey.
by rewrite mulr_infty gtr0_sg// ?mul1e ?leey// (lt_le_trans x10).
- rewrite le_eqVlt => /predU1P[<- _ y10 _|x10 _ xy1 _].
by rewrite mul0e mule_ge0// leey.
rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// ?mul1e//.
exact: (lt_le_trans x10).
- move=> x10; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].
by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0.
by rewrite mulr_infty gtr0_sg ?mul1e ?leey// (lt_le_trans x20).
- by move=> x10 x20 _ _; rewrite mulyy leey.
- rewrite le_eqVlt => /predU1P[<- _ _ _|x10 _ _ _].
by rewrite mulyy mul0e leey.
by rewrite mulyy mulr_infty gtr0_sg// mul1e.
- move=> _; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].
by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0.
rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg ?mul1e//.
exact: (lt_le_trans x20).
- move=> _; rewrite le_eqVlt => /predU1P[<- _ _|x20 _ _].
by rewrite mule0 mulyy leey.
by rewrite mulr_infty gtr0_sg// mul1e// mulyy.
Qed.
- exact: ler_pM.
- rewrite le_eqVlt => /predU1P[<- x20 y10 _|x10 x20 xy1 _].
by rewrite mul0e mule_ge0// leey.
by rewrite mulr_infty gtr0_sg// ?mul1e ?leey// (lt_le_trans x10).
- rewrite le_eqVlt => /predU1P[<- _ y10 _|x10 _ xy1 _].
by rewrite mul0e mule_ge0// leey.
rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// ?mul1e//.
exact: (lt_le_trans x10).
- move=> x10; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].
by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0.
by rewrite mulr_infty gtr0_sg ?mul1e ?leey// (lt_le_trans x20).
- by move=> x10 x20 _ _; rewrite mulyy leey.
- rewrite le_eqVlt => /predU1P[<- _ _ _|x10 _ _ _].
by rewrite mulyy mul0e leey.
by rewrite mulyy mulr_infty gtr0_sg// mul1e.
- move=> _; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2].
by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0.
rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg ?mul1e//.
exact: (lt_le_trans x20).
- move=> _; rewrite le_eqVlt => /predU1P[<- _ _|x20 _ _].
by rewrite mule0 mulyy leey.
by rewrite mulr_infty gtr0_sg// mul1e// mulyy.
Qed.
Lemma lee_pmul2l x : x \is a fin_num -> 0 < x -> {mono *%E x : x y / x <= y}.
Proof.
move: x => [x _|//|//] /[!(@lte_fin R)] x0 [y| |] [z| |].
- by rewrite -2!EFinM 2!lee_fin ler_pM2l.
- by rewrite mulry gtr0_sg// mul1e 2!leey.
- by rewrite mulrNy gtr0_sg// mul1e 2!leeNy_eq.
- by rewrite mulry gtr0_sg// mul1e 2!leye_eq.
- by rewrite mulry gtr0_sg// mul1e.
- by rewrite mulry mulrNy gtr0_sg// mul1e mul1e.
- by rewrite mulrNy gtr0_sg// mul1e 2!leNye.
- by rewrite mulrNy mulry gtr0_sg// 2!mul1e.
- by rewrite mulrNy gtr0_sg// mul1e.
Qed.
- by rewrite -2!EFinM 2!lee_fin ler_pM2l.
- by rewrite mulry gtr0_sg// mul1e 2!leey.
- by rewrite mulrNy gtr0_sg// mul1e 2!leeNy_eq.
- by rewrite mulry gtr0_sg// mul1e 2!leye_eq.
- by rewrite mulry gtr0_sg// mul1e.
- by rewrite mulry mulrNy gtr0_sg// mul1e mul1e.
- by rewrite mulrNy gtr0_sg// mul1e 2!leNye.
- by rewrite mulrNy mulry gtr0_sg// 2!mul1e.
- by rewrite mulrNy gtr0_sg// mul1e.
Qed.
Lemma lee_pmul2r x : x \is a fin_num -> 0 < x -> {mono *%E^~ x : x y / x <= y}.
Proof.
Lemma lee_sqr x y : 0 <= x -> 0 <= y -> (x ^+ 2 <= y ^+ 2) = (x <= y).
Proof.
Lemma lte_sqr x y : 0 <= x -> 0 <= y -> (x ^+ 2 < y ^+ 2) = (x < y).
Proof.
Lemma lee_sqrE x y : 0 <= y -> x ^+ 2 <= y ^+ 2 -> x <= y.
Proof.
Lemma lte_sqrE x y : 0 <= y -> x ^+ 2 < y ^+ 2 -> x < y.
Proof.
move=> yge0; have [xge0|xlt0 x2ley2] := leP 0 x; first by rewrite lte_sqr.
exact: lt_le_trans xlt0 _.
Qed.
exact: lt_le_trans xlt0 _.
Qed.
Lemma sqre_ge0 x : 0 <= x ^+ 2.
Lemma lee_paddl y x z : 0 <= x -> y <= z -> y <= x + z.
Lemma lte_paddl y x z : 0 <= x -> y < z -> y < x + z.
Proof.
Lemma lee_paddr y x z : 0 <= x -> y <= z -> y <= z + x.
Lemma lte_paddr y x z : 0 <= x -> y < z -> y < z + x.
Lemma lte_spaddre z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.
Lemma lte_spadder z x y : x \is a fin_num -> 0 < y -> z <= x -> z < x + y.
Proof.
End ERealArithTh_realDomainType.
Arguments lee_sum_nneg_ord {R}.
Arguments lee_sum_npos_ord {R}.
Arguments lee_sum_nneg_natr {R}.
Arguments lee_sum_npos_natr {R}.
Arguments lee_sum_nneg_natl {R}.
Arguments lee_sum_npos_natl {R}.
#[global] Hint Extern 0 (is_true (0 <= `| _ |)%E) => solve [apply: abse_ge0] : core.
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDl instead.")]
Notation lee_addl := leeDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeDr instead.")]
Notation lee_addr := leeDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD2l instead.")]
Notation lee_add2l := leeD2l (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD2r instead.")]
Notation lee_add2r := leeD2r (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD instead.")]
Notation lee_add := leeD (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeB instead.")]
Notation lee_sub := leeB (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeD2lE instead.")]
Notation lee_add2lE := leeD2lE (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeNl instead.")]
Notation lee_oppl := leeNl (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use leeNr instead.")]
Notation lee_oppr := leeNr (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteNl instead.")]
Notation lte_oppl := lteNl (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteNr instead.")]
Notation lte_oppr := lteNr (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteD instead.")]
Notation lte_add := lteD (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteD2lE instead.")]
Notation lte_add2lE := lteD2lE (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteDl instead.")]
Notation lte_addl := lteDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.1.0", note="Use lteDr instead.")]
Notation lte_addr := lteDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use gee_pMl instead.")]
Notation gee_pmull := gee_pMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use geeDl instead.")]
Notation gee_addl := geeDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use geeDr instead.")]
Notation gee_addr := geeDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use gteDr instead.")]
Notation gte_addr := gteDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use gteDl instead.")]
Notation gte_addl := gteDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBlDr instead.")]
Notation lte_subl_addr := lteBlDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBlDl instead.")]
Notation lte_subl_addl := lteBlDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBrDr instead.")]
Notation lte_subr_addr := lteBrDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use lteBrDl instead.")]
Notation lte_subr_addl := lteBrDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBlDr instead.")]
Notation lee_subl_addr := leeBlDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBlDl instead.")]
Notation lee_subl_addl := leeBlDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBrDr instead.")]
Notation lee_subr_addr := leeBrDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="Use leeBrDl instead.")]
Notation lee_subr_addl := leeBrDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leD` instead.")]
Notation lte_le_add := lte_leD (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lee_ltD` instead.")]
Notation lee_lt_add := lee_ltD (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="Use `lte_leB` instead.")]
Notation lte_le_sub := lte_leB (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="Use leeN2 instead.")]
Notation lee_opp2 := leeN2 (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="Use lteN2 instead.")]
Notation lte_opp2 := lteN2 (only parsing).
#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMr")]
Notation maxeMr := maxe_pMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to maxe_pMl")]
Notation maxeMl := maxe_pMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to mine_pMr")]
Notation mineMr := mine_pMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.8.0", note="renamed to mine_pMl")]
Notation mineMl := mine_pMl (only parsing).
Module DualAddTheoryRealDomain.
Section DualERealArithTh_realDomainType.
Import DualAddTheoryNumDomain.
Local Open Scope ereal_dual_scope.
Context {R : realDomainType}.
Implicit Types x y z a b : \bar^d R.
Lemma dsube_lt0 x y : (x - y < 0) = (x < y).
Proof.
Lemma dsube_ge0 x y : (0 <= y - x) = (x <= y).
Proof.
Lemma dsuber_le0 x y : y \is a fin_num -> (x - y <= 0) = (x <= y).
Proof.
Lemma dsubre_le0 y x : y \is a fin_num -> (y - x <= 0) = (y <= x).
Proof.
Lemma dsube_le0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(y - x <= 0) = (y <= x).
Proof.
Lemma lte_dD a b x y : a < b -> x < y -> a + x < b + y.
Proof.
Lemma lee_dDl x y : 0 <= y -> x <= x + y.
Proof.
Lemma lee_dDr x y : 0 <= y -> x <= y + x.
Proof.
Lemma gee_dDl x y : y <= 0 -> x + y <= x.
Proof.
Lemma gee_dDr x y : y <= 0 -> y + x <= x.
Proof.
Lemma lte_dDl y x : y \is a fin_num -> (y < y + x) = (0 < x).
Proof.
Lemma lte_dDr y x : y \is a fin_num -> (y < x + y) = (0 < x).
Proof.
Lemma gte_dBl y x : y \is a fin_num -> (y - x < y) = (0 < x).
Proof.
Lemma gte_dBr y x : y \is a fin_num -> (- x + y < y) = (0 < x).
Proof.
Lemma gte_dDl x y : x \is a fin_num -> (x + y < x) = (y < 0).
Lemma gte_dDr x y : x \is a fin_num -> (y + x < x) = (y < 0).
Lemma lte_dD2lE x a b : x \is a fin_num -> (x + a < x + b) = (a < b).
Proof.
Lemma lte_dD2rE x a b : x \is a fin_num -> (a + x < b + x) = (a < b).
Proof.
Lemma lee_dD2rE x a b : x \is a fin_num -> (a + x <= b + x) = (a <= b).
Proof.
Lemma lee_dD2l x a b : a <= b -> x + a <= x + b.
Proof.
Lemma lee_dD2lE x a b : x \is a fin_num -> (x + a <= x + b) = (a <= b).
Proof.
Lemma lee_dD2r x a b : a <= b -> a + x <= b + x.
Proof.
Lemma lee_dD a b x y : a <= b -> x <= y -> a + x <= b + y.
Proof.
Lemma lte_le_dD a b x y : b \is a fin_num -> a < x -> b <= y -> a + b < x + y.
Proof.
Lemma lee_lt_dD a b x y : a \is a fin_num -> a <= x -> b < y -> a + b < x + y.
Lemma lee_dB x y z t : x <= y -> t <= z -> x - z <= y - t.
Lemma lte_le_dB z u x y : u \is a fin_num -> x < z -> u <= y -> x - y < z - u.
Proof.
Lemma lee_dsum I (f g : I -> \bar^d R) s (P : pred I) :
(forall i, P i -> f i <= g i) ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | P i) g i.
Proof.
Lemma lee_dsum_nneg_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar^d R) :
{subset Q <= P} -> {in [predD P & Q], forall i, 0 <= f i} ->
\sum_(i <- s | Q i) f i <= \sum_(i <- s | P i) f i.
Proof.
move=> QP PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_subset => [//|i iPQ]; rewrite oppe_le0; exact: PQf.
Qed.
apply: lee_sum_npos_subset => [//|i iPQ]; rewrite oppe_le0; exact: PQf.
Qed.
Lemma lee_dsum_npos_subset I (s : seq I) (P Q : {pred I}) (f : I -> \bar^d R) :
{subset Q <= P} -> {in [predD P & Q], forall i, f i <= 0} ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | Q i) f i.
Proof.
move=> QP PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_subset => [//|i iPQ]; rewrite oppe_ge0; exact: PQf.
Qed.
apply: lee_sum_nneg_subset => [//|i iPQ]; rewrite oppe_ge0; exact: PQf.
Qed.
Lemma lee_dsum_nneg (I : eqType) (s : seq I) (P Q : pred I)
(f : I -> \bar^d R) : (forall i, P i -> ~~ Q i -> 0 <= f i) ->
\sum_(i <- s | P i && Q i) f i <= \sum_(i <- s | P i) f i.
Proof.
move=> PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos => i Pi nQi; rewrite oppe_le0; exact: PQf.
Qed.
apply: lee_sum_npos => i Pi nQi; rewrite oppe_le0; exact: PQf.
Qed.
Lemma lee_dsum_npos (I : eqType) (s : seq I) (P Q : pred I)
(f : I -> \bar^d R) : (forall i, P i -> ~~ Q i -> f i <= 0) ->
\sum_(i <- s | P i) f i <= \sum_(i <- s | P i && Q i) f i.
Proof.
move=> PQf; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg => i Pi nQi; rewrite oppe_ge0; exact: PQf.
Qed.
apply: lee_sum_nneg => i Pi nQi; rewrite oppe_ge0; exact: PQf.
Qed.
Lemma lee_dsum_nneg_ord (f : nat -> \bar^d R) (P : pred nat) :
(forall n, P n -> 0 <= f n)%E ->
{homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}.
Proof.
move=> f0 m n mlen; rewrite !dual_sumeE leeN2.
apply: (lee_sum_npos_ord (fun i => - f i)%E) => [i Pi|//].
rewrite oppe_le0; exact: f0.
Qed.
apply: (lee_sum_npos_ord (fun i => - f i)%E) => [i Pi|//].
rewrite oppe_le0; exact: f0.
Qed.
Lemma lee_dsum_npos_ord (f : nat -> \bar^d R) (P : pred nat) :
(forall n, P n -> f n <= 0)%E ->
{homo (fun n => \sum_(i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
Proof.
move=> f0 m n mlen; rewrite !dual_sumeE leeN2.
apply: (lee_sum_nneg_ord (fun i => - f i)%E) => [i Pi|//].
rewrite oppe_ge0; exact: f0.
Qed.
apply: (lee_sum_nneg_ord (fun i => - f i)%E) => [i Pi|//].
rewrite oppe_ge0; exact: f0.
Qed.
Lemma lee_dsum_nneg_natr (f : nat -> \bar^d R) (P : pred nat) m :
(forall n, (m <= n)%N -> P n -> 0 <= f n) ->
{homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}.
Proof.
move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_natr => [n ? ?|//]; rewrite oppe_le0; exact: f0.
Qed.
apply: lee_sum_npos_natr => [n ? ?|//]; rewrite oppe_le0; exact: f0.
Qed.
Lemma lee_dsum_npos_natr (f : nat -> \bar^d R) (P : pred nat) m :
(forall n, (m <= n)%N -> P n -> f n <= 0) ->
{homo (fun n => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
Proof.
move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_natr => [n ? ?|//]; rewrite oppe_ge0; exact: f0.
Qed.
apply: lee_sum_nneg_natr => [n ? ?|//]; rewrite oppe_ge0; exact: f0.
Qed.
Lemma lee_dsum_nneg_natl (f : nat -> \bar^d R) (P : pred nat) n :
(forall m, (m < n)%N -> P m -> 0 <= f m) ->
{homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> j <= i}.
Proof.
move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_natl => [m ? ?|//]; rewrite oppe_le0; exact: f0.
Qed.
apply: lee_sum_npos_natl => [m ? ?|//]; rewrite oppe_le0; exact: f0.
Qed.
Lemma lee_dsum_npos_natl (f : nat -> \bar^d R) (P : pred nat) n :
(forall m, (m < n)%N -> P m -> f m <= 0) ->
{homo (fun m => \sum_(m <= i < n | P i) (f i)) : i j / (i <= j)%N >-> i <= j}.
Proof.
move=> f0 i j le_ij; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_natl => [m ? ?|//]; rewrite oppe_ge0; exact: f0.
Qed.
apply: lee_sum_nneg_natl => [m ? ?|//]; rewrite oppe_ge0; exact: f0.
Qed.
Lemma lee_dsum_nneg_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T -> \bar^d R) : {subset A <= B} ->
{in [predD B & A], forall t, P t -> 0 <= f t} ->
\sum_(t <- A | P t) f t <= \sum_(t <- B | P t) f t.
Proof.
move=> AB f0; rewrite !dual_sumeE leeN2.
apply: lee_sum_npos_subfset => [//|? ? ?]; rewrite oppe_le0; exact: f0.
Qed.
apply: lee_sum_npos_subfset => [//|? ? ?]; rewrite oppe_le0; exact: f0.
Qed.
Lemma lee_dsum_npos_subfset (T : choiceType) (A B : {fset T}%fset) (P : pred T)
(f : T -> \bar^d R) : {subset A <= B} ->
{in [predD B & A], forall t, P t -> f t <= 0} ->
\sum_(t <- B | P t) f t <= \sum_(t <- A | P t) f t.
Proof.
move=> AB f0; rewrite !dual_sumeE leeN2.
apply: lee_sum_nneg_subfset => [//|? ? ?]; rewrite oppe_ge0; exact: f0.
Qed.
apply: lee_sum_nneg_subfset => [//|? ? ?]; rewrite oppe_ge0; exact: f0.
Qed.
Lemma lte_dBlDr x y z : y \is a fin_num -> (x - y < z) = (x < z + y).
Proof.
Lemma lte_dBlDl x y z : y \is a fin_num -> (x - y < z) = (x < y + z).
Proof.
Lemma lte_dBrDr x y z : z \is a fin_num -> (x < y - z) = (x + z < y).
Proof.
Lemma lte_dBrDl x y z : z \is a fin_num -> (x < y - z) = (z + x < y).
Proof.
Lemma lte_dsuber_addr x y z : y \is a fin_num -> (x < y - z) = (x + z < y).
Proof.
Lemma lte_dsuber_addl x y z : y \is a fin_num -> (x < y - z) = (z + x < y).
Proof.
Lemma lte_dsubel_addr x y z : z \is a fin_num -> (x - y < z) = (x < z + y).
Proof.
Lemma lte_dsubel_addl x y z : z \is a fin_num -> (x - y < z) = (x < y + z).
Proof.
Lemma lee_dsubl_addr x y z : y \is a fin_num -> (x - y <= z) = (x <= z + y).
Proof.
Lemma lee_dsubl_addl x y z : y \is a fin_num -> (x - y <= z) = (x <= y + z).
Proof.
Lemma lee_dsubr_addr x y z : z \is a fin_num -> (x <= y - z) = (x + z <= y).
Proof.
Lemma lee_dsubr_addl x y z : z \is a fin_num -> (x <= y - z) = (z + x <= y).
Proof.
Lemma lee_dsubel_addr x y z : x \is a fin_num -> (x - y <= z) = (x <= z + y).
Proof.
Lemma lee_dsubel_addl x y z : x \is a fin_num -> (x - y <= z) = (x <= y + z).
Proof.
Lemma lee_dsuber_addr x y z : x \is a fin_num -> (x <= y - z) = (x + z <= y).
Proof.
Lemma lee_dsuber_addl x y z : x \is a fin_num -> (x <= y - z) = (z + x <= y).
Proof.
Lemma dsuber_gt0 x y : x \is a fin_num -> (0 < y - x) = (x < y).
Lemma dsubre_gt0 x y : y \is a fin_num -> (0 < y - x) = (x < y).
Proof.
Lemma dsube_gt0 x y : (x \is a fin_num) || (y \is a fin_num) ->
(0 < y - x) = (x < y).
Proof.
Lemma dmuleDr x y z : x \is a fin_num -> y +? z -> x * (y + z) = x * y + x * z.
Proof.
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.
Proof.
Lemma dge0_muleDr x y z : 0 <= y -> 0 <= z -> x * (y + z) = x * y + x * z.
Proof.
Lemma dle0_muleDl x y z : y <= 0 -> z <= 0 -> (y + z) * x = y * x + z * x.
Proof.
Lemma dle0_muleDr x y z : y <= 0 -> z <= 0 -> x * (y + z) = x * y + x * z.
Proof.
Lemma ge0_dsume_distrl (I : Type) (s : seq I) x (P : pred I)
(F : I -> \bar^d R) :
(forall i, P i -> 0 <= F i) ->
(\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x).
Proof.
move=> F0; rewrite !dual_sumeE !mulNe le0_sume_distrl => [|i Pi].
- by under eq_bigr => i _ do rewrite mulNe.
- by rewrite oppe_le0 F0.
Qed.
- by under eq_bigr => i _ do rewrite mulNe.
- by rewrite oppe_le0 F0.
Qed.
Lemma ge0_dsume_distrr (I : Type) (s : seq I) x (P : pred I)
(F : I -> \bar^d R) :
(forall i, P i -> 0 <= F i) ->
x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i).
Proof.
Lemma le0_dsume_distrl (I : Type) (s : seq I) x (P : pred I)
(F : I -> \bar^d R) :
(forall i, P i -> F i <= 0) ->
(\sum_(i <- s | P i) F i) * x = \sum_(i <- s | P i) (F i * x).
Proof.
move=> F0; rewrite !dual_sumeE mulNe ge0_sume_distrl => [|i Pi].
- by under eq_bigr => i _ do rewrite mulNe.
- by rewrite oppe_ge0 F0.
Qed.
- by under eq_bigr => i _ do rewrite mulNe.
- by rewrite oppe_ge0 F0.
Qed.
Lemma le0_dsume_distrr (I : Type) (s : seq I) x (P : pred I)
(F : I -> \bar^d R) :
(forall i, P i -> F i <= 0) ->
x * (\sum_(i <- s | P i) F i) = \sum_(i <- s | P i) (x * F i).
Proof.
Lemma lee_abs_dadd x y : `|x + y| <= `|x| + `|y|.
Lemma lee_abs_dsum (I : Type) (s : seq I) (F : I -> \bar^d R) (P : pred I) :
`|\sum_(i <- s | P i) F i| <= \sum_(i <- s | P i) `|F i|.
Proof.
elim/big_ind2 : _ => //; first by rewrite abse0.
by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dD _ _)).
Qed.
by move=> *; exact/(le_trans (lee_abs_dadd _ _) (lee_dD _ _)).
Qed.
Lemma lee_abs_dsub x y : `|x - y| <= `|x| + `|y|.
Lemma dadde_minl : left_distributive (@GRing.add (\bar^d R)) mine.
Proof.
Lemma dadde_minr : right_distributive (@GRing.add (\bar^d R)) mine.
Proof.
Lemma dmule_natl x n : n%:R%:E * x = x *+ n.
Lemma lee_pdaddl y x z : 0 <= x -> y <= z -> y <= x + z.
Lemma lte_pdaddl y x z : 0 <= x -> y < z -> y < x + z.
Proof.
Lemma lee_pdaddr y x z : 0 <= x -> y <= z -> y <= z + x.
Proof.
Lemma lte_pdaddr y x z : 0 <= x -> y < z -> y < z + x.
Proof.
Lemma lte_spdaddre z x y : z \is a fin_num -> 0 < y -> z <= x -> z < x + y.
Proof.
Lemma lte_spdadder z x y : x \is a fin_num -> 0 < y -> z <= x -> z < x + y.
Proof.
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}.
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD`")]
Notation lte_dadd := lte_dD (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDl`")]
Notation lee_daddl := lee_dDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dDr`")]
Notation lee_daddr := lee_dDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDl`")]
Notation gee_daddl := gee_dDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gee_dDr`")]
Notation gee_daddr := gee_dDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDl`")]
Notation lte_daddl := lte_dDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dDr`")]
Notation lte_daddr := lte_dDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBl`")]
Notation gte_dsubl := gte_dBl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dBr`")]
Notation gte_dsubr := gte_dBr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDl`")]
Notation gte_daddl := gte_dDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `gte_dDr`")]
Notation gte_daddr := gte_dDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dD2lE`")]
Notation lte_dadd2lE := lte_dD2lE (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2rE`")]
Notation lee_dadd2rE := lee_dD2rE (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2l`")]
Notation lee_dadd2l := lee_dD2l (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD2r`")]
Notation lee_dadd2r := lee_dD2r (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dD`")]
Notation lee_dadd := lee_dD (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_dB`")]
Notation lee_dsub := lee_dB (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDr`")]
Notation lte_dsubl_addr := lte_dBlDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBlDl`")]
Notation lte_dsubl_addl := lte_dBlDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDr`")]
Notation lte_dsubr_addr := lte_dBrDr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_dBrDl`")]
Notation lte_dsubr_addl := lte_dBrDl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dD`")]
Notation lte_le_dadd := lte_le_dD (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_lt_dD`")]
Notation lee_lt_dadd := lee_lt_dD (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_le_dB`")]
Notation lte_le_dsub := lte_le_dD (only parsing).
End DualAddTheoryRealDomain.
Section realFieldType_lemmas.
Variable R : realFieldType.
Implicit Types x y : \bar R.
Implicit Types r : R.
Lemma lee_addgt0Pr x y :
reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).
Proof.
apply/(iffP idP) => [|].
- move: x y => [x| |] [y| |]//.
+ by rewrite lee_fin => xy e e0; rewrite -EFinD lee_fin ler_wpDr// ltW.
+ by move=> _ e e0; rewrite leNye.
- move: x y => [x| |] [y| |]// xy; rewrite ?leey ?leNye//;
[|by move: xy => /(_ _ lte01)..].
by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy.
Qed.
- move: x y => [x| |] [y| |]//.
+ by rewrite lee_fin => xy e e0; rewrite -EFinD lee_fin ler_wpDr// ltW.
+ by move=> _ e e0; rewrite leNye.
- move: x y => [x| |] [y| |]// xy; rewrite ?leey ?leNye//;
[|by move: xy => /(_ _ lte01)..].
by rewrite lee_fin; apply/ler_addgt0Pr => e e0; rewrite -lee_fin EFinD xy.
Qed.
Lemma lee_subgt0Pr x y :
reflect (forall e, (0 < e)%R -> x - e%:E <= y) (x <= y).
Proof.
apply/(iffP idP) => [xy e|xy].
by rewrite leeBlDr//; move: e; exact/lee_addgt0Pr.
by apply/lee_addgt0Pr => e e0; rewrite -leeBlDr// xy.
Qed.
by rewrite leeBlDr//; move: e; exact/lee_addgt0Pr.
by apply/lee_addgt0Pr => e e0; rewrite -leeBlDr// xy.
Qed.
Lemma lee_mul01Pr x y : 0 <= x ->
reflect (forall r, (0 < r < 1)%R -> r%:E * x <= y) (x <= y).
Proof.
move=> x0; apply/(iffP idP) => [xy r /andP[r0 r1]|h].
move: x0 xy; rewrite le_eqVlt => /predU1P[<-|x0 xy]; first by rewrite mule0.
by rewrite (le_trans _ xy)// gee_pMl// ltW.
have h01 : (0 < (2^-1 : R) < 1)%R by rewrite invr_gt0 ?invf_lt1 ?ltr0n ?ltr1n.
move: x y => [x||] [y||] // in x0 h *.
- move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0].
by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin.
have y0 : (0 < y)%R.
by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin.
rewrite lee_fin leNgt; apply/negP => yx.
have /h : (0 < (y + x) / (2 * x) < 1)%R.
apply/andP; split; first by rewrite divr_gt0 // ?addr_gt0// ?mulr_gt0.
by rewrite ltr_pdivrMr ?mulr_gt0// mul1r mulr_natl mulr2n ltrD2r.
rewrite -(EFinM _ x) lee_fin invrM ?unitfE// ?gt_eqF// -mulrA mulrAC.
by rewrite mulVr ?unitfE ?gt_eqF// mul1r; apply/negP; rewrite -ltNge midf_lt.
- by rewrite leey.
- by have := h _ h01.
- by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
- by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
Qed.
move: x0 xy; rewrite le_eqVlt => /predU1P[<-|x0 xy]; first by rewrite mule0.
by rewrite (le_trans _ xy)// gee_pMl// ltW.
have h01 : (0 < (2^-1 : R) < 1)%R by rewrite invr_gt0 ?invf_lt1 ?ltr0n ?ltr1n.
move: x y => [x||] [y||] // in x0 h *.
- move: (x0); rewrite lee_fin le_eqVlt => /predU1P[<-|{}x0].
by rewrite (le_trans _ (h _ h01))// mule_ge0// lee_fin.
have y0 : (0 < y)%R.
by rewrite -lte_fin (lt_le_trans _ (h _ h01))// mule_gt0// lte_fin.
rewrite lee_fin leNgt; apply/negP => yx.
have /h : (0 < (y + x) / (2 * x) < 1)%R.
apply/andP; split; first by rewrite divr_gt0 // ?addr_gt0// ?mulr_gt0.
by rewrite ltr_pdivrMr ?mulr_gt0// mul1r mulr_natl mulr2n ltrD2r.
rewrite -(EFinM _ x) lee_fin invrM ?unitfE// ?gt_eqF// -mulrA mulrAC.
by rewrite mulVr ?unitfE ?gt_eqF// mul1r; apply/negP; rewrite -ltNge midf_lt.
- by rewrite leey.
- by have := h _ h01.
- by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
- by have := h _ h01; rewrite mulr_infty sgrV gtr0_sg // mul1e.
Qed.
Lemma lte_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y < x) = (y < r%:E * x).
Proof.
move=> r0; move: x y => [x| |] [y| |] //=.
- by rewrite 2!lte_fin ltr_pdivrMl.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e 2!ltNge 2!leey.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e -EFinM 2!ltNyr.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltry.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e ltxx.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
Qed.
- by rewrite 2!lte_fin ltr_pdivrMl.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e 2!ltNge 2!leey.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e -EFinM 2!ltNyr.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltry.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e ltxx.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
Qed.
Lemma lte_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E < x) = (y < x * r%:E).
Proof.
Lemma lte_pdivlMl r y x : (0 < r)%R -> (x < r^-1%:E * y) = (r%:E * x < y).
Proof.
move=> r0; move: x y => [x| |] [y| |] //=.
- by rewrite 2!lte_fin ltr_pdivlMl.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e 2!ltry.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltNyr.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
Qed.
- by rewrite 2!lte_fin ltr_pdivlMl.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e 2!ltry.
- by rewrite mulr_infty sgrV gtr0_sg// mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty gtr0_sg// mul1e 2!ltNyr.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// 2!mul1e.
- by rewrite mulr_infty [in RHS]mulr_infty sgrV gtr0_sg// mul1e.
Qed.
Lemma lte_pdivlMr r x y : (0 < r)%R -> (x < y * r^-1%:E) = (x * r%:E < y).
Proof.
Lemma lte_ndivlMr r x y : (r < 0)%R -> (x < y * r^-1%:E) = (y < x * r%:E).
Proof.
Lemma lte_ndivlMl r x y : (r < 0)%R -> (x < r^-1%:E * y) = (y < r%:E * x).
Proof.
Lemma lte_ndivrMl r x y : (r < 0)%R -> (r^-1%:E * y < x) = (r%:E * x < y).
Proof.
Lemma lte_ndivrMr r x y : (r < 0)%R -> (y * r^-1%:E < x) = (x * r%:E < y).
Proof.
Lemma lee_pdivrMl r x y : (0 < r)%R -> (r^-1%:E * y <= x) = (y <= r%:E * x).
Proof.
Lemma lee_pdivrMr r x y : (0 < r)%R -> (y * r^-1%:E <= x) = (y <= x * r%:E).
Proof.
Lemma lee_pdivlMl r y x : (0 < r)%R -> (x <= r^-1%:E * y) = (r%:E * x <= y).
Proof.
Lemma lee_pdivlMr r x y : (0 < r)%R -> (x <= y * r^-1%:E) = (x * r%:E <= y).
Proof.
Lemma lee_ndivlMr r x y : (r < 0)%R -> (x <= y * r^-1%:E) = (y <= x * r%:E).
Proof.
Lemma lee_ndivlMl r x y : (r < 0)%R -> (x <= r^-1%:E * y) = (y <= r%:E * x).
Proof.
Lemma lee_ndivrMl r x y : (r < 0)%R -> (r^-1%:E * y <= x) = (r%:E * x <= y).
Proof.
Lemma lee_ndivrMr r x y : (r < 0)%R -> (y * r^-1%:E <= x) = (x * r%:E <= y).
Proof.
Lemma eqe_pdivrMl r x y : (r != 0)%R ->
((r^-1)%:E * y == x) = (y == r%:E * x).
Proof.
rewrite neq_lt => /orP[|] r0.
- by rewrite eq_le lee_ndivrMl// lee_ndivlMl// -eq_le.
- by rewrite eq_le lee_pdivrMl// lee_pdivlMl// -eq_le.
Qed.
- by rewrite eq_le lee_ndivrMl// lee_ndivlMl// -eq_le.
- by rewrite eq_le lee_pdivrMl// lee_pdivlMl// -eq_le.
Qed.
End realFieldType_lemmas.
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMl`")]
Notation lte_pdivr_mull := lte_pdivrMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivrMr`")]
Notation lte_pdivr_mulr := lte_pdivrMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMl`")]
Notation lte_pdivl_mull := lte_pdivlMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_pdivlMr`")]
Notation lte_pdivl_mulr := lte_pdivlMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMl`")]
Notation lee_pdivr_mull := lee_pdivrMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivrMr`")]
Notation lee_pdivr_mulr := lee_pdivrMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMl`")]
Notation lee_pdivl_mull := lee_pdivlMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_pdivlMr`")]
Notation lee_pdivl_mulr := lee_pdivlMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMl`")]
Notation lte_ndivr_mull := lte_ndivrMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivrMr`")]
Notation lte_ndivr_mulr := lte_ndivrMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMl`")]
Notation lte_ndivl_mull := lte_ndivlMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lte_ndivlMr`")]
Notation lte_ndivl_mulr := lte_ndivlMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMl`")]
Notation lee_ndivr_mull := lee_ndivrMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivrMr`")]
Notation lee_ndivr_mulr := lee_ndivrMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMl`")]
Notation lee_ndivl_mull := lee_ndivlMl (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `lee_ndivlMr`")]
Notation lee_ndivl_mulr := lee_ndivlMr (only parsing).
#[deprecated(since="mathcomp-analysis 1.3.0", note="renamed `eqe_pdivrMl`")]
Notation eqe_pdivr_mull := eqe_pdivrMl (only parsing).
Module DualAddTheoryRealField.
Import DualAddTheoryNumDomain DualAddTheoryRealDomain.
Section DualRealFieldType_lemmas.
Local Open Scope ereal_dual_scope.
Variable R : realFieldType.
Implicit Types x y : \bar^d R.
Lemma lee_daddgt0Pr x y :
reflect (forall e, (0 < e)%R -> x <= y + e%:E) (x <= y).
Proof.
End DualRealFieldType_lemmas.
End DualAddTheoryRealField.
Section sqrte.
Variable R : rcfType.
Implicit Types x y : \bar R.
Definition sqrte x :=
if x is +oo then +oo else if x is r%:E then (Num.sqrt r)%:E else 0.
Lemma sqrte0 : sqrte 0 = 0 :> \bar R.
Proof.
Lemma sqrte_ge0 x : 0 <= sqrte x.
Lemma lee_sqrt x y : 0 <= y -> (sqrte x <= sqrte y) = (x <= y).
Proof.
Lemma sqrteM x y : 0 <= x -> sqrte (x * y) = sqrte x * sqrte y.
Proof.
case: x y => [x||] [y||] //= age0.
- by rewrite sqrtrM ?EFinM.
- move: age0; rewrite le_eqVlt eqe => /predU1P[<-|x0].
by rewrite mul0e sqrte0 sqrtr0 mul0e.
by rewrite mulry gtr0_sg ?mul1e// mulry gtr0_sg ?mul1e// sqrtr_gt0.
- move: age0; rewrite mule0 mulrNy lee_fin -sgr_ge0.
by case: sgrP; rewrite ?mul0e ?sqrte0// ?mul1e// ler0N1.
- rewrite !mulyr; case: (sgrP y) => [->||].
+ by rewrite sqrtr0 sgr0 mul0e sqrte0.
+ by rewrite mul1e/= -sqrtr_gt0 -sgr_gt0 -lte_fin => /gt0_muley->.
+ by move=> y0; rewrite EFinN mulN1e/= ltr0_sqrtr// sgr0 mul0e.
- by rewrite mulyy.
- by rewrite mulyNy mule0.
Qed.
- by rewrite sqrtrM ?EFinM.
- move: age0; rewrite le_eqVlt eqe => /predU1P[<-|x0].
by rewrite mul0e sqrte0 sqrtr0 mul0e.
by rewrite mulry gtr0_sg ?mul1e// mulry gtr0_sg ?mul1e// sqrtr_gt0.
- move: age0; rewrite mule0 mulrNy lee_fin -sgr_ge0.
by case: sgrP; rewrite ?mul0e ?sqrte0// ?mul1e// ler0N1.
- rewrite !mulyr; case: (sgrP y) => [->||].
+ by rewrite sqrtr0 sgr0 mul0e sqrte0.
+ by rewrite mul1e/= -sqrtr_gt0 -sgr_gt0 -lte_fin => /gt0_muley->.
+ by move=> y0; rewrite EFinN mulN1e/= ltr0_sqrtr// sgr0 mul0e.
- by rewrite mulyy.
- by rewrite mulyNy mule0.
Qed.
Lemma sqr_sqrte x : 0 <= x -> sqrte x ^+ 2 = x.
Proof.
Lemma sqrte_sqr x : sqrte (x ^+ 2) = `|x|%E.
Lemma sqrte_fin_num x : 0 <= x -> (sqrte x \is a fin_num) = (x \is a fin_num).
Proof.
End sqrte.
Module DualAddTheory.
Export DualAddTheoryNumDomain.
Export DualAddTheoryRealDomain.
Export DualAddTheoryRealField.
End DualAddTheory.
Module ConstructiveDualAddTheory.
Export DualAddTheory.
End ConstructiveDualAddTheory.
Section Itv.
Context {R : numDomainType}.
Definition ext_num_sem (i : interval int) (x : \bar R) :=
(0 >=< x)%O && (x \in map_itv (EFin \o intr) i).
Local Notation num_spec := (Itv.spec (@Itv.num_sem _)).
Local Notation num_def R := (Itv.def (@Itv.num_sem R)).
Local Notation num_itv_bound R := (@map_itv_bound _ R intr).
Local Notation ext_num_spec := (Itv.spec ext_num_sem).
Local Notation ext_num_def := (Itv.def ext_num_sem).
Local Notation ext_num_itv_bound :=
(@map_itv_bound _ (\bar R) (EFin \o intr)).
Lemma ext_num_num_sem i (x : R) : Itv.ext_num_sem i x%:E = Itv.num_sem i x.
Proof.
Lemma ext_num_num_spec i (x : R) : ext_num_spec i x%:E = num_spec i x.
Proof.
Lemma le_map_itv_bound_EFin (x y : itv_bound R) :
(map_itv_bound EFin x <= map_itv_bound EFin y)%O = (x <= y)%O.
Proof.
by case: x y => [xb x | x] [yb y | y]. Qed.
Lemma map_itv_bound_EFin_le_BLeft (x : itv_bound R) (y : R) :
(map_itv_bound EFin x <= BLeft y%:E)%O = (x <= BLeft y)%O.
Proof.
Lemma BRight_le_map_itv_bound_EFin (x : R) (y : itv_bound R) :
(BRight x%:E <= map_itv_bound EFin y)%O = (BRight x <= y)%O.
Proof.
Lemma le_ext_num_itv_bound (x y : itv_bound int) :
(ext_num_itv_bound x <= ext_num_itv_bound y)%O = (x <= y)%O.
Proof.
Lemma ext_num_spec_sub (x y : Itv.t) : Itv.sub x y ->
forall z : \bar R, ext_num_spec x z -> ext_num_spec y z.
Proof.
case: x y => [| x] [| y] //= x_sub_y z /andP[rz]; rewrite /Itv.ext_num_sem rz/=.
move: x y x_sub_y => [lx ux] [ly uy] /andP[lel leu] /=.
move=> /andP[lxz zux]; apply/andP; split.
- by apply: le_trans lxz; rewrite le_ext_num_itv_bound.
- by apply: le_trans zux _; rewrite le_ext_num_itv_bound.
Qed.
move: x y x_sub_y => [lx ux] [ly uy] /andP[lel leu] /=.
move=> /andP[lxz zux]; apply/andP; split.
- by apply: le_trans lxz; rewrite le_ext_num_itv_bound.
- by apply: le_trans zux _; rewrite le_ext_num_itv_bound.
Qed.
Section ItvTheory.
Context {i : Itv.t}.
Implicit Type x : ext_num_def i.
Lemma ext_widen_itv_subproof x i' : Itv.sub i i' ->
ext_num_spec i' x%:inum.
Proof.
Definition ext_widen_itv x i' (uni : unify_itv i i') :=
Itv.mk (ext_widen_itv_subproof x uni).
Lemma gt0e x : unify_itv i (Itv.Real `]0%Z, +oo[) -> 0%E < x%:inum :> \bar R.
Proof.
Lemma lte0 x : unify_itv i (Itv.Real `]-oo, 0%Z[) -> x%:inum < 0%E :> \bar R.
Proof.
Lemma ge0e x : unify_itv i (Itv.Real `[0%Z, +oo[) -> 0%E <= x%:inum :> \bar R.
Proof.
Lemma lee0 x : unify_itv i (Itv.Real `]-oo, 0%Z]) -> x%:inum <= 0%E :> \bar R.
Proof.
Lemma cmp0e x : unify_itv i (Itv.Real `]-oo, +oo[) -> (0%E >=< x%:inum)%O.
Lemma neqe0 x :
unify (fun ix iy => ~~ Itv.sub ix iy) (Itv.Real `[0%Z, 0%Z]) i ->
x%:inum != 0 :> \bar R.
Proof.
End ItvTheory.
End Itv.
Arguments gt0e {R i} _ {_}.
Arguments lte0 {R i} _ {_}.
Arguments ge0e {R i} _ {_}.
Arguments lee0 {R i} _ {_}.
Arguments cmp0e {R i} _ {_}.
Arguments neqe0 {R i} _ {_}.
Arguments ext_widen_itv {R i} _ {_ _}.
Definition posnume (R : numDomainType) of phant R :=
Itv.def (@ext_num_sem R) (Itv.Real `]0%Z, +oo[).
Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
Definition nonnege (R : numDomainType) of phant R :=
Itv.def (@ext_num_sem R) (Itv.Real `[0%Z, +oo[).
Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
Notation "x %:pos" := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:pos" := (ext_widen_itv x%:itv : {posnum \bar _}) (only parsing)
: ereal_scope.
Notation "x %:pos" := (@ext_widen_itv _ _
(@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _)
(only printing) : ereal_dual_scope.
Notation "x %:pos" := (@ext_widen_itv _ _
(@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `]Posz 0, +oo[) _)
(only printing) : ereal_scope.
Notation "x %:nng" := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:nng" := (ext_widen_itv x%:itv : {nonneg \bar _}) (only parsing)
: ereal_scope.
Notation "x %:nng" := (@ext_widen_itv _ _
(@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _)
(only printing) : ereal_dual_scope.
Notation "x %:nng" := (@ext_widen_itv _ _
(@Itv.from _ _ _ (Phantom _ x)) (Itv.Real `[Posz 0, +oo[) _)
(only printing) : ereal_scope.
#[export] Hint Extern 0 (is_true (0%R < _)%E) => solve [apply: gt0e] : core.
#[export] Hint Extern 0 (is_true (_ < 0%R)%E) => solve [apply: lte0] : core.
#[export] Hint Extern 0 (is_true (0%R <= _)%E) => solve [apply: ge0e] : core.
#[export] Hint Extern 0 (is_true (_ <= 0%R)%E) => solve [apply: lee0] : core.
#[export] Hint Extern 0 (is_true (0%R >=< _)%O) => solve [apply: cmp0e] : core.
#[export] Hint Extern 0 (is_true (_ != 0%R)%O) => solve [apply: neqe0] : core.
Module ItvInstances.
Import IntItv.
Import Instances.
Section Itv.
Context {R : numDomainType}.
Local Notation num_spec := (Itv.spec (@Itv.num_sem _)).
Local Notation num_def R := (Itv.def (@Itv.num_sem R)).
Local Notation num_itv_bound R := (@map_itv_bound _ R intr).
Local Notation ext_num_spec := (Itv.spec ext_num_sem).
Local Notation ext_num_def := (Itv.def ext_num_sem).
Local Notation ext_num_itv_bound := (@map_itv_bound _ (\bar R) (EFin \o intr)).
Lemma ext_num_spec_pinfty : ext_num_spec (Itv.Real `]1%Z, +oo[) (+oo : \bar R).
Canonical pinfty_inum := Itv.mk (ext_num_spec_pinfty).
Lemma ext_num_spec_ninfty :
ext_num_spec (Itv.Real `]-oo, (-1)%Z[) (-oo : \bar R).
Proof.
Canonical ninfty_snum := Itv.mk (ext_num_spec_ninfty).
Lemma ext_num_spec_EFin i (x : num_def R i) : ext_num_spec i x%:num%:E.
Proof.
Canonical EFin_inum i (x : num_def R i) := Itv.mk (ext_num_spec_EFin x).
Lemma num_spec_fine i (x : ext_num_def i) (r := Itv.real1 keep_sign i) :
num_spec r (fine x%:num : R).
Proof.
rewrite {}/r; case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
apply/and3P; split; rewrite -?real_fine//.
- case: x lx {xu xr} => [x||]/=; [|by case: l => [? []|]..].
by case: l => [[] [l |//] |//] /[!bnd_simp] => [|/ltW]/=; rewrite lee_fin;
apply: le_trans.
- case: x xu {lx xr} => [x||]/=; [|by case: u => [? [[]|] |]..].
by case: u => [bu [[|//] | u] |//]; case: bu => /[!bnd_simp] [/ltW|]/=;
rewrite lee_fin// => /le_trans; apply; rewrite lerz0.
Qed.
apply/and3P; split; rewrite -?real_fine//.
- case: x lx {xu xr} => [x||]/=; [|by case: l => [? []|]..].
by case: l => [[] [l |//] |//] /[!bnd_simp] => [|/ltW]/=; rewrite lee_fin;
apply: le_trans.
- case: x xu {lx xr} => [x||]/=; [|by case: u => [? [[]|] |]..].
by case: u => [bu [[|//] | u] |//]; case: bu => /[!bnd_simp] [/ltW|]/=;
rewrite lee_fin// => /le_trans; apply; rewrite lerz0.
Qed.
Canonical fine_inum i (x : ext_num_def i) := Itv.mk (num_spec_fine x).
Lemma ext_num_sem_y l u :
ext_num_sem (Interval l u) (+oo : \bar R) = ((l != +oo%O) && (u == +oo%O)).
Proof.
Lemma ext_num_sem_Ny l u :
ext_num_sem (Interval l u) (-oo : \bar R) = ((l == -oo%O) && (u != -oo%O)).
Proof.
apply/and3P/andP => [[_ ly uy] | [ly uy]]; split.
- by case: l ly => -[].
- by case: u uy => -[].
- exact: real0.
- by case: l ly => -[].
- case: u uy => [|[]//].
by case=> u _ /=; rewrite bnd_simp ?real_leNye ?real_ltNyr /= realz.
Qed.
- by case: l ly => -[].
- by case: u uy => -[].
- exact: real0.
- by case: l ly => -[].
- case: u uy => [|[]//].
by case=> u _ /=; rewrite bnd_simp ?real_leNye ?real_ltNyr /= realz.
Qed.
Lemma oppe_boundr (x : \bar R) b :
(BRight (- x) <= ext_num_itv_bound (opp_bound b))%O
= (ext_num_itv_bound b <= BLeft x)%O.
Lemma oppe_boundl (x : \bar R) b :
(ext_num_itv_bound (opp_bound b) <= BLeft (- x))%O
= (BRight x <= ext_num_itv_bound b)%O.
Lemma ext_num_spec_opp i (x : ext_num_def i) (r := Itv.real1 opp i) :
ext_num_spec r (- x%:inum : \bar R).
Proof.
rewrite {}/r; case: x => -[x||]/=;
[|by case: i => [//| [l u]]; rewrite /= ext_num_sem_y ext_num_sem_Ny;
case: l u => [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px.
by rewrite -[x]/(Itv.mk Px)%:inum num_spec_opp.
Qed.
[|by case: i => [//| [l u]]; rewrite /= ext_num_sem_y ext_num_sem_Ny;
case: l u => [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px.
by rewrite -[x]/(Itv.mk Px)%:inum num_spec_opp.
Qed.
Canonical oppe_inum i (x : ext_num_def i) := Itv.mk (ext_num_spec_opp x).
Lemma ext_num_spec_add xi yi (x : ext_num_def xi) (y : ext_num_def yi)
(r := Itv.real2 add xi yi) :
ext_num_spec r (adde x%:inum y%:inum : \bar R).
Proof.
rewrite {}/r; case: x y => -[x||] + [[y||]]/=;
[|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
rewrite /adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px Py.
by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum num_spec_add.
Qed.
[|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
rewrite /adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px Py.
by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum num_spec_add.
Qed.
Canonical adde_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) :=
Itv.mk (ext_num_spec_add x y).
Import DualAddTheory.
Lemma ext_num_spec_dEFin i (x : num_def R i) : ext_num_spec i (dEFin x%:num).
Proof.
Canonical dEFin_inum i (x : num_def R i) := Itv.mk (ext_num_spec_dEFin x).
Lemma ext_num_spec_dadd xi yi (x : ext_num_def xi) (y : ext_num_def yi)
(r := Itv.real2 add xi yi) :
ext_num_spec r (dual_adde x%:inum y%:inum : \bar^d R).
Proof.
rewrite {}/r; case: x y => -[x||] + [[y||]]/=;
[|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
rewrite /dual_adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px Py.
by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum num_spec_add.
Qed.
[|by case: xi yi => [//| [xl xu]] [//| [yl yu]];
rewrite /dual_adde/= ?ext_num_sem_y ?ext_num_sem_Ny;
case: xl xu yl yu => [[] ?|[]] [[] ?|[]] [[] ?|[]] [[] ?|[]]..].
rewrite !ext_num_num_spec => Px Py.
by rewrite -[x]/(Itv.mk Px)%:inum -[y]/(Itv.mk Py)%:inum num_spec_add.
Qed.
Canonical dadde_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) :=
Itv.mk (ext_num_spec_dadd x y).
Variant ext_sign_spec (l u : itv_bound int) (x : \bar R) : signi -> Set :=
| ISignEqZero : l = BLeft 0%Z -> u = BRight 0%Z -> x = 0 ->
ext_sign_spec l u x (Known EqZero)
| ISignNonNeg : (BLeft 0%:Z <= l)%O -> (BRight 0%:Z < u)%O -> 0 <= x ->
ext_sign_spec l u x (Known NonNeg)
| ISignNonPos : (l < BLeft 0%:Z)%O -> (u <= BRight 0%:Z)%O -> x <= 0 ->
ext_sign_spec l u x (Known NonPos)
| ISignBoth : (l < BLeft 0%:Z)%O -> (BRight 0%:Z < u)%O ->
(0 >=< x)%O -> ext_sign_spec l u x Unknown.
Lemma ext_signP (l u : itv_bound int) (x : \bar R) :
(ext_num_itv_bound l <= BLeft x)%O -> (BRight x <= ext_num_itv_bound u)%O ->
(0 >=< x)%O ->
ext_sign_spec l u x (sign (Interval l u)).
Proof.
case: x => [x||] xl xu xs.
- case: (@signP R l u x _ _ xs).
+ by case: l xl => -[].
+ by case: u xu => -[].
+ by move=> l0 u0 x0; apply: ISignEqZero => //; rewrite x0.
+ by move=> l0 u0 x0; apply: ISignNonNeg.
+ by move=> l0 u0 x0; apply: ISignNonPos.
+ by move=> l0 u0 x0; apply: ISignBoth.
- have uy : u = +oo%O by case: u xu => -[].
have u0 : (BRight 0%:Z < u)%O by rewrite uy.
case: (leP (BLeft 0%Z) l) => l0.
+ suff -> : sign (Interval l u) = Known NonNeg.
by apply: ISignNonNeg => //; apply: le0y.
rewrite /=/sign_boundl /sign_boundr uy/=.
by case: eqP => [//| /eqP lneq0]; case: ltgtP l0 lneq0.
+ suff -> : sign (Interval l u) = Unknown by exact: ISignBoth.
rewrite /=/sign_boundl /sign_boundr uy/=.
by case: eqP l0 => [->//| /eqP leq0] /ltW->.
- have ly : l = -oo%O by case: l xl => -[].
have l0 : (l < BLeft 0%:Z)%O by rewrite ly.
case: (leP u (BRight 0%Z)) => u0.
+ suff -> : sign (Interval l u) = Known NonPos by exact: ISignNonPos.
rewrite /=/sign_boundl /sign_boundr ly/=.
by case: eqP => [//| /eqP uneq0]; case: ltgtP u0 uneq0.
+ suff -> : sign (Interval l u) = Unknown by exact: ISignBoth.
rewrite /=/sign_boundl /sign_boundr ly/=.
by case: eqP u0 => [->//| /eqP ueq0]; rewrite ltNge => /negbTE->.
Qed.
- case: (@signP R l u x _ _ xs).
+ by case: l xl => -[].
+ by case: u xu => -[].
+ by move=> l0 u0 x0; apply: ISignEqZero => //; rewrite x0.
+ by move=> l0 u0 x0; apply: ISignNonNeg.
+ by move=> l0 u0 x0; apply: ISignNonPos.
+ by move=> l0 u0 x0; apply: ISignBoth.
- have uy : u = +oo%O by case: u xu => -[].
have u0 : (BRight 0%:Z < u)%O by rewrite uy.
case: (leP (BLeft 0%Z) l) => l0.
+ suff -> : sign (Interval l u) = Known NonNeg.
by apply: ISignNonNeg => //; apply: le0y.
rewrite /=/sign_boundl /sign_boundr uy/=.
by case: eqP => [//| /eqP lneq0]; case: ltgtP l0 lneq0.
+ suff -> : sign (Interval l u) = Unknown by exact: ISignBoth.
rewrite /=/sign_boundl /sign_boundr uy/=.
by case: eqP l0 => [->//| /eqP leq0] /ltW->.
- have ly : l = -oo%O by case: l xl => -[].
have l0 : (l < BLeft 0%:Z)%O by rewrite ly.
case: (leP u (BRight 0%Z)) => u0.
+ suff -> : sign (Interval l u) = Known NonPos by exact: ISignNonPos.
rewrite /=/sign_boundl /sign_boundr ly/=.
by case: eqP => [//| /eqP uneq0]; case: ltgtP u0 uneq0.
+ suff -> : sign (Interval l u) = Unknown by exact: ISignBoth.
rewrite /=/sign_boundl /sign_boundr ly/=.
by case: eqP u0 => [->//| /eqP ueq0]; rewrite ltNge => /negbTE->.
Qed.
Lemma ext_num_itv_mul_boundl b1 b2 (x1 x2 : \bar R) :
(BLeft 0%:Z <= b1 -> BLeft 0%:Z <= b2 ->
ext_num_itv_bound b1 <= BLeft x1 ->
ext_num_itv_bound b2 <= BLeft x2 ->
ext_num_itv_bound (mul_boundl b1 b2) <= BLeft (x1 * x2))%O.
Proof.
move=> b10 b20 b1x1 b2x2.
have x10 : 0 <= x1.
by case: x1 b1x1 (le_trans (eqbRL (le_ext_num_itv_bound _ _) b10) b1x1).
have x20 : 0 <= x2.
by case: x2 b2x2 (le_trans (eqbRL (le_ext_num_itv_bound _ _) b20) b2x2).
have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have ley b1' b2' :
(map_itv_bound EFin (num_itv_bound R (mul_boundl b1' b2'))
<= BLeft +oo%E)%O.
by case: b1' b2' => [[] [[| ?] | ?] | []] [[] [[| ?] | ?] | []]//=;
rewrite bnd_simp ?real_leey ?real_ltry/= ?realz.
case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
- rewrite !(map_itv_bound_comp, map_itv_bound_EFin_le_BLeft)/=.
exact: num_itv_mul_boundl.
- rewrite !(map_itv_bound_comp EFin intr) real_mulry//= => b1x1 _.
case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
by rewrite gtr0_sg ?mul1e ?bnd_simp.
rewrite -x10 sgr0 mul0e/= map_itv_bound_EFin_le_BLeft.
suff -> : b1 = BLeft 0%Z by case: b2 {b20}.
apply/le_anti; rewrite b10 andbT.
move: b1x1; rewrite map_itv_bound_EFin_le_BLeft.
by rewrite -x10 -(mulr0z 1) num_itv_bound_le_BLeft.
- rewrite !(map_itv_bound_comp EFin intr) real_mulyr//= => _ b2x2.
case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
by rewrite gtr0_sg ?mul1e ?bnd_simp.
rewrite -x20 sgr0 mul0e/= map_itv_bound_EFin_le_BLeft.
suff -> : b2 = BLeft 0%Z by case: b1 {b10} => [[] [] []|].
apply/le_anti; rewrite b20 andbT.
move: b2x2; rewrite map_itv_bound_EFin_le_BLeft.
by rewrite -x20 -(mulr0z 1) num_itv_bound_le_BLeft.
- by rewrite mulyy/= 3!map_itv_bound_comp.
Qed.
have x10 : 0 <= x1.
by case: x1 b1x1 (le_trans (eqbRL (le_ext_num_itv_bound _ _) b10) b1x1).
have x20 : 0 <= x2.
by case: x2 b2x2 (le_trans (eqbRL (le_ext_num_itv_bound _ _) b20) b2x2).
have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have ley b1' b2' :
(map_itv_bound EFin (num_itv_bound R (mul_boundl b1' b2'))
<= BLeft +oo%E)%O.
by case: b1' b2' => [[] [[| ?] | ?] | []] [[] [[| ?] | ?] | []]//=;
rewrite bnd_simp ?real_leey ?real_ltry/= ?realz.
case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
- rewrite !(map_itv_bound_comp, map_itv_bound_EFin_le_BLeft)/=.
exact: num_itv_mul_boundl.
- rewrite !(map_itv_bound_comp EFin intr) real_mulry//= => b1x1 _.
case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
by rewrite gtr0_sg ?mul1e ?bnd_simp.
rewrite -x10 sgr0 mul0e/= map_itv_bound_EFin_le_BLeft.
suff -> : b1 = BLeft 0%Z by case: b2 {b20}.
apply/le_anti; rewrite b10 andbT.
move: b1x1; rewrite map_itv_bound_EFin_le_BLeft.
by rewrite -x10 -(mulr0z 1) num_itv_bound_le_BLeft.
- rewrite !(map_itv_bound_comp EFin intr) real_mulyr//= => _ b2x2.
case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
by rewrite gtr0_sg ?mul1e ?bnd_simp.
rewrite -x20 sgr0 mul0e/= map_itv_bound_EFin_le_BLeft.
suff -> : b2 = BLeft 0%Z by case: b1 {b10} => [[] [] []|].
apply/le_anti; rewrite b20 andbT.
move: b2x2; rewrite map_itv_bound_EFin_le_BLeft.
by rewrite -x20 -(mulr0z 1) num_itv_bound_le_BLeft.
- by rewrite mulyy/= 3!map_itv_bound_comp.
Qed.
Lemma ext_num_itv_mul_boundr_pos b1 b2 (x1 x2 : \bar R) :
(0 <= x1 -> 0 <= x2 ->
BRight x1 <= ext_num_itv_bound b1 ->
BRight x2 <= ext_num_itv_bound b2 ->
BRight (x1 * x2) <= ext_num_itv_bound (mul_boundr b1 b2))%O.
Proof.
move=> x10 x20 b1x1 b2x2.
have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
- rewrite !(map_itv_bound_comp, BRight_le_map_itv_bound_EFin)/=.
exact: num_itv_mul_boundr.
- rewrite real_mulry// => b1x1 b2x2.
have -> : b2 = +oo%O by case: b2 b2x2 => -[].
rewrite mul_boundrC/= map_itv_bound_comp.
case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
+ rewrite gtr0_sg ?mul1e ?bnd_simp//.
suff: (BRight 0%Z < b1)%O by case: b1 b1x1 => [[] [] [] |].
move: b1x1; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
case: b1 => [[] b1 |//]; rewrite !bnd_simp -(@ltr0z R).
* exact/le_lt_trans/ltW.
* exact/lt_le_trans.
+ rewrite -x10 sgr0 mul0e/= BRight_le_map_itv_bound_EFin.
suff: (BRight 0%Z <= b1)%O by case: b1 b1x1 => [[] [] [] |].
move: b1x1; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
by rewrite -x10 -(@mulr0z R 1) BRight_le_num_itv_bound.
- rewrite real_mulyr// => b1x1 b2x2.
have -> : b1 = +oo%O by case: b1 b1x1 => -[].
rewrite /= map_itv_bound_comp.
case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
+ rewrite gtr0_sg ?mul1e ?bnd_simp//.
suff: (BRight 0%Z < b2)%O by case: b2 b2x2 => [[] [] [] |].
move: b2x2; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
case: b2 => [[] b2 |//]; rewrite !bnd_simp -(@ltr0z R).
* exact/le_lt_trans/ltW.
* exact/lt_le_trans.
+ rewrite -x20 sgr0 mul0e/= BRight_le_map_itv_bound_EFin.
suff: (BRight 0%Z <= b2)%O by case: b2 b2x2 => [[] [] [] |].
move: b2x2; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
by rewrite -x20 -(@mulr0z R 1) BRight_le_num_itv_bound.
- rewrite mulyy/= => b1x1 b2x2.
have -> : b1 = +oo%O by case: b1 b1x1 => -[].
by have -> : b2 = +oo%O by case: b2 b2x2 => -[].
Qed.
have x1r : (0 >=< x1)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
have x2r : (0 >=< x2)%O by rewrite real_fine; exact/ger0_real/fine_ge0.
case: x1 x2 x10 x20 x1r x2r b1x1 b2x2 => [x1||] [x2||] //= x10 x20 x1r x2r.
- rewrite !(map_itv_bound_comp, BRight_le_map_itv_bound_EFin)/=.
exact: num_itv_mul_boundr.
- rewrite real_mulry// => b1x1 b2x2.
have -> : b2 = +oo%O by case: b2 b2x2 => -[].
rewrite mul_boundrC/= map_itv_bound_comp.
case: (comparable_ltgtP x1r) x10 => [x10 |//| [x10]] _.
+ rewrite gtr0_sg ?mul1e ?bnd_simp//.
suff: (BRight 0%Z < b1)%O by case: b1 b1x1 => [[] [] [] |].
move: b1x1; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
case: b1 => [[] b1 |//]; rewrite !bnd_simp -(@ltr0z R).
* exact/le_lt_trans/ltW.
* exact/lt_le_trans.
+ rewrite -x10 sgr0 mul0e/= BRight_le_map_itv_bound_EFin.
suff: (BRight 0%Z <= b1)%O by case: b1 b1x1 => [[] [] [] |].
move: b1x1; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
by rewrite -x10 -(@mulr0z R 1) BRight_le_num_itv_bound.
- rewrite real_mulyr// => b1x1 b2x2.
have -> : b1 = +oo%O by case: b1 b1x1 => -[].
rewrite /= map_itv_bound_comp.
case: (comparable_ltgtP x2r) x20 => [x20 |//| [x20]] _.
+ rewrite gtr0_sg ?mul1e ?bnd_simp//.
suff: (BRight 0%Z < b2)%O by case: b2 b2x2 => [[] [] [] |].
move: b2x2; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
case: b2 => [[] b2 |//]; rewrite !bnd_simp -(@ltr0z R).
* exact/le_lt_trans/ltW.
* exact/lt_le_trans.
+ rewrite -x20 sgr0 mul0e/= BRight_le_map_itv_bound_EFin.
suff: (BRight 0%Z <= b2)%O by case: b2 b2x2 => [[] [] [] |].
move: b2x2; rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
by rewrite -x20 -(@mulr0z R 1) BRight_le_num_itv_bound.
- rewrite mulyy/= => b1x1 b2x2.
have -> : b1 = +oo%O by case: b1 b1x1 => -[].
by have -> : b2 = +oo%O by case: b2 b2x2 => -[].
Qed.
Lemma ext_num_itv_mul_boundr b1 b2 (x1 x2 : \bar R) :
(0 <= x1 -> (0 >=< x2)%O -> BRight 0%Z <= b2 ->
BRight x1 <= ext_num_itv_bound b1 ->
BRight x2 <= ext_num_itv_bound b2 ->
BRight (x1 * x2) <= ext_num_itv_bound (mul_boundr b1 b2))%O.
Proof.
move=> x1ge0 x2r b2ge0 lex1b1 lex2b2.
have /orP[x2ge0 | x2le0] : (0 <= x2) || (x2 <= 0).
- by case: x2 x2r {lex2b2} => [x2 /=|_|_]; rewrite ?lee_fin ?le0y ?leNy0.
- exact: ext_num_itv_mul_boundr_pos.
have : (BRight (x1 * x2) <= BRight 0%R)%O.
by have:= mule_ge0_le0 x1ge0 x2le0; case: mule.
move/le_trans; apply.
rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin/=.
rewrite -(@mulr0z R 1) BRight_le_num_itv_bound.
apply: mul_boundr_gt0 => //.
move: x1 x1ge0 lex1b1 => [x1||//]/= x1ge0; last by case: b1 => -[].
rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
rewrite -(@BRight_le_num_itv_bound R)/=.
by apply: le_trans; rewrite bnd_simp -lee_fin.
Qed.
have /orP[x2ge0 | x2le0] : (0 <= x2) || (x2 <= 0).
- by case: x2 x2r {lex2b2} => [x2 /=|_|_]; rewrite ?lee_fin ?le0y ?leNy0.
- exact: ext_num_itv_mul_boundr_pos.
have : (BRight (x1 * x2) <= BRight 0%R)%O.
by have:= mule_ge0_le0 x1ge0 x2le0; case: mule.
move/le_trans; apply.
rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin/=.
rewrite -(@mulr0z R 1) BRight_le_num_itv_bound.
apply: mul_boundr_gt0 => //.
move: x1 x1ge0 lex1b1 => [x1||//]/= x1ge0; last by case: b1 => -[].
rewrite map_itv_bound_comp BRight_le_map_itv_bound_EFin.
rewrite -(@BRight_le_num_itv_bound R)/=.
by apply: le_trans; rewrite bnd_simp -lee_fin.
Qed.
Lemma comparable_ext_num_itv_bound (x y : itv_bound int) :
(ext_num_itv_bound x >=< ext_num_itv_bound y)%O.
Proof.
apply/orP; rewrite !(map_itv_bound_comp EFin intr)/= !le_map_itv_bound_EFin.
exact/orP/comparable_num_itv_bound.
Qed.
exact/orP/comparable_num_itv_bound.
Qed.
Lemma ext_num_itv_bound_min (x y : itv_bound int) :
ext_num_itv_bound (Order.min x y)
= Order.min (ext_num_itv_bound x) (ext_num_itv_bound y).
Proof.
have [lexy | ltyx] := leP x y; [by rewrite !minEle le_ext_num_itv_bound lexy|].
rewrite minElt -if_neg -comparable_leNgt ?le_ext_num_itv_bound ?ltW//.
exact: comparable_ext_num_itv_bound.
Qed.
rewrite minElt -if_neg -comparable_leNgt ?le_ext_num_itv_bound ?ltW//.
exact: comparable_ext_num_itv_bound.
Qed.
Lemma ext_num_itv_bound_max (x y : itv_bound int) :
ext_num_itv_bound (Order.max x y)
= Order.max (ext_num_itv_bound x) (ext_num_itv_bound y).
Proof.
have [lexy | ltyx] := leP x y; [by rewrite !maxEle le_ext_num_itv_bound lexy|].
rewrite maxElt -if_neg -comparable_leNgt ?le_ext_num_itv_bound ?ltW//.
exact: comparable_ext_num_itv_bound.
Qed.
rewrite maxElt -if_neg -comparable_leNgt ?le_ext_num_itv_bound ?ltW//.
exact: comparable_ext_num_itv_bound.
Qed.
Lemma ext_num_spec_mul xi yi (x : ext_num_def xi) (y : ext_num_def yi)
(r := Itv.real2 mul xi yi) :
ext_num_spec r (x%:inum * y%:inum : \bar R).
Proof.
rewrite {}/r; case: xi yi x y => [//| [xl xu]] [//| [yl yu]].
case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]].
rewrite -/(sign (Interval xl xu)) -/(sign (Interval yl yu)).
have ns000 : ext_num_sem `[0%Z, 0%Z] (0 : \bar R).
by apply/and3P; rewrite ?comparablexx.
have xyr : (0 >=< (x * y)%E)%O by exact: realMe.
case: (ext_signP xlx xxu xr) => xlb xub xs.
- by rewrite xs mul0e; case: (ext_signP yly yyu yr).
- case: (ext_signP yly yyu yr) => ylb yub ys.
+ by rewrite ys mule0.
+ apply/and3P; split=> //=.
* exact: ext_num_itv_mul_boundl.
* exact: ext_num_itv_mul_boundr_pos.
+ apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_muleN//.
* by rewrite oppe_boundl ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
* rewrite oppe_boundr ext_num_itv_mul_boundl ?oppe_boundl//.
by rewrite opp_bound_ge0.
+ apply/and3P; split=> //=.
* rewrite -[x * y]oppeK -real_muleN// oppe_boundl.
rewrite ext_num_itv_mul_boundr -?real_fine ?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
* by rewrite ext_num_itv_mul_boundr// ltW.
- case: (ext_signP yly yyu yr) => ylb yub ys.
+ by rewrite ys mule0.
+ apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_mulNe//.
* by rewrite oppe_boundl ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
* rewrite oppe_boundr ext_num_itv_mul_boundl ?oppe_boundl//.
by rewrite opp_bound_ge0.
+ apply/and3P; split=> //=; rewrite -real_muleNN//.
* by rewrite ext_num_itv_mul_boundl ?opp_bound_ge0 ?oppe_boundl.
* by rewrite ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
+ apply/and3P; split=> //=; rewrite -[x * y]oppeK.
* rewrite -real_mulNe// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
* rewrite oppeK -real_muleNN//.
by rewrite ext_num_itv_mul_boundr ?oppe_boundr
?oppe_ge0 ?oppe_cmp0 ?opp_bound_gt0// ltW.
case: (ext_signP yly yyu yr) => ylb yub ys.
- by rewrite ys mule0.
- apply/and3P; split=> //=; rewrite muleC mul_boundrC.
+ rewrite -[y * x]oppeK -real_muleN// oppe_boundl.
rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
+ by rewrite ext_num_itv_mul_boundr// ltW.
- apply/and3P; split=> //=; rewrite muleC mul_boundrC.
+ rewrite -[y * x]oppeK -real_mulNe// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
+ rewrite -real_muleNN// ext_num_itv_mul_boundr ?oppe_ge0
?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
apply/and3P; rewrite xyr/= ext_num_itv_bound_min ext_num_itv_bound_max.
rewrite (comparable_ge_min _ (comparable_ext_num_itv_bound _ _)).
rewrite (comparable_le_max _ (comparable_ext_num_itv_bound _ _)).
have [x0 | /ltW x0] : 0 <= x \/ x < 0; [|split=> //..].
case: x xr {xlx xxu xyr xs} => [x||] /= xr.
- by case: (comparable_leP xr) => x0; [left | right].
- by left; rewrite le0y.
- by right; rewrite ltNy0.
- apply/orP; right; rewrite -[x * y]oppeK -real_muleN// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_cmp0 ?oppe_boundr// opp_bound_gt0 ltW.
- by apply/orP; right; rewrite ext_num_itv_mul_boundr// ltW.
- apply/orP; left; rewrite -[x * y]oppeK -real_mulNe// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
- apply/orP; left; rewrite -real_muleNN//.
rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
Qed.
case=> [x /=/and3P[xr /= xlx xxu]] [y /=/and3P[yr /= yly yyu]].
rewrite -/(sign (Interval xl xu)) -/(sign (Interval yl yu)).
have ns000 : ext_num_sem `[0%Z, 0%Z] (0 : \bar R).
by apply/and3P; rewrite ?comparablexx.
have xyr : (0 >=< (x * y)%E)%O by exact: realMe.
case: (ext_signP xlx xxu xr) => xlb xub xs.
- by rewrite xs mul0e; case: (ext_signP yly yyu yr).
- case: (ext_signP yly yyu yr) => ylb yub ys.
+ by rewrite ys mule0.
+ apply/and3P; split=> //=.
* exact: ext_num_itv_mul_boundl.
* exact: ext_num_itv_mul_boundr_pos.
+ apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_muleN//.
* by rewrite oppe_boundl ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
* rewrite oppe_boundr ext_num_itv_mul_boundl ?oppe_boundl//.
by rewrite opp_bound_ge0.
+ apply/and3P; split=> //=.
* rewrite -[x * y]oppeK -real_muleN// oppe_boundl.
rewrite ext_num_itv_mul_boundr -?real_fine ?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
* by rewrite ext_num_itv_mul_boundr// ltW.
- case: (ext_signP yly yyu yr) => ylb yub ys.
+ by rewrite ys mule0.
+ apply/and3P; split=> //=; rewrite -[x * y]oppeK -real_mulNe//.
* by rewrite oppe_boundl ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
* rewrite oppe_boundr ext_num_itv_mul_boundl ?oppe_boundl//.
by rewrite opp_bound_ge0.
+ apply/and3P; split=> //=; rewrite -real_muleNN//.
* by rewrite ext_num_itv_mul_boundl ?opp_bound_ge0 ?oppe_boundl.
* by rewrite ext_num_itv_mul_boundr_pos ?oppe_ge0 ?oppe_boundr.
+ apply/and3P; split=> //=; rewrite -[x * y]oppeK.
* rewrite -real_mulNe// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
* rewrite oppeK -real_muleNN//.
by rewrite ext_num_itv_mul_boundr ?oppe_boundr
?oppe_ge0 ?oppe_cmp0 ?opp_bound_gt0// ltW.
case: (ext_signP yly yyu yr) => ylb yub ys.
- by rewrite ys mule0.
- apply/and3P; split=> //=; rewrite muleC mul_boundrC.
+ rewrite -[y * x]oppeK -real_muleN// oppe_boundl.
rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
+ by rewrite ext_num_itv_mul_boundr// ltW.
- apply/and3P; split=> //=; rewrite muleC mul_boundrC.
+ rewrite -[y * x]oppeK -real_mulNe// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
+ rewrite -real_muleNN// ext_num_itv_mul_boundr ?oppe_ge0
?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
apply/and3P; rewrite xyr/= ext_num_itv_bound_min ext_num_itv_bound_max.
rewrite (comparable_ge_min _ (comparable_ext_num_itv_bound _ _)).
rewrite (comparable_le_max _ (comparable_ext_num_itv_bound _ _)).
have [x0 | /ltW x0] : 0 <= x \/ x < 0; [|split=> //..].
case: x xr {xlx xxu xyr xs} => [x||] /= xr.
- by case: (comparable_leP xr) => x0; [left | right].
- by left; rewrite le0y.
- by right; rewrite ltNy0.
- apply/orP; right; rewrite -[x * y]oppeK -real_muleN// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_cmp0 ?oppe_boundr// opp_bound_gt0 ltW.
- by apply/orP; right; rewrite ext_num_itv_mul_boundr// ltW.
- apply/orP; left; rewrite -[x * y]oppeK -real_mulNe// oppe_boundl.
by rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_boundr// ltW.
- apply/orP; left; rewrite -real_muleNN//.
rewrite ext_num_itv_mul_boundr ?oppe_ge0 ?oppe_cmp0 ?oppe_boundr//.
by rewrite opp_bound_gt0 ltW.
Qed.
Canonical mule_inum xi yi (x : ext_num_def xi) (y : ext_num_def yi) :=
Itv.mk (ext_num_spec_mul x y).
Definition abse_itv (i : Itv.t) : Itv.t :=
match i with
| Itv.Top => Itv.Real `[0%Z, +oo[
| Itv.Real (Interval l u) =>
match l with
| BRight (Posz _) | BLeft (Posz (S _)) => Itv.Real `]0%Z, +oo[
| _ => Itv.Real `[0%Z, +oo[
end
end.
Arguments abse_itv /.
Lemma ext_num_spec_abse i (x : ext_num_def i) (r := abse_itv i) :
ext_num_spec r (`|x%:inum| : \bar R).
Proof.
have: ext_num_sem `[0%Z, +oo[ `|x%:inum|.
apply/and3P; split; rewrite ?bnd_simp ?abse_ge0//.
by case: x%:inum => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
have: 0 < x%:inum -> ext_num_sem `]0%Z, +oo[ `|x%:inum|.
move=> xgt0; apply/and3P; split; rewrite ?bnd_simp//.
- by case: x%:num => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
- case: x%:inum xgt0 => [x'|//|//]/=.
by rewrite !lte_fin normr_gt0; apply: lt0r_neq0.
rewrite {}/r; case: i x => [//| [[[] [[//| l] | //] | //] u]] [x /=] + + _;
move/and3P => [xr /= /[!bnd_simp]lx _]; apply.
- by apply: lt_le_trans lx; rewrite lte_fin ltr0z.
- by apply: le_lt_trans lx; rewrite lee_fin ler0z.
- by apply: lt_trans lx; rewrite lte_fin ltr0z.
Qed.
apply/and3P; split; rewrite ?bnd_simp ?abse_ge0//.
by case: x%:inum => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
have: 0 < x%:inum -> ext_num_sem `]0%Z, +oo[ `|x%:inum|.
move=> xgt0; apply/and3P; split; rewrite ?bnd_simp//.
- by case: x%:num => [x'||]; rewrite ?cmp0y// le_comparable ?abse_ge0.
- case: x%:inum xgt0 => [x'|//|//]/=.
by rewrite !lte_fin normr_gt0; apply: lt0r_neq0.
rewrite {}/r; case: i x => [//| [[[] [[//| l] | //] | //] u]] [x /=] + + _;
move/and3P => [xr /= /[!bnd_simp]lx _]; apply.
- by apply: lt_le_trans lx; rewrite lte_fin ltr0z.
- by apply: le_lt_trans lx; rewrite lee_fin ler0z.
- by apply: lt_trans lx; rewrite lte_fin ltr0z.
Qed.
Canonical abse_inum i (x : ext_num_def i) := Itv.mk (ext_num_spec_abse x).
Lemma ext_min_itv_boundl_spec x1 x2 b1 b2 :
(ext_num_itv_bound b1 <= BLeft x1)%O ->
(ext_num_itv_bound b2 <= BLeft x2)%O ->
(ext_num_itv_bound (Order.min b1 b2) <= BLeft (Order.min x1 x2))%O.
Proof.
case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- have sb1_le_sb2 := eqbRL (le_ext_num_itv_bound _ _) b1_le_b2.
by rewrite minElt; case: (x1 < x2)%O => [//|_]; apply: le_trans.
- have sb2_le_sb1 := eqbRL (le_ext_num_itv_bound _ _) b2_le_b1.
by rewrite minElt; case: (x1 < x2)%O => [+ _|//]; apply: le_trans.
Qed.
- have sb1_le_sb2 := eqbRL (le_ext_num_itv_bound _ _) b1_le_b2.
by rewrite minElt; case: (x1 < x2)%O => [//|_]; apply: le_trans.
- have sb2_le_sb1 := eqbRL (le_ext_num_itv_bound _ _) b2_le_b1.
by rewrite minElt; case: (x1 < x2)%O => [+ _|//]; apply: le_trans.
Qed.
Lemma ext_min_itv_boundr_spec x1 x2 b1 b2 : (x1 >=< x2)%O ->
(BRight x1 <= ext_num_itv_bound b1)%O ->
(BRight x2 <= ext_num_itv_bound b2)%O ->
(BRight (Order.min x1 x2) <= ext_num_itv_bound (Order.min b1 b2))%O.
Proof.
move=> x1_cmp_x2; case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- have sb1_le_sb2 := eqbRL (le_ext_num_itv_bound _ _) b1_le_b2.
by case: (comparable_leP x1_cmp_x2) => [//| /ltW ? + _]; apply: le_trans.
- have sb2_le_sb1 := eqbRL (le_ext_num_itv_bound _ _) b2_le_b1.
by case: (comparable_leP x1_cmp_x2) => [? _ |//]; apply: le_trans.
Qed.
- have sb1_le_sb2 := eqbRL (le_ext_num_itv_bound _ _) b1_le_b2.
by case: (comparable_leP x1_cmp_x2) => [//| /ltW ? + _]; apply: le_trans.
- have sb2_le_sb1 := eqbRL (le_ext_num_itv_bound _ _) b2_le_b1.
by case: (comparable_leP x1_cmp_x2) => [? _ |//]; apply: le_trans.
Qed.
Lemma ext_num_spec_min (xi yi : Itv.t) (x : ext_num_def xi) (y : ext_num_def yi)
(r := Itv.real2 min xi yi) :
ext_num_spec r (Order.min x%:inum y%:inum : \bar R).
Proof.
apply: Itv.spec_real2 (Itv.P x) (Itv.P y).
case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
apply/and3P; split.
- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
+ by move=> ? ?; apply: comparable_minr.
+ by move=> ? ?; rewrite real_miney.
+ by move=> ? ?; rewrite real_minNye.
- exact: ext_min_itv_boundl_spec.
- by apply: ext_min_itv_boundr_spec => //; apply: ereal_comparable.
Qed.
case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
apply/and3P; split.
- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
+ by move=> ? ?; apply: comparable_minr.
+ by move=> ? ?; rewrite real_miney.
+ by move=> ? ?; rewrite real_minNye.
- exact: ext_min_itv_boundl_spec.
- by apply: ext_min_itv_boundr_spec => //; apply: ereal_comparable.
Qed.
Lemma ext_max_itv_boundl_spec x1 x2 b1 b2 : (x1 >=< x2)%O ->
(ext_num_itv_bound b1 <= BLeft x1)%O ->
(ext_num_itv_bound b2 <= BLeft x2)%O ->
(ext_num_itv_bound (Order.max b1 b2) <= BLeft (Order.max x1 x2))%O.
Proof.
move=> x1_cmp_x2.
case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- case: (comparable_leP x1_cmp_x2) => [//| /ltW ? _ sb2_x2].
exact: le_trans sb2_x2 _.
- case: (comparable_leP x1_cmp_x2) => [? sb1_x1 _ |//].
exact: le_trans sb1_x1 _.
Qed.
case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- case: (comparable_leP x1_cmp_x2) => [//| /ltW ? _ sb2_x2].
exact: le_trans sb2_x2 _.
- case: (comparable_leP x1_cmp_x2) => [? sb1_x1 _ |//].
exact: le_trans sb1_x1 _.
Qed.
Lemma ext_max_itv_boundr_spec x1 x2 b1 b2 :
(BRight x1 <= ext_num_itv_bound b1)%O ->
(BRight x2 <= ext_num_itv_bound b2)%O ->
(BRight (Order.max x1 x2) <= ext_num_itv_bound (Order.max b1 b2))%O.
Proof.
case: (leP b1 b2) => [b1_le_b2 | /ltW b2_le_b1].
- have sb1_le_sb2 := eqbRL (@le_ext_num_itv_bound R _ _) b1_le_b2.
by rewrite maxElt; case: ifP => [//|_ ? _]; apply: le_trans sb1_le_sb2.
- have sb2_le_sb1 := eqbRL (@le_ext_num_itv_bound R _ _) b2_le_b1.
by rewrite maxElt; case: ifP => [_ _ ?|//]; apply: le_trans sb2_le_sb1.
Qed.
- have sb1_le_sb2 := eqbRL (@le_ext_num_itv_bound R _ _) b1_le_b2.
by rewrite maxElt; case: ifP => [//|_ ? _]; apply: le_trans sb1_le_sb2.
- have sb2_le_sb1 := eqbRL (@le_ext_num_itv_bound R _ _) b2_le_b1.
by rewrite maxElt; case: ifP => [_ _ ?|//]; apply: le_trans sb2_le_sb1.
Qed.
Lemma ext_num_spec_max (xi yi : Itv.t) (x : ext_num_def xi) (y : ext_num_def yi)
(r := Itv.real2 max xi yi) :
ext_num_spec r (Order.max x%:inum y%:inum : \bar R).
Proof.
apply: Itv.spec_real2 (Itv.P x) (Itv.P y).
case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
apply/and3P; split.
- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
+ by move=> ? ?; apply: comparable_maxr.
+ by move=> ? ?; rewrite real_maxey.
+ by move=> ? ?; rewrite real_maxNye.
- by apply: ext_max_itv_boundl_spec => //; apply: ereal_comparable.
- exact: ext_max_itv_boundr_spec.
Qed.
case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
apply/and3P; split.
- case: x y xr yr {lxx xux lyy yuy} => [x||] [y||]//=.
+ by move=> ? ?; apply: comparable_maxr.
+ by move=> ? ?; rewrite real_maxey.
+ by move=> ? ?; rewrite real_maxNye.
- by apply: ext_max_itv_boundl_spec => //; apply: ereal_comparable.
- exact: ext_max_itv_boundr_spec.
Qed.
Canonical ext_min_max_typ := MinMaxTyp ext_num_spec_min ext_num_spec_max.
End Itv.
End ItvInstances.
Export (canonicals) ItvInstances.
Section MorphNum.
Context {R : numDomainType} {i : Itv.t}.
Local Notation nR := (Itv.def (@ext_num_sem R) i).
Implicit Types (a : \bar R).
Lemma num_abse_eq0 a : (`|a|%:nng == 0%:E%:nng) = (a == 0).
Proof.
End MorphNum.
Section MorphReal.
Context {R : numDomainType} {xi yi : interval int}.
Implicit Type x : (Itv.def (@ext_num_sem R) (Itv.Real xi)).
Implicit Type y : (Itv.def (@ext_num_sem R) (Itv.Real yi)).
Lemma num_lee_max a x y :
a <= maxe x%:num y%:num = (a <= x%:num) || (a <= y%:num).
Proof.
Lemma num_gee_max a x y :
maxe x%:num y%:num <= a = (x%:num <= a) && (y%:num <= a).
Proof.
Lemma num_lee_min a x y :
a <= mine x%:num y%:num = (a <= x%:num) && (a <= y%:num).
Proof.
Lemma num_gee_min a x y :
mine x%:num y%:num <= a = (x%:num <= a) || (y%:num <= a).
Proof.
Lemma num_lte_max a x y :
a < maxe x%:num y%:num = (a < x%:num) || (a < y%:num).
Proof.
Lemma num_gte_max a x y :
maxe x%:num y%:num < a = (x%:num < a) && (y%:num < a).
Proof.
Lemma num_lte_min a x y :
a < mine x%:num y%:num = (a < x%:num) && (a < y%:num).
Proof.
Lemma num_gte_min a x y :
mine x%:num y%:num < a = (x%:num < a) || (y%:num < a).
Proof.
End MorphReal.
Variant posnume_spec (R : numDomainType) (x : \bar R) :
\bar R -> bool -> bool -> bool -> Type :=
| IsPinftyPosnume :
posnume_spec x +oo false true true
| IsRealPosnume (p : {posnum R}) :
posnume_spec x (p%:num%:E) false true true.
Lemma posnumeP (R : numDomainType) (x : \bar R) : 0 < x ->
posnume_spec x x (x == 0) (0 <= x) (0 < x).
Proof.
Variant nonnege_spec (R : numDomainType) (x : \bar R) :
\bar R -> bool -> Type :=
| IsPinftyNonnege : nonnege_spec x +oo true
| IsRealNonnege (p : {nonneg R}) : nonnege_spec x (p%:num%:E) true.
Lemma nonnegeP (R : numDomainType) (x : \bar R) : 0 <= x ->
nonnege_spec x x (0 <= x).
Proof.
case: x => [x|_|//]; last by rewrite le0y; exact: IsPinftyNonnege.
by rewrite lee_fin => /[dup] x_ge0 ->; exact: IsRealNonnege (NngNum x_ge0).
Qed.
by rewrite lee_fin => /[dup] x_ge0 ->; exact: IsRealNonnege (NngNum x_ge0).
Qed.
Section contract_expand.
Variable R : realFieldType.
Implicit Types (x : \bar R) (r : R).
Local Open Scope ereal_scope.
Definition contract x : R :=
match x with
| r%:E => r / (1 + `|r|) | +oo => 1 | -oo => -1
end.
Lemma contract_lt1 r : (`|contract r%:E| < 1)%R.
Proof.
Lemma contract_le1 x : (`|contract x| <= 1)%R.
Proof.
Lemma contract0 : contract 0 = 0%R.
Lemma contractN x : contract (- x) = (- contract x)%R.
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.
Proof.
Lemma expandN r : expand (- r)%R = - expand r.
Proof.
rewrite /expand; case: ifPn => [r1|].
rewrite ifF; [by rewrite ifT // -lerNr|apply/negbTE].
by rewrite -ltNge -(opprK r) -ltrNl (lt_le_trans _ r1) // -subr_gt0 opprK.
rewrite -ltNge => r1; case: ifPn; rewrite lerNl opprK; [by move=> ->|].
by rewrite -ltNge leNgt => ->; rewrite leNgt -ltrNl r1 /= mulNr normrN.
Qed.
rewrite ifF; [by rewrite ifT // -lerNr|apply/negbTE].
by rewrite -ltNge -(opprK r) -ltrNl (lt_le_trans _ r1) // -subr_gt0 opprK.
rewrite -ltNge => r1; case: ifPn; rewrite lerNl opprK; [by move=> ->|].
by rewrite -ltNge leNgt => ->; rewrite leNgt -ltrNl r1 /= mulNr normrN.
Qed.
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}.
Proof.
move=> r; rewrite inE le_eqVlt => /orP[|r1].
rewrite eqr_norml => /andP[/orP[]/eqP->{r}] _;
by [rewrite expand1|rewrite expandN1].
rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : (r1) => -> -> /=.
have r_pneq0 : (1 + r / (1 - r) != 0)%R.
rewrite -[X in (X + _)%R](@divrr _ (1 - r)%R) -?mulrDl; last first.
by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt_eqF // ltr_normlW.
have r_nneq0 : (1 - r / (1 + r) != 0)%R.
rewrite -[X in (X + _)%R](@divrr _ (1 + r)%R) -?mulrBl; last first.
by rewrite unitfE addrC addr_eq0 gt_eqF // ltrNnormlW.
rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym gt_eqF //.
exact: ltrNnormlW.
wlog : r r1 r_pneq0 r_nneq0 / (0 <= r)%R => wlog_r0.
have [r0|r0] := lerP 0 r; first by rewrite wlog_r0.
move: (wlog_r0 (- r)%R).
rewrite !(normrN, opprK, mulNr) oppr_ge0 => /(_ r1 r_nneq0 r_pneq0 (ltW r0)).
by move/eqP; rewrite eqr_opp => /eqP.
rewrite /contract !ger0_norm //; last first.
by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW r1)) // ler_norm.
apply: (@mulIr _ (1 + r / (1 - r))%R); first by rewrite unitfE.
rewrite -(mulrA (r / _)) mulVr ?unitfE // mulr1.
rewrite -[X in (X + _ / _)%R](@divrr _ (1 - r)%R) -?mulrDl ?subrK ?div1r //.
by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
Qed.
rewrite eqr_norml => /andP[/orP[]/eqP->{r}] _;
by [rewrite expand1|rewrite expandN1].
rewrite /expand 2!leNgt ltrNl; case/ltr_normlP : (r1) => -> -> /=.
have r_pneq0 : (1 + r / (1 - r) != 0)%R.
rewrite -[X in (X + _)%R](@divrr _ (1 - r)%R) -?mulrDl; last first.
by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
by rewrite subrK mulf_neq0 // invr_eq0 subr_eq0 eq_sym lt_eqF // ltr_normlW.
have r_nneq0 : (1 - r / (1 + r) != 0)%R.
rewrite -[X in (X + _)%R](@divrr _ (1 + r)%R) -?mulrBl; last first.
by rewrite unitfE addrC addr_eq0 gt_eqF // ltrNnormlW.
rewrite addrK mulf_neq0 // invr_eq0 addr_eq0 -eqr_oppLR eq_sym gt_eqF //.
exact: ltrNnormlW.
wlog : r r1 r_pneq0 r_nneq0 / (0 <= r)%R => wlog_r0.
have [r0|r0] := lerP 0 r; first by rewrite wlog_r0.
move: (wlog_r0 (- r)%R).
rewrite !(normrN, opprK, mulNr) oppr_ge0 => /(_ r1 r_nneq0 r_pneq0 (ltW r0)).
by move/eqP; rewrite eqr_opp => /eqP.
rewrite /contract !ger0_norm //; last first.
by rewrite divr_ge0 // subr_ge0 (le_trans _ (ltW r1)) // ler_norm.
apply: (@mulIr _ (1 + r / (1 - r))%R); first by rewrite unitfE.
rewrite -(mulrA (r / _)) mulVr ?unitfE // mulr1.
rewrite -[X in (X + _ / _)%R](@divrr _ (1 - r)%R) -?mulrDl ?subrK ?div1r //.
by rewrite unitfE subr_eq0 eq_sym lt_eqF // ltr_normlW.
Qed.
Lemma le_contract : {mono contract : x y / (x <= y)%O}.
Proof.
apply: le_mono; move=> -[r0 | | ] [r1 | _ | _] //=.
- rewrite lte_fin => r0r1; rewrite ltr_pdivrMr ?ltr_wpDr//.
rewrite mulrAC ltr_pdivlMr ?ltr_wpDr// 2?mulrDr 2?mulr1.
have [r10|?] := ler0P r1; last first.
rewrite ltr_leD // mulrC; have [r00|//] := ler0P r0.
by rewrite (@le_trans _ _ 0%R) // ?pmulr_rle0// mulr_ge0// ?oppr_ge0// ltW.
have [?|r00] := ler0P r0; first by rewrite ltr_leD // 2!mulrN mulrC.
by move: (le_lt_trans r10 (lt_trans r00 r0r1)); rewrite ltxx.
- by rewrite ltr_pdivrMr ?ltr_wpDr// mul1r ltr_pwDl // ler_norm.
- rewrite ltr_pdivlMr ?mulN1r ?ltr_wpDr// => _.
by rewrite ltrNl ltr_pwDl // ler_normr lexx orbT.
Qed.
- rewrite lte_fin => r0r1; rewrite ltr_pdivrMr ?ltr_wpDr//.
rewrite mulrAC ltr_pdivlMr ?ltr_wpDr// 2?mulrDr 2?mulr1.
have [r10|?] := ler0P r1; last first.
rewrite ltr_leD // mulrC; have [r00|//] := ler0P r0.
by rewrite (@le_trans _ _ 0%R) // ?pmulr_rle0// mulr_ge0// ?oppr_ge0// ltW.
have [?|r00] := ler0P r0; first by rewrite ltr_leD // 2!mulrN mulrC.
by move: (le_lt_trans r10 (lt_trans r00 r0r1)); rewrite ltxx.
- by rewrite ltr_pdivrMr ?ltr_wpDr// mul1r ltr_pwDl // ler_norm.
- rewrite ltr_pdivlMr ?mulN1r ?ltr_wpDr// => _.
by rewrite ltrNl ltr_pwDl // ler_normr lexx orbT.
Qed.
Definition lt_contract := leW_mono le_contract.
Definition contract_inj := mono_inj lexx le_anti le_contract.
Lemma le_expand_in : {in [pred r | `|r| <= 1]%R &,
{mono expand : x y / (x <= y)%O}}.
Proof.
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.
Proof.
Lemma le_expand : {homo expand : x y / (x <= y)%O}.
Proof.
move=> x y xy; have [x1|] := lerP `|x| 1.
have [y_le1|/ltW /expand1->] := leP y 1%R; last by rewrite leey.
rewrite le_expand_in ?inE// ler_norml y_le1 (le_trans _ xy)//.
by rewrite lerNl (ler_normlP _ _ _).
rewrite ltr_normr => /orP[|] x1; last first.
by rewrite expandN1 // ?leNye // lerNr ltW.
by rewrite expand1; [rewrite expand1 // (le_trans _ xy) // ltW | exact: ltW].
Qed.
have [y_le1|/ltW /expand1->] := leP y 1%R; last by rewrite leey.
rewrite le_expand_in ?inE// ler_norml y_le1 (le_trans _ xy)//.
by rewrite lerNl (ler_normlP _ _ _).
rewrite ltr_normr => /orP[|] x1; last first.
by rewrite expandN1 // ?leNye // lerNr ltW.
by rewrite expand1; [rewrite expand1 // (le_trans _ xy) // ltW | exact: ltW].
Qed.
Lemma expand_eqoo r : (expand r == +oo) = (1 <= r)%R.
Lemma expand_eqNoo r : (expand r == -oo) = (r <= -1)%R.
Proof.
End contract_expand.
Section ereal_PseudoMetric.
Context {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.
Proof.
Lemma ereal_ball_sym x y r : ereal_ball x r y -> ereal_ball y r x.
Proof.
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.
Proof.
rewrite /ereal_ball => h1 h2; rewrite -[X in (X - _)%R](subrK (contract y)).
by rewrite -addrA (le_lt_trans (ler_normD _ _)) // ltrD.
Qed.
by rewrite -addrA (le_lt_trans (ler_normD _ _)) // ltrD.
Qed.
Lemma ereal_ballN x y (e : {posnum R}) :
ereal_ball (- x) e%:num (- y) -> ereal_ball x e%:num y.
Lemma ereal_ball_ninfty_oversize (e : {posnum R}) x :
(2 < e%:num)%R -> ereal_ball -oo e%:num x.
Proof.
move=> e2; rewrite /ereal_ball /= (le_lt_trans _ e2) // -opprB normrN opprK.
rewrite (le_trans (ler_normD _ _)) // normr1 -lerBrDr.
by rewrite (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1)%R // addrK.
Qed.
rewrite (le_trans (ler_normD _ _)) // normr1 -lerBrDr.
by rewrite (le_trans (contract_le1 _)) // (_ : 2 = 1 + 1)%R // addrK.
Qed.
Lemma contract_ereal_ball_pinfty r (e : {posnum R}) :
(1 < contract r%:E + e%:num)%R -> ereal_ball r%:E e%:num +oo.
Proof.
move=> re1; rewrite /ereal_ball; rewrite [contract +oo]/= ler0_norm; last first.
by rewrite subr_le0; case/ler_normlP: (contract_le1 r%:E).
by rewrite opprB ltrBlDl.
Qed.
by rewrite subr_le0; case/ler_normlP: (contract_le1 r%:E).
by rewrite opprB ltrBlDl.
Qed.
End ereal_PseudoMetric.
Lemma lt_ereal_nbhs (R : realFieldType) (a b : \bar R) (r : R) :
a < r%:E -> r%:E < b ->
exists delta : {posnum R},
forall y, (`|y - r| < delta%:num)%R -> (a < y%:E) && (y%:E < b).
Proof.
move=> [:wlog]; case: a b => [a||] [b||] //= ltax ltxb.
- move: a b ltax ltxb; abstract: wlog. (*BUG*)
move=> {}a {}b ltxa ltxb.
have m_gt0 : (Num.min ((r - a) / 2) ((b - r) / 2) > 0)%R.
by rewrite lt_min !divr_gt0 // ?subr_gt0.
exists (PosNum m_gt0) => y //=; rewrite lt_min !ltr_distl.
move=> /andP[/andP[ay _] /andP[_ yb]].
rewrite 2!lte_fin (lt_trans _ ay) ?(lt_trans yb) //=.
rewrite -subr_gt0 opprD addrA {1}[(b - r)%R]splitr addrK.
by rewrite divr_gt0 ?subr_gt0.
by rewrite -subr_gt0 addrAC {1}[(r - a)%R]splitr addrK divr_gt0 ?subr_gt0.
- have [//||d dP] := wlog a (r + 1)%R; rewrite ?lte_fin ?ltrDl //.
by exists d => y /dP /andP[->] /= /lt_le_trans; apply; rewrite leey.
- have [//||d dP] := wlog (r - 1)%R b; rewrite ?lte_fin ?gtrDl ?ltrN10 //.
by exists d => y /dP /andP[_ ->] /=; rewrite ltNyr.
- by exists 1%:pos%R => ? ?; rewrite ltNyr ltry.
Qed.
- move: a b ltax ltxb; abstract: wlog. (*BUG*)
move=> {}a {}b ltxa ltxb.
have m_gt0 : (Num.min ((r - a) / 2) ((b - r) / 2) > 0)%R.
by rewrite lt_min !divr_gt0 // ?subr_gt0.
exists (PosNum m_gt0) => y //=; rewrite lt_min !ltr_distl.
move=> /andP[/andP[ay _] /andP[_ yb]].
rewrite 2!lte_fin (lt_trans _ ay) ?(lt_trans yb) //=.
rewrite -subr_gt0 opprD addrA {1}[(b - r)%R]splitr addrK.
by rewrite divr_gt0 ?subr_gt0.
by rewrite -subr_gt0 addrAC {1}[(r - a)%R]splitr addrK divr_gt0 ?subr_gt0.
- have [//||d dP] := wlog a (r + 1)%R; rewrite ?lte_fin ?ltrDl //.
by exists d => y /dP /andP[->] /= /lt_le_trans; apply; rewrite leey.
- have [//||d dP] := wlog (r - 1)%R b; rewrite ?lte_fin ?gtrDl ?ltrN10 //.
by exists d => y /dP /andP[_ ->] /=; rewrite ltNyr.
- by exists 1%:pos%R => ? ?; rewrite ltNyr ltry.
Qed.