Merge pull request #177 from math-comp/mathcomp_master_hausdorff_close

Mathcomp master hausdorff close

theories/altreals/distr.v

@@ -1220,7 +1220,7 @@ set c1 : R := _ / _; set c2 : R := _ / _; have eqc2: c2 = 1 - c1.
 set c := (li + l j); pose z := (c * c1 * f xi + c * c2 * f (x j)).
 apply/(@le_trans _ _ z); last by rewrite /z ![_*(_/_)]mulrC !mulfVK.
 rewrite {}/z -![c * _ * _]mulrA -mulrDr ler_wpmul2l ?addr_ge0 //.
-rewrite eqc2 cvx_f // divr_ge0 ?addr_ge0 //=.
+rewrite eqc2 cvx_f // ?lee_ninfty ?lee_pinfty // divr_ge0 ?addr_ge0 //=.
 by rewrite ler_pdivr_mulr ?mul1r ?ler_addl ?ltr_paddl.
 Qed.
 End Jensen.

theories/altreals/realseq.v

@@ -75,14 +75,14 @@ Qed.
 Lemma nbh_pinfW (P : forall x, nbh x -> Prop) :
   (forall M, P _ (@NPInf R M)) -> forall (v : nbh +oo), P _ v.
 Proof.
-move=> ih ; move: {-2}+oo (erefl (@ERPInf R)).
+move=> ih; move: {-2}+oo%E (erefl (@ERPInf R)).
 by move=> e eE v; case: v eE => // c' e' h [->].
 Qed.
 
 Lemma nbh_ninfW (P : forall x, nbh x -> Prop) :
   (forall M, P _ (@NNInf R M)) -> forall (v : nbh -oo), P _ v.
 Proof.
-move=> ih ; move: {-2}-oo (erefl (@ERNInf R)).
+move=> ih ; move: {-2}-oo%E (erefl (@ERNInf R)).
 by move=> e eE v; case: v eE => // c' e' h [->].
 Qed.
 End NbhElim.
@@ -386,7 +386,8 @@ Lemma ncvg_gt (u : nat -> R) (l1 l2 : {ereal R}) :
     exists K, forall n, (K <= n)%N -> (l1 < (u n)%:E)%E.
 Proof.
 case: l1 l2 => [l1||] [l2||] //=; first last.
-+ by move=> _ _; exists 0%N. + by move=> _ _; exists 0%N.
++ by move=> _ _; exists 0%N => ? ?; exact: lte_ninfty.
++ by move=> _ _; exists 0%N => ? ?; exact: lte_ninfty.
 + by move=> _ /(_ (NPInf l1)) [K cv]; exists K => n /cv.
 move=> lt_12; pose e := l2 - l1 => /(_ (B l2 e)).
 case=> K cv; exists K => n /cv; rewrite !inE eclamp_id ?subr_gt0 //.
@@ -439,7 +440,7 @@ move=> p; rewrite -[xchooseb _](ncvg_uniq cv_u_l) //.
 by apply/asboolP/(xchoosebP p).
 Qed.
 
-Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo.
+Lemma nlim_out u : ~ (exists l, ncvg u l) -> nlim u = -oo%E.
 Proof.
 move=> h; rewrite /nlim; case: {-}_ / idP => // p.
 by case: h; case/existsbP: p => l /asboolP; exists l.

theories/altreals/realsum.v

@@ -174,10 +174,11 @@ Proof.
 move=> mono_u; pose E := [pred x | `[exists n, x == u n]].
 have nzE: nonempty E by exists (u 0%N); apply/imsetbP; exists 0%N.
 case/boolP: `[< has_sup E >] => /asboolP; last first.
-  move/has_supPn=> -/(_ nzE) h; exists +oo => //; elim/nbh_pinfW => M /=.
+  move/has_supPn=> -/(_ nzE) h; exists +oo%E => //; elim/nbh_pinfW => M /=.
   case/(_ M): h=> x /imsetbP[K -> lt_MuK]; exists K=> n le_Kn; rewrite inE.
   by apply/(lt_le_trans lt_MuK)/mono_u.
-move=> supE; exists (sup E)%:E => //; elim/nbh_finW=>e /= gt0_e.
+move=> supE; exists (sup E)%:E => //; first exact: lte_ninfty.
+elim/nbh_finW=>e /= gt0_e.
 case: (sup_adherent supE gt0_e)=> x /imsetbP[K ->] lt_uK.
 exists K=> n le_Kn; rewrite inE distrC ger0_norm ?subr_ge0.
   by apply/sup_upper_bound/imsetbP=> //; exists n.

theories/classical_sets.v

@@ -1,5 +1,5 @@
 From mathcomp Require Import ssreflect ssrfun ssrbool ssrnat eqtype choice.
-From mathcomp Require Import ssralg matrix.
+From mathcomp Require Import fintype bigop ssralg matrix.
 Require Import boolp.
 
 (******************************************************************************)
@@ -349,6 +349,14 @@ Qed.
 Lemma subIset {A} (X Y Z : set A) : X `<=` Z \/ Y `<=` Z -> X `&` Y `<=` Z.
 Proof. case => H a; by [move=> [/H] | move=> [_ /H]]. Qed.
 
+Lemma subsetI_neq0 T (A B C D : set T) :
+  A `<=` B -> C `<=` D -> A `&` C !=set0 -> B `&` D !=set0.
+Proof. by move=> AB CD [x [/AB Bx /CD Dx]]; exists x. Qed.
+
+Lemma subsetI_eq0 T (A B C D : set T) :
+  A `<=` B -> C `<=` D -> B `&` D = set0 -> A `&` C = set0.
+Proof. by move=> AB /(subsetI_neq0 AB); rewrite -!set0P => /contra_eq. Qed.
+
 Lemma setD_eq0 A (X Y : set A) : (X `\` Y = set0) = (X `<=` Y).
 Proof.
 rewrite propeqE; split=> [XDY0 a|sXY].
@@ -371,14 +379,17 @@ Proof. by rewrite predeqE => ?; split=> [[]|[]]. Qed.
 Lemma setIT {A} (X : set A) : X `&` setT = X.
 Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
 
+Lemma setTI {A} (X : set A) : setT `&` X = X.
+Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
+
 Lemma setI0 {A} (X : set A) : X `&` set0 = set0.
 Proof. by rewrite predeqE => ?; split=> [[]|]. Qed.
 
 Lemma set0I A (Y : set A) : set0 `&` Y = set0.
 Proof. by rewrite setIC setI0. Qed.
 
 Lemma setICl {A} (X : set A) : ~` X `&` X = set0.
-Proof. by rewrite predeqE => ?; split => // -[]. Qed.
+Proof. by rewrite predeqE => ?; split => // -[]. Qed.
 
 Lemma setIA {A} (X Y Z : set A) : X `&` (Y `&` Z) = X `&` Y `&` Z.
 Proof. by rewrite predeqE => ?; split=> [[? []]|[[]]]. Qed.
@@ -403,10 +414,16 @@ Lemma setUC A : commutative (@setU A).
 Proof. move=> p q; rewrite /setU predeqE => a; tauto. Qed.
 
 Lemma set0U T (X : set T) : set0 `|` X = X.
-Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|right]. Qed.
+Proof. by rewrite predeqE => t; split; [case|right]. Qed.
 
 Lemma setU0 T (X : set T) : X `|` set0 = X.
-Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|left]. Qed.
+Proof. by rewrite predeqE => t; split; [case|left]. Qed.
+
+Lemma setTU T (X : set T) : setT `|` X = setT.
+Proof. by rewrite predeqE => t; split; [case|left]. Qed.
+
+Lemma setUT T (X : set T) : X `|` setT = setT.
+Proof. by rewrite predeqE => t; split; [case|right]. Qed.
 
 Lemma setU_eq0 T (X Y : set T) : (X `|` Y = set0) = ((X = set0) /\ (Y = set0)).
 Proof. by rewrite -!subset0 subUset. Qed.
@@ -425,6 +442,26 @@ move=> [i Di]; rewrite predeqE => a; split=> [[Ifa Xa] j Dj|IfIXa].
 by split=> [j /IfIXa [] | ] //; have /IfIXa [] := Di.
 Qed.
 
+Lemma setIDl T : left_distributive (@setI T) (@setU T).
+Proof.
+move=> X Y Z; rewrite predeqE => t; split.
+  by move=> [[Xt|Yt] Zt]; [left|right].
+by move=> [[Xt Zt]|[Yt Zt]]; split => //; [left|right].
+Qed.
+
+Lemma setIDr T : right_distributive (@setI T) (@setU T).
+Proof. by move=> X Y Z; rewrite ![X `&` _]setIC setIDl. Qed.
+
+Lemma setUDl T : left_distributive (@setU T) (@setI T).
+Proof.
+move=> X Y Z; rewrite predeqE => t; split.
+  by move=> [[Xt Yt]|Zt]; split; by [left|right].
+by move=> [[Xt|Zt] [Yt|Zt']]; by [left|right].
+Qed.
+
+Lemma setUDr T : right_distributive (@setU T) (@setI T).
+Proof. by move=> X Y Z; rewrite ![X `|` _]setUC setUDl. Qed.
+
 Definition is_subset1 {A} (X : set A) := forall x y, X x -> X y -> x = y.
 Definition is_fun {A B} (f : A -> B -> Prop) := all (is_subset1 \o f).
 Definition is_total {A B} (f : A -> B -> Prop) := all (nonempty \o f).
@@ -476,6 +513,39 @@ Lemma fun_of_rel_uniq {A} {B : choiceType} (f : A -> B -> Prop) (f0 : A -> B) a
   is_subset1 (f a) -> forall b, f a b ->  fun_of_rel f0 f a = b.
 Proof. by move=> fa_prop b /xget_subset1 xgeteq; rewrite /fun_of_rel xgeteq. Qed.
 
+Section SetMonoids.
+Variable (T : Type).
+
+Import Monoid.
+Canonical setU_monoid := Law (@setUA T) (@set0U T) (@setU0 T).
+Canonical setU_comoid := ComLaw (@setUC T).
+Canonical setU_mul_monoid := MulLaw (@setTU T) (@setUT T).
+Canonical setI_monoid := Law (@setIA T) (@setTI T) (@setIT T).
+Canonical setI_comoid := ComLaw (@setIC T).
+Canonical setI_mul_monoid := MulLaw (@set0I T) (@setI0 T).
+Canonical setU_add_monoid := AddLaw (@setUDl T) (@setUDr T).
+Canonical setI_add_monoid := AddLaw (@setIDl T) (@setIDr T).
+
+End SetMonoids.
+
+Lemma bigcup_ord T n (A : nat -> set T) :
+ \big[setU/set0]_(i < n) A i = \bigcup_(i in [set k | (k < n)%N]) A i.
+Proof.
+elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE; split => -[].
+rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
+  by move=> [A0|[i AS]]; [exists 0%N|exists i.+1].
+by move=> [[|i] Ai]; [left|right; exists i].
+Qed.
+
+Lemma bigcap_ord T n (A : nat -> set T) :
+ \big[setI/setT]_(i < n) A i = \bigcap_(i in [set k | (k < n)%N]) A i.
+Proof.
+elim: n => [|n IHn] in A *; first by rewrite big_ord0 predeqE.
+rewrite big_ord_recl /= (IHn (fun i => A i.+1)) predeqE => x; split.
+  by move=> [A0 AS] [|i]// /AS.
+by move=> AP; split => [|i i_lt]; apply: AP.
+Qed.
+
 Module Pointed.
 
 Definition point_of (T : Type) := T.

theories/derive.v

@@ -108,10 +108,10 @@ Lemma diff_locallyxP (x : V) (f : V -> W) :
 Proof.
 split=> [dxf|[dfc dxf]].
   split => //; apply: eqaddoEx => h; have /diffE -> := dxf.
-  rewrite lim_id addrK; congr (_ + _); rewrite littleo_center0 /= addrK.
+  rewrite lim_id // addrK; congr (_ + _); rewrite littleo_center0 /= addrK.
   by congr ('o); rewrite funeqE => k /=; rewrite addrK.
 apply/diffP; split=> //; apply: eqaddoEx; move=> y.
-rewrite lim_id -[in LHS](subrK x y) dxf; congr (_ + _).
+rewrite lim_id // -[in LHS](subrK x y) dxf; congr (_ + _).
 rewrite -(comp_centerK x id) -[X in the_littleo _ _ _ X](comp_centerK x).
 by rewrite -[_ (y - x)]/((_ \o (center x)) y) -littleo_center0.
 Qed.
@@ -297,7 +297,7 @@ rewrite /derive => /diff_locally -> /=; set k := 'o _.
 evar (g : R -> W); rewrite [X in X @ _](_ : _ = g) /=; last first.
   rewrite funeqE=> h; rewrite !scalerDr scalerN /cst /=.
   by rewrite addrC !addrA addNr add0r linearZ /= scalerA /g.
-apply: cvg_map_lim.
+apply: cvg_map_lim => //.
 pose g1 : R -> W := fun h => (h^-1 * h) *: 'd f a v.
 pose g2 : R -> W := fun h : R => h^-1 *: k (h *: v ).
 rewrite (_ : g = g1 + g2) ?funeqE // -(addr0 (_ _ v)); apply: (@cvgD _ _ [topologicalType of R^o]).
@@ -525,7 +525,7 @@ suff /diff_locally /hdf -> : differentiable f x.
 apply/diffP; apply: (@getPex _ (fun (df : {linear V -> W}) => continuous df /\
   forall y, f y = f (lim x) + df (y - lim x) +o_(y \near x) (y - lim x))).
 exists df; split=> //; apply: eqaddoEx => z.
-rewrite (hdf _ dxf) !addrA lim_id /(_ \o _) /= subrK [f _ + _]addrC addrK.
+rewrite (hdf _ dxf) !addrA lim_id // /(_ \o _) /= subrK [f _ + _]addrC addrK.
 rewrite -addrA -[LHS]addr0; congr (_ + _).
 apply/eqP; rewrite eq_sym addrC addr_eq0 oppox; apply/eqP.
 by rewrite littleo_center0 (comp_centerK x id) -[- _ in RHS](comp_centerK x).
@@ -1376,7 +1376,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_right_proper_filter x.
-apply: (@cvg_map_lim _ _ _ (at_right _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
+apply: (@cvg_map_lim _ _ _ (at_right _)) => // A /cvfx /locallyP [_ /posnumP[e] xe_A].
 by exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _]; apply: xe_A.
 Qed.
 
@@ -1386,7 +1386,7 @@ Proof.
 move=> cvfx; apply/Logic.eq_sym.
 (* should be inferred *)
 have atrF := at_left_proper_filter x.
-apply: (@cvg_map_lim _ _ _ (at_left _)) => A /cvfx /locallyP [_ /posnumP[e] xe_A].
+apply: (@cvg_map_lim _ _ _ (at_left _)) => // A /cvfx /locallyP [_ /posnumP[e] xe_A].
 exists e%:num => // y xe_y; rewrite lt_def => /andP [xney _].
 by apply: xe_A => //; rewrite eq_sym.
 Qed.
@@ -1411,7 +1411,7 @@ Lemma ler0_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T))
 Proof.
 move=> fle0 fcv; rewrite -oppr_ge0.
 have limopp : - lim (f @ F) = lim (- f @ F).
-  by apply: Logic.eq_sym; apply: cvg_map_lim; apply: cvgN.
+  by apply: Logic.eq_sym; apply: cvg_map_lim => //; apply: cvgN.
 rewrite limopp; apply: le0r_cvg_map; last by rewrite -limopp; apply: cvgN.
 by move: fle0; apply: filterS => x; rewrite oppr_ge0.
 Qed.
@@ -1423,7 +1423,7 @@ Lemma ler_cvg_map (R : realFieldType) (T : topologicalType) (F : set (set T)) (F
 Proof.
 move=> lefg fcv gcv; rewrite -subr_ge0.
 have eqlim : lim (g @ F) - lim (f @ F) = lim ((g - f) @ F).
-  by apply: Logic.eq_sym; apply: cvg_map_lim; apply: cvgD => //; apply: cvgN.
+  by apply/esym; apply: cvg_map_lim => //; apply: cvgD => //; apply: cvgN.
 rewrite eqlim; apply: le0r_cvg_map; last first.
   by rewrite /(cvg _) -eqlim /=; apply: cvgD => //; apply: cvgN.
 by move: lefg; apply: filterS => x; rewrite subr_ge0.

theories/ereal.v

@@ -29,16 +29,18 @@ End ExtendedReals.
 (* TODO: the following notations should have scopes. *)
 
 (*Notation "\+inf" := (@ERPInf _).*)
-Notation "+oo" := (@ERPInf _).
+Notation "+oo" := (@ERPInf _) : ereal_scope.
 (*Notation "\-inf" := (@ERNInf _).*)
-Notation "-oo" := (@ERNInf _).
+Notation "-oo" := (@ERNInf _) : ereal_scope.
 Notation "x %:E" := (@ERFin _ x) (at level 2, format "x %:E").
 
 Notation "{ 'ereal' R }" := (er R) (format "{ 'ereal'  R }").
 
 Bind    Scope ereal_scope with er.
 Delimit Scope ereal_scope with E.
 
+Local Open Scope ereal_scope.
+
 Section EqEReal.
 Variable (R : eqType).
 
@@ -65,7 +67,7 @@ Variable (R : choiceType).
 
 Definition code (x : {ereal R}) :=
   match x with
-  | x%:E  => GenTree.Node 0 [:: GenTree.Leaf x]
+  | x%:E => GenTree.Node 0 [:: GenTree.Leaf x]
   | +oo => GenTree.Node 1 [::]
   | -oo => GenTree.Node 2 [::]
   end.
@@ -99,19 +101,19 @@ Implicit Types (x y : {ereal R}).
 
 Definition le_ereal x1 x2 :=
   match x1, x2 with
-  | -oo, _ | _, +oo => true
-  | +oo, _ | _, -oo => false
-
+  | -oo, x%:E | x%:E, +oo => x \is Num.real
   | x1%:E, x2%:E => x1 <= x2
+  | -oo, _    | _, +oo => true
+  | +oo, _    | _, -oo => false
   end.
 
 Definition lt_ereal x1 x2 :=
   match x1, x2 with
-  | -oo, -oo | +oo, +oo => false
-  | -oo, _   | _  , +oo => true
-  | +oo, _   | _  , -oo => false
-
+  | -oo, x%:E | x%:E, +oo => x \is Num.real
   | x1%:E, x2%:E => x1 < x2
+  | -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.
@@ -121,10 +123,14 @@ Lemma le_refl_ereal : reflexive le_ereal.
 Proof. by case => /=. Qed.
 
 Lemma le_anti_ereal : ssrbool.antisymmetric le_ereal.
-Proof. by case=> [?||][?||] //= /le_anti ->. Qed.
+Proof. by case=> [?||][?||]/=; rewrite ?andbF => // /le_anti ->. Qed.
 
 Lemma le_trans_ereal : ssrbool.transitive le_ereal.
-Proof. by case=> [?||][?||][?||] //=; exact: le_trans. Qed.
+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.
 
 Fact ereal_display : unit. Proof. by []. Qed.
 
@@ -151,12 +157,24 @@ Notation "x < y <= z"  := ((lte x y) && (lee y z)) : ereal_scope.
 Notation "x <= y < z"  := ((lee x y) && (lte y z)) : ereal_scope.
 Notation "x < y < z"   := ((lte x y) && (lte y z)) : ereal_scope.
 
-Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E)%E = (x <= y).
+Lemma lee_fin (R : numDomainType) (x y : R) : (x%:E <= y%:E)%E = (x <= y)%O.
 Proof. by []. Qed.
 
-Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y).
+Lemma lte_fin (R : numDomainType) (x y : R) : (x%:E < y%:E)%E = (x < y)%O.
 Proof. by []. Qed.
 
+Lemma lte_pinfty (R : realDomainType) (x : R) : (x%:E < +oo).
+Proof. exact: num_real. Qed.
+
+Lemma lee_pinfty (R : realDomainType) (x : {ereal R}) : (x <= +oo).
+Proof. case: x => //= r; exact: num_real. Qed.
+
+Lemma lte_ninfty (R : realDomainType) (x : R) : (-oo < x%:E).
+Proof. exact: num_real. Qed.
+
+Lemma lee_ninfty (R : realDomainType) (x : {ereal R}) : (-oo <= x).
+Proof. case: x => //= r; exact: num_real. Qed.
+
 Section ERealOrder_realDomainType.
 Context {R : realDomainType}.
 Implicit Types (x y : {ereal R}).
@@ -196,22 +214,24 @@ Lemma meetKU_ereal y x : max_ereal x (min_ereal x y) = x.
 Proof. by case: x y => [?||][?||] //=; rewrite (meetKU, joinxx). Qed.
 
 Lemma leEmeet_ereal x y : (x <= y)%E = (min_ereal x y == x).
-Proof. by case: x y => [x||][y||] //=; [exact: leEmeet | rewrite eqxx]. Qed.
+Proof.
+case: x y => [x||][y||] //=; rewrite ?eqxx ?lee_pinfty ?lee_ninfty //.
+exact: leEmeet.
+Qed.
 
 Lemma meetUl_ereal : left_distributive min_ereal max_ereal.
 Proof.
 by case=> [?||][?||][?||] //=; rewrite ?(meetUl, meetUK, meetKUC, joinxx).
 Qed.
 
 Lemma minE_ereal x y : min_ereal x y = if le_ereal x y then x else y.
-Proof. by case: x y => [?||][?||] //=; case: leP. Qed.
+Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: leP. Qed.
 
 Lemma maxE_ereal x y : max_ereal x y = if le_ereal y x then x else y.
-Proof.
-Proof. by case: x y => [?||][?||] //=; case: ltP. Qed.
+Proof. by case: x y => [?||][?||] //=; rewrite ?num_real //; case: ltP. Qed.
 
 Lemma le_total_ereal : total (@le_ereal R).
-Proof. by case=> [?||][?||] //=; exact: le_total. Qed.
+Proof. by case=> [?||][?||] //=; rewrite ?num_real //; exact: le_total. Qed.
 
 Definition ereal_latticeMixin :=
   LatticeMixin min_erealC max_erealC min_erealA max_erealA

theories/landau.v

@@ -1139,7 +1139,7 @@ Hypothesis (normm_s : forall k x, `|s k x| = `|k| * `|x|).
 (* - locally lipschitz => continuous at a point *)
 (* - lipschitz => uniformly continous *)
 
-Local Notation "'+oo'" := (@ERPInf R).
+Local Notation "'+oo'" := (@pinfty_locally R).
 
 Lemma linear_for_continuous (f : {linear U -> V | GRing.Scale.op s_law}) :
   (f : _ -> _) =O_ (0 : U) (cst (1 : R^o)) -> continuous f.