variants of {sup,inf}_le (#2021)

- le_supP and gt_sup

Co-authored-by: Marie Kerjean <marie.kerjean@cnrs.fr>
Co-authored-by: adjevahi <arthur.djevahirdjian@ens-lyon.fr>

Author: 3 people

CHANGELOG_UNRELEASED.md

@@ -284,6 +284,10 @@
 - in `pseudometric_normed_Zmodule.v`:
   + factory `isPseudoMetricNormedZmodule`
   + structure `PseudoMetricNormedZmod0`
+- in `reals.v`:
+  + lemmas `supS`, `infS`
+  + lemmas `ge0_infZl`, `inf_ge0`, `inf_pos`
+  + lemmas `le_supP`, `gt_sup`
 
 ### Changed
 

reals/reals.v

@@ -47,7 +47,8 @@ From HB Require Import structures.
 From mathcomp Require Import boot order algebra.
 #[warning="-warn-library-file-internal-analysis"]
 From mathcomp Require Import unstable.
-From mathcomp Require Import mathcomp_extra boolp classical_sets set_interval.
+From mathcomp Require Import mathcomp_extra boolp classical_sets contra
+  set_interval.
 
 Declare Scope real_scope.
 
@@ -647,13 +648,35 @@ move=> SBA AB Ai; rewrite lerNl opprK sup_le// ?has_inf_supN//.
 exact/nonemptyN.
 Qed.
 
+Lemma supS A B : A !=set0 -> has_sup B -> A `<=` B -> sup A <= sup B.
+Proof.
+by move=> ? ? AB; apply: sup_le => //; apply: (subset_trans AB (@le_down _)).
+Qed.
+
+Lemma infS A B : has_inf A -> B !=set0 -> B `<=` A -> inf A <= inf B.
+Proof.
+by move=> infA B0 AB; rewrite /inf lerN2 supS//;
+  [exact/nonemptyN|exact/has_inf_supN|exact/image_subset].
+Qed.
+
+Lemma le_supP A x : has_sup A -> sup A <= x <-> ubound A x.
+Proof.
+move=> hsA; split=> [? ? ?|Ax]; first exact: (le_trans (sup_upper_bound hsA _)).
+by apply: ge_sup => //; apply/set0P; contra: (@has_sup0 _ R) => <-.
+Qed.
+
+Lemma gt_sup A x : has_sup A -> sup A < x -> forall y, A y -> y < x.
+Proof.
+by move=> hsA sAx y Ay; apply: le_lt_trans sAx; exact: sup_upper_bound.
+Qed.
+
 Lemma sup_down A : sup (down A) = sup A.
 Proof.
 have [supA|supNA] := pselect (has_sup A); last first.
   by rewrite !sup_out // => /has_sup_down.
 have supDA : has_sup (down A) by apply/has_sup_down.
 apply/eqP; rewrite eq_le !sup_le //.
-- by case: supA => -[x xA] _; exists x; apply/le_down.
+- by case: supA => -[x xA] _; exists x; exact/le_down.
 - by rewrite downK; exact: le_down.
 - by case: supA.
 Qed.
@@ -687,6 +710,12 @@ have [[_ Aub]|supA] := pselect (has_sup A); last by rewrite sup_out.
 by rewrite (le_trans (A0 _ Aa))// ub_le_sup.
 Qed.
 
+Lemma inf_ge0 A : (forall x, A x -> 0 <= x) -> 0 <= inf A.
+Proof.
+move=> BA; have [->|A0] := eqVneq A set0; first by rewrite inf0.
+by apply: lb_le_inf => //; exact/set0P.
+Qed.
+
 Lemma has_sup_wpZl A (a : R) : 0 <= a -> has_sup A ->
   has_sup [set a * x | x in A ].
 Proof.
@@ -701,7 +730,7 @@ move=> a0 [[_ [x Ax _]] [b ub]]; split; first by exists x.
 by exists (b / a) => y Ay; rewrite ler_pdivlMr// mulrC ub//; exists y.
 Qed.
 
-Lemma ge0_supZl A (a : R) : 0 <= a -> sup [set a * x  | x in A ] = a * sup A.
+Lemma ge0_supZl A (a : R) : 0 <= a -> sup [set a * x | x in A ] = a * sup A.
 Proof.
 rewrite le_eqVlt => /predU1P[<-|an0].
   have [->|A0] := eqVneq A set0; first by rewrite image_set0 sup0 mulr0.
@@ -721,6 +750,20 @@ have [x1 ubx1] := ubA.
 by exists (a * x1) => _ [x2 Ax2 <-]; rewrite ler_pM2l// ubx1.
 Qed.
 
+Lemma ge0_infZl A (a : R) : 0 <= a -> inf [set a * x | x in A] = a * inf A.
+Proof.
+move=> a0; rewrite /inf mulrN -(ge0_supZl (-%R @` A) a0); congr (- sup _).
+by rewrite !image_comp/=; apply: eq_imagel => //= ? _; rewrite mulrN.
+Qed.
+
+Lemma inf_pos : inf [set r : R | 0 < r] = 0.
+Proof.
+apply/eqP; rewrite eq_le; apply/andP; split; last first.
+  by apply: inf_ge0 => x /ltW.
+apply/ler_addgt0Pr => e e0; rewrite add0r; apply: ge_inf => //=.
+by exists 0 => r /ltW.
+Qed.
+
 Lemma has_sup_Mn A n : has_sup A -> has_sup [set x *+n | x in A].
 Proof.
 move=> [[x Ax] [y Ay]]; split; first by exists (x *+ n), x.

theories/lebesgue_measure.v

@@ -144,15 +144,14 @@ have [J0|/set0P J0] := eqVneq J set0.
 move=> /subset_itvP ij; apply: leeB => /=.
   have [ui|ui] := asboolP (has_ubound I).
     have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey.
-    by rewrite lee_fin sup_le // => r Ir; exists r; split => //; apply: ij.
+    by rewrite lee_fin supS.
   have [uj /=|//] := asboolP (has_ubound J).
   by move: ui; have := subset_has_ubound ij uj.
 have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye.
 have [li /=|li] := asboolP (has_lbound I); last first.
   by move: li; have := subset_has_lbound ij lj.
-rewrite lee_fin lerNl opprK sup_le// ?has_inf_supN//; last exact/nonemptyN.
-move=> r [r' Ir' <-{r}]; exists (- r')%R.
-by split => //; exists r' => //; apply: ij.
+rewrite lee_fin lerNl opprK supS// ?has_inf_supN//; first exact/nonemptyN.
+by move=> r/= [s Is <-]; exists s => //; exact: ij.
 Qed.
 
 Lemma le_hlength : {homo hlength : A B / (A `<=` B) >-> A <= B}.

theories/lebesgue_stieltjes_measure.v

@@ -686,16 +686,13 @@ have [J0|/set0P J0] := eqVneq J set0.
 move=> /subset_itvP ij; apply: leeB => /=.
   have [ui|ui] := asboolP (has_ubound I).
     have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey.
-    rewrite lee_fin; apply: ndf; apply: sup_le => //.
-    by move=> r Ir; exists r; split => //; apply: ij.
+    by rewrite lee_fin ndf// supS.
   have [uj /=|//] := asboolP (has_ubound J).
   by move: ui; have := subset_has_ubound ij uj.
 have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye.
 have [li /=|li] := asboolP (has_lbound I); last first.
   by move: li; have := subset_has_lbound ij lj.
-rewrite lee_fin; apply/ndf/inf_le => //.
-move=> r [r' Ir' <-{r}]; exists (- r')%R.
-by split => //; exists r' => //; apply: ij.
+by rewrite lee_fin; exact/ndf/infS.
 Qed.
 
 Lemma le_wlength (ndf : {homo f : x y / (x <= y)%R}) :

theories/realfun.v

@@ -2042,14 +2042,14 @@ rewrite ereal_sup_EFin//; first exact: variations_neq0.
 rewrite -EFinD -sup_sumE.
 - by split => //; exact: variations_neq0.
 - by split => //; exact: variations_neq0.
-apply: sup_le.
-- move=> r/= [s [l' acl' <-{s}]] [t [l cbl] <-{t} <-{r}].
-  exists (variation a b f (l' ++ l)); split; last by rewrite -variation_cat// ltW.
-  exact/variations_variation/(itv_partition_cat acl' cbl).
+apply: supS.
 - have [r acfr] := variations_neq0 f ac.
   have [s cbfs] := variations_neq0 f cb.
   by exists (r + s); exists r => //; exists s.
 - by split => //; apply: variations_neq0; rewrite (lt_trans ac).
+- move=> r/= [s [l' acl' <-{s}]] [t [l cbl] <-{t} <-{r}].
+  exists (l' ++ l); last by rewrite -variation_cat// ltW.
+  exact/(itv_partition_cat acl' cbl).
 Qed.
 
 Let total_variationD2 a b c f : a <= c -> c <= b ->

theories/sequences.v

@@ -2133,10 +2133,10 @@ Qed.
 Lemma nonincreasing_sups u : has_ubound (range u) ->
   nonincreasing_seq (sups u).
 Proof.
-move=> u_ub m n mn; apply: sup_le => [_ /= [p np] <-| |].
-- by apply/downP; exists (u p) => //=; exists p => //; exact: leq_trans np.
+move=> u_ub m n mn; apply: supS => [| |_ [p /= np] <-].
 - by exists (u n) => /=; exists n => /=.
-- by split; [exists (u m); exists m => //=|exact/has_ubound_sdrop].
+- by split; [exists (u m); exists m => /=|exact/has_ubound_sdrop].
+- by exists p => //=; exact: leq_trans np.
 Qed.
 
 Lemma nondecreasing_infs u : has_lbound (range u) ->

theories/trigo.v

@@ -1263,13 +1263,12 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
   by apply: ge_sup => //; exists 0, 0 => //; exact: atan0.
 have -> : pi / 2 = sup `[0, pi / 2[ :> R.
   by rewrite real_interval.sup_itv// bnd_simp divr_gt0// pi_gt0.
-apply: sup_le; last 2 first.
+apply: supS.
 - by exists 0; rewrite /= in_itv/= lexx/= divr_gt0// pi_gt0.
 - split; first by exists 0, 0 => //; rewrite atan0.
   by exists (pi / 2) => _ [x _ <-]; exact/ltW/atan_ltpi2.
-move=> x/= /[!in_itv]/= /andP[x0 xpi2].
-apply/downP; exists (atan (tan x)) => /=; first by exists (tan x).
-rewrite tanK// in_itv/= xpi2 andbT (lt_le_trans _ x0)//.
+move=> x/= /itvP x0pi2; exists (tan x) => //=.
+rewrite tanK// in_itv/= x0pi2 andbT (@lt_le_trans _ _ 0) ?x0pi2//.
 by rewrite ltrNl oppr0 divr_gt0// pi_gt0.
 Qed.