diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f420fa60e..5724ef64c 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/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 diff --git a/classical/filter.v b/classical/filter.v index b69519887..0398c8a5d 100644 --- a/classical/filter.v +++ b/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,7 +427,7 @@ 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 @@ -434,8 +435,9 @@ Class ProperFilter {T : Type} (F : set_system T) := { 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. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index a72375ede..2f38b1708 100644 --- a/theories/lebesgue_integral.v +++ b/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. diff --git a/theories/normedtype.v b/theories/normedtype.v index 4d4b0d41e..238c5d0a7 100644 --- a/theories/normedtype.v +++ b/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 /=. diff --git a/theories/realfun.v b/theories/realfun.v index a2551b9bf..05046d38c 100644 --- a/theories/realfun.v +++ b/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}. diff --git a/theories/topology.v b/theories/topology.v index 274fd86df..7600e7f76 100644 --- a/theories/topology.v +++ b/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),