Add generic facts about einfs and limn_einf

CHANGELOG_UNRELEASED.md

@@ -4,10 +4,21 @@
 
 ### Added
 
+- in `sequences.v`:
+  + lemma `sdrop_shift`
+  + lemma `ge_einfs`
+  + lemma `einfs_shift`
+  + lemma `limn_einf_shift_new`
+  + lemma `limn_einf_shiftS`
+  + lemma `limn_einf_cst`
+
 ### Changed
 
 ### Renamed
 
+- in `sequences.v`:
+  + `limn_einf_shift` -> `limn_einf_addl`
+
 ### Generalized
 
 ### Deprecated

theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v

@@ -105,9 +105,9 @@ Proof. by move=> Dx; rewrite gg_. Qed.
 Local Lemma dominated_cvg0 : [sequence \int[mu]_(x in D) g_ n x]_n @ \oo --> 0.
 Proof.
 have := fatou mu mD mgg gg_ge0.
-rewrite [X in X <= _ -> _](_ : _ = \int[mu]_(x in D) (2%:E * g x) ).
+rewrite [X in X <= _ -> _](_ : _ = \int[mu]_(x in D) (2%:E * g x)).
   apply: eq_integral => t; rewrite inE => Dt.
-  rewrite limn_einf_shift//; first by rewrite fin_numM// fing.
+  rewrite limn_einf_addl//; first by rewrite fin_numM// fing.
   rewrite is_cvg_limn_einfE//.
     by apply: is_cvgeN; apply/cvg_ex; eexists; exact: cvg_g_.
   rewrite [X in _ + X](_ : _ = 0) ?adde0//; apply/cvg_lim => //.
@@ -124,7 +124,7 @@ rewrite [X in _ <= X -> _](_ : _ = \int[mu]_(x in D) (2%:E * g x)  + -
   by apply/limn_esup_le_cvg => // n; rewrite integral_ge0// => x _; rewrite /g_.
 rewrite (_ : (fun _ => _) = (fun n => \int[mu]_(x in D) (2%:E * g x)  +
     \int[mu]_(x in D) - g_ n x)); last first.
-  rewrite limn_einf_shift // -limn_einfN; congr (_ + limn_einf _).
+  rewrite limn_einf_addl// -limn_einfN; congr (_ + limn_einf _).
   by rewrite funeqE => n /=; rewrite -integral_ge0N// => x Dx; rewrite /g_.
 rewrite funeqE => n; rewrite integralB//; last 1 first.
 - by rewrite -integral_ge0N// => x Dx//; rewrite /g_.

theories/sequences.v

@@ -2090,9 +2090,18 @@ End mine_cvg_0.
 Definition sdrop T (u : T^nat) n := [set u k | k in [set k | k >= n]]%N.
 
 Section sdrop.
-Variables (d : Order.disp_t) (R : porderType d).
+Context {d} {R : porderType d}.
 Implicit Types (u : R^o^nat).
 
+Lemma sdrop_shift u N n : sdrop (fun i => u (i + N)%N) n = sdrop u (n + N).
+Proof.
+apply/seteqP; split => _ /= [i /= ni] <-.
+- by exists (i + N)%N => //=; rewrite leq_add2r.
+- have Ni : (N <= i)%N by rewrite (leq_trans _ ni)// leq_addl.
+  exists (i - N)%N => /=; last by rewrite subnK.
+  by rewrite -(leq_add2r N) (leq_trans ni)// subnK.
+Qed.
+
 Lemma has_lbound_sdrop u : has_lbound (range u) ->
   forall m, has_lbound (sdrop u m).
 Proof.
@@ -2419,6 +2428,12 @@ by rewrite [in RHS](_ : u = -%E \o -%E \o u);
   rewrite ?esupsN funeqE => n /=; rewrite oppeK.
 Qed.
 
+Lemma ge_einfs u n m : (m <= n)%N -> einfs u m <= u n.
+Proof. by move=> mn; apply: ereal_inf_lbound; exists n; first exact: mn. Qed.
+
+Lemma einfs_shift u N n : einfs (fun k => u (k + N)%N) n = einfs u (n + N)%N.
+Proof. by congr ereal_inf; exact: sdrop_shift. Qed.
+
 Lemma nonincreasing_esups u : nonincreasing_seq (esups u).
 Proof.
 move=> m n mn; apply: ereal_sup_le => _ /= [k nk <-]; exists k => //=.
@@ -2511,7 +2526,7 @@ Local Open Scope ereal_scope.
 Context {R : realType}.
 Implicit Types (u v : (\bar R)^nat) (l : \bar R).
 
-Lemma limn_einf_shift u l : l \is a fin_num ->
+Lemma limn_einf_addl u l : l \is a fin_num ->
   limn_einf (fun x => l + u x) = l + limn_einf u.
 Proof.
 move=> lfin; rewrite !limn_einf_lim; apply/cvg_lim => //.
@@ -2642,7 +2657,25 @@ move=> /cvg_ex[l ul]; have [_ ->] := cvg_limn_einf_sup ul.
 by move/cvg_lim : ul => ->.
 Qed.
 
+#[deprecated(since="mathcomp-analysis 1.19.0", note="to be renamed `limn_einf_shift`")]
+Lemma limn_einf_shift_new u N :
+  limn_einf (fun n => u (n + N)%N) = limn_einf u.
+Proof.
+rewrite !limn_einf_lim.
+rewrite [X in limn X = _](_ : _ = (fun n => einfs u (n + N)%N)).
+  by apply/funext => n; exact: einfs_shift.
+by apply/cvg_lim => //; rewrite (cvg_shiftn N (einfs u)); exact: is_cvg_einfs.
+Qed.
+
+Lemma limn_einf_shiftS u : limn_einf (fun n => u n.+1) = limn_einf u.
+Proof. by under eq_fun do rewrite -addn1; exact: limn_einf_shift_new. Qed.
+
+Lemma limn_einf_cst (c : \bar R) : limn_einf (cst c) = c.
+Proof. by rewrite is_cvg_limn_einfE ?lim_cst//; exact: is_cvg_cst. Qed.
+
 End lim_esup_inf.
+#[deprecated(since="mathcomp-analysis 1.19.0", note="renamed to `limn_einf_addl`")]
+Notation limn_einf_shift := limn_einf_addl (only parsing).
 
 Lemma geometric_le_lim {R : realType} (n : nat) (a x : R) :
   0 <= a -> 0 < x -> `|x| < 1 -> series (geometric a x) n <= a * (1 - x)^-1.