Merge pull request #1862 from pi8027/num_bound

pi8027 · web-flow · commit ba93a117b7e5 · 2026-02-27T23:02:31.000+01:00
Use `Num.bound`
diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
@@ -26,6 +26,8 @@
 
 - in `unstable.v`:
   + lemmas `oppr_itvNy`, `oppr_itvy`
+  + lemmas `ltr_norm_bound`, `real_ltr_bound`, `real_ltrNbound`, `ltr_bound`,
+    `ltrNbound`
 
 - in `set_interval.v`:
   + lemmas `opp_preimage_itvbndy`, `opp_preimage_itvbndbnd`
diff --git a/classical/unstable.v b/classical/unstable.v
@@ -574,3 +574,20 @@ End ProperNotations.
 
 Lemma sqrtK {K : rcfType} : {in Num.nneg, cancel (@Num.sqrt K) (fun x => x ^+ 2)}.
 Proof. by move=> r r0; rewrite sqr_sqrtr. Qed.
+
+Lemma ltr_norm_bound {R : archiNumDomainType} (x : R) : `|x| < (Num.bound x)%:R.
+Proof. by rewrite /Num.bound -[in ltRHS]normr_id archi_boundP. Qed.
+
+Lemma real_ltr_bound {R : archiNumDomainType} (x : R) :
+  x \is Num.real -> x < (Num.bound x)%:R.
+Proof. by move=> /real_ler_norm /le_lt_trans -> //; apply: ltr_norm_bound. Qed.
+
+Lemma real_ltrNbound {R : archiNumDomainType} (x : R) :
+  x \is Num.real -> - x < (Num.bound x)%:R.
+Proof. by rewrite /Num.bound -realN -normrN; exact: real_ltr_bound. Qed.
+
+Lemma ltr_bound {R : archiRealDomainType} (x : R) : x < (Num.bound x)%:R.
+Proof. exact: real_ltr_bound. Qed.
+
+Lemma ltrNbound {R : archiRealDomainType} (x : R) : - x < (Num.bound x)%:R.
+Proof. exact: real_ltrNbound. Qed.
diff --git a/experimental_reals/realsum.v b/experimental_reals/realsum.v
@@ -4,6 +4,8 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 (* -------------------------------------------------------------------- *)
 From mathcomp Require Import all_ssreflect_compat all_algebra.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp.classical Require Import boolp.
 From mathcomp Require Import xfinmap constructive_ereal reals discrete realseq.
 From mathcomp.classical Require Import classical_sets functions.
@@ -137,24 +139,22 @@ Variable (T : choiceType) (R : realType) (f : T -> R).
 
 Lemma summable_countn0 : summable f -> countable [pred x | f x != 0].
 Proof.
-case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > 1 / p.+1%:~R].
+case/summableP=> M ge0_M bM; pose E (p : nat) := [pred x | `|f x| > p.+1%:~R^-1].
 set F := [pred x | _]; have le: {subset F <= [pred x | `[< exists p, x \in E p >]]}.
   move=> x; rewrite !inE => nz_fx; exists (Num.truncn `|f x|^-1).
-  rewrite inE mul1r invf_plt ?unfold_in /= ?normr_gt0 //.
-  by have/truncn_itv/andP[]: 0 <= `|f x|^-1 by rewrite invr_ge0 normr_ge0.
+  by rewrite inE invf_plt ?unfold_in/= ?normr_gt0 // -normfV ltr_norm_bound.
 apply/(countable_sub le)/cunion_countable=> i /=.
 case: (existsTP (fun s : seq T => {subset E i <= s}))=> /= [[s le_Eis]|].
   by apply/finite_countable/finiteP; exists s => x /le_Eis.
 move=> /finiteNP/(_ ((Num.truncn M).+1 * i.+1)%N)/asboolP/exists_asboolP h.
 have/asboolP[] := xchooseP h.
 set s := xchoose h=> eq_si uq_s le_sEi; pose J := [fset x in s].
 suff: \sum_(x : J) `|f (val x)| > M by rewrite ltNge bM.
-apply/(@lt_le_trans _ _ (\sum_(x : J) 1 / i.+1%:~R)); last first.
+apply/(@lt_le_trans _ _ (\sum_(x : J) i.+1%:~R^-1)); last first.
   apply/ler_sum=> /= m _; apply/ltW.
   by have:= fsvalP m; rewrite in_fset => /le_sEi.
-rewrite mul1r sumr_const -cardfE card_fseq undup_id // eq_si.
-rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0//.
-by case/truncn_itv/andP: ge0_M.
+rewrite sumr_const -cardfE card_fseq undup_id // eq_si.
+by rewrite -mulr_natr natrM mulrC mulfK ?pnatr_eq0// truncnS_gt.
 Qed.
 
 End SummableCountable.
diff --git a/reals/real_interval.v b/reals/real_interval.v
@@ -1,6 +1,8 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval.
 From mathcomp Require Import archimedean.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Export set_interval.
 From mathcomp Require Import reals interval_inference constructive_ereal.
@@ -170,8 +172,8 @@ Lemma itvNybndEbigcup b x : [set` Interval -oo%O (BSide b x)] =
 Proof.
 rewrite predeqE => y; split=> /=; last first.
   by move=> [n _]/=; rewrite in_itv => /andP[ny yx]; rewrite in_itv.
-rewrite in_itv /= => yx; exists (truncn `|y|).+1 => //=; rewrite in_itv/=.
-by rewrite yx /= andbT ltrNl (le_lt_trans (ler_norm _))// normrN truncnS_gt.
+rewrite in_itv /= => yx; exists (Num.bound y) => //=; rewrite in_itv/=.
+by rewrite yx /= andbT ltrNl ltrNbound.
 Qed.
 
 Lemma itvoyEbigcup x :
@@ -354,10 +356,6 @@ Notation itv_infty_bnd_bigcup := itvNy_bnd_bigcup_BLeft (only parsing).
 Lemma bigcup_itvT {R : archiRealDomainType} b1 b2 :
   \bigcup_n [set` Interval (BSide b1 (- n%:R)) (BSide b2 n%:R)] = [set: R].
 Proof.
-rewrite -subTset => x _ /=; exists (truncn `|x|).+1 => //=.
-have := truncnS_gt `|x|; rewrite in_itv/=; move: b1 b2 => [] []/=.
-- by rewrite ltr_norml => /andP[/ltW ->].
-- by move/ltW; rewrite ler_norml => /andP[-> ->].
-- by rewrite ltr_norml => /andP[-> ->].
-- by rewrite ltr_norml => /andP[-> /ltW].
+rewrite -subTset => x _ /=; exists (Num.bound x) => //=.
+by rewrite in_itv lteifNl 2?lteifS// (ltr_bound, ltrNbound).
 Qed.
diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
@@ -880,8 +880,7 @@ move=> Ef; have {Ef} : mu.-negligible (E `&` [set x | 0 < f^* x]).
   near \oo => m; exists m => //=.
   rewrite -(@fineK _ (f^* x)) ?gt0_fin_numE ?ltey// lte_fin.
   rewrite invf_plt ?posrE//; last by rewrite fine_gt0// ltey fx0.
-  set r := _^-1%R; rewrite (lt_le_trans (truncnS_gt _))//.
-  by rewrite ler_nat ltnS; near: m; exact: nbhs_infty_ge.
+  by rewrite -truncn_le_nat; near: m; exact: nbhs_infty_ge.
 apply: negligibleS => z /= /not_implyP[Ez H]; split => //.
 rewrite ltNge; apply: contra_notN H.
 rewrite le_eqVlt ltNge limf_esup_ge0/= ?orbF//; last first.
diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v
@@ -2,6 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval.
 From mathcomp Require Import archimedean.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets functions fsbigop cardinality.
 From mathcomp Require Import reals ereal interval_inference topology numfun.
 From mathcomp Require Import normedtype sequences esum real_interval measure.
@@ -484,8 +486,7 @@ Lemma wlength_sigma_finite (f : R -> R) :
 Proof.
 exists (fun k => `](- k%:R), k%:R]%classic).
   apply/esym; rewrite -subTset => /= x _ /=.
-  exists (truncn `|x|).+1; rewrite //= in_itv/=.
-  by have := truncnS_gt `|x|; rewrite ltr_norml => /andP[-> /ltW->].
+  by exists (Num.bound x); rewrite //= in_itv/= ltrNl ltrNbound ltW// ltr_bound.
 move=> k; split => //; rewrite wlength_itv /= -EFinB.
 by case: ifP; rewrite ltey.
 Qed.
diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v
@@ -2,6 +2,8 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval.
 From mathcomp Require Import archimedean rat.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import boolp classical_sets.
 From mathcomp Require Import functions cardinality fsbigop reals ereal.
 From mathcomp Require Import interval_inference topology numfun tvs normedtype.
@@ -324,11 +326,9 @@ rewrite [X in measurable X](_ : _ =
   apply: bigcupT_measurable => k; rewrite -(setIid D) setIACA.
   exact/measurableI/emeasurable_fun_infty_c/emeasurable_fun_c_infty.
 rewrite predeqE => t; split => [/= [Dt ft]|].
-  exists (truncn `|fine (f t)|).+1 => //=; split=> //; split.
-    rewrite -[leRHS](fineK ft) lee_fin lerNl.
-    by rewrite (le_trans (ler_norm _))// normrN ltW// truncnS_gt.
-  rewrite -[leLHS](fineK ft) lee_fin (le_trans (ler_norm _))//.
-  by rewrite ltW// truncnS_gt.
+  exists (Num.bound (fine (f t))) => //=.
+  rewrite -(fineK ft) !lee_fin (fineK ft) lerNl.
+  by rewrite !ltW// (ltrNbound, ltr_bound).
 move=> [n _] [/= Dt [nft fnt]]; split => //; rewrite fin_numElt.
 by rewrite (lt_le_trans _ nft) ?ltNyr//= (le_lt_trans fnt)// ltry.
 Qed.
@@ -567,21 +567,15 @@ Lemma eset1Ny :
   [set -oo] = \bigcap_k `]-oo, (-k%:R%:E)[%classic :> set (\bar R).
 Proof.
 rewrite eqEsubset; split=> [_ -> i _ |]; first by rewrite /= in_itv /= ltNyr.
-move=> [r|/(_ O Logic.I)|]//.
-move=> /(_ `|floor r|%N Logic.I); rewrite /= in_itv/= ltNge.
-rewrite lee_fin; have [r0|r0] := leP 0%R r.
-  by rewrite (le_trans _ r0) // lerNl oppr0 ler0n.
-rewrite lerNl -abszN natr_absz gtr0_norm; last by rewrite ltrNr oppr0 floor_lt0.
-by rewrite mulrNz lerNl opprK floor_le_tmp.
+move=> [r|/(_ O Logic.I)|]// /(_ (Num.bound r) Logic.I) /=.
+by rewrite in_itv/= lte_fin ltNge lerNl ltW// ltrNbound.
 Qed.
 
 Lemma eset1y : [set +oo] = \bigcap_k `]k%:R%:E, +oo[%classic :> set (\bar R).
 Proof.
 rewrite eqEsubset; split=> [_ -> i _/=|]; first by rewrite in_itv /= ltry.
-move=> [r| |/(_ O Logic.I)] // /(_ `|ceil r|%N Logic.I); rewrite /= in_itv /=.
-rewrite andbT lte_fin ltNge.
-have [r0|r0] := ltP 0%R r; last by rewrite (le_trans r0).
-by rewrite natr_absz gtr0_norm// ?ceil_ge// ceil_gt0.
+move=> [r| |/(_ O Logic.I)] // /(_ (Num.bound r) Logic.I) /=.
+by rewrite in_itv/= andbT lte_fin ltNge ltW// ltr_bound.
 Qed.
 
 End erealwithrays.
diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v
@@ -2014,7 +2014,7 @@ Lemma compact_bounded (K : realType) (V : normedModType K) (A : set V) :
 Proof.
 rewrite compact_cover => Aco.
 have covA : A `<=` \bigcup_(n : int) [set p | `|p| < n%:~R].
-  by move=> p _; exists (floor `|p| + 1) => //=; rewrite floorD1_gt.
+  by move=> p _; exists (truncn `|p|).+1; rewrite //= truncnS_gt.
 have /Aco [] := covA.
   move=> n _; rewrite openE => p; rewrite /= -subr_gt0 => ltpn.
   apply/nbhs_ballP; exists (n%:~R - `|p|) => // q.
diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v
@@ -714,28 +714,22 @@ Notation near_in_itv := near_in_itvoo (only parsing).
 Lemma nbhs_infty_gtr {R : archiRealFieldType} (r : R) :
   \forall n \near \oo, r < n%:R.
 Proof.
-exists `|ceil r|.+1 => // n/=; rewrite -(ler_nat R); apply: lt_le_trans.
-rewrite -natr1 -[ltLHS]addr0 ler_ltD//.
-by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
+exists (Num.bound r) => // n /=.
+by rewrite truncn_lt_nat//; apply/le_lt_trans/ler_norm.
 Qed.
 
 Lemma near_infty_natSinv_lt (R : archiRealFieldType) (e : {posnum R}) :
   \forall n \near \oo, n.+1%:R^-1 < e%:num.
 Proof.
-near=> n; rewrite -(@ltr_pM2r _ n.+1%:R) // mulVf.
-rewrite -(@ltr_pM2l _ e%:num^-1) // mulr1 mulrA mulVf// mul1r.
-rewrite (lt_trans (archi_boundP _)) // ltr_nat.
-by near: n; exists (Num.bound e%:num^-1).
+near=> n; rewrite invf_plt ?unfold_in//= -truncn_le_nat.
+by near: n; exists (Num.truncn e%:num^-1).
 Unshelve. all: by end_near. Qed.
 
 Lemma near_infty_natSinv_expn_lt (R : archiRealFieldType) (e : {posnum R}) :
   \forall n \near \oo, 1 / 2 ^+ n < e%:num.
 Proof.
 near=> n.
-rewrite -(@ltr_pM2r _ (2 ^+ n))// -?natrX ?ltr0n ?expn_gt0//.
-rewrite mul1r mulVf ?gt_eqF//.
-rewrite -(@ltr_pM2l _ e%:num^-1)// mulr1 mulrA mulVf// mul1r.
-rewrite (lt_trans (archi_boundP _))// natrX upper_nthrootP//.
+rewrite mul1r invf_plt ?unfold_in//=; apply: upper_nthrootP.
 near: n; eexists; last by move=> m; exact.
 by [].
 Unshelve. all: by end_near. Qed.
diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v
@@ -269,7 +269,7 @@ have cdf_n1 : cdf X n%:R @[n --> \oo] --> 1.
   pose F n := X @^-1` `]-oo, n%:R].
   have <- : \bigcup_n F n = setT.
     rewrite -preimage_bigcup -subTset => t _/=.
-    by exists (truncn (X t)).+1 => //=; rewrite in_itv/= ltW// truncnS_gt.
+    by exists (truncn (X t)).+1; rewrite //= in_itv/= ltW// truncnS_gt.
   apply: nondecreasing_cvg_mu => //; first exact: bigcup_measurable.
   move=> n m nm; apply/subsetPset => x/=; rewrite !in_itv/= => /le_trans.
   by apply; rewrite ler_nat.
@@ -290,10 +290,8 @@ have cdf_opp_n0 : (cdf X \o -%R) n%:R @[n --> \oo] --> 0.
   rewrite -(measure0 P).
   pose F n := X @^-1` `]-oo, (- n%:R)%R].
   have <- : \bigcap_n F n = set0.
-    rewrite -subset0 => t.
-    set m := (truncn `|X t|).+1.
-    move=> /(_ m I); rewrite /F/= in_itv/= leNgt => /negP; apply.
-    by rewrite ltrNl /m (le_lt_trans (ler_norm _))// normrN truncnS_gt.
+    rewrite -subset0 => t /(_ (Num.bound (X t)) I).
+    by rewrite /F/= in_itv/= leNgt => /negP; apply; rewrite ltrNl ltrNbound.
   apply: nonincreasing_cvg_mu => //=.
   + by rewrite (le_lt_trans (probability_le1 _ _)) ?ltry.
   + exact: bigcap_measurable.
diff --git a/theories/realfun.v b/theories/realfun.v
@@ -169,7 +169,7 @@ exists (fun n => sval (cid (He (PosNum (invn n))))).
   rewrite /sval/=; case: cid => x [px xpt _].
   rewrite distrC (lt_le_trans xpt)// -(@invrK _ r) lef_pV2 ?posrE ?invr_gt0//.
   near: t; exists (truncn r^-1) => // s /= rs.
-  by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
+  by apply/ltW; rewrite -truncn_le_nat.
 move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
 rewrite /sval/=; case: cid => // x [px xpn].
 by rewrite leNgt distrC => /negP.
@@ -229,7 +229,7 @@ have y_p : y_ n @[n --> \oo] --> p.
   rewrite -ltrBlDl => /lt_le_trans; apply.
   rewrite -(invrK e) lef_pV2// ?posrE ?invr_gt0//.
   near: t; exists (truncn e^-1) => // s /= es.
-  by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
+  by apply/ltW; rewrite -truncn_le_nat.
 have /fine_cvgP[[m _ mfy_] /= _] := h _ (conj py_ y_p).
 near \oo => n.
 have mn : (m <= n)%N by near: n; exists m.
diff --git a/theories/sequences.v b/theories/sequences.v
@@ -1194,8 +1194,7 @@ Qed.
 Lemma is_cvg_series_exp_coeff_pos : cvgn (series (exp x)).
 Proof.
 rewrite /series; near \oo => N; have xN : x < N%:R.
-  near: N; exists (truncn x).+2 => // m/= xm.
-  by rewrite (lt_trans (truncnS_gt _))// ltr_nat.
+  by near: N; exists (truncn x).+1 => // m/= xm; rewrite -truncn_lt_nat// ltW.
 rewrite -(@is_cvg_series_restrict N.+1).
 by apply: (nondecreasing_is_cvgn (incr_S1 N)); eexists; exact: S1_sup.
 Unshelve. all: by end_near. Qed.
@@ -3287,7 +3286,7 @@ have O_infempty : O_inf = set0.
   rewrite -subset0 => x.
   have [M FxM] := BoundedF x; rewrite /O_inf /O /=.
   move=> /(_ (truncn M).+1 Logic.I)[f Ff]; apply/negP; rewrite -leNgt.
-  by rewrite (le_trans (FxM _ Ff))// ltW// truncnS_gt.
+  by apply/ltW; rewrite -truncn_le_nat le_truncn ?FxM.
 have ContraBaire : exists i, not (dense (O i)).
   have dOinf : ~ dense O_inf.
     rewrite /dense O_infempty ; apply /existsNP; exists setT; elim.
diff --git a/theories/topology_theory/metric_structure.v b/theories/topology_theory/metric_structure.v
@@ -306,7 +306,7 @@ exists (fun n => sval (cid (He n.+1%:R^-1%:pos))).
   rewrite metric_sym (lt_le_trans xpt)//.
   rewrite -[leRHS]invrK lef_pV2 ?posrE ?invr_gt0//.
   near: t; exists (truncn r^-1) => // s /= rs.
-  by rewrite (le_trans (ltW (truncnS_gt _)))// ler_nat.
+  by apply/ltW; rewrite -truncn_le_nat.
 move=> /cvgrPdist_lt/(_ e%:num (ltac:(by [])))[] n _ /(_ _ (leqnn _)).
 rewrite /sval/=; case: cid => // x [px xpn].
 by rewrite ltNge metric_sym => /negP.
diff --git a/theories/topology_theory/nat_topology.v b/theories/topology_theory/nat_topology.v
@@ -1,6 +1,8 @@
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect_compat all_algebra all_classical.
+#[warning="-warn-library-file-internal-analysis"]
+From mathcomp Require Import unstable.
 From mathcomp Require Import reals topology_structure uniform_structure.
 From mathcomp Require Import pseudometric_structure order_topology.
 From mathcomp Require Import discrete_topology.
@@ -50,8 +52,8 @@ Proof. by exists N. Qed.
 Lemma nbhs_infty_ger {R : realType} (r : R) :
   \forall n \near \oo, (r <= n%:R)%R.
 Proof.
-exists `|Num.ceil r|%N => // n /=; rewrite -(ler_nat R); apply: le_trans.
-by rewrite (le_trans (ceil_ge _))// natr_absz ler_int ler_norm.
+exists (Num.bound r) => // n /=; rewrite -(ler_nat R).
+by apply/le_trans/ltW/ltr_bound.
 Qed.
 
 Lemma cvg_addnl N : addn N @ \oo --> \oo.
