Merge branch 'math-comp:master' into Holder-for-extended-reals

CHANGELOG_UNRELEASED.md

@@ -56,6 +56,7 @@
     `nbhs_one_point_compactification_weakE`,
     `locally_compact_completely_regular`, and
     `completely_regular_regular`.
+  + new lemmas `near_in_itvoy`, `near_in_itvNyo`
 
 - in file `mathcomp_extra.v`,
   + new definition `sigT_fun`.
@@ -69,6 +70,28 @@
 
 - in `measure.v`:
   + lemma `countable_measurable`
+- in `realfun.v`:
+  + lemma `cvgr_dnbhsP`
+  + new definitions `prodA`, and `prodAr`.
+  + new lemmas `prodAK`, `prodArK`, and `swapK`.
+- in file `product_topology.v`,
+  + new lemmas `swap_continuous`, `prodA_continuous`, and 
+    `prodAr_continuous`.
+
+- file `homotopy_theory/homotopy.v`
+- file `homotopy_theory/wedge_sigT.v`
+- in file `homotopy_theory/wedge_sigT.v`
+  + new definitions `wedge_rel`, `wedge`, `wedge_lift`, `pwedge`.
+  + new lemmas `wedge_lift_continuous`, `wedge_lift_nbhs`,
+    `wedge_liftE`, `wedge_openP`,
+    `wedge_pointE`, `wedge_point_nbhs`, `wedge_nbhs_specP`, `wedgeTE`,
+    `wedge_compact`, `wedge_connected`.
+
+- in `boolp.`:
+  + lemma `existT_inj`
+- in file `order_topology.v`
+  + new lemmas `min_continuous`, `min_fun_continuous`, `max_continuous`, and
+    `max_fun_continuous`.
 
 ### Changed
 
@@ -125,6 +148,9 @@
 
 ### Renamed
 
+- in `normedtype.v`:
+  + `near_in_itv` -> `near_in_itvoo`
+
 ### Generalized
 
 - in `lebesgue_integral.v`:

_CoqProject

@@ -61,6 +61,9 @@ theories/topology_theory/quotient_topology.v
 theories/topology_theory/one_point_compactification.v
 theories/topology_theory/sigT_topology.v
 
+theories/homotopy_theory/homotopy.v
+theories/homotopy_theory/wedge_sigT.v
+
 theories/separation_axioms.v
 theories/function_spaces.v
 theories/ereal.v

classical/boolp.v

@@ -88,6 +88,13 @@ move=> PQA; suff: {x | P x /\ Q x} by move=> [a [*]]; exists a.
 by apply: cid; case: PQA => x; exists x.
 Qed.
 
+Lemma existT_inj (A : eqType) (P : A -> Type) (p : A) (x y : P p) :
+  existT P p x = existT P p y -> x = y.
+Proof.
+apply: Eqdep_dec.inj_pair2_eq_dec => a b.
+by have [|/eqP] := eqVneq a b; [left|right].
+Qed.
+
 Record mextensionality := {
   _ : forall (P Q : Prop), (P <-> Q) -> (P = Q);
   _ : forall {T U : Type} (f g : T -> U),

classical/mathcomp_extra.v

@@ -18,6 +18,8 @@ From mathcomp Require Import finset interval.
 (*                           {in A &, {mono f : x y /~ x <= y}}               *)
 (*             sigT_fun f := lifts a family of functions f into a function on *)
 (*                           the dependent sum                                *)
+(*                prodA x := sends (X * Y) * Z to X * (Y * Z)                 *)
+(*               prodAr x := sends X * (Y * Z) to (X * Y) * Z                 *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)
@@ -373,7 +375,27 @@ Lemma real_ltr_distlC [R : numDomainType] [x y : R] (e : R) :
   x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e).
 Proof. by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed.
 
-Definition swap (T1 T2 : Type) (x : T1 * T2) := (x.2, x.1).
+Definition swap {T1 T2 : Type} (x : T1 * T2) := (x.2, x.1).
+
+Section reassociate_products.
+Context {X Y Z : Type}.
+
+Definition prodA (xyz : (X * Y) * Z) : X * (Y * Z) :=
+  (xyz.1.1, (xyz.1.2, xyz.2)).
+
+Definition prodAr (xyz : X * (Y * Z)) : (X * Y) * Z :=
+  ((xyz.1, xyz.2.1), xyz.2.2).
+
+Lemma prodAK : cancel prodA prodAr.
+Proof. by case; case. Qed.
+
+Lemma prodArK : cancel prodAr prodA.
+Proof. by case => ? []. Qed.
+
+End reassociate_products.
+
+Lemma swapK {T1 T2 : Type} : cancel (@swap T1 T2) (@swap T2 T1).
+Proof. by case=> ? ?. Qed.
 
 Definition map_pair {S U : Type} (f : S -> U) (x : (S * S)) : (U * U) :=
   (f x.1, f x.2).

theories/Make

@@ -29,6 +29,9 @@ topology_theory/quotient_topology.v
 topology_theory/one_point_compactification.v
 topology_theory/sigT_topology.v
 
+homotopy_theory/homotopy.v
+homotopy_theory/wedge_sigT.v
+
 separation_axioms.v
 function_spaces.v
 cantor.v

theories/ftc.v

@@ -979,7 +979,7 @@ rewrite (@integration_by_substitution_decreasing (- F)%R); first last.
   rewrite -derive1E.
   have /cvgN := cF' _ xab; apply: cvg_trans; apply: near_eq_cvg.
   rewrite near_simpl; near=> y; rewrite fctE !derive1E deriveN//.
-  by case: Fab => + _ _; apply; near: y; exact: near_in_itv.
+  by case: Fab => + _ _; apply; near: y; exact: near_in_itvoo.
 - by move=> x y xab yab yx; rewrite ltrN2 incrF.
 - by [].
 have mGF : measurable_fun `]a, b[ (G \o F).

theories/homotopy_theory/homotopy.v

@@ -0,0 +1,2 @@
+(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C.              *)
+From mathcomp Require Export wedge_sigT.

theories/homotopy_theory/wedge_sigT.v

@@ -0,0 +1,202 @@
+(* mathcomp analysis (c) 2024 Inria and AIST. License: CeCILL-C.              *)
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
+From mathcomp Require Import boolp classical_sets functions.
+From mathcomp Require Import cardinality mathcomp_extra fsbigop.
+From mathcomp Require Import reals signed topology separation_axioms.
+Require Import EqdepFacts.
+
+(**md**************************************************************************)
+(* # wedge sum for sigT                                                       *)
+(* A foundational construction for homotopy theory. It glues a dependent sum  *)
+(* at a single point. It's classicaly used in the proof that every free group *)
+(* is a fundamental group of some space. We also will use it as part of our   *)
+(* construction of paths and path concatenation.                              *)
+(* ```                                                                        *)
+(*    wedge_rel p0 x y == x and y are equal, or they are (p0 i) and           *)
+(*                        (p0 j) for some i and j                             *)
+(*            wedge p0 == the quotient of {i : X i} along `wedge_rel p0`      *)
+(*        wedge_lift i == the lifting of elements of (X i) into the wedge     *)
+(*           pwedge p0 == the wedge of ptopologicalTypes at their designated  *)
+(*                        point                                               *)
+(* ```                                                                        *)
+(* The type `wedge p0` is endowed with the structures of:                     *)
+(* - topology via `quotient_topology`                                         *)
+(* - quotient                                                                 *)
+(*                                                                            *)
+(* The type `pwedge` is endowed with the structures of:                       *)
+(* - topology via `quotient_topology`                                         *)
+(* - quotient                                                                 *)
+(* - pointed                                                                  *)
+(*                                                                            *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope classical_set_scope.
+Local Open Scope ring_scope.
+Local Open Scope quotient_scope.
+
+Section wedge.
+Context {I : choiceType} (X : I -> topologicalType) (p0 : forall i, X i).
+Implicit Types i : I.
+
+Let wedge_rel' (a b : {i & X i}) :=
+  (a == b) || ((projT2 a == p0 _) && (projT2 b == p0 _)).
+
+Local Lemma wedge_rel_refl : reflexive wedge_rel'.
+Proof. by move=> ?; rewrite /wedge_rel' eqxx. Qed.
+
+Local Lemma wedge_rel_sym : symmetric wedge_rel'.
+Proof.
+by move=> a b; apply/is_true_inj/propext; rewrite /wedge_rel'; split;
+  rewrite (eq_sym b) andbC.
+Qed.
+
+Local Lemma wedge_rel_trans : transitive wedge_rel'.
+Proof.
+move=> a b c /predU1P[-> //|] + /predU1P[<- //|]; rewrite /wedge_rel'.
+by move=> /andP[/eqP -> /eqP <-] /andP[_ /eqP <-]; rewrite !eqxx orbC.
+Qed.
+
+Definition wedge_rel := EquivRel _ wedge_rel_refl wedge_rel_sym wedge_rel_trans.
+Global Opaque wedge_rel.
+
+Definition wedge := {eq_quot wedge_rel}.
+Definition wedge_lift i : X i -> wedge := \pi_wedge \o existT X i.
+
+HB.instance Definition _ := Topological.copy wedge (quotient_topology wedge).
+HB.instance Definition _ := Quotient.on wedge.
+Global Opaque wedge.
+
+Lemma wedge_lift_continuous i : continuous (@wedge_lift i).
+Proof. by move=> ?; apply: continuous_comp => //; exact: pi_continuous. Qed.
+
+HB.instance Definition _ i :=
+  @isContinuous.Build _ _ (@wedge_lift i) (@wedge_lift_continuous i).
+
+Lemma wedge_lift_nbhs i (x : X i) :
+  closed [set p0 i] -> x != p0 _ -> @wedge_lift i @ x = nbhs (@wedge_lift _ x).
+Proof.
+move=> clx0 xNx0; rewrite eqEsubset; split => U; first last.
+  by move=> ?; exact: wedge_lift_continuous.
+rewrite ?nbhsE /= => -[V [oV Vx VU]].
+exists (@wedge_lift i @` (V `&` ~` [set p0 i])); first last.
+  by move=> ? /= [l] [Vl lx] <-; exact: VU.
+split; last by exists x => //; split => //=; exact/eqP.
+rewrite /open /= /quotient_open /wedge_lift /=.
+suff -> : \pi_wedge @^-1` (@wedge_lift i @` (V `&` ~`[set p0 i])) =
+          existT X i @` (V `&` ~` [set p0 i]).
+  by apply: existT_open_map; apply: openI => //; exact: closed_openC.
+rewrite eqEsubset; split => t /= [l [Vl] lNx0]; last by move=> <-; exists l.
+by case/eqmodP/predU1P => [<-|/andP [/eqP]//]; exists l.
+Qed.
+
+Lemma wedge_liftE i (x : X i) j (y : X j) :
+  wedge_lift (p0 j) = wedge_lift (p0 i).
+Proof. by apply/eqmodP/orP; right; rewrite !eqxx. Qed.
+
+Lemma wedge_openP (U : set wedge) :
+  open U <-> forall i, open (@wedge_lift i @^-1` U).
+Proof.
+split=> [oU i|oiU].
+  by apply: open_comp => // x _; exact: wedge_lift_continuous.
+have : open (\bigcup_i (@wedge_lift i @` (@wedge_lift i @^-1` U))).
+  apply/sigT_openP => i; move: (oiU i); congr open.
+  rewrite eqEsubset; split => x /=.
+    by move=> Ux; exists i => //; exists x.
+  case=> j _ /= [] y Uy /eqmodP /predU1P[R|].
+    have E : j = i by move: R; exact: eq_sigT_fst.
+    by rewrite -E in x R *; rewrite -(existT_inj R).
+  case/andP => /eqP/= + /eqP -> => yj.
+  by rewrite yj (wedge_liftE x y) in Uy.
+congr open; rewrite eqEsubset; split => /= z.
+  by case=> i _ /= [x] Ux <-.
+move=> Uz; exists (projT1 (repr z)) => //=.
+by exists (projT2 (repr z)); rewrite /wedge_lift /= -sigT_eta reprK.
+Qed.
+
+Lemma wedge_point_nbhs i0 :
+  nbhs (wedge_lift (p0 i0)) = \bigcap_i (@wedge_lift i @ p0 i).
+Proof.
+rewrite eqEsubset; split => //= U /=; rewrite ?nbhs_simpl.
+  case=> V [/= oV Vp] VU j _; apply: wedge_lift_continuous.
+  apply: (filterS VU); first exact: (@nbhs_filter wedge).
+  apply: open_nbhs_nbhs; split => //.
+  by rewrite (wedge_liftE (p0 i0)).
+move=> Uj; have V_ : forall i, {V : set (X i) |
+    [/\ open V, V (p0 i) & V `<=` @wedge_lift i @^-1` U]}.
+  move=> j; apply: cid; have /Uj : [set: I] j by [].
+  by rewrite nbhsE /= => -[B [? ? ?]]; exists B.
+pose W := \bigcup_i (@wedge_lift i) @` (projT1 (V_ i)).
+exists W; split.
+- apply/wedge_openP => i; rewrite /W; have [+ Vpj _] := projT2 (V_ i).
+  congr (_ _); rewrite eqEsubset; split => z; first by move=> Viz; exists i.
+  case => j _ /= [] w /= svw /eqmodP /predU1P[[E]|].
+    by rewrite E in w svw * => R; rewrite -(existT_inj R).
+  by case/andP => /eqP /= _ /eqP ->.
+- by exists i0 => //=; exists (p0 i0) => //; have [_ + _] := projT2 (V_ i0).
+- by move=> ? [j _ [x ? <-]]; have [_ _] := projT2 (V_ j); exact.
+Qed.
+
+Variant wedge_nbhs_spec (z : wedge) : wedge -> set_system wedge -> Type :=
+  | wedge_liftsPoint i0 :
+      wedge_nbhs_spec z (wedge_lift (p0 i0)) (\bigcap_i (@wedge_lift i @ p0 i))
+  | WedgeNotPoint (i : I) (x : X i) of (x != p0 i):
+      wedge_nbhs_spec z (wedge_lift x) (@wedge_lift i @ x).
+
+Lemma wedge_nbhs_specP (z : wedge) : (forall i, closed [set p0 i]) ->
+  wedge_nbhs_spec z z (nbhs z).
+Proof.
+move=> clP; rewrite -[z](@reprK _ wedge); case: (repr z) => i x.
+have [->|xpi] := eqVneq x (p0 i).
+  by rewrite wedge_point_nbhs => /=; exact: wedge_liftsPoint.
+by rewrite /= -wedge_lift_nbhs //; exact: WedgeNotPoint.
+Qed.
+
+Lemma wedgeTE : \bigcup_i (@wedge_lift i) @` setT = [set: wedge].
+Proof.
+rewrite -subTset => z _; rewrite -[z]reprK; exists (projT1 (repr z)) => //.
+by exists (projT2 (repr z)) => //; rewrite /wedge_lift/= -sigT_eta.
+Qed.
+
+Lemma wedge_compact : finite_set [set: I] -> (forall i, compact [set: X i]) ->
+  compact [set: wedge].
+Proof.
+move=> fsetI cptX; rewrite -wedgeTE -fsbig_setU //; apply: big_ind.
+- exact: compact0.
+- by move=> ? ? ? ?; exact: compactU.
+move=> i _; apply: continuous_compact; last exact: cptX.
+exact/continuous_subspaceT/wedge_lift_continuous.
+Qed.
+
+Lemma wedge_connected : (forall i, connected [set: X i]) ->
+  connected [set: wedge].
+Proof.
+move=> ctdX; rewrite -wedgeTE.
+have [I0|/set0P[i0 Ii0]] := eqVneq [set: I] set0.
+  rewrite [X in connected X](_ : _ = set0); first exact: connected0.
+  by rewrite I0 bigcup_set0.
+apply: bigcup_connected.
+  exists (@wedge_lift i0 (p0 _)) => i Ii; exists (p0 i) => //.
+  exact: wedge_liftE.
+move=> i ? /=; apply: connected_continuous_connected => //.
+exact/continuous_subspaceT/wedge_lift_continuous.
+Qed.
+
+End wedge.
+
+Section pwedge.
+Context {I : pointedType} (X : I -> ptopologicalType).
+
+Definition pwedge := wedge (fun i => @point (X i)).
+
+Let pwedge_point : pwedge := wedge_lift _ (@point (X (@point I))).
+
+HB.instance Definition _ := Topological.on pwedge.
+HB.instance Definition _ := Quotient.on pwedge.
+HB.instance Definition _ := isPointed.Build pwedge pwedge_point.
+
+End pwedge.

theories/normedtype.v

@@ -5336,10 +5336,42 @@ Lemma bound_itvE (R : numDomainType) (a b : R) :
   (a \in `]-oo, a]).
 Proof. by rewrite !(boundr_in_itv, boundl_in_itv). Qed.
 
-Lemma near_in_itv {R : realFieldType} (a b : R) :
+Section near_in_itv.
+Context {R : realFieldType} (a b : R).
+
+Lemma near_in_itvoo :
   {in `]a, b[, forall y, \forall z \near y, z \in `]a, b[}.
 Proof. exact: interval_open. Qed.
 
+Lemma near_in_itvoy :
+  {in `]a, +oo[, forall y, \forall z \near y, z \in `]a, +oo[}.
+Proof.
+move=> x ax.
+near=> z.
+suff : z \in `]a, +oo[%classic by rewrite inE.
+near: z.
+rewrite near_nbhs.
+apply: (@open_in_nearW _ _ `]a, +oo[%classic) => //.
+by rewrite inE.
+Unshelve. end_near. Qed.
+
+Lemma near_in_itvNyo :
+  {in `]-oo, b[, forall y, \forall z \near y, z \in `]-oo, b[}.
+Proof.
+move=> x xb.
+near=> z.
+suff : z \in `]-oo, b[%classic by rewrite inE.
+near: z.
+rewrite near_nbhs.
+apply: (@open_in_nearW _ _ `]-oo, b[%classic) => //.
+by rewrite inE/=.
+Unshelve. end_near. Qed.
+
+End near_in_itv.
+#[deprecated(since="mathcomp-analysis 1.7.0",
+  note="use `near_in_itvoo` instead")]
+Notation near_in_itv := near_in_itvoo (only parsing).
+
 Lemma cvg_patch {R : realType} (f : R -> R^o) (a b : R) (x : R) : (a < b)%R ->
   x \in `]a, b[ ->
   f @ (x : subspace `[a, b]) --> f x ->
@@ -5350,15 +5382,15 @@ move/cvgrPdist_lt : xf => /(_ e e0) xf.
 near=> z.
 rewrite patchE ifT//; last first.
   rewrite inE; apply: subset_itv_oo_cc.
-  by near: z; exact: near_in_itv.
+  by near: z; exact: near_in_itvoo.
 near: z.
 rewrite /prop_near1 /nbhs/= /nbhs_subspace ifT// in xf; last first.
   by rewrite inE/=; exact: subset_itv_oo_cc xab.
 case: xf => x0 /= x00 xf.
 near=> z.
 apply: xf => //=.
 rewrite inE; apply: subset_itv_oo_cc.
-by near: z; exact: near_in_itv.
+by near: z; exact: near_in_itvoo.
 Unshelve. all: by end_near. Qed.
 
 Notation "f @`[ a , b ]" :=