inf_lb -> inf_lbound

math-comp · Jul 30, 2024 · 960cd3b · 960cd3b
1 parent 9f25a01
commit 960cd3b
Show file tree

Hide file tree

Showing 13 changed files with 173 additions and 149 deletions.
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -132,6 +132,12 @@
   + `lte_le_sub` -> `lte_leB`
   + `lte_le_dsub` -> `lte_le_dB`
 
+- in `reals.v`:
+  + `inf_lb` -> `inf_lbound`
+  + `sup_ub` -> `sup_ubound`
+  + `ereal_inf_lb` -> `ereal_inf_lbound`
+  + `ereal_sup_ub` -> `ereal_sup_ubound`
+
 ### Generalized
 
 - in `constructive_ereal.v`:

diff --git a/theories/charge.v b/theories/charge.v
@@ -630,7 +630,7 @@ Let subDD A := [set nu E | E in [set E | measurable E /\ E `<=` D `\` A] ].
 Let d_ A := ereal_sup (subDD A).
 
 Let d_ge0 X : 0 <= d_ X.
-Proof. by apply: ereal_sup_ub => /=; exists set0; rewrite ?charge0. Qed.
+Proof. by apply: ereal_sup_ubound => /=; exists set0; rewrite ?charge0. Qed.
 
 Let elt_rel i j :=
   [/\ g_ j = d_ (U_ i),  A_ j `<=` D `\` U_ i & U_ j = U_ i `|` A_ j ].
@@ -714,7 +714,7 @@ have EH n : [set nu E] `<=` H n.
   by apply: (subset_trans FDAoo); apply: setDS; exact: bigsetU_bigcup.
 have nudelta n : nu E <= g_ (v n).
   move: n => [|n].
-    rewrite v0/=; apply: ereal_sup_ub => /=; exists E; split => //.
+    rewrite v0/=; apply: ereal_sup_ubound => /=; exists E; split => //.
     by apply: (subset_trans EDAoo); exact: setDS.
   suff : nu E <= d_ (U_ (v n)) by have [<- _] := Pv n.
   have /le_ereal_sup := EH n.+1; rewrite ereal_sup1 => /le_trans; apply.
@@ -763,7 +763,7 @@ Let s_ A := ereal_inf (subC A).
 
 Let s_le0 X : s_ X <= 0.
 Proof.
-by apply: ereal_inf_lb => /=; exists set0; rewrite ?charge0//=; split.
+by apply: ereal_inf_lbound => /=; exists set0; rewrite ?charge0//=; split.
 Qed.
 
 Let elt_rel i j :=
@@ -813,8 +813,9 @@ exists P, N; split; [|exact: neg_set_N|by rewrite /P setvU|by rewrite /P setICl]
 split=> // D mD DP; rewrite leNgt; apply/negP => nuD0.
 have znuD n : z_ (v n) <= nu D.
   move: n => [|n].
-    by rewrite v0 /=; apply: ereal_inf_lb; exists D; split => //; rewrite setC0.
-  have [-> _ _] := Pv n; apply: ereal_inf_lb => /=; exists D; split => //.
+    rewrite v0 /=; apply: ereal_inf_lbound; exists D; split => //.
+    by rewrite setC0.
+  have [-> _ _] := Pv n; apply: ereal_inf_lbound => /=; exists D; split => //.
   apply: (subset_trans DP); apply: subsetC; rewrite Ubig.
   exact: bigsetU_bigcup.
 have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0.
@@ -1277,7 +1278,7 @@ Let M_g_F m : M - m.+1%:R^-1%:E < \int[mu]_x g m x /\
 Proof.
 split; first by have [] := approxRN_seq_prop mu nu m.
 apply/andP; split; last first.
-  by apply: ereal_sup_ub; exists (F m)  => //; have := F_G m; rewrite inE.
+  by apply: ereal_sup_ubound; exists (F m)  => //; have := F_G m; rewrite inE.
 apply: ge0_le_integral => //.
 - by move=> x _; exact: approxRN_seq_ge0.
 - exact: measurable_approxRN_seq.

diff --git a/theories/ereal.v b/theories/ereal.v
@@ -503,7 +503,7 @@ move/sup_upper_bound/ubP; apply.
 by case: y' Sy' => [r1 /= Sr1 | // | /= _]; [exists r1%:E | exists r%:E].
 Qed.
 
-Lemma ereal_sup_ub S : ubound S (ereal_sup S).
+Lemma ereal_sup_ubound S : ubound S (ereal_sup S).
 Proof.
 move=> y Sy; rewrite /ereal_sup /supremum ifF; last first.
   by apply/eqP; rewrite predeqE => /(_ y)[+ _]; exact.
@@ -513,43 +513,47 @@ Qed.
 
 Lemma ereal_supy S : S +oo -> ereal_sup S = +oo.
 Proof.
-by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub.
+by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ubound.
 Qed.
 
 Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
-Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed.
+Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ubound. Qed.
 
 Lemma ereal_sup_ninfty S : ereal_sup S = -oo <-> S `<=` [set -oo].
 Proof.
 split.
-  by move=> supS [r /ereal_sup_ub | /ereal_sup_ub |//]; rewrite supS.
-move=> /(@subset_set1 _ S) [] ->; [exact: ereal_sup0|exact: ereal_sup1].
+  by move=> supS [r /ereal_sup_ubound|/ereal_sup_ubound|//]; rewrite supS.
+by move=> /(@subset_set1 _ S) [] ->; [exact: ereal_sup0|exact: ereal_sup1].
 Qed.
 
-Lemma ereal_inf_lb S : lbound S (ereal_inf S).
+Lemma ereal_inf_lbound S : lbound S (ereal_inf S).
 Proof.
-by move=> x Sx; rewrite /ereal_inf leeNl; apply ereal_sup_ub; exists x.
+by move=> x Sx; rewrite /ereal_inf leeNl; apply: ereal_sup_ubound; exists x.
 Qed.
 
 Lemma ereal_inf_le S x : (exists2 y, S y & y <= x) -> ereal_inf S <= x.
-Proof. by move=> [y Sy]; apply: le_trans; exact: ereal_inf_lb. Qed.
+Proof. by move=> [y Sy]; apply: le_trans; exact: ereal_inf_lbound. Qed.
 
 Lemma ereal_inf_pinfty S : ereal_inf S = +oo <-> S `<=` [set +oo].
 Proof. rewrite eqe_oppLRP oppe_subset image_set1; exact: ereal_sup_ninfty. Qed.
 
 Lemma le_ereal_sup : {homo @ereal_sup R : A B / A `<=` B >-> A <= B}.
-Proof. by move=> A B AB; apply: ub_ereal_sup => x Ax; apply/ereal_sup_ub/AB. Qed.
+Proof.
+by move=> A B AB; apply: ub_ereal_sup => x Ax; exact/ereal_sup_ubound/AB.
+Qed.
 
 Lemma le_ereal_inf : {homo @ereal_inf R : A B / A `<=` B >-> B <= A}.
-Proof. by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lb/AB. Qed.
+Proof.
+by move=> A B AB; apply: lb_ereal_inf => x Bx; exact/ereal_inf_lbound/AB.
+Qed.
 
 Lemma hasNub_ereal_sup (A : set R) : ~ has_ubound A ->
   A !=set0 -> ereal_sup (EFin @` A) = +oo%E.
 Proof.
 move=> + A0; apply: contra_notP => /eqP; rewrite -ltey => Aoo.
 exists (fine (ereal_sup (EFin @` A))) => x Ax.
 rewrite -lee_fin -(@fineK _ x%:E)// lee_fin fine_le//; last first.
-  by apply: ereal_sup_ub => /=; exists x.
+  by apply: ereal_sup_ubound => /=; exists x.
 rewrite fin_numE// -ltey Aoo andbT.
 apply/eqP => /ereal_sup_ninfty/(_ x%:E).
 by have /[swap] /[apply]: (EFin @` A) x%:E by exists x.
@@ -559,7 +563,7 @@ Lemma ereal_sup_EFin (A : set R) :
   has_ubound A -> A !=set0 -> ereal_sup (EFin @` A) = (sup A)%:E.
 Proof.
 move=> has_ubA A0; apply/eqP; rewrite eq_le; apply/andP; split.
-  by apply: ub_ereal_sup => /= y [r Ar <-{y}]; rewrite lee_fin sup_ub.
+  by apply: ub_ereal_sup => /= y [r Ar <-{y}]; rewrite lee_fin sup_ubound.
 set esup := ereal_sup _; have := leey esup.
 rewrite le_eqVlt => /predU1P[->|esupoo]; first by rewrite leey.
 have := leNye esup; rewrite le_eqVlt => /predU1P[/esym|ooesup].
@@ -569,7 +573,7 @@ have esup_fin_num : esup \is a fin_num.
   by rewrite fin_numE -leeNy_eq -ltNge ooesup /= -leye_eq -ltNge esupoo.
 rewrite -(@fineK _ esup) // lee_fin leNgt.
 apply/negP => /(sup_gt A0)[r Ar]; apply/negP; rewrite -leNgt.
-by rewrite -lee_fin fineK//; apply: ereal_sup_ub; exists r.
+by rewrite -lee_fin fineK//; apply: ereal_sup_ubound; exists r.
 Qed.
 
 Lemma ereal_inf_EFin (A : set R) : has_lbound A -> A !=set0 ->
@@ -581,6 +585,10 @@ by rewrite !image_comp.
 Qed.
 
 End ereal_supremum_realType.
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_sup_ubound`.")]
+Notation ereal_sup_ub := ereal_sup_ubound (only parsing).
+#[deprecated(since="mathcomp-analysis 1.3.0", note="Renamed `ereal_inf_lbound`.")]
+Notation ereal_inf_lb := ereal_inf_lbound (only parsing).
 
 Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) :
   (abse \o f) \_ D = abse \o (f \_ D).
@@ -931,16 +939,16 @@ case=> x Sx; rewrite ler_norml; apply/andP; split; last first.
   by move=> r [y Sy] <-; case/ler_normlP : (contract_le1 y).
 rewrite (@le_trans _ _ (contract x)) //.
   by case/ler_normlP : (contract_le1 x); rewrite lerNl.
-apply sup_ub; last by exists x.
+apply: sup_ubound; last by exists x.
 by exists 1%R => r [y Sy <-]; case/ler_normlP : (contract_le1 y).
 Qed.
 
 Lemma contract_sup S : S !=set0 -> contract (ereal_sup S) = sup (contract @` S).
 Proof.
 move=> S0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
-  apply sup_le_ub.
+  apply: sup_le_ub.
     by case: S0 => x Sx; exists (contract x), x.
-  move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ub.
+  by move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ubound.
 rewrite leNgt; apply/negP.
 set supc := sup _; set csup := contract _; move=> ltsup.
 suff [y [ysupS ?]] : exists y, y < ereal_sup S /\ ubound S y.
@@ -954,7 +962,7 @@ suff [x [? [ubSx x1]]] : exists x, (x < csup)%R /\ ubound (contract @` S) x /\
 exists ((supc + csup) / 2); split; first by rewrite midf_lt.
 split => [r [y Sy <-{r}]|].
   rewrite (@le_trans _ _ supc) ?midf_le //; last by rewrite ltW.
-  apply sup_ub; last by exists y.
+  apply: sup_ubound; last by exists y.
   by exists 1%R => r [z Sz <-]; case/ler_normlP : (contract_le1 z).
 rewrite ler_norml; apply/andP; split; last first.
   rewrite ler_pdivrMr // mul1r (_ : 2 = 1 + 1)%R // lerD //.
@@ -968,7 +976,8 @@ Qed.
 Lemma contract_inf S : S !=set0 -> contract (ereal_inf S) = inf (contract @` S).
 Proof.
 move=> -[x Sx]; rewrite /ereal_inf /contract (contractN (ereal_sup (-%E @` S))).
-by rewrite -/contract contract_sup /inf; [rewrite contract_imageN | exists (- x), x].
+by rewrite -/contract contract_sup /inf;
+  [rewrite contract_imageN|exists (- x), x].
 Qed.
 
 End contract_expand_realType.
@@ -1020,7 +1029,7 @@ Lemma ball_ereal_ball_fin_lt r r' (e : {posnum R}) :
   let e' := (r - fine (expand (contract r%:E - e%:num)))%R in
   ball r e' r' -> (r' < r)%R ->
   (`|contract r%:E - (e)%:num| < 1)%R ->
-  ereal_ball r%:E (e)%:num r'%:E.
+  ereal_ball r%:E e%:num r'%:E.
 Proof.
 move=> e' re'r' rr' X; rewrite /ereal_ball.
 rewrite gtr0_norm ?subr_gt0// ?lt_contract ?lte_fin//.
@@ -1035,7 +1044,7 @@ Lemma ball_ereal_ball_fin_le r r' (e : {posnum R}) :
   let e' : R := (fine (expand (contract r%:E + e%:num)) - r)%R in
   ball r e' r' -> (r <= r')%R ->
   (`| contract r%:E + e%:num | < 1)%R ->
-  (ereal_ball r%:E e%:num r'%:E).
+  ereal_ball r%:E e%:num r'%:E.
 Proof.
 move=> e' r'e'r rr' re1; rewrite /ereal_ball.
 move: rr'; rewrite le_eqVlt => /predU1P[->|rr']; first by rewrite subrr normr0.
@@ -1321,8 +1330,7 @@ rewrite predeq2E => x A; split.
       apply: MA; rewrite lte_fin.
       rewrite ger0_norm in rM1; last first.
         by rewrite subr_ge0 // (le_trans _ (contract_le1 r%:E)) // ler_norm.
-      rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr in rM1.
-      rewrite subr_gt0 in rM1.
+      rewrite ltrBlDr addrC addrCA addrC -ltrBlDr subrr subr_gt0 in rM1.
       by rewrite -lte_fin -lt_contract.
     * by rewrite /ereal_ball /= subrr normr0 => h; exact: MA.
     * rewrite /ereal_ball /= opprK => h {MA}.

diff --git a/theories/esum.v b/theories/esum.v
@@ -79,7 +79,7 @@ Implicit Types (a : T -> \bar R).
 Lemma esum_ge0 (S : set T) a :
   (forall x, S x -> 0 <= a x) -> 0 <= \esum_(i in S) a i.
 Proof.
-move=> a0; apply: ereal_sup_ub.
+move=> a0; apply: ereal_sup_ubound.
 by exists set0; [exact: fsets_set0|rewrite fsbig_set0].
 Qed.
 
@@ -88,7 +88,7 @@ Lemma esum_fset (F : set T) a : finite_set F ->
   \esum_(i in F) a i = \sum_(i \in F) a i.
 Proof.
 move=> finF f0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
-  by apply ereal_sup_ub; exists F => //; exact: fsets_self.
+  by apply: ereal_sup_ubound; exists F => //; exact: fsets_self.
 apply ub_ereal_sup => /= ? -[F' [finF' F'F] <-].
 apply/lee_fsum_nneg_subset => //; first exact/subsetP.
 by  move=> t; rewrite inE/= => /andP[_] /f0.
@@ -101,11 +101,6 @@ Qed.
 
 End esum_realType.
 
-Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x :
-  (exists2 X : set T, fsets I X & x <= \sum_(i \in X) a i) ->
-  x <= \esum_(i in I) a i.
-Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ub => /=; exists X. Qed.
-
 Lemma esum1 [R : realFieldType] [I : choiceType] (D : set I) (a : I -> \bar R) :
   (forall i, D i -> a i = 0) -> \esum_(i in D) a i = 0.
 Proof.
@@ -115,6 +110,11 @@ apply/seteqP; split=> x //= => [[X [finX XI]] <-|->].
 by exists set0; rewrite ?fsbig_set0//; exact: fsets_set0.
 Qed.
 
+Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x :
+  (exists2 X : set T, fsets I X & x <= \sum_(i \in X) a i) ->
+  x <= \esum_(i in I) a i.
+Proof. by move=> [X IX /le_trans->//]; apply: ereal_sup_ubound; exists X. Qed.
+
 Lemma le_esum [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
   (forall i, I i -> a i <= b i) ->
   \esum_(i in I) a i <= \esum_(i in I) b i.
@@ -134,7 +134,7 @@ Lemma esumD [R : realType] [T : choiceType] (I : set T) (a b : T -> \bar R) :
 Proof.
 move=> ag0 bg0; apply/eqP; rewrite eq_le; apply/andP; split.
   rewrite ub_ereal_sup//= => x [X [finX XI]] <-; rewrite fsbig_split//=.
-  by rewrite leeD// ereal_sup_ub//=; exists X.
+  by rewrite leeD// ereal_sup_ubound//=; exists X.
 wlog : a b ag0 bg0 / \esum_(i in I) a i \isn't a fin_num => [saoo|]; last first.
   move=> /fin_numPn[->|/[dup] aoo ->]; first by rewrite leNye.
   rewrite (@le_trans _ _ +oo)//; first by rewrite /adde/=; case: esum.
@@ -156,11 +156,12 @@ have saX : \sum_(i \in X) a i \is a fin_num.
 rewrite leeBrDr// addeC -leeBrDr// ub_ereal_sup//= => _ [Y [finY YI]] <-.
 rewrite leeBrDr// addeC esum_ge//; exists (X `|` Y).
   by split; [rewrite finite_setU|rewrite subUset].
-rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset//= ?finite_setU//.
+rewrite fsbig_split ?finite_setU//= leeD// lee_fsum_nneg_subset ?finite_setU//=.
 - exact/subsetP/subsetUl.
-- by move=> x; rewrite !inE in_setU andb_orr andNb/= => /andP[_] /[!inE] /YI/ag0.
+- by move=> x; rewrite !inE in_setU andb_orr andNb => /andP[_] /[!inE] /YI/ag0.
 - exact/subsetP/subsetUr.
-- by move=> x; rewrite !inE in_setU andb_orr andNb/= orbF => /andP[_] /[!inE] /XI/bg0.
+- move=> x; rewrite !inE in_setU andb_orr andNb/= orbF.
+  by move=> /andP[_] /[!inE] /XI/bg0.
 Qed.
 
 Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T)
@@ -169,20 +170,23 @@ Lemma esum_mkcond [R : realType] [T : choiceType] (I : set T)
 Proof.
 apply/eqP; rewrite eq_le !ub_ereal_sup//= => _ [X [finX XI]] <-.
   rewrite -big_mkcond/= big_fset_condE/=; set Y := [fset _ | _ in _ & _]%fset.
-  rewrite ereal_sup_ub//=; exists [set` Y]; last by rewrite fsbig_finite// set_fsetK.
-  by split => // i/=; rewrite !inE/= => /andP[_]; rewrite inE.
-rewrite ereal_sup_ub//; exists X => //; apply: eq_fsbigr => x; rewrite inE => Xx.
+  rewrite ereal_sup_ubound//=; exists [set` Y].
+    by split => // i/=; rewrite !inE/= => /andP[_]; rewrite inE.
+  by rewrite fsbig_finite// set_fsetK.
+rewrite ereal_sup_ubound//; exists X => //; apply: eq_fsbigr => x /[!inE] Xx.
 by rewrite ifT// inE; exact: XI.
 Qed.
 
-Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T) (a : T -> \bar R) :
+Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T)
+    (a : T -> \bar R) :
   \esum_(i in I `&` J) a i = \esum_(i in I) if i \in J then a i else 0.
 Proof.
 rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
 by rewrite in_setI; case: (i \in I) (i \in J) => [] [].
 Qed.
 
-Lemma esum_mkcondl [R : realType] [T : choiceType] (I J : set T) (a : T -> \bar R) :
+Lemma esum_mkcondl [R : realType] [T : choiceType] (I J : set T)
+    (a : T -> \bar R) :
   \esum_(i in I `&` J) a i = \esum_(i in J) if i \in I then a i else 0.
 Proof.
 rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _.
@@ -208,7 +212,7 @@ Lemma esum_sum [R : realType] [T1 T2 : choiceType]
 Proof.
 move=> a_ge0; elim: r => [|j r IHr]; rewrite ?(big_nil, big_cons)// -?IHr.
   by rewrite esum1// => i; rewrite big_nil.
-case: (boolP (P j)) => Pj; last first.
+case: ifPn => Pj; last first.
   by apply: eq_esum => i Ii; rewrite big_cons (negPf Pj).
 have aj_ge0 i : I i -> a i j >= 0 by move=> ?; apply: a_ge0.
 rewrite -esumD//; last by move=> i Ii; apply: sume_ge0 => *; apply: a_ge0.
@@ -227,7 +231,7 @@ move=> a_ge0; apply/eqP; rewrite eq_le; apply/andP; split.
     move=> i j _ /[!in_fset_set]// /[!inE] /XI Ij.
     by case: ifPn => // /[!inE] /a_ge0-/(_ Ij).
   under eq_esum do rewrite -big_seq -big_mkcond/=.
-  apply: ub_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ub => /=.
+  apply: ub_ereal_sup => /= _ [Y [finY _] <-]; apply: ereal_sup_ubound => /=.
   set XYJ := [set z | z \in X `*` Y /\ z.2 \in J z.1].
   have ? : finite_set XYJ.
     apply: sub_finite_set (finite_setM finX finY) => z/=.
@@ -266,7 +270,7 @@ apply: (@le_trans _ _
   by rewrite mem_set//; move/XIJ : Xij => [].
 rewrite -fsbig_finite; last exact: finite_set_fst.
 apply lee_fsum=> [|i Xi]; first exact: finite_set_fst.
-rewrite ereal_sup_ub => //=; have ? : finite_set (X.`2 `&` J i).
+rewrite ereal_sup_ubound //=; have ? : finite_set (X.`2 `&` J i).
   by apply: finite_setI; left; exact: finite_set_snd.
 exists (X.`2 `&` J i) => //.
 rewrite [in RHS]big_fset_condE/= fsbig_finite//; apply eq_fbigl => j.
@@ -308,10 +312,11 @@ Lemma nneseries_esum (R : realType) (a : nat -> \bar R) (P : pred nat) :
 Proof.
 move=> a0; apply/eqP; rewrite eq_le; apply/andP; split.
   apply: (lime_le (is_cvg_nneseries_cond a0)); apply: nearW => n.
-  apply: ereal_sup_ub => /=; exists [set` [fset val i | i in 'I_n & P i]%fset].
+  apply: ereal_sup_ubound; exists [set` [fset val i | i in 'I_n & P i]%fset].
     split; first exact: finite_fset.
     by move=> /= k /imfsetP[/= i]; rewrite inE => + ->.
-  rewrite fsbig_finite//= set_fsetK big_imfset/=; last by move=> ? ? ? ? /val_inj.
+  rewrite fsbig_finite//= set_fsetK big_imfset/=; last first.
+    by move=> ? ? ? ? /val_inj.
   by rewrite big_filter big_enum_cond/= big_mkord.
 apply: ub_ereal_sup => _ [/= F [finF PF] <-].
 rewrite fsbig_finite//= -(big_rmcond_in P)/=; first exact: lee_sum_fset_lim.
@@ -334,7 +339,7 @@ gen have le_esum : T T' a P Q e /
   rewrite [leRHS](_ : _ = \esum_(j in Q) a (e (e^-1%FUN j))); last first.
     by apply: eq_esum => i Qi; rewrite invK ?inE.
   by rewrite le_esum => //= i Qi; rewrite a_ge0//; exact: funS.
-rewrite ub_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ub => //=.
+rewrite ub_ereal_sup => //= _ [X [finX XQ] <-]; rewrite ereal_sup_ubound => //=.
 exists [set` (e^-1 @` (fset_set X))%fset].
   split=> [|t /= /imfsetP[t'/=]]; first exact: finite_fset.
   by rewrite in_fset_set// inE => /XQ Qt' ->; exact: funS.

diff --git a/theories/kernel.v b/theories/kernel.v
@@ -368,7 +368,7 @@ HB.builders Context d d' (X : measurableType d) (Y : measurableType d')
 Let finite : @Kernel_isFinite d d' X Y R k.
 Proof.
 split; exists 2%R => /= ?; rewrite (@le_lt_trans _ _ 1%:E) ?lte_fin ?ltr1n//.
-by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ub.
+by rewrite (le_trans _ sprob_kernel)//; exact: ereal_sup_ubound.
 Qed.
 
 HB.instance Definition _ := finite.