isolate the theory of lime_sup (#1121)

* isolate the theory of lime_sup

- generic def of limsup

---------

Co-authored-by: Zachary Stone <[email protected]>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -83,6 +83,54 @@
   + lemma `maxe_cvg_0_cvg_fin_num`
   + lemma `maxe_cvg_maxr_cvg`
   + lemma `maxe_cvg_0_cvg_0`
+- in `constructive_ereal.v`
+  + lemma `lee_subgt0Pr`
+
+- in `topology.v`:
+  + lemma `nbhs_dnbhs_neq`
+
+- in `normedtype.v`:
+  + lemma `not_near_at_rightP`
+
+- in `realfun.v`:
+  + lemma `cvg_at_right_left_dnbhs`
+  + lemma `cvg_at_rightP`
+  + lemma `cvg_at_leftP`
+  + lemma `cvge_at_rightP`
+  + lemma `cvge_at_leftP`
+  + lemma `lime_sup`
+  + lemma `lime_inf`
+  + lemma `lime_supE`
+  + lemma `lime_infE`
+  + lemma `lime_infN`
+  + lemma `lime_supN`
+  + lemma `lime_sup_ge0`
+  + lemma `lime_inf_ge0`
+  + lemma `lime_supD`
+  + lemma `lime_sup_le`
+  + lemma `lime_inf_sup`
+  + lemma `lim_lime_inf`
+  + lemma `lim_lime_sup`
+  + lemma `lime_sup_inf_at_right`
+  + lemma `lime_sup_inf_at_left`
+
+- in `normedtype.v`:
+  + lemmas `withinN`, `at_rightN`, `at_leftN`, `cvg_at_leftNP`, `cvg_at_rightNP`
+  + lemma `dnbhsN`
+  + lemma `limf_esup_dnbhsN`
+
+- in `topology.v`:
+  + lemma `dnbhs_ball`
+
+- in `normedtype.v`
+  + definitions `limf_esup`, `limf_einf`
+  + lemmas `limf_esupE`, `limf_einfE`, `limf_esupN`, `limf_einfN`
+
+- in `sequences.v`:
+  + lemmas `limn_esup_lim`, `limn_einf_lim`
+
+- in `realfun.v`:
+  + lemmas `lime_sup_lim`, `lime_inf_lim`
 
 ### Changed
 
@@ -118,6 +166,10 @@
 - moved from `topology.v` to `mathcomp_extra.v`
   + definition `monotonous`
 
+- in `sequences.v`:
+  + `limn_esup` now defined from `lime_sup`
+  + `limn_einf` now defined from `limn_esup`
+  
 ### Renamed
 
 - in `exp.v`:

theories/constructive_ereal.v

@@ -3035,6 +3035,14 @@ apply/(iffP idP) => [|].
   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 lee_subl_addr//; move: e; exact/lee_addgt0Pr.
+by apply/lee_addgt0Pr => e e0; rewrite -lee_subl_addr// xy.
+Qed.
+
 Lemma lee_mul01Pr x y : 0 <= x ->
   reflect (forall r, (0 < r < 1)%R -> r%:E * x <= y) (x <= y).
 Proof.

theories/lebesgue_integral.v

@@ -2370,7 +2370,8 @@ pose g n := fun x => einfs (f ^~ x) n.
 have mg := measurable_fun_einfs mf.
 have g0 n x : D x -> 0 <= g n x.
   by move=> Dx; apply: lb_ereal_inf => _ [m /= nm <-]; exact: f0.
-rewrite monotone_convergence //; last first.
+under eq_integral do rewrite limn_einf_lim.
+rewrite limn_einf_lim monotone_convergence //; last first.
   move=> x Dx m n mn /=; apply: le_ereal_inf => _ /= [p /= np <-].
   by exists p => //=; rewrite (leq_trans mn).
 apply: lee_lim.

theories/lebesgue_measure.v

@@ -1823,7 +1823,7 @@ Proof.
 move=> mf mD; rewrite (_ :  (fun _ => _) =
     (fun x => ereal_inf [set esups (f^~ x) n | n in [set n | n >= 0]%N])).
   by apply: measurable_fun_einfs => // k; exact: measurable_fun_esups.
-rewrite funeqE => t; apply/cvg_lim => //.
+rewrite funeqE => t; rewrite limn_esup_lim; apply/cvg_lim => //.
 rewrite [X in _ --> X](_ : _ = ereal_inf (range (esups (f^~t)))).
   exact: cvg_esups_inf.
 by congr (ereal_inf [set _ | _ in _]); rewrite predeqE.
@@ -1834,6 +1834,7 @@ Lemma emeasurable_fun_cvg D (f_ : (T -> \bar R)^nat) (f : T -> \bar R) :
   (forall x, D x -> f_ ^~ x --> f x) -> measurable_fun D f.
 Proof.
 move=> mf_ f_f; have fE x : D x -> f x = limn_esup (f_^~ x).
+  rewrite limn_esup_lim.
   by move=> Dx; have /cvg_lim  <-// := @cvg_esups _ (f_^~x) (f x) (f_f x Dx).
 apply: (eq_measurable_fun (fun x => limn_esup (f_ ^~ x))) => //.
   by move=> x; rewrite inE => Dx; rewrite fE.

theories/normedtype.v

@@ -10,6 +10,11 @@ Require Import ereal reals signed topology prodnormedzmodule.
 (*                                                                            *)
 (* Note that balls in topology.v are not necessarily open, here they are.     *)
 (*                                                                            *)
+(* * Limit superior and inferior:                                             *)
+(*   limf_esup f F, limf_einf f F == limit sup/inferior of f at "filter" F    *)
+(*                                   f has type X -> \bar R.                  *)
+(*                                   F has type set (set X).                  *)
+(*                                                                            *)
 (* * Normed Topological Abelian groups:                                       *)
 (*  pseudoMetricNormedZmodType R  == interface type for a normed topological  *)
 (*                                   Abelian group equipped with a norm       *)
@@ -144,6 +149,35 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 
+Section limf_esup_einf.
+Variables (T : choiceType) (X : filteredType T) (R : realFieldType).
+Implicit Types (f : X -> \bar R) (F : set (set X)).
+Local Open Scope ereal_scope.
+
+Definition limf_esup f F := ereal_inf [set ereal_sup (f @` V) | V in F].
+
+Definition limf_einf f F := - limf_esup (\- f) F.
+
+Lemma limf_esupE f F :
+  limf_esup f F = ereal_inf [set ereal_sup (f @` V) | V in F].
+Proof. by []. Qed.
+
+Lemma limf_einfE f F :
+  limf_einf f F = ereal_sup [set ereal_inf (f @` V) | V in F].
+Proof.
+rewrite /limf_einf limf_esupE /ereal_inf oppeK -[in RHS]image_comp /=.
+congr (ereal_sup [set _ | _ in [set ereal_sup _ | _ in _]]).
+by under eq_fun do rewrite -image_comp.
+Qed.
+
+Lemma limf_esupN f F : limf_esup (\- f) F = - limf_einf f F.
+Proof. by rewrite /limf_einf oppeK. Qed.
+
+Lemma limf_einfN f F : limf_einf (\- f) F = - limf_esup f F.
+Proof. by rewrite /limf_einf; under eq_fun do rewrite oppeK. Qed.
+
+End limf_esup_einf.
+
 Definition pointed_of_zmodule (R : zmodType) : pointedType := PointedType R 0.
 
 Definition filtered_of_normedZmod (K : numDomainType) (R : normedZmodType K)
@@ -214,6 +248,20 @@ move=> [y [[z Az oppzey] [t Bt opptey]]]; exists (- y).
 by split; [rewrite -oppzey opprK|rewrite -opptey opprK].
 Qed.
 
+Lemma dnbhsN {R : numFieldType} (r : R) :
+  (- r)%R^' = (fun A => -%R @` A) @` r^'.
+Proof.
+apply/seteqP; split=> [A [e/= e0 reA]|_/= [A [e/= e0 reA <-]]].
+  exists (-%R @` A).
+    exists e => // x/= rxe xr; exists (- x)%R; rewrite ?opprK//.
+    by apply: reA; rewrite ?eqr_opp//= opprK addrC distrC.
+  rewrite image_comp (_ : _ \o _ = idfun) ?image_id// funeqE => x/=.
+  by rewrite opprK.
+exists e => //= x/=; rewrite -opprD normrN => axe xa.
+exists (- x)%R; rewrite ?opprK//; apply: reA; rewrite ?eqr_oppLR//=.
+by rewrite opprK.
+Qed.
+
 Module PseudoMetricNormedZmodule.
 Section ClassDef.
 Variable R : numDomainType.
@@ -1629,6 +1677,15 @@ End Exports.
 End numFieldNormedType.
 Import numFieldNormedType.Exports.
 
+Lemma limf_esup_dnbhsN {R : realType} (f : R -> \bar R) (a : R) :
+  limf_esup f a^' = limf_esup (fun x => f (- x)%R) (- a)%R^'.
+Proof.
+rewrite /limf_esup dnbhsN image_comp/=.
+congr (ereal_inf [set _ | _ in _]); apply/funext => A /=.
+rewrite image_comp/= -compA (_ : _ \o _ = idfun)// funeqE => x/=.
+by rewrite opprK.
+Qed.
+
 Section NormedModule_numDomainType.
 Variables (R : numDomainType) (V : normedModType R).
 
@@ -2077,6 +2134,47 @@ Lemma nbhs_left_ge x z : z < x -> \forall y \near x^'-, z <= y.
 Proof. by move=> xz; near do apply/ltW; apply: nbhs_left_gt.
 Unshelve. all: by end_near. Qed.
 
+Lemma not_near_at_rightP T (f : R -> T) (p : R) (P : pred T) :
+  ~ (\forall x \near p^'+, P (f x)) ->
+  forall e : {posnum R}, exists2 x, p < x < p + e%:num & ~ P (f x).
+Proof.
+move=> pPf e; apply: contrapT => /forallPNP pePf; apply: pPf; near=> t.
+apply: contrapT; apply: pePf; apply/andP; split.
+- by near: t; exact: nbhs_right_gt.
+- by near: t; apply: nbhs_right_lt; rewrite ltr_addl.
+Unshelve. all: by end_near. Qed.
+
+Lemma withinN (A : set R) a :
+  within A (nbhs (- a)) = - x @[x --> within (-%R @` A) (nbhs a)].
+Proof.
+rewrite eqEsubset /=; split; move=> E /= [e e0 aeE]; exists e => //.
+  move=> r are ra; apply: aeE; last by rewrite memNE opprK.
+  by rewrite /= opprK addrC distrC.
+move=> r aer ar; rewrite -(opprK r); apply: aeE; last by rewrite -memNE.
+by rewrite /= opprK -normrN opprD.
+Qed.
+
+Let fun_predC (T : choiceType) (f : T -> T) (p : pred T) : involutive f ->
+  [set f x | x in p] = [set x | x in p \o f].
+Proof.
+by move=> fi; apply/seteqP; split => _/= [y hy <-];
+  exists (f y) => //; rewrite fi.
+Qed.
+
+Lemma at_rightN a : (- a)^'+ = -%R @ a^'-.
+Proof.
+rewrite /at_right withinN [X in within X _](_ : _ = [set u | u < a])//.
+rewrite (@fun_predC _ -%R)/=; last exact: opprK.
+by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
+Qed.
+
+Lemma at_leftN a : (- a)^'- = -%R @ a^'+.
+Proof.
+rewrite /at_left withinN [X in within X _](_ : _ = [set u | a < u])//.
+rewrite (@fun_predC _ -%R)/=; last exact: opprK.
+by rewrite image_id; under eq_fun do rewrite ltr_oppl opprK.
+Qed.
+
 End at_left_right.
 #[global] Typeclasses Opaque at_left at_right.
 Notation "x ^'-" := (at_left x) : classical_set_scope.
@@ -2088,6 +2186,20 @@ Notation "x ^'+" := (at_right x) : classical_set_scope.
 #[global] Hint Extern 0 (Filter (nbhs _^'-)) =>
   (apply: at_left_proper_filter) : typeclass_instances.
 
+Lemma cvg_at_leftNP {T : topologicalType} {R : numFieldType}
+    (f : R -> T) a (l : T) :
+  f @ a^'- --> l <-> f \o -%R @ (- a)^'+ --> l.
+Proof.
+by rewrite at_rightN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
+Qed.
+
+Lemma cvg_at_rightNP {T : topologicalType} {R : numFieldType}
+    (f : R -> T) a (l : T) :
+  f @ a^'+ --> l <-> f \o -%R @ (- a)^'- --> l.
+Proof.
+by rewrite at_leftN -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK.
+Qed.
+
 Section open_itv_subset.
 Context {R : realType}.
 Variables (A : set R) (x : R).