change inequality in ereal_{d,}nbhs

- from strict to large
- also in {p,n}infty_{d,}nbhs

closed #122

CHANGELOG_UNRELEASED.md

@@ -31,6 +31,14 @@
   + lemmas `cvgr_expR`, `cvgn_expR`
 
 ### Changed
+
+
+- in `ereal.v`:
+  + definitions `ereal_dnbhs` and `ereal_nbhs` changed to use large inequality instead
+    of strict inequality
+- in `normedtype.v`:
+  + definitions `pinfty_dnbhs` and `ninfty_nbhs` changed to use large inequality instead
+    of strict inequality
 
 - The file `topology.v` has been split into several files in the directory 
   `topology_theory`. Unless stated otherwise, definitions, lemmas, etc. 

theories/derive.v

@@ -1409,8 +1409,8 @@ have imf_sup : has_sup imf.
   split; first by exists (f a); apply/imageP; rewrite /= in_itv /= lexx.
   have [M [Mreal imfltM]] : bounded_set (f @` `[a, b]).
     by apply/compact_bounded/continuous_compact => //; exact: segment_compact.
-  exists (M + 1) => y /imfltM yleM.
-  by rewrite (le_trans _ (yleM _ _)) ?ler_norm ?ltrDl.
+  exists (M + 1); apply/ubP => y /imfltM/= yleM.
+  by rewrite (le_trans _ (yleM _ _)) ?lerDl ?ler_norm.
 have [|imf_ltsup] := pselect (exists2 c, c \in `[a, b]%R & f c = sup imf).
   move=> [c cab fceqsup]; exists c => // t tab; rewrite fceqsup.
   by apply/sup_upper_bound => //; exact/imageP.

theories/exp.v

@@ -69,7 +69,7 @@ apply: series_le_cvg Kzxn _ _ => [//=| /= n|].
     rewrite !normrM normr_id mulrAC mulfK // normr_eq0 expf_eq0 andbC.
     by case: ltrgt0P zLx; rewrite //= normr_lt0.
   do! (apply: ler_pM || apply: mulr_ge0 || rewrite invr_ge0) => //.
-  by apply Kf => //; rewrite (lt_le_trans _ (ler_norm _))// ltrDl.
+  by apply Kf => //; rewrite (le_trans _ (ler_norm _))// lerDl.
 have F : `|z / x| < 1.
   by rewrite normrM normfV ltr_pdivrMr ?mul1r // (le_lt_trans _ zLx).
 rewrite (_ : (fun _ => _) = geometric `|K + 1| `|z / x|); last first.

theories/landau.v

@@ -481,8 +481,8 @@ split=> [[k k0 fOg] | [k [kreal fOg]]].
   exists k; rewrite realE (ltW k0) /=; split=> // l ltkl; move: fOg.
   by apply: filter_app; near=> x => /le_trans; apply; rewrite ler_wpM2r // ltW.
 exists (Num.max 1 `|k + 1|) => //.
-apply: fOg; rewrite (@lt_le_trans _ _ `|k + 1|) //.
-  by rewrite (@lt_le_trans _ _ (k + 1)) ?ltrDl // real_ler_norm ?realD.
+apply: fOg; rewrite (@le_trans _ _ `|k + 1|) //.
+  by rewrite (@le_trans _ _ (k + 1)) ?lerDl// real_ler_norm ?realD.
 by rewrite comparable_le_max ?real_comparable// lexx orbT.
 Unshelve. end_near. Qed.
 
@@ -680,9 +680,11 @@ Notation "[o_ x e 'of' f ]" := (mklittleo gen_tag x f e).
 (*Printing*)
 Notation "[o '_' x e 'of' f ]" := (the_littleo _ _ (PhantomF x) f e).
 
-Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) :
-  [o_F e of f] =O_F e.
-Proof. by apply/eqOP; exists 0; split => // k kgt0; apply: littleoP. Qed.
+Lemma eqoO (F : filter_on T) (f : T -> V) (e : T -> W) : [o_F e of f] =O_F e.
+Proof.
+apply/eqOP; exists 1; split => // k kge1; apply: littleoP.
+by rewrite (lt_le_trans _ kge1).
+Qed.
 Hint Resolve eqoO : core.
 
 (* NB: duplicate from Section Domination *)
@@ -1117,10 +1119,10 @@ rewrite -linearB opprD addrC addrNK linearN normrN; near: y.
 suff flip : \forall k \near +oo, forall x, `|f x| <= k * `|x|.
   near +oo => k; near=> y.
   rewrite (le_lt_trans (near flip k _ _)) // -ltr_pdivlMl; last first.
-    by near: k; exists 0.
+    by near: k; exact: nbhs_pinfty_gt.
   near: y; apply/nbhs_normP.
   eexists; last by move=> ?; rewrite /= sub0r normrN; apply.
-  by rewrite /= mulr_gt0 // invr_gt0; near: k; exists 0.
+  by rewrite /= mulr_gt0 // invr_gt0; near: k; exact: nbhs_pinfty_gt.
 have /nbhs_normP [_/posnumP[d]] := Of1.
 rewrite /cst [X in _ * X]normr1 mulr1 => fk; near=> k => y.
 case: (ler0P `|y|) => [|y0].
@@ -1132,7 +1134,7 @@ rewrite -(ler_pM2l [gt0 of k0%:num]) mulr1 mulrA -[_ / _]ger0_norm //.
 rewrite -normm_s.
 rewrite -linearZ fk //= /= distrC subr0 normrZ ger0_norm //.
 rewrite invfM mulrA mulfVK ?lt0r_neq0 // ltr_pdivrMr //.
-by rewrite -ltr_pdivrMl//.
+by rewrite -ltr_pdivrMl.
 Unshelve. all: by end_near. Qed.
 
 End Linear3.
@@ -1338,7 +1340,7 @@ rewrite (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(W1 * W2) x|)) //.
   rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
   rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (W1 x)).
   by rewrite ler_pM ?mulr_ge0 //; near: x.
-by rewrite ler_wpM2r // ltW //.
+by rewrite ler_wpM2r // ltW.
 Unshelve. all: by end_near. Qed.
 
 End big_omega_in_R.
@@ -1500,7 +1502,7 @@ rewrite [`|_|]normrM (@le_trans _ _ ((k2%:num * k1%:num)^-1 * `|(T1 * T2) x|)) /
   rewrite invrM ?unitfE ?gtr_eqF // -mulrA ler_pdivlMl //.
   rewrite ler_pdivlMl // (mulrA k1%:num) mulrCA (@normrM _ (T1 x)) ler_pM //;
   by [rewrite mulr_ge0 //|near: x].
-by rewrite ler_wpM2r // ltW //.
+by rewrite ler_wpM2r // ltW.
 Unshelve. all: by end_near. Qed.
 
 End big_theta_in_R.

theories/lebesgue_integral.v

@@ -445,7 +445,7 @@ Lemma simple_bounded (f : {sfun T >-> R}) : bounded_fun f.
 Proof.
 have /finite_seqP[r fr] := fimfunP f.
 exists (fine (\big[maxe/-oo%E]_(i <- r) `|i|%:E)).
-split; rewrite ?num_real// => x mx z _; apply/ltW/(le_lt_trans _ mx).
+split; rewrite ?num_real// => x mx z _; apply/(le_trans _ mx).
 have ? : f z \in r by have := imageT f z; rewrite fr.
 rewrite -[leLHS]/(fine `|f z|%:E) fine_le//.
   have := @bigmaxe_fin_num _ (map normr r) `|f z|.
@@ -3115,7 +3115,7 @@ apply/le_lt_trans/ge0_le_integral => //.
 - apply/emeasurable_funM => //; apply/measurableT_comp => //.
   exact: measurable_int gi.
 - move=> x Dx; rewrite lee_wpmul2r//= lee_fin Mh//=.
-  by rewrite (lt_le_trans _ (ler_norm _))// ltrDl.
+  by rewrite (le_trans _ (ler_norm _))// lerDl.
 Qed.
 
 Lemma integrableMl f (h : T -> R) :
@@ -4969,7 +4969,7 @@ Proof.
 move=> Afin mfA bdA; apply/integrableP; split; first exact/EFin_measurable_fun.
 have [M [_ mrt]] := bdA; apply: le_lt_trans.
   apply: (integral_le_bound (`|M| + 1)%:E) => //; first exact: measurableT_comp.
-  by apply: aeW => z Az; rewrite lee_fin mrt// ltr_pwDr// ler_norm.
+  by apply: aeW => z Az; rewrite lee_fin mrt// ler_wpDr// ler_norm.
 by rewrite lte_mul_pinfty.
 Qed.
 
@@ -5063,7 +5063,7 @@ Lemma compact_finite_measure (A : set R^o) : compact A -> mu A < +oo.
 Proof.
 move=> /[dup]/compact_measurable => mA /compact_bounded[N [_ N1x]].
 have AN1 : (A `<=` `[- (`|N| + 1), `|N| + 1])%R.
-  by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ltr_pwDr// ler_norm.
+  by move=> z Az; rewrite set_itvcc /= -ler_norml N1x// ler_wpDr// ler_norm.
 rewrite (le_lt_trans (le_measure _ _ _ AN1)) ?inE//=.
 by rewrite lebesgue_measure_itv/= lte_fin gtrN// EFinD ltry.
 Qed.
@@ -5121,7 +5121,7 @@ have mg : measurable_fun E g by exact: measurable_funTS.
 have [M Mpos Mbd] : (exists2 M, 0 < M & forall x, `|g x| <= M)%R.
   have [M [_ /= bdM]] := simple_bounded g.
   exists (`|M| + 1)%R; first exact: ltr_pwDr.
-  by move=> x; rewrite bdM// ltr_pwDr// ler_norm.
+  by move=> x; rewrite bdM// ler_wpDr// ler_norm.
 have [] // := @measurable_almost_continuous _ _ mE _ g (eps%:num / 2 / (M *+ 2)).
   by rewrite divr_gt0// mulrn_wgt0.
 move=> A [cptA AE /= muAE ctsAF].
@@ -5135,7 +5135,7 @@ move=> h [gh ctsh hbdM]; have mh : measurable_fun E h.
 have intg : mu.-integrable E (EFin \o h).
   apply: measurable_bounded_integrable => //.
   exists M; split; rewrite ?num_real // => x Mx y _ /=.
-  by rewrite (le_trans _ (ltW Mx)).
+  by rewrite (le_trans _ Mx).
 exists h; split => //; rewrite [eps%:num]splitr; apply: le_lt_trans.
   pose fgh x := `|(f x - g x)%:E| + `|(g x - h x)%:E|.
   apply: (@ge0_le_integral _ _ _ mu _ mE _ fgh) => //.