Utility lemmas in filter.v

CHANGELOG_UNRELEASED.md

@@ -274,6 +274,10 @@
 - in `lebesgue_Rintegral.v`:
   + lemma `Rdominated_cvg`
 
+- in `filter.v`:
+  + lemmas `near_eq_cvg_eq`, `near_eq_is_cvg`, `near_eq_lim`,
+    `cvg_to_withinP`, `within_cvg_to_within`
+
 ### Changed
 
 - in `realsum.v`:

classical/filter.v

@@ -925,18 +925,36 @@ Lemma near_eq_cvg {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
   {near F, f =1 g} -> g @ F `=>` f @ F.
 Proof. by move=> eq_fg P /=; apply: filterS2 eq_fg => x /= <-. Qed.
 
-Lemma eq_cvg (T T' : Type) (F : set_system T) (f g : T -> T') (x : set_system T') :
+Lemma near_eq_cvg_eq {T U} {F : set_system T} {FF : Filter F} (f g : T -> U) :
+  {near F, f =1 g} -> f @ F = g @ F.
+Proof.
+move=> fg; apply/seteqP; split; apply: near_eq_cvg => //.
+by near do symmetry.
+Unshelve. all: by end_near. Qed.
+
+Lemma eq_cvg (T U : Type) (F : set_system T) (f g : T -> U) (x : set_system U) :
   f =1 g -> (f @ F --> x) = (g @ F --> x).
 Proof. by move=> /funext->. Qed.
 
-Lemma eq_is_cvg_in (T T' : Type) (fT : pfilteredType T') (F : set_system T) (f g : T -> T') :
+Lemma near_eq_is_cvg (T : Type) (U : pnbhsType) (F : set_system T)
+  (f g : T -> U) :
+  Filter F -> {near F, f =1 g} -> cvg (f x @[x --> F]) -> cvg(g x @[x --> F]).
+Proof. by move=> FF /near_eq_cvg_eq ->. Qed.
+
+Lemma eq_is_cvg_in (T U : Type) (fT : pfilteredType U) (F : set_system T)
+    (f g : T -> U) :
   f =1 g -> [cvg (f @ F) in fT] = [cvg (g @ F) in fT].
-Proof. by move=> /funext->. Qed.
+Proof. by move=> /funext ->. Qed.
 
-Lemma eq_is_cvg (T : Type) (T' : pnbhsType) (F : set_system T) (f g : T -> T') :
+Lemma eq_is_cvg (T : Type) (U : pnbhsType) (F : set_system T) (f g : T -> U) :
   f =1 g -> cvg (f @ F) = cvg (g @ F).
 Proof. by move=> /funext->. Qed.
 
+Lemma near_eq_lim (T : Type) (U : pnbhsType) {F : set_system T} {FF : Filter F}
+    (f g : T -> U) :
+  {near F, f =1 g} -> lim (f @ F) = lim (g @ F).
+Proof. by move=> /near_eq_cvg_eq ->. Qed.
+
 Lemma neari_eq_loc {T U} {F : set_system T} {FF : Filter F} (f g : T -> set U) :
   {near F, f =2 g} -> g `@ F `=>` f `@ F.
 Proof.
@@ -1197,11 +1215,23 @@ Qed.
 
 End within.
 
+Lemma cvg_to_withinP (T U : Type) {F : set_system T} {FF : Filter F}
+    {G : set_system U} {FG : Filter G} (f : T -> U) (A : set U) :
+  (f @ F --> within A G) <-> (f @ F --> G /\ \forall x \near F, A (f x)).
+Proof.
+split.
+- move=> fFAG; split.
+  + exact/(cvg_trans fFAG)/cvg_within.
+  + by apply/fFAG; exact: withinT.
+- move=> [+ fA] B => /[apply]; rewrite 2!nbhs_nearE !near_map.
+  by apply: filterS2 fA => t ?; exact.
+Unshelve. all: by end_near. Qed.
+
 Global Instance within_filter T D F : Filter F -> Filter (@within T D F).
 Proof.
 move=> FF; rewrite /within; constructor => /=.
-- by apply: filterE.
-- by move=> P Q/=; apply: filterS2 => x DP DQ Dx; split; [apply: DP|apply: DQ].
+- exact: filterE.
+- by move=> P Q/=; apply: filterS2 => x DP DQ Dx; split; [exact: DP|exact: DQ].
 - by move=> P Q subPQ; apply: filterS => x DP /DP /subPQ.
 Qed.
 
@@ -1210,8 +1240,18 @@ Qed.
 Canonical within_filter_on T D (F : filter_on T) :=
   FilterType (within D F) (within_filter _ _).
 
+Lemma within_cvg_to_within {T U : Type} {F : set_system T} {FF : Filter F}
+    {G : set_system U} {FG : Filter G} (f : T -> U) (A : set T) (B : set U) :
+  (\forall x \near F, A x -> B (f x)) -> f @ F --> G ->
+  f @ within A F --> within B G.
+Proof.
+move=> near_hom fFG; apply/cvg_to_withinP; split.
+- by apply: cvg_trans fFG; apply: cvg_app; exact: cvg_within.
+- by rewrite near_withinE.
+Qed.
+
 Lemma filter_bigI_within T (I : choiceType) (D : {fset I}) (f : I -> set T)
-  (F : set_system T) (P : set T) :
+    (F : set_system T) (P : set T) :
   Filter F -> (forall i, i \in D -> F [set j | P j -> f i j]) ->
   F ([set j | P j -> (\bigcap_(i in [set` D]) f i) j]).
 Proof. move=> FF FfD; exact: (@filter_bigI T I D f _ (within_filter P FF)). Qed.