Merge pull request #360 from proux01/a-few-lemmas

A few lemmas

CHANGELOG_UNRELEASED.md

@@ -30,11 +30,15 @@
   + lemmas `ereal_ballN`, `le_ereal_ball`, `ereal_ball_ninfty_oversize`,
     `contract_ereal_ball_pinfty`, `expand_ereal_ball_pinfty`,
     `contract_ereal_ball_fin_le`, `contract_ereal_ball_fin_lt`,
-    `expand_ereal_ball_fin_lt`, `ball_ereal_ball_fin_lt`, `ball_ereal_ball_fin_le`
+    `expand_ereal_ball_fin_lt`, `ball_ereal_ball_fin_lt`, `ball_ereal_ball_fin_le`,
+    `sumERFin`, `ereal_inf1`, `eqe_oppP`, `eqe_oppLRP`, `oppe_subset`,
+    `ereal_inf_pinfty`
+  + definition `er_map`
+  + definition `er_map`
 - in `classical_sets.v`:
   + notation `[disjoint ... & ..]`
   + lemmas `mkset_nil`, `bigcup_mkset`, `bigcup_nonempty`, `bigcup0`, `bigcup0P`,
-    `subset_bigcup_r`, `eqbigcup_r`
+    `subset_bigcup_r`, `eqbigcup_r`, `eq_set_inl`, `set_in_in`
 - in `ereal.v`:
   + lemmas `adde_undefC`, `real_of_erD`, `fin_num_add_undef`, `addeK`,
     `subeK`, `subee`, `sube_le0`, `lee_sub`
@@ -44,6 +48,10 @@
   + definition `dense` and lemma `denseNE`
 - in `reals.v`:
   + lemmas `has_sup1`, `has_inf1`
+- in `nngnum.v`:
+  + instance `invr_nngnum`
+- in `posnum.v`:
+  + instance `posnum_nngnum`
 
 ### Changed
 

theories/classical_sets.v

@@ -288,6 +288,12 @@ Lemma eq_set T (P Q : T -> Prop) : (forall x : T, P x = Q x) ->
   [set x | P x] = [set x | Q x].
 Proof. by move=> /funext->. Qed.
 
+Lemma eq_set_inl T1 T2 (A : set T1) (f f' : T1 -> T2) :
+  (forall x, A x -> f x = f' x) -> [set f x | x in A] = [set f' x | x in A].
+Proof.
+by move=> h; rewrite predeqE=> y; split=> [][x ? <-]; exists x=> //; rewrite h.
+Qed.
+
 Section basic_lemmas.
 Context {T : Type}.
 Implicit Types A B C D : set T.
@@ -695,6 +701,10 @@ by rewrite eqEsubset; split => [x [b [a Aa] <- <-]|x [a Aa] <-];
   [apply/imageP |apply/imageP/imageP].
 Qed.
 
+Lemma set_in_in T1 T2 T3 A (f : T1 -> T2) (f' : T2 -> T3) :
+  [set f' x | x in [set f y | y in A]] = [set f' (f y) | y in A].
+Proof. exact: image_comp. Qed.
+
 Section bigop_lemmas.
 Context {T I : Type}.
 Implicit Types (A : set T) (i : I) (P : set I) (F G : I -> set T).

theories/ereal.v

@@ -64,6 +64,13 @@ Local Open Scope ring_scope.
 
 Inductive er (R : Type) := ERFin of R | ERPInf | ERNInf.
 
+Definition er_map T T' (f : T -> T') (x : er T) : er T' :=
+  match x with
+  | ERFin x => ERFin (f x)
+  | ERPInf => ERPInf _
+  | ERNInf => ERNInf _
+  end.
+
 Section ExtendedReals.
 Variable (R : numDomainType).
 
@@ -388,6 +395,10 @@ Proof. by case: x => //=; rewrite oppr0. Qed.
 Lemma addERFin (r r' : R) : (r + r')%R%:E = r%:E + r'%:E.
 Proof. by []. Qed.
 
+Lemma sumERFin I r P (F : I -> R) :
+  \sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%R%:E.
+Proof. by rewrite (big_morph _ addERFin erefl). Qed.
+
 Lemma subERFin (r r' : R) : (r - r')%R%:E = r%:E - r'%:E.
 Proof. by []. Qed.
 
@@ -448,9 +459,26 @@ move: x y => [r| |] [r'| |] //=; apply/idP/idP => [|/eqP[->]//].
 by move/eqP => -[] /eqP; rewrite eqr_opp => /eqP ->.
 Qed.
 
+Lemma eqe_oppP x y : (- x = - y) <-> (x = y).
+Proof. by split=> [/eqP | -> //]; rewrite eqe_opp => /eqP. Qed.
+
 Lemma eqe_oppLR x y : (- x == y) = (x == - y).
 Proof. by move: x y => [r0| |] [r1| |] //=; rewrite !eqe eqr_oppLR. Qed.
 
+Lemma eqe_oppLRP x y : (- x = y) <-> (x = - y).
+Proof.
+split=> /eqP; first by rewrite eqe_oppLR => /eqP.
+by rewrite -eqe_oppLR => /eqP.
+Qed.
+
+Lemma oppe_subset (A B : set {ereal R}) :
+  ((A `<=` B) <-> (-%E @` A `<=` -%E @` B))%classic.
+Proof.
+split=> [AB _ [] x ? <-|AB x Ax]; first by exists x => //; exact: AB.
+have /AB[y By] : ((-%E @` A) (- x)%E)%classic by exists x.
+by rewrite eqe_oppP => <-.
+Qed.
+
 Lemma fin_numN x : (- x \is a fin_num) = (x \is a fin_num).
 Proof. by rewrite !fin_numE 2!eqe_oppLR andbC. Qed.
 
@@ -816,6 +844,9 @@ Qed.
 Lemma ereal_inf0 : ereal_inf set0 = +oo.
 Proof. by rewrite /ereal_inf image_set0 ereal_sup0. Qed.
 
+Lemma ereal_inf1 x : ereal_inf [set x] = x.
+Proof. by rewrite /ereal_inf image_set1 ereal_sup1 oppeK. Qed.
+
 Lemma ub_ereal_sup S M : ubound S M -> ereal_sup S <= M.
 Proof.
 rewrite /ereal_sup /supremum; case: ifPn => [/eqP ->|].
@@ -912,6 +943,9 @@ Proof.
 by move=> x Sx; rewrite /ereal_inf lee_oppl; apply ereal_sup_ub; exists x.
 Qed.
 
+Lemma ereal_inf_pinfty S : ereal_inf S = +oo -> S `<=` [set +oo].
+Proof. rewrite eqe_oppLRP oppe_subset image_set1; exact: ereal_sup_ninfty. Qed.
+
 Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A <= B}.
 Proof. by move=> A B AB; apply ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
 

theories/nngnum.v

@@ -108,6 +108,10 @@ Canonical mulrn_nngnum x n := NngNum (x%:nngnum *+ n) (mulrn_wge0 n x).
 Canonical zeror_nngnum := @NngNum R 0 (lexx 0).
 Canonical oner_nngnum := @NngNum R 1 ler01.
 
+Lemma inv_nng_ge0 (x : R) : 0 <= x -> 0 <= x^-1.
+Proof. by rewrite invr_ge0. Qed.
+Canonical invr_nngnum x := NngNum (x%:nngnum^-1) (inv_nng_ge0 x).
+
 Lemma nngnum_lt0 x : (x%:nngnum < 0 :> R) = false.
 Proof. by rewrite le_gtF. Qed.
 

theories/posnum.v

@@ -1,7 +1,7 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From Coq Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum.
-Require Import boolp.
+Require Import boolp nngnum.
 
 (******************************************************************************)
 (* This file develops tools to make the manipulation of positive numbers      *)
@@ -100,6 +100,8 @@ Lemma posnum_ge0 x : x%:num >= 0 :> R. Proof. by apply: ltW. Qed.
 Lemma posnum_eq0 x : (x%:num == 0 :> R) = false. Proof. by rewrite gt_eqF. Qed.
 Lemma posnum_neq0 x : (x%:num != 0 :> R). Proof. by rewrite gt_eqF. Qed.
 
+Canonical posnum_nngnum x := Nonneg.NngNum x%:num (posnum_ge0 x).
+
 Lemma posnum_eq : {mono numpos R : x y / x == y}. Proof. by []. Qed.
 Lemma posnum_le : {mono numpos R : x y / x <= y}. Proof. by []. Qed.
 Lemma posnum_lt : {mono numpos R : x y / x < y}. Proof. by []. Qed.