Module mathcomp.analysis.constructive_ereal
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra finmap.
From mathcomp Require Import mathcomp_extra signed.
# 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 ad -oo respectively.
```
\bar R == coproduct of R and {+oo, -oo};
notation for extended (R:Type)
r%:E == injects real numbers into \bar R
+%E, -%E, *%E == addition/opposite/multiplication for extended
reals
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
maxe x y, mine x y == notation for the maximum/minimum of two
extended real numbers
```
## Signed extended real numbers
```
{posnum \bar R} == interface type for elements in \bar R that are
positive, c.f., signed.v, notation in scope %E
{nonneg \bar R} == interface types for elements in \bar R that are
non-negative, c.f. signed.v, notation in scope %E
x%:pos == explicitly casts x to {posnum \bar R}, in scope %E
x%:nng == explicitly casts x to {nonneg \bar R}, in scope %E
```
## Topology of extended real numbers
```
contract == order-preserving bijective function
from extended real numbers to [-1; 1]
expand == function from real numbers to extended
real numbers that cancels contract in
[-1; 1]
```
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Reserved Notation "x %:E" (at level 2, format "x %:E").
Reserved Notation "x %: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 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 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.
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 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.
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 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 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 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 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.
move: x y => [x| |] [y| |] //=; rewrite /mule/=; try by rewrite ltry.
- by rewrite mulrN.
- by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0.
- by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0.
- rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0.
by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0.
- rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0.
by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0.
Qed.
- by rewrite mulrN.
- by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0.
- by rewrite !eqe !lte_fin; case: ltrgtP => //; rewrite oppe0.
- rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0.
by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0.
- rewrite !eqe oppr_eq0 eq_sym; case: ifP; rewrite ?oppe0// => y0.
by rewrite [RHS]fun_if ltNge if_neg EFinN leeNl oppe0 le_eqVlt eqe y0.
Qed.
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 EFin_max : {morph (@EFin R) : r s / Num.max r s >-> maxe r s}.
Proof.
Lemma fine_min :
{in fin_num &, {mono @fine R : x y / mine x y >-> (Num.min x y)%:E}}.
Proof.
Lemma EFin_min : {morph (@EFin R) : r s / Num.min r s >-> mine r s}.
Proof.
Lemma adde_maxl : left_distributive (@GRing.add (\bar R)) maxe.
Proof.
Lemma adde_maxr : right_distributive (@GRing.add (\bar R)) maxe.
Proof.
Lemma maxye : left_zero (+oo : \bar R) maxe.
Lemma maxey : right_zero (+oo : \bar R) maxe.
Lemma maxNye : left_id (-oo : \bar R) maxe.
Lemma maxeNy : right_id (-oo : \bar R) maxe.
HB.instance Definition _ :=
Monoid.isLaw.Build (\bar R) -oo maxe maxA maxNye maxeNy.
Lemma minNye : left_zero (-oo : \bar R) mine.
Lemma mineNy : right_zero (-oo : \bar R) mine.
Lemma minye : left_id (+oo : \bar R) mine.
Lemma miney : right_id (+oo : \bar R) mine.
Lemma oppe_max : {morph -%E : x y / maxe x y >-> mine x y : \bar R}.
Proof.
Lemma oppe_min : {morph -%E : x y / mine x y >-> maxe x y : \bar R}.
Lemma maxeMr z x y : z \is a fin_num -> 0 <= z ->
z * maxe x y = maxe (z * x) (z * y).
Proof.
Lemma maxeMl z x y : z \is a fin_num -> 0 <= z ->
maxe x y * z = maxe (x * z) (y * z).
Lemma mineMr z x y : z \is a fin_num -> 0 <= z ->
z * mine x y = mine (z * x) (z * y).
Lemma mineMl z x y : z \is a fin_num -> 0 <= z ->
mine x y * z = mine (x * z) (y * z).
Lemma 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 0.6.5", note="Use leeN2 instead.")]
Notation lee_opp := leeN2 (only parsing).
#[deprecated(since="mathcomp-analysis 0.6.5", note="Use lteN2 instead.")]
Notation lte_opp := lteN2 (only parsing).
#[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).
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.
Definition posnume (R : numDomainType) of phant R := {> 0 : \bar R}.
Notation "{ 'posnum' '\bar' R }" := (@posnume _ (Phant R)) : type_scope.
Definition nonnege (R : numDomainType) of phant R := {>= 0 : \bar R}.
Notation "{ 'nonneg' '\bar' R }" := (@nonnege _ (Phant R)) : type_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:pos" := (widen_signed x%:sgn : {posnum \bar _}) (only parsing)
: ereal_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
: ereal_dual_scope.
Notation "x %:nng" := (widen_signed x%:sgn : {nonneg \bar _}) (only parsing)
: ereal_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_dual_scope.
Notation "x %:pos" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
!=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_dual_scope.
Notation "x %:nng" := (@widen_signed ereal_display _ _ _ _
(@Signed.from _ _ _ _ _ _ (Phantom _ x))
?=0 (KnownSign.Real (KnownSign.Sign >=0)) _ _)
(only printing) : ereal_scope.
#[global] Hint Extern 0 (is_true (0%E < _)%O) => solve [apply: gt0] : core.
#[global] Hint Extern 0 (is_true (_ < 0%E)%O) => solve [apply: lt0] : core.
#[global] Hint Extern 0 (is_true (0%E <= _)%O) => solve [apply: ge0] : core.
#[global] Hint Extern 0 (is_true (_ <= 0%E)%O) => solve [apply: le0] : core.
#[global] Hint Extern 0 (is_true (0%E >=< _)%O) => solve [apply: cmp0] : core.
#[global] Hint Extern 0 (is_true (_ != 0%E)%O) => solve [apply: neq0] : core.
Section SignedNumDomainStability.
Context {R : numDomainType}.
Lemma pinfty_snum_subproof : Signed.spec 0 !=0 >=0 (+oo : \bar R).
Proof.
Canonical pinfty_snum := Signed.mk (pinfty_snum_subproof).
Lemma ninfty_snum_subproof : Signed.spec 0 !=0 <=0 (-oo : \bar R).
Proof.
Canonical ninfty_snum := Signed.mk (ninfty_snum_subproof).
Lemma EFin_snum_subproof nz cond (x : {num R & nz & cond}) :
Signed.spec 0 nz cond x%:num%:E.
Proof.
Canonical EFin_snum nz cond (x : {num R & nz & cond}) :=
Signed.mk (EFin_snum_subproof x).
Lemma fine_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :
Signed.spec 0%R ?=0 xr (fine x%:num).
Proof.
Canonical fine_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (fine_snum_subproof x).
Lemma oppe_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := opp_reality_subdef xnz xr) :
Signed.spec 0 xnz r (- x%:num).
Proof.
Canonical oppe_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (oppe_snum_subproof x).
Lemma adde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (adde x%:num y%:num).
Proof.
rewrite {}/rnz {}/rrl; apply/andP; split.
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
by rewrite 1?adde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
do ?[by case: (bottom x)|by case: (bottom y)
|by rewrite adde_ge0|by rewrite adde_le0
|exact: realDe|by rewrite 2!eq0 /adde/= addr0].
Qed.
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
by rewrite 1?adde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
do ?[by case: (bottom x)|by case: (bottom y)
|by rewrite adde_ge0|by rewrite adde_le0
|exact: realDe|by rewrite 2!eq0 /adde/= addr0].
Qed.
Canonical adde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (adde_snum_subproof x y).
Import DualAddTheory.
Lemma dEFin_snum_subproof nz cond (x : {num R & nz & cond}) :
Signed.spec 0 nz cond (dEFin x%:num).
Proof.
Canonical dEFin_snum nz cond (x : {num R & nz & cond}) :=
Signed.mk (dEFin_snum_subproof x).
Lemma dadde_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := add_nonzero_subdef xnz ynz xr yr)
(rrl := add_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (dual_adde x%:num y%:num)%dE.
Proof.
rewrite {}/rnz {}/rrl; apply/andP; split.
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
by rewrite 1?dadde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
do ?[by case: (bottom x)|by case: (bottom y)
|by rewrite dadde_ge0|by rewrite dadde_le0
|exact: realDed|by rewrite 2!eq0 /dual_adde/= addr0].
Qed.
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
by rewrite 1?dadde_ss_eq0 ?(eq0F, ge0, le0, andbF, orbT).
move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []//= x y;
do ?[by case: (bottom x)|by case: (bottom y)
|by rewrite dadde_ge0|by rewrite dadde_le0
|exact: realDed|by rewrite 2!eq0 /dual_adde/= addr0].
Qed.
Canonical dadde_snum (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (dadde_snum_subproof x y).
Lemma mule_snum_subproof (xnz ynz : KnownSign.nullity)
(xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr})
(rnz := mul_nonzero_subdef xnz ynz xr yr)
(rrl := mul_reality_subdef xnz ynz xr yr) :
Signed.spec 0 rnz rrl (x%:num * y%:num).
Proof.
rewrite {}/rnz {}/rrl; apply/andP; split.
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y;
rewrite mule_neq0.
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //;
do ?[by case: (bottom x)|by case: (bottom y)
|by rewrite mule_ge0|by rewrite mule_le0_ge0
|by rewrite mule_ge0_le0|by rewrite mule_le0|exact: realMe
|by rewrite eq0 ?mule0// mul0e].
Qed.
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []// x y;
rewrite mule_neq0.
by move: xr yr xnz ynz x y => [[[]|]|] [[[]|]|] [] []/= x y //;
do ?[by case: (bottom x)|by case: (bottom y)
|by rewrite mule_ge0|by rewrite mule_le0_ge0
|by rewrite mule_ge0_le0|by rewrite mule_le0|exact: realMe
|by rewrite eq0 ?mule0// mul0e].
Qed.
Canonical mule_snum (xnz ynz : KnownSign.nullity) (xr yr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr})
(y : {compare (0 : \bar R) & ynz & yr}) :=
Signed.mk (mule_snum_subproof x y).
Definition abse_reality_subdef (xnz : KnownSign.nullity)
(xr : KnownSign.reality) := (if xr is =0 then =0 else >=0)%snum_sign.
Arguments abse_reality_subdef /.
Lemma abse_snum_subproof (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) (r := abse_reality_subdef xnz xr) :
Signed.spec 0 xnz r `|x%:num|.
Proof.
Canonical abse_snum (xnz : KnownSign.nullity) (xr : KnownSign.reality)
(x : {compare (0 : \bar R) & xnz & xr}) :=
Signed.mk (abse_snum_subproof x).
End SignedNumDomainStability.
Section MorphNum.
Context {R : numDomainType} {nz : KnownSign.nullity} {cond : KnownSign.reality}.
Local Notation nR := {compare (0 : \bar R) & nz & cond}.
Implicit Types (a : \bar R).
Lemma num_abse_eq0 a : (`|a|%:nng == 0%:E%:nng) = (a == 0).
Proof.
End MorphNum.
Section MorphReal.
Context {R : numDomainType} {nz : KnownSign.nullity} {r : KnownSign.real}.
Local Notation nR := {compare (0 : \bar R) & nz & r}.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : R) nz r).
Lemma num_lee_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.
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_max`")]
Notation num_lee_maxr := num_lee_max (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_max`")]
Notation num_lee_maxl := num_gee_max (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lee_min`")]
Notation num_lee_minr := num_lee_min (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gee_min`")]
Notation num_lee_minl := num_gee_min (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_max`")]
Notation num_lte_maxr := num_lte_max (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_max`")]
Notation num_lte_maxl := num_gte_max (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_lte_min`")]
Notation num_lte_minr := num_lte_min (only parsing).
#[deprecated(since="mathcomp-analysis 1.2.0", note="renamed `num_gte_min`")]
Notation num_lte_minl := num_gte_min (only parsing).
Section MorphGe0.
Context {R : numDomainType} {nz : KnownSign.nullity}.
Local Notation nR := {compare (0 : \bar R) & ?=0 & >=0}.
Implicit Type x y : nR.
Local Notation num := (@num _ _ (0 : \bar R) ?=0 >=0).
Lemma num_abse_le a x : 0 <= a -> (`|a|%:nng <= x)%O = (a <= x%:num).
Lemma num_abse_lt a x : 0 <= a -> (`|a|%:nng < x)%O = (a < x%:num).
End MorphGe0.
Variant posnume_spec (R : numDomainType) (x : \bar R) :
\bar R -> bool -> bool -> bool -> Type :=
| IsPinftyPosnume :
posnume_spec x +oo false true true
| IsRealPosnume (p : {posnum R}) :
posnume_spec x (p%:num%:E) false true true.
Lemma posnumeP (R : numDomainType) (x : \bar R) : 0 < x ->
posnume_spec x x (x == 0) (0 <= x) (0 < x).
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.
- by rewrite -subr_gt0 opprK.
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.
- by rewrite -subr_gt0 opprK.
Qed.
Definition lt_contract := leW_mono le_contract.
Definition contract_inj := mono_inj lexx le_anti le_contract.
Lemma le_expand_in : {in [pred r | `|r| <= 1]%R &,
{mono expand : x y / (x <= y)%O}}.
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.