generalize lime_sup_ge0 (#1252)

* generalize lime_sup_ge0

* fixes #1342

* fixes #1343

CHANGELOG_UNRELEASED.md

@@ -52,6 +52,9 @@
   + lemma `vitali_coverS`
   + lemma `vitali_theorem_corollary`
 
+- in `normedtype.v`:
+  + lemma `limf_esup_ge0`
+
 ### Changed
 
 - in `numfun.v`:
@@ -231,6 +234,8 @@
 
 - in `separation_axioms.v`:
   + definition `cvg_toi_locally_close`
+- in `realfun.v`:
+  + lemma `lime_sup_ge0`
 
 ### Removed
 

classical/filter.v

@@ -43,6 +43,9 @@ From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
 (*                  filter_prod F G == product of the filters F and G         *)
 (*                        F `=>` G <-> G is included in F                     *)
 (*                                     F and G are sets of sets.              *)
+(*                              \oo == "eventually" filter on nat: set of     *)
+(*                                     predicates on natural numbers that are *)
+(*                                     eventually true                        *)
 (*                         F --> G <-> the canonical filter associated to G   *)
 (*                                     is included in the canonical filter    *)
 (*                                     associated to F                        *)
@@ -210,18 +213,16 @@ HB.mixin Record isFiltered U T := {
 
 #[short(type="filteredType")]
 HB.structure Definition Filtered (U : Type) := {T of Choice T & isFiltered U T}.
+Arguments nbhs {_ _} _ _ : simpl never.
 
 #[short(type="pfilteredType")]
 HB.structure Definition PointedFiltered (U : Type) := {T of Pointed T & isFiltered U T}.
-Arguments nbhs {_ _} _ _ : simpl never.
 
 HB.instance Definition _ T := Equality.on (set_system T).
 HB.instance Definition _ T := Choice.on (set_system T).
 HB.instance Definition _ T := Pointed.on (set_system T).
 HB.instance Definition _ T := isFiltered.Build T (set_system T) id.
 
-Arguments nbhs {_ _} _ _ : simpl never.
-
 HB.mixin Record selfFiltered T := {}.
 
 HB.factory Record hasNbhs T := { nbhs : T -> set_system T }.
@@ -426,16 +427,17 @@ Class Filter {T : Type} (F : set_system T) := {
 Global Hint Mode Filter - ! : typeclass_instances.
 
 Class ProperFilter {T : Type} (F : set_system T) := {
-  filter_not_empty : not (F (fun _ => False)) ;
+  filter_not_empty : ~ F set0 ;
   filter_filter : Filter F
 }.
 (* TODO: Reuse :> above and remove the following line and the coercion below
    after 8.21 is the minimum required version for Coq *)
 Global Existing Instance filter_filter.
 Global Hint Mode ProperFilter - ! : typeclass_instances.
 Arguments filter_not_empty {T} F {_}.
+Hint Extern 0 (~ _ set0) => solve [apply: filter_not_empty] : core.
 
-Lemma filter_setT (T' : Type) : Filter [set: set T'].
+Lemma filter_setT (T : Type) : Filter [set: set T].
 Proof. by constructor. Qed.
 
 Lemma filterP_strong T (F : set_system T) {FF : Filter F} (P : set T) :
@@ -753,6 +755,17 @@ move=> FF BN0; apply: Build_ProperFilter_ex => P [i Di BiP].
 by have [x Bix] := BN0 _ Di; exists x; apply: BiP.
 Qed.
 
+Global Instance eventually_filter : ProperFilter eventually.
+Proof.
+eapply @filter_from_proper; last by move=> i _; exists i => /=.
+apply: filter_fromT_filter; first by exists 0%N.
+move=> i j; exists (maxn i j) => n //=.
+by rewrite geq_max => /andP[ltin ltjn].
+Qed.
+
+Canonical eventually_filterType := FilterType eventually _.
+Canonical eventually_pfilterType := PFilterType eventually (filter_not_empty _).
+
 Lemma filter_bigI T (I : choiceType) (D : {fset I}) (f : I -> set T)
   (F : set_system T) :
   Filter F -> (forall i, i \in D -> F (f i)) ->
@@ -816,7 +829,7 @@ Qed.
 Global Instance fmap_proper_filter T U (f : T -> U) (F : set_system T) :
   ProperFilter F -> ProperFilter (f @ F).
 Proof.
-by move=> FF; apply: Build_ProperFilter; rewrite fmapE; apply: filter_not_empty.
+by move=> FF; apply: Build_ProperFilter; rewrite fmapE preimage_set0.
 Qed.
 
 Definition fmapi {T U : Type} (f : T -> set U) (F : set_system T) :
@@ -946,8 +959,8 @@ by move=> AP AQ x Ax; split; [apply: AP|apply: AQ].
 Qed.
 
 Global Instance globally_properfilter {T : Type} (A : set T) a :
-  (A a) -> ProperFilter (globally A).
-Proof. by move=> Aa; apply: Build_ProperFilter => /(_ a). Qed.
+  A a -> ProperFilter (globally A).
+Proof. by move=> Aa; apply: Build_ProperFilter => /(_ a); exact. Qed.
 
 (** Specific filters *)
 
@@ -1222,7 +1235,6 @@ Definition powerset_filter_from : set_system (set Y) := filter_from
 Global Instance powerset_filter_from_filter : ProperFilter powerset_filter_from.
 Proof.
 split.
-  rewrite (_ : xpredp0 = set0); last by rewrite eqEsubset; split.
   by move=> [W [_ _ [N +]]]; rewrite subset0 => /[swap] ->; apply.
 apply: filter_from_filter.
   by exists F; split => //; exists setT; exact: filterT.
@@ -1601,4 +1613,4 @@ by rewrite AB0 in FAB.
 Qed.
 
 Lemma proper_meetsxx T (F : set_system T) (FF : ProperFilter F) : F `#` F.
-Proof. by rewrite meetsxx; apply: filter_not_empty. Qed.
+Proof. by rewrite meetsxx. Qed.

theories/lebesgue_integral.v

@@ -6288,7 +6288,7 @@ Definition lim_sup_davg f x := lime_sup (davg f x) 0.
 Local Notation "f ^*" := (lim_sup_davg f).
 
 Lemma lim_sup_davg_ge0 f x : 0 <= f^* x.
-Proof. by apply: lime_sup_ge0 => y; rewrite /davg iavg_ge0. Qed.
+Proof. by apply: limf_esup_ge0 => // => y; exact: iavg_ge0. Qed.
 
 Lemma lim_sup_davg_le f g x (U : set R) : open_nbhs x U -> measurable U ->
   measurable_fun U f -> measurable_fun U g ->
@@ -6565,7 +6565,8 @@ move=> Ef; have {Ef} : mu.-negligible (E `&` [set x | 0 < f^* x]).
   by rewrite ltr_nat ltnS; near: m; exact: nbhs_infty_gt.
 apply: negligibleS => z /= /not_implyP[Ez H]; split => //.
 rewrite ltNge; apply: contra_notN H.
-rewrite le_eqVlt ltNge lime_sup_ge0 /= ?orbF; last by move=> x; exact: iavg_ge0.
+rewrite le_eqVlt ltNge limf_esup_ge0/= ?orbF//; last first.
+  by move=> x; exact: iavg_ge0.
 move=> /eqP fz0.
 suff: lime_inf (davg f z) 0 = 0 by exact: lime_sup_inf_at_right.
 apply/eqP; rewrite eq_le -[X in _ <= X <= _]fz0 lime_inf_sup/= fz0.

theories/normedtype.v

@@ -181,6 +181,21 @@ Proof. by rewrite /limf_einf; under eq_fun do rewrite oppeK. Qed.
 
 End limf_esup_einf.
 
+Section limf_esup_einf_realType.
+Variables (T : choiceType) (X : filteredType T) (R : realType).
+Implicit Types (f : X -> \bar R) (F : set (set X)).
+Local Open Scope ereal_scope.
+
+Lemma limf_esup_ge0 f F : ~ F set0 ->
+  (forall x, 0 <= f x) -> 0 <= limf_esup f F.
+Proof.
+move=> F0 f0; rewrite limf_esupE; apply: lb_ereal_inf => /= x [A].
+have [-> /F0//|/set0P[y Ay FA] <-{x}] := eqVneq A set0.
+by apply: ereal_sup_le; exists (f y).
+Qed.
+
+End limf_esup_einf_realType.
+
 Lemma nbhsN (R : numFieldType) (x : R) : nbhs (- x) = -%R @ x.
 Proof.
 rewrite predeqE => A; split=> //= -[] e e_gt0 xeA; exists e => //= y /=.

theories/realfun.v

@@ -858,16 +858,8 @@ Proof. by rewrite /lime_sup -limf_einfN. Qed.
 Lemma lime_supN f a : lime_sup (\- f) a = - lime_inf f a.
 Proof. by rewrite /lime_inf oppeK. Qed.
 
-Lemma lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a.
-Proof.
-move=> f0; rewrite lime_supE; apply: lb_ereal_inf => /= x [e /=].
-rewrite in_itv/= andbT => e0 <-{x}; rewrite -(ereal_sup1 0) ereal_sup_le //=.
-exists (f (a + e / 2)%R); last by rewrite ereal_sup1 f0.
-exists (a + e / 2)%R => //=; split.
-  rewrite /ball/= opprD addrA subrr sub0r normrN gtr0_norm ?divr_gt0//.
-  by rewrite ltr_pdivrMr// ltr_pMr// ltr1n.
-by apply/eqP; rewrite gt_eqF// ltr_pwDr// divr_gt0.
-Qed.
+Lemma __deprecated__lime_sup_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_sup f a.
+Proof. by move=> f0; exact: limf_esup_ge0. Qed.
 
 Lemma lime_inf_ge0 f a : (forall x, 0 <= f x) -> 0 <= lime_inf f a.
 Proof.
@@ -1066,6 +1058,8 @@ move=> supfal inffal; apply/cvg_at_leftNP/lime_sup_inf_at_right.
 Qed.
 
 End lime_sup_inf.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="use `limf_esup_ge0` instead")]
+Notation lime_sup_ge0 := __deprecated__lime_sup_ge0 (only parsing).
 
 Section derivable_oo_continuous_bnd.
 Context {R : numFieldType} {V : normedModType R}.

theories/topology.v

@@ -65,9 +65,6 @@ Require Import reals signed.
 (* - matrices `'M[T]_(m, n)`                                                  *)
 (* - natural numbers `nat`                                                    *)
 (* ```                                                                        *)
-(*                              \oo == "eventually" filter on nat: set of     *)
-(*                                     predicates on natural numbers that are *)
-(*                                     eventually true                        *)
 (*                  weak_topology f == weak topology by a function f : S -> T *)
 (*                                     on S                                   *)
 (*                                     S must be a choiceType and T a         *)
@@ -754,17 +751,6 @@ HB.instance Definition _ := isBaseTopological.Build nat bT bD.
 
 End nat_topologicalType.
 
-Global Instance eventually_filter : ProperFilter eventually.
-Proof.
-eapply @filter_from_proper; last by move=> i _; exists i => /=.
-apply: filter_fromT_filter; first by exists 0%N.
-move=> i j; exists (maxn i j) => n //=.
-by rewrite geq_max => /andP[ltin ltjn].
-Qed.
-
-Canonical eventually_filterType := FilterType eventually _.
-Canonical eventually_pfilterType := PFilterType eventually (filter_not_empty _).
-
 Lemma nbhs_infty_gt N : \forall n \near \oo, (N < n)%N.
 Proof. by exists N.+1. Qed.
 #[global] Hint Resolve nbhs_infty_gt : core.
@@ -1427,7 +1413,7 @@ Definition near_covering (K : set X) :=
 Let near_covering_compact : near_covering `<=` compact.
 Proof.
 move=> K locK F PF FK; apply/set0P/eqP=> KclstF0; case: (PF) => + FF; apply.
-rewrite (_ : xpredp0 = set0)// -(setICr K); apply: filterI => //.
+rewrite -(setICr K); apply: filterI => //.
 have /locK : forall x, K x ->
     \forall x' \near x & i \near powerset_filter_from F, (~` i) x'.
   move=> x Kx; have : ~ cluster F x.
@@ -4488,7 +4474,6 @@ have : f @` closure (AfE b) `&` f @` AfE (~~ b) = set0.
 by rewrite predeqE => /(_ (f t)) [fcAfEb] _; apply: fcAfEb; split; exists t.
 Qed.
 
-
 Lemma continuous_localP {X Y : topologicalType} (f : X -> Y) :
   continuous f <->
   forall (x : X), \forall U \near powerset_filter_from (nbhs x),