refactor essential_supremum / infimum theory

.nix/config.nix

@@ -55,7 +55,6 @@ in
 
   bundles."8.20".coqPackages = common-bundle // {
     coq.override.version = "8.20";
-    mathcomp.override.version = "2.2.0";
   };
 
   bundles."9.0".coqPackages = common-bundle // {

_CoqProject

@@ -67,6 +67,7 @@ theories/homotopy_theory/homotopy.v
 theories/homotopy_theory/wedge_sigT.v
 theories/homotopy_theory/continuous_path.v
 
+theories/ess_sup_inf.v
 theories/separation_axioms.v
 theories/function_spaces.v
 theories/ereal.v
@@ -97,3 +98,4 @@ theories/gauss_integral.v
 theories/showcase/summability.v
 analysis_stdlib/Rstruct_topology.v
 analysis_stdlib/showcase/uniform_bigO.v
+theories/lspace.v

classical/boolp.v

@@ -329,6 +329,30 @@ Proof. by rewrite /asbool; case: pselect=> h; constructor. Qed.
 Lemma asboolW (P : Prop) : `[<P>] -> P.
 Proof. by case: asboolP. Qed.
 
+Lemma orW A B : A \/ B -> A + B.
+Proof.
+have [|NA] := asboolP A; first by left.
+have [|NB] := asboolP B; first by right.
+by move=> AB; exfalso; case: AB.
+Qed.
+
+Lemma or3W A B C : [\/ A, B | C] -> A + B + C.
+Proof.
+have [|NA] := asboolP A; first by left; left.
+have [|NB] := asboolP B; first by left; right.
+have [|NC] := asboolP C; first by right.
+by move=> ABC; exfalso; case: ABC.
+Qed.
+
+Lemma or4W A B C D : [\/ A, B, C | D] -> A + B + C + D.
+Proof.
+have [|NA] := asboolP A; first by left; left; left.
+have [|NB] := asboolP B; first by left; left; right.
+have [|NC] := asboolP C; first by left; right.
+have [|ND] := asboolP D; first by right.
+by move=> ABCD; exfalso; case: ABCD.
+Qed.
+
 (* Shall this be a coercion ?*)
 Lemma asboolT (P : Prop) : P -> `[<P>].
 Proof. by case: asboolP. Qed.

classical/classical_sets.v

@@ -1523,6 +1523,9 @@ Proof. by move=> b [x [Aa Ba <-]]; split; apply: imageP. Qed.
 Lemma nonempty_image f A : f @` A !=set0 -> A !=set0.
 Proof. by case=> b [a]; exists a. Qed.
 
+Lemma image_nonempty f A : A !=set0 -> f @` A !=set0.
+Proof. by move=> [x] Ax; exists (f x), x. Qed.
+
 Lemma image_subset f A B : A `<=` B -> f @` A `<=` f @` B.
 Proof. by move=> AB _ [a Aa <-]; exists a => //; apply/AB. Qed.
 
@@ -1645,6 +1648,8 @@ Proof. by rewrite preimage_false; under eq_fun do rewrite inE. Qed.
 
 End image_lemmas.
 Arguments sub_image_setI {aT rT f A B} t _.
+Arguments subset_set1 {_ _ _}.
+Arguments subset_set2 {_ _ _ _}.
 
 Lemma image2_subset {aT bT rT : Type} (f : aT -> bT -> rT)
     (A B : set aT) (C D : set bT) : A `<=` B -> C `<=` D ->

classical/mathcomp_extra.v

@@ -681,3 +681,17 @@ Proof. exact: comparable_max_le_max. Qed.
 Lemma real_sqrtC {R : numClosedFieldType} (x : R) : 0 <= x ->
   sqrtC x \in Num.real.
 Proof. by rewrite -sqrtC_ge0; apply: ger0_real. Qed.
+
+Lemma eq_exists2l (A : Type) (P P' Q : A -> Prop) :
+  (forall x, P x <-> P' x) ->
+  (exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x).
+Proof.
+by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ.
+Qed.
+
+Lemma eq_exists2r (A : Type) (P Q Q' : A -> Prop) :
+  (forall x, Q x <-> Q' x) ->
+  (exists2 x, P x & Q x) <-> (exists2 x, P x & Q' x).
+Proof.
+by move=> eqP; split=> -[x p q]; exists x; move: p q; rewrite ?eqP.
+Qed.

experimental_reals/discrete.v

@@ -4,7 +4,7 @@
 (* Copyright (c) - 2016--2018 - Polytechnique                           *)
 
 (* -------------------------------------------------------------------- *)
-From Corelib Require Setoid.
+From Coq Require Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp.classical Require Import boolp.

reals/reals.v

@@ -38,7 +38,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
-From Corelib Require Import Setoid.
+From Coq Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra archimedean.
 From mathcomp Require Import boolp classical_sets set_interval.

theories/Make

@@ -9,6 +9,7 @@
 
 ereal.v
 landau.v
+ess_sup_inf.v
 topology_theory/topology.v
 topology_theory/bool_topology.v
 topology_theory/compact.v

theories/all_analysis.v

@@ -25,3 +25,4 @@ From mathcomp Require Export charge.
 From mathcomp Require Export kernel.
 From mathcomp Require Export pi_irrational.
 From mathcomp Require Export gauss_integral.
+From mathcomp Require Export ess_sup_inf.

theories/charge.v

@@ -1866,7 +1866,7 @@ have nuf A : d.-measurable A -> nu A = \int[mu]_(x in A) f x.
 move=> A mA; rewrite nuf ?inE//; apply: ae_eq_integral => //.
 - exact/measurable_funTS.
 - exact/measurable_funTS.
-- exact: ae_eq_subset ff'.
+- exact: (@ae_eq_subset _ _ _ _ mu setT A f f' (@subsetT _ A)).
 Qed.
 
 End radon_nikodym_sigma_finite.
@@ -2092,6 +2092,10 @@ move=> mE; apply: integral_ae_eq => //.
   by rewrite -Radon_Nikodym_SigmaFinite.f_integral.
 Qed.
 
+(* TODO: move back to measure.v, current version incompatible *)
+Lemma ae_eq_mul2l (f g h : T -> \bar R) D : f = g %[ae mu in D] -> (h \* f) = (h \* g) %[ae mu in D].
+Proof. by apply: filterS => x /= /[apply] ->. Qed.
+
 Lemma Radon_Nikodym_change_of_variables f E : measurable E ->
     nu.-integrable E f ->
   \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) =

theories/ereal.v

@@ -463,6 +463,21 @@ rewrite lteNl => /ereal_sup_gt[_ [y Sy <-]].
 by rewrite lteNl oppeK => xlty; exists y.
 Qed.
 
+Lemma ereal_infEN S : ereal_inf S = - ereal_sup [set - x | x in S].
+Proof. by []. Qed.
+
+Lemma ereal_supN S : ereal_sup [set - x | x in S] = - ereal_inf S.
+Proof. by rewrite oppeK. Qed.
+
+Lemma ereal_infN S : ereal_inf [set - x | x in S] = - ereal_sup S.
+Proof.
+rewrite /ereal_inf; congr (- ereal_sup _) => /=.
+by rewrite image_comp/=; under eq_imagel do rewrite /= oppeK; rewrite image_id.
+Qed.
+
+Lemma ereal_supEN S : ereal_sup S = - ereal_inf [set - x | x in S].
+Proof. by rewrite ereal_infN oppeK. Qed.
+
 End ereal_supremum.
 
 Section ereal_supremum_realType.
@@ -523,7 +538,7 @@ Proof.
 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.
+Lemma ereal_sup_ge S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S.
 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].
@@ -591,11 +606,84 @@ rewrite -ereal_sup_EFin; [|exact/has_lb_ubN|exact/nonemptyN].
 by rewrite !image_comp.
 Qed.
 
+Lemma ereal_supP S x :
+  reflect (forall y : \bar R, S y -> y <= x) (ereal_sup S <= x).
+Proof.
+apply/(iffP idP) => [+ y Sy|].
+  by move=> /(le_trans _)->//; rewrite ereal_sup_ge//; exists y.
+apply: contraPP => /negP; rewrite -ltNge -existsPNP.
+by move=> /ereal_sup_gt[y Sy ltyx]; exists y => //; rewrite lt_geF.
+Qed.
+
+Lemma ereal_infP S x :
+  reflect (forall y : \bar R, S y -> x <= y) (x <= ereal_inf S).
+Proof.
+rewrite leeNr; apply/(equivP (ereal_supP _ _)); setoid_rewrite leeNr.
+split=> [ge_x y Sy|ge_x _ [y Sy <-]]; rewrite ?oppeK// ?ge_x//.
+by rewrite -[y]oppeK ge_x//; exists y.
+Qed.
+
+Lemma ereal_sup_gtP S x :
+  reflect (exists2 y : \bar R, S y & x < y) (x < ereal_sup S).
+Proof.
+rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_supP _ _)) -existsPNP.
+by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge.
+Qed.
+
+Lemma ereal_inf_ltP S x :
+  reflect (exists2 y : \bar R, S y & y < x) (ereal_inf S < x).
+Proof.
+rewrite ltNge; apply/(equivP negP); rewrite -(rwP (ereal_infP _ _)) -existsPNP.
+by apply/eq_exists2r => y; rewrite (rwP2 negP idP) -ltNge.
+Qed.
+
+Lemma ereal_inf_leP S x : S (ereal_inf S) ->
+  reflect (exists2 y : \bar R, S y & y <= x) (ereal_inf S <= x).
+Proof.
+move=> Sinf; apply: (iffP idP); last exact: ereal_inf_le.
+by move=> Sx; exists (ereal_inf S).
+Qed.
+
+Lemma ereal_sup_geP S x : S (ereal_sup S) ->
+  reflect (exists2 y : \bar R, S y & x <= y) (x <= ereal_sup S).
+Proof.
+move=> Ssup; apply: (iffP idP); last exact: ereal_sup_ge.
+by move=> Sx; exists (ereal_sup S).
+Qed.
+
+Lemma lb_ereal_infNy_adherent S e :
+  ereal_inf S = -oo -> exists2 x : \bar R, S x & x < e%:E.
+Proof. by move=> infNy; apply/ereal_inf_ltP; rewrite infNy ltNyr. Qed.
+
+Lemma ereal_sup_real : @ereal_sup R (range EFin) = +oo.
+Proof.
+rewrite hasNub_ereal_sup//; last by exists 0%R.
+by apply/has_ubPn => x; exists (x+1)%R => //; rewrite ltrDl.
+Qed.
+
+Lemma ereal_inf_real : @ereal_inf R (range EFin) = -oo.
+Proof.
+rewrite /ereal_inf [X in ereal_sup X](_ : _ = range EFin); last first.
+  apply/seteqP; split => x/=[y].
+    by move=> [z] _ <- <-; exists (-z)%R.
+  by move=> _ <-; exists (-y%:E); first (by exists (-y)%R); rewrite oppeK.
+by rewrite ereal_sup_real.
+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).
+#[deprecated(since="mathcomp-analysis 1.10.0", note="Renamed `ereal_sup_ge`.")]
+Notation ereal_sup_le := ereal_sup_ge.
+
+Arguments ereal_supP {R S x}.
+Arguments ereal_infP {R S x}.
+Arguments ereal_sup_gtP {R S x}.
+Arguments ereal_inf_ltP {R S x}.
+Arguments ereal_sup_geP {R S x}.
+Arguments ereal_inf_leP {R S x}.
 
 Lemma restrict_abse T (R : numDomainType) (f : T -> \bar R) (D : set T) :
   (abse \o f) \_ D = abse \o (f \_ D).