Kernel

CHANGELOG.md

@@ -1,6 +1,96 @@
 # Changelog
 
-Lastest releases: [[0.5.3] - 2022-08-10](#053---2022-08-10) and [[0.5.2] - 2022-06-08](#052---2022-07-08)
+Lastest releases: [[0.5.4] - 2022-09-07](#055---2022-09-07) and [[0.5.3] - 2022-08-10](#053---2022-08-10)
+
+## [0.5.4] - 2022-09-07
+
+### Added
+
+- in `mathcomp_extra.v`:
+  + defintion `onem` and notation ``` `1- ```
+  + lemmas `onem0`, `onem1`, `onemK`, `onem_gt0`, `onem_ge0`, `onem_le1`, `onem_lt1`,
+    `onemX_ge0`, `onemX_lt1`, `onemD`, `onemMr`, `onemM`
+  + lemmas `natr1`, `nat1r`
+- in `classical_sets.v`:
+  + lemmas `subset_fst_set`, `subset_snd_set`, `fst_set_fst`, `snd_set_snd`,
+    `fset_setM`, `snd_setM`, `fst_setMR`
+  + lemmas `xsection_snd_set`, `ysection_fst_set`
+- in `constructive_ereal.v`:
+  + lemmas `ltNye_eq`, `sube_lt0`, `subre_lt0`, `suber_lt0`, `sube_ge0`
+  + lemmas `dsubre_gt0`, `dsuber_gt0`, `dsube_gt0`, `dsube_le0`
+- in `signed.v`:
+  + lemmas `onem_PosNum`, `onemX_NngNum`
+- in `fsbigop.v`:
+  + lemmas `lee_fsum_nneg_subset`, `lee_fsum`
+- in `topology.v`:
+  + lemma `near_inftyS`
+  + lemma `continuous_closedP`, `closedU`, `pasting`
+  + lemma `continuous_inP`
+  + lemmas `open_setIS`, `open_setSI`, `closed_setIS`, `closed_setSI`
+- in `normedtype.v`:
+  + definitions `contraction` and `is_contraction`
+  + lemma `contraction_fixpoint_unique`
+- in `sequences.v`:
+  + lemmas `contraction_dist`, `contraction_cvg`,
+    `contraction_cvg_fixed`, `banach_fixed_point`,
+    `contraction_unique`
+- in `derive.v`:
+  + lemma `diff_derivable`
+- in `measure.v`:
+  + lemma `measurable_funTS`
+- in `lebesgue_measure.v`:
+  + lemma `measurable_fun_fine`
+  + lemma `open_measurable_subspace`
+  + lemma ``subspace_continuous_measurable_fun``
+  + corollary `open_continuous_measurable_fun`
+  + Hint about `measurable_fun_normr`
+- in `lebesgue_integral.v`:
+  + lemma `measurable_fun_indic`
+  + lemma `ge0_integral_mscale`
+  + lemma `integral_pushforward`
+
+### Changed
+
+- in `esum.v`:
+  + definition `esum`
+- moved from `lebesgue_integral.v` to `classical_sets.v`:
+  + `mem_set_pair1` -> `mem_xsection`
+  + `mem_set_pair2` -> `mem_ysection`
+- in `derive.v`:
+  + generalized `is_diff_scalel`
+- in `measure.v`:
+  + generalize `measurable_uncurry`
+- in `lebesgue_measure.v`:
+  + `pushforward` requires a proof that its argument is measurable
+- in `lebesgue_integral.v`:
+  + change implicits of `integralM_indic`
+
+### Renamed
+
+- in `constructive_ereal.v`:
+  + `lte_pinfty_eq` -> `ltey_eq`
+  + `le0R` -> `fine_ge0`
+  + `lt0R` -> `fine_gt0`
+- in `ereal.v`:
+  + `lee_pinfty_eq` -> `leye_eq`
+  + `lee_ninfty_eq` -> `leeNy_eq`
+- in `esum.v`:
+  + `esum0` -> `esum1`
+- in `sequences.v`:
+  + `nneseries_lim_ge0` -> `nneseries_ge0`
+- in `measure.v`:
+  + `ring_fsets` -> `ring_finite_set`
+  + `discrete_measurable` -> `discrete_measurable_nat`
+  + `cvg_mu_inc` -> `nondecreasing_cvg_mu`
+- in `lebesgue_integral.v`:
+  + `muleindic_ge0` -> `nnfun_muleindic_ge0`
+  + `mulem_ge0` -> `mulemu_ge0`
+  + `nnfun_mulem_ge0` -> `nnsfun_mulemu_ge0`
+
+### Removed
+
+- in `esum.v`:
+  + lemma `fsetsP`, `sum_fset_set`
 
 ## [0.5.3] - 2022-08-10
 

CHANGELOG_UNRELEASED.md

@@ -3,49 +3,15 @@
 ## [Unreleased]
 
 ### Added
-- in `normedtype.v`:
-  + definitions `contraction` and `is_contraction`
-  + lemma `contraction_fixpoint_unique`
-
-- in `constructive_ereal.v`:
-  + lemmas `ltNye_eq`, `sube_lt0`, `subre_lt0`, `suber_lt0`, `sube_ge0`
-  + lemmas `dsubre_gt0`, `dsuber_gt0`, `dsube_gt0`, `dsube_le0`
-
 - in `topology.v`:
-  + lemma `near_inftyS`
-- in `sequences.v`:
-  + lemmas `contraction_dist`, `contraction_cvg`,
-    `contraction_cvg_fixed`, `banach_fixed_point`,
-    `contraction_unique`
-- in `mathcomp_extra.v`:
-  + defintion `onem` and notation ``` `1- ```
-  + lemmas `onem0`, `onem1`, `onemK`, `onem_gt0`, `onem_ge0`, `onem_le1`, `onem_lt1`,
-    `onemX_ge0`, `onemX_lt1`, `onemD`, `onemMr`, `onemM`
-- in `signed.v`:
-  + lemmas `onem_PosNum`, `onemX_NngNum`
+  + lemmas `continuous_subspaceT`, `subspaceT_continuous`
 
 ### Changed
 
-- in `measure.v`:
-  + generalize `measurable_uncurry`
-
 ### Renamed
 
-- in `constructive_ereal.v`:
-  + `lte_pinfty_eq` -> `ltey_eq`
-- in `sequences.v`:
-  + `nneseries_lim_ge0` -> `nneseries_ge0`
-- in `constructive_ereal.v`:
-  + `le0R` -> `fine_ge0`
-  + `lt0R` -> `fine_gt0`
-- in `measure.v`:
-  + `ring_fsets` -> `ring_finite_set`
-  + `discrete_measurable` -> `discrete_measurable_nat`
-- in `ereal.v`:
-  + `lee_pinfty_eq` -> `leye_eq`
-  + `lee_ninfty_eq` -> `leeNy_eq`
-- in `measure.v`:
-  + `cvg_mu_inc` -> `nondecreasing_cvg_mu`
+- in `topology.v`:
+  + renamed `continuous_subspaceT` to `continuous_in_subspaceT`
 
 ### Removed
 

INSTALL.md

@@ -5,7 +5,7 @@
 - [The Coq Proof Assistant version ≥ 8.13](https://coq.inria.fr)
 - [Mathematical Components version ≥ 1.13.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 1.5.1](https://github.com/math-comp/finmap)
-- [Hierarchy builder version >= 1.2.0](https://github.com/math-comp/hierarchy-builder)
+- [Hierarchy builder version >= 1.3.0](https://github.com/math-comp/hierarchy-builder)
 
 These requirements can be installed in a custom way, or through
 [opam](https://opam.ocaml.org/) (the recommended way) using
@@ -47,7 +47,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.0.5.3
+$ opam install coq-mathcomp-analysis.0.5.4
 ```
 4. Everytime you want to work in this same context, you need to type
 ```

README.md

@@ -33,7 +33,7 @@ the Coq proof-assistant and using the Mathematical Components library.
   - Pierre-Yves Strub (initial)
   - Laurent Théry
 - License: [CeCILL-C](LICENSE)
-- Compatible Coq versions: Coq 8.14 to 8.15 (or dev)
+- Compatible Coq versions: Coq 8.14 to 8.16 (or dev)
 - Additional dependencies:
   - [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
   - [MathComp fingroup 1.13 or later](https://math-comp.github.io)

_CoqProject

@@ -32,6 +32,9 @@ theories/derive.v
 theories/measure.v
 theories/numfun.v
 theories/lebesgue_integral.v
+theories/kernel.v
+theories/prob_lang.v
+theories/wip.v
 theories/summability.v
 theories/functions.v
 theories/signed.v

coq-mathcomp-analysis.opam

@@ -18,7 +18,7 @@ the Coq proof-assistant and using the Mathematical Components library."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" { (>= "8.14" & < "8.16~") | (= "dev") }
+  "coq" { (>= "8.14" & < "8.17~") | (= "dev") }
   "coq-mathcomp-ssreflect" { (>= "1.13.0" & < "1.16~") | (= "dev") }
   "coq-mathcomp-fingroup" { (>= "1.13.0" & < "1.16~") | (= "dev") }
   "coq-mathcomp-algebra" { (>= "1.13.0" & < "1.16~") | (= "dev") }

meta.yml

@@ -49,8 +49,8 @@ license:
   file: LICENSE
 
 supported_coq_versions:
-  text: Coq 8.14 to 8.15 (or dev)
-  opam: '{ (>= "8.14" & < "8.16~") | (= "dev") }'
+  text: Coq 8.14 to 8.16 (or dev)
+  opam: '{ (>= "8.14" & < "8.17~") | (= "dev") }'
 
 tested_coq_opam_versions:
 - version: '1.13.0-coq-8.14'

theories/Rstruct.v

@@ -503,15 +503,19 @@ Section bigmaxr.
 Context {R : realDomainType}.
 
 (* bigop pour le max pour des listes non vides ? *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Definition bigmaxr (r : R) s := \big[Num.max/head r s]_(i <- s) i.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_nil (x0 : R) : bigmaxr x0 [::] = x0.
 Proof. by rewrite /bigmaxr /= big_nil. Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_un (x0 x : R) : bigmaxr x0 [:: x] = x.
 Proof. by rewrite /bigmaxr /= big_cons big_nil maxxx. Qed.
 
 (* previous definition *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxrE (r : R) s : bigmaxr r s = foldr Num.max (head r s) (behead s).
 Proof.
 rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s) i).
@@ -520,6 +524,7 @@ rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_(i <- s
 by case: s => //=; rewrite /bigmaxr big_nil.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigrmax_dflt (x y : R) s : Num.max x (\big[Num.max/x]_(j <- y :: s) j) =
   Num.max x (\big[Num.max/y]_(i <- y :: s) i).
 Proof.
@@ -528,10 +533,12 @@ by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC.
 by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_cons (x0 x y : R) lr :
   bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)).
 Proof. by rewrite [y :: lr]lock /bigmaxr /= -lock big_cons bigrmax_dflt. Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_ler (x0 : R) s i :
   (i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).
 Proof.
@@ -542,6 +549,7 @@ by rewrite big_cons bigrmax_dflt le_maxr orbC IH.
 Qed.
 
 (* Compatibilité avec l'addition *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_addr (x0 : R) lr (x : R) :
   bigmaxr (x0 + x) (map (fun y : R => y + x) lr) = (bigmaxr x0 lr) + x.
 Proof.
@@ -550,6 +558,7 @@ elim: t h => /= [|h' t IH] h; first by rewrite ?(big_cons,big_nil) -addr_maxl.
 by rewrite [in RHS]big_cons bigrmax_dflt addr_maxl -IH big_cons bigrmax_dflt.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_mem (x0 : R) lr : (0 < size lr)%N -> bigmaxr x0 lr \in lr.
 Proof.
 rewrite /bigmaxr; case: lr => // h t _.
@@ -560,6 +569,7 @@ rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
 Qed.
 
 (* TODO: bigmaxr_morph? *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_mulr (A : finType) (s : seq A) (k : R) (x : A -> R) :
   0 <= k -> bigmaxr 0 (map (fun i => k * x i) s) = k * bigmaxr 0 (map x s).
 Proof.
@@ -569,6 +579,7 @@ by rewrite !bigmaxr_un.
 by rewrite bigmaxr_cons {}ih bigmaxr_cons maxr_pmulr.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_index (x0 : R) lr :
   (0 < size lr)%N -> (index (bigmaxr x0 lr) lr < size lr)%N.
 Proof.
@@ -577,6 +588,7 @@ move: (@bigmaxr_mem x0 (h :: t) isT).
 by rewrite ltnS index_mem inE /= eq_sym H.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_lerP (x0 : R) lr (x : R) :
   (0 < size lr)%N ->
   reflect (forall i, (i < size lr)%N -> (nth x0 lr i) <= x) ((bigmaxr x0 lr) <= x).
@@ -586,6 +598,7 @@ move=> lr_size; apply: (iffP idP) => [le_x i i_size | H].
 by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_ltrP (x0 : R) lr (x : R) :
   (0 < size lr)%N ->
   reflect (forall i, (i < size lr)%N -> (nth x0 lr i) < x) ((bigmaxr x0 lr) < x).
@@ -595,6 +608,7 @@ move=> lr_size; apply: (iffP idP) => [lt_x i i_size | H].
 by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxrP (x0 : R) lr (x : R) :
   (x \in lr /\ forall i, (i < size lr) %N -> (nth x0 lr i) <= x) -> (bigmaxr x0 lr = x).
 Proof.
@@ -614,6 +628,7 @@ apply/negP => /eqP H; apply: neq_i; rewrite -H eq_sym; apply/eqP.
 by apply: index_uniq.
 Qed. *)
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bigmaxr_lerif (x0 : R) lr :
   uniq lr -> forall i, (i < size lr)%N ->
      (nth x0 lr i) <= (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr).
@@ -625,9 +640,11 @@ by apply: bigmaxr_mem; apply: (leq_trans _ i_size).
 Qed.
 
 (* bigop pour le max pour des listes non vides ? *)
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Definition bmaxrf n (f : {ffun 'I_n.+1 -> R}) :=
   bigmaxr (f ord0) (codom f).
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bmaxrf_ler n (f : {ffun 'I_n.+1 -> R}) i :
   (f i) <= (bmaxrf f).
 Proof.
@@ -637,6 +654,7 @@ suff -> : nth (f ord0) (codom f) i = f i; first by [].
 by rewrite /codom (nth_map ord0) ?size_enum_ord // nth_ord_enum.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bmaxrf_index n (f : {ffun 'I_n.+1 -> R}) :
   (index (bmaxrf f) (codom f) < n.+1)%N.
 Proof.
@@ -646,11 +664,14 @@ rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)); last first.
 by apply: bigmaxr_index; rewrite size_codom card_ord.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Definition index_bmaxrf n f := Ordinal (@bmaxrf_index n f).
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma ordnat i n (ord_i : (i < n)%N) : i = Ordinal ord_i :> nat.
 Proof. by []. Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma eq_index_bmaxrf n (f : {ffun 'I_n.+1 -> R}) :
   f (index_bmaxrf f) = bmaxrf f.
 Proof.
@@ -661,6 +682,7 @@ move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0).
 by rewrite size_enum_ord; apply: bmaxrf_index.
 Qed.
 
+#[deprecated(note="To be removed. Use topology.v's bigmax/min lemmas instead.")]
 Lemma bmaxrf_lerif n (f : {ffun 'I_n.+1 -> R}) :
   injective f -> forall i,
      (f i) <= (bmaxrf f) ?= iff (i == index_bmaxrf f).