fix #1972 (#2095)

Co-authored-by: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -84,6 +84,12 @@
 - in `Rstruct_topology.v`:
   + lemma `RealsE` to include `RcosE`, `Rtrigo_PIE`, `RsinE`
 
+- in `metric_structure.v`:
+  + order of arguments and implicit arguments of `squeeze_cvgr`
+
+- in `normed_module.v`:
+  + implicit arguments of `squeeze_cvge` and `sequeeze_fin`
+
 ### Renamed
 
 - in `esum.v`:

theories/gauss_integral.v

@@ -305,9 +305,8 @@ Qed.
 
 Let cvg_integral01_u : integral01_u x @[x --> +oo] --> 0.
 Proof.
-apply: (@squeeze_cvgr _ _ _ _ (cst 0) gauss_fun) => //.
-- by near=> n => /=; rewrite integral01_u_gauss_fun integral01_u_ge0.
-- exact: cvg_gauss_fun.
+apply: (squeeze_cvgr (cst 0) _ _ _ _ _ cvg_gauss_fun) => //.
+by near=> n => /=; rewrite integral01_u_gauss_fun integral01_u_ge0.
 Unshelve. all: end_near. Qed.
 
 Lemma cvg_integral0_gauss_sqr :

theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v

@@ -1129,7 +1129,7 @@ apply: (sube_cvg0 _ _).1 => //.
 move: Ax; rewrite /lebesgue_pt /davg /= -/mu => Ax.
 have : (mu (ball x r))^-1 *
        `|\int[mu]_(y in ball x r) (\1_A y - \1_A x)%:E | @[r --> 0^'+] --> 0.
-  apply: (@squeeze_cvge _ _ _ R (cst 0) _ _ _ _ _ Ax) => //.
+  apply: (squeeze_cvge (cst 0) _ _ _ _ _ Ax) => //.
   near=> a; rewrite mule_ge0 ?inve_ge0///= lee_pmul2l//.
     by rewrite lebesgue_measure_ball// fin_numV// eqe mulrn_eq0/= gt_eqF.
     rewrite lebesgue_measure_ball// inver mulrn_eq0/= gt_eqF// lte_fin.
@@ -1241,7 +1241,7 @@ have E_r_ n : E x n `<=` ball x (r_ x n)%:num.
   by rewrite /r_ /sval/=; case: cid => -[? ?] [].
 have muEr_ n : mu (ball x (r_ x n)%:num) <= C%:E * mu (E x n).
   by rewrite /C /r_ /sval/=; case: cid => -[? ?] [].
-apply: (@squeeze_cvge _ _ _ _ (cst 0) _
+apply: (squeeze_cvge (cst 0) _
     (fun n => C%:E * davg f x (r_ x n)%:num)) => //; last first.
   move/cvge_at_rightP: fx => /(_ (fun r => (r_ x r)%:num)) fx.
   by rewrite -(mule0 C%:E); apply: cvgeM => //; apply: fx; split => //;

theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v

@@ -156,7 +156,7 @@ suff: `| \int[mu]_(x in D) f_ n x - \int[mu]_(x in D) f x | @[n \oo] --> 0.
    rewrite fin_numElt (_ : -oo = - +oo)// -lte_absl.
    move: dominated_integrable => /integrableP[?]; apply: le_lt_trans.
    by apply: (le_trans _ (@le_abse_integral _ _ _ mu D f mD _)).
-apply: (@squeeze_cvge _ _ _ _ (cst 0) _ (fun n => \int[mu]_(x in D) g_ n x)) => //.
+apply: (squeeze_cvge (cst 0) _ (fun n => \int[mu]_(x in D) g_ n x)) => //.
 - by apply: nearW => n; rewrite abse_ge0//=; exact: h.
 - exact: dominated_cvg0.
 Qed.

theories/lebesgue_integral_theory/lebesgue_integral_under.v

@@ -269,7 +269,7 @@ rewrite [X in X @ _ --> _](_ : _ =
 apply: norm_cvg0.
 have {}g_d1f_0 : (\int[mu]_(y in B) `|g_ n y - ('d1 f) a y|) @[n --> \oo] --> 0.
   exact/fine_cvg.
-apply: (@squeeze_cvgr _ _ _ _ (cst 0) _ _ _ _ _ g_d1f_0) => //.
+apply: (squeeze_cvgr (cst 0) _ _ _ _ _ g_d1f_0) => //.
 apply/nearW => n.
 rewrite /= normr_ge0/= le_normr_Rintegral//.
 rewrite /comp; under eq_fun do rewrite EFinB.

theories/measure_theory/signed_measure.v

@@ -738,7 +738,7 @@ have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0.
   move: cvg_nuA; rewrite -(@fineK _ (nu Aoo)) ?fin_num_measure//.
   by move=> /fine_cvgP[_ ?]; apply/cvg_ex; exists (fine (nu Aoo)).
 have mine_cvg_0 : (mine (g_ (v n) * 2^-1%:E) 1) @[n --> \oo] --> 0.
-  apply: (@squeeze_cvge _ _ _ _ _ _ (fun n => nu (A_ (v n)))) => //.
+  apply: (squeeze_cvge _ _ (fun n => nu (A_ (v n)))) => //.
   by apply: nearW => n /=; rewrite nuA_g_ andbT le_min lee01 andbT mule_ge0.
 have g_cvg_0 : (g_ \o v) n @[n --> \oo] --> 0 by apply: mine2_cvg_0_cvg_0 => /=.
 have nuDAoo : nu D >= nu (D `\` Aoo).

theories/normedtype_theory/normed_module.v

@@ -1416,7 +1416,7 @@ by rewrite (lt_le_trans oof) ?(le_lt_trans gh).
 Qed.
 
 Lemma squeeze_cvge f g h : (\near a, f a <= g a <= h a) ->
-  forall (l : \bar R), f @ a --> l -> h @ a --> l -> g @ a --> l.
+  forall l : \bar R, f @ a --> l -> h @ a --> l -> g @ a --> l.
 Proof.
 move=> fgh [l||]; last 2 first.
 - by move=> + _; apply: gee_cvgy; apply: filterS fgh => ? /andP[].
@@ -1428,6 +1428,8 @@ by have /(_ _)/andP[//|fg gh] := near fgh x; rewrite !fine_le//=; near: x.
 Unshelve. all: end_near. Qed.
 
 End FilterERealType.
+Arguments squeeze_fin {T a Fa R} f g h.
+Arguments squeeze_cvge {T a Fa R} f g h.
 
 Section TopoProperFilterERealType.
 Context {T : topologicalType} {a : set_system T} {Fa : ProperFilter a}.

theories/sequences.v

@@ -890,7 +890,7 @@ Lemma cvg_expr (R : archiRealFieldType) (z : R) :
   `|z| < 1 -> (GRing.exp z : R ^nat) @ \oo --> 0.
 Proof.
 move=> Nz_lt1; apply/norm_cvg0P; pose t := 1 - `|z|.
-apply: (@squeeze_cvgr _ _ _ _ (cst 0) (t^-1 *: @harmonic R)) => //; last first.
+apply: (squeeze_cvgr (cst 0) _ (t^-1 *: @harmonic R)) => //; last first.
   by rewrite -(scaler0 _ t^-1); exact: (cvgZl_tmp cvg_harmonic).
 near=> n; rewrite normr_ge0 normrX/= ler_pdivlMl ?subr_gt0//.
 rewrite -(@ler_pM2l _ n.+1%:R)// mulfV// [t * _]mulrC mulr_natl.
@@ -2535,7 +2535,7 @@ Proof.
 move=> supul ul; have usupu n : l <= u n <= esups u n.
   by rewrite ul /=; apply/ereal_sup_ubound; exists n => /=.
 suff : esups u @ \oo --> l.
-  by apply: (@squeeze_cvge _ _ _ _ (cst l)) => //; exact: nearW.
+  by apply: (squeeze_cvge (cst l)) => //; exact: nearW.
 apply/cvg_closeP; split; first exact: is_cvg_esups.
 rewrite closeE//; apply/eqP.
 rewrite eq_le -[X in X <= _ <= _]limn_esup_lim supul/=.

theories/topology_theory/metric_structure.v

@@ -400,8 +400,8 @@ Proof.
 by move=> /cvgr_gt + ? z0 => /(_ _ z0); apply: filterS => ?; apply/ltW.
 Qed.
 
-Lemma squeeze_cvgr f h g : (\near F, f F <= g F <= h F) ->
-  forall (l : R), f @ F --> l -> h @ F --> l -> g @ F --> l.
+Lemma squeeze_cvgr f g h : (\near F, f F <= g F <= h F) ->
+  forall l : R, f @ F --> l -> h @ F --> l -> g @ F --> l.
 Proof.
 move=> fgh l lfa lga.
 apply/(@metricType_numDomainType.cvgrPdist_lt R R^o) => e e_gt0.
@@ -416,3 +416,4 @@ Arguments cvgr_lt {T F FF R f}.
 Arguments cvgr_gt {T F FF R f}.
 Arguments cvgr_le {T F FF R f}.
 Arguments cvgr_ge {T F FF R f}.
+Arguments squeeze_cvgr {T F FF R} f g h.