Changelog for version 1.13.0 (#1701)

* changelog for version 1.13.0

Author: affeldt-aist

CHANGELOG.md

@@ -1,6 +1,130 @@
 # Changelog
 
-Latest releases: [[1.12.0] - 2025-07-03](#1120---2025-07-03), [[1.11.0] - 2025-05-02](#1110---2025-05-02), and [[1.10.0] - 2025-04-21](#1100---2025-04-21)
+Latest releases: [[1.13.0] - 2025-08-16](#1130---2025-08-16), [[1.12.0] - 2025-07-03](#1120---2025-07-03), and [[1.11.0] - 2025-05-02](#1110---2025-05-02)
+
+## [1.13.0] - 2025-08-16
+
+### Added
+
+- in `unstable.v`:
+  + lemma `sqrtK`
+
+- in `mathcomp_extra.v`:
+  + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1`
+
+- in `functions.v`:
+  + lemmas `fct_prodE`, `prodrfctE`
+
+- in `classical_orders.v`:
+  + lemma `big_lexi_order_prefix_closed_itv`
+
+- in `topology_structure.v`:
+  + lemmas `denseI`, `dense0`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `dense_set1C`
+
+- in `constructive_ereal.v`:
+  + lemma `expe0`, `mule0n`, `muleS`
+
+- in `reals.v`:
+  + definition `irrational`
+  + lemmas `irrationalE`, `rationalP`
+
+- new file `borel_hierarchy.v`:
+  + definitions `Gdelta`, `Fsigma`
+  + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`,
+    `irrational_Gdelta`, `not_rational_Gdelta`
+
+- in `realfun.v`:
+  + instance `is_derive1_sqrt`
+
+- in `exp.v`:
+  + lemma `norm_expR`
+  + lemmas `expeR_eqy`
+  + lemmas `lt0_powR1`, `powR_eq1`
+  + definition `lne`
+  + lemmas `le0_lneNy`, `lne_EFin`, `expeRK`, `lneK`, `lneK_eq`, `lne1`, `lneM`,
+    `lne_inj`, `lneV`, `lne_div`, `lte_lne`, `lee_lne`, `lneXn`, `le_lne1Dx`,
+    `lne_sublinear`, `lne_ge0`, `lne_lt0`, `lne_gt0`, `lne_le0`
+  + lemma `lne_eq0`
+
+- in `lebesgue_measure.v`:
+  + lemma `countable_lebesgue_measure0`
+
+- in `charge.v`:
+  + definition `copp`, lemma `cscaleN1`
+
+- in `hoelder.v`
+  + lemma `hoelder_conj_ge1`
+
+### Changed
+
+- in `constructive_ereal.v`:
+  + lemma `mulN1e`
+
+- moved from `pi_irrational.v` to `reals.v` and changed
+  + definition `rational`
+
+- in `measurable_realfun.v`:
+  + generalized and renamed:
+    * `measurable_fun_itv_bndo_bndc` -> `measurable_fun_itv_bndo_bndcP`
+    * `measurable_fun_itv_obnd_cbnd` -> `measurable_fun_itv_obnd_cbndP`
+
+- moved from `simple_functions.v` to `measure.v`
+  + notations `{mfun _ >-> _}`, `[mfun of _]`
+  + mixin `isMeasurableFun`, structure `MesurableFun`, lemmas `measurable_funP`
+  + definitions `mfun`, `mfun_key`, canonical `mfun_keyed`
+  + definitions `mfun_Sub_subproof`, `mfun_Sub`
+  + lemmas `mfun_rect`, `mfun_valP`, `mfuneqP`
+  + lemma `measurableT_comp_subproof`
+
+- moved from `simple_functions.v` to `measure.v` and renamed:
+  + lemma `measurable_sfunP` -> `measurable_funPTI`
+
+- moved from `simple_functions.v` to `measurable_realfun.v`
+  + lemmas `mfun_subring_closed`, `mfun0`, `mfun1`, `mfunN`,
+    `mfunD`, `mfunB`, `mfunM`, `mfunMn`, `mfun_sum`, `mfun_prod`, `mfunX`
+  + definitions `mindic`, `indic_mfun`, `scale_mfun`, `max_mfun`
+  + lemmas `mindicE`, `max_mfun_subproof`
+
+- moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v` and renamed:
+  + lemma `measurable_sfun_inP` -> `measurable_funP1`
+
+### Renamed
+
+- in `derive.v`:
+  + `derivemxE` -> `deriveEjacobian`
+
+- in `exp.v`:
+  + `ltr_expeR` -> `lte_expeR`
+  + `ler_expeR` -> `lee_expeR`
+
+- in `lebesgue_stieltjes_measure.v`:
+  + `cumulativeNy0` -> `cumulativeNy`
+  + `cumulativey1` -> `cumulativey`
+
+- `measurable_sfunP` -> `measurable_funPTI`
+  (and moved from from `simple_functions.v` to `measure.v`)
+
+- `measurable_sfun_inP` -> `measurable_funP1`
+  (and moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v`)
+
+### Generalized
+
+- in `functions.v`
+  + lemma `fct_sumE` (from a pointwise equality to a functional one)
+
+### Removed
+
+- file `forms.v` (superseded by MathComp's `sesquilinear.v`)
+
+- in `unstable.v`:
+  + `dependent_choice_Type` (use Rocq's `dependent_choice` instead)
+
+- in `simple_functions.v`:
+  + duplicated hints about `measurable_set1`
+  + lemma `measurableT_comp_subproof` turned into a `Let` (now in `measure.v`)
 
 ## [1.12.0] - 2025-07-03
 

CHANGELOG_UNRELEASED.md

@@ -4,125 +4,16 @@
 
 ### Added
 
-- in `unstable.v`:
-  + lemma `sqrtK`
-
-- in `realfun.v`:
-  + instance `is_derive1_sqrt`
-
-- in `mathcomp_extra.v`:
-  + lemmas `subrKC`, `sumr_le0`, `card_fset_sum1`
-
-- in `functions.v`:
-  + lemmas `fct_prodE`, `prodrfctE`
-
-- in `exp.v`:
-  + lemma `norm_expR`
-
-- in `hoelder.v`
-  + lemma `hoelder_conj_ge1`
-
-- in `reals.v`:
-  + definition `irrational`
-  + lemmas `irrationalE`, `rationalP` 
-
-- in `topology_structure.v`:
-  + lemmas `denseI`, `dense0`
-
-- in `pseudometric_normed_Zmodule.v`:
-  + lemma `dense_set1C`
-
-- new file `borel_hierarchy.v`:
-  + definitions `Gdelta`, `Fsigma`
-  + lemmas `closed_Fsigma`, `Gdelta_measurable`, `Gdelta_subspace_open`,
-    `irrational_Gdelta`, `not_rational_Gdelta`
-
-- in `constructive_ereal.v`:
-  + lemma `expe0`, `mule0n`, `muleS`
-
-- in `exp.v`:
-  + lemmas `expeR_eqy`
-  + lemmas `lt0_powR1`, `powR_eq1`
-  + definition `lne`
-  + lemmas `le0_lneNy`, `lne_EFin`, `expeRK`, `lneK`, `lneK_eq`, `lne1`, `lneM`, 
-    `lne_inj`, `lneV`, `lne_div`, `lte_lne`, `lee_lne`, `lneXn`, `le_lne1Dx`, 
-    `lne_sublinear`, `lne_ge0`, `lne_lt0`, `lne_gt0`, `lne_le0`
-  + lemma `lne_eq0`
-
-- in `charge.v`:
-  + definition `copp`, lemma `cscaleN1`
-- in `classical_orders.v`:
-  + lemma `big_lexi_order_prefix_closed_itv`
-
-- in `lebesgue_measure.v`:
-  + lemma `countable_lebesgue_measure0`
-
 ### Changed
 
-- moved from `pi_irrational.v` to `reals.v` and changed
-  + definition `rational`
-
-- in `constructive_ereal.v`:
-  + lemma `mulN1e`
-
-- in `measurable_realfun.v`:
-  + generalized and renamed:
-    * `measurable_fun_itv_bndo_bndc` -> `measurable_fun_itv_bndo_bndcP`
-    * `measurable_fun_itv_obnd_cbnd` -> `measurable_fun_itv_obnd_cbndP`
-- moved from `simple_functions.v` to `measure.v`
-  + notations `{mfun _ >-> _}`, `[mfun of _]`
-  + mixin `isMeasurableFun`, structure `MesurableFun`, lemmas `measurable_funP`
-  + definitions `mfun`, `mfun_key`, canonical `mfun_keyed`
-  + definitions `mfun_Sub_subproof`, `mfun_Sub`
-  + lemmas `mfun_rect`, `mfun_valP`, `mfuneqP`
-  + lemma `measurableT_comp_subproof`
-
-- moved from `simple_functions.v` to `measure.v` and renamed:
-  + lemma `measurable_sfunP` -> `measurable_funPTI`
-
-- moved from `simple_functions.v` to `measurable_realfun.v`
-  + lemmas `mfun_subring_closed`, `mfun0`, `mfun1`, `mfunN`,
-    `mfunD`, `mfunB`, `mfunM`, `mfunMn`, `mfun_sum`, `mfun_prod`, `mfunX`
-  + definitions `mindic`, `indic_mfun`, `scale_mfun`, `max_mfun`
-  + lemmas `mindicE`, `max_mfun_subproof`
-
-- moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v` and renamed:
-  + lemma `measurable_sfun_inP` -> `measurable_funP1`
-
 ### Renamed
 
-- in `lebesgue_stieltjes_measure.v`:
-  + `cumulativeNy0` -> `cumulativeNy`
-  + `cumulativey1` -> `cumulativey`
-
-- in `exp.v`:
-  + `ltr_expeR` -> `lte_expeR`
-  + `ler_expeR` -> `lee_expeR`
-
-- in `derive.v`:
-  + `derivemxE` -> `deriveEjacobian`
-
-- `measurable_sfunP` -> `measurable_funPTI`
-  (and moved from from `simple_functions.v` to `measure.v`)
-
-- `measurable_sfun_inP` -> `measurable_funP1`
-  (and moved from `simple_functions.v` to `lebesgue_stieltjes_measure.v`)
-
 ### Generalized
 
-- in `functions.v`
-  + lemma `fct_sumE` (from a pointwise equality to a functional one)
-
 ### Deprecated
 
 ### Removed
 
-- file `forms.v` (superseded by MathComp's `sesquilinear.v`)
-
-- in `simple_functions.v`:
-  + duplicated hints about `measurable_set1`
-  + lemma `measurableT_comp_subproof` turned into a `Let` (now in `measure.v`)
-
 ### Infrastructure
 
 ### Misc

INSTALL.md

@@ -3,7 +3,7 @@
 ## Requirements
 
 - [The Coq Proof Assistant version ≥ 8.20 / Rocq Prover version ≥ 9.0](https://rocq-prover.org)
-- [Mathematical Components version ≥ 2.2.0](https://github.com/math-comp/math-comp)
+- [Mathematical Components version ≥ 2.3.0](https://github.com/math-comp/math-comp)
 - [Finmap library version ≥ 2.1.0](https://github.com/math-comp/finmap)
 - [Hierarchy builder version ≥ 1.8.0](https://github.com/math-comp/hierarchy-builder)
 - [bigenough ≥ 1.0.0](https://github.com/math-comp/bigenough)
@@ -50,7 +50,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.1.12.0
+$ opam install coq-mathcomp-analysis.1.13.0
 ```
 4. Everytime you want to work in this same context, you need to type
 ```

README.md

@@ -26,12 +26,12 @@ In terms of [opam](https://opam.ocaml.org/doc/Install.html), it comes as the fol
 - License: [CeCILL-C](LICENSE)
 - Compatible Rocq versions: Coq 8.20, Rocq 9.0 (or dev)
 - Additional dependencies:
-  - [MathComp ssreflect 2.1.0 or later](https://math-comp.github.io)
-  - [MathComp fingroup 2.1.0 or later](https://math-comp.github.io)
-  - [MathComp algebra 2.1.0 or later](https://math-comp.github.io)
-  - [MathComp solvable 2.1.0 or later](https://math-comp.github.io)
-  - [MathComp field 2.1.0 or later](https://math-comp.github.io)
-  - [MathComp finmap 2.0.0](https://github.com/math-comp/finmap)
+  - [MathComp ssreflect 2.3.0 or later](https://math-comp.github.io)
+  - [MathComp fingroup 2.3.0 or later](https://math-comp.github.io)
+  - [MathComp algebra 2.3.0 or later](https://math-comp.github.io)
+  - [MathComp solvable 2.3.0 or later](https://math-comp.github.io)
+  - [MathComp field 2.3.0 or later](https://math-comp.github.io)
+  - [MathComp finmap 2.1.0](https://github.com/math-comp/finmap)
   - [MathComp bigenough 1.0.0](https://github.com/math-comp/bigenough)
   - [Hierarchy Builder 1.8.0 or later](https://github.com/math-comp/hierarchy-builder)
 - Coq/Rocq namespace: `mathcomp.analysis`
@@ -73,7 +73,7 @@ We try to preserve backward compatibility as best as we can.
 
 Each file is documented in its header in ASCII.
 
-[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_12_0/index.html) (using [`rocqnavi`](https://github.com/affeldt-aist/rocqnavi)).
+[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_13_0/index.html) (using [`rocqnavi`](https://github.com/affeldt-aist/rocqnavi)).
 It includes inheritance diagrams for the mathematical structures that MathComp-Analysis adds on top of MathComp's ones.
 
 Overview presentations:

classical/unstable.v

@@ -35,26 +35,12 @@ Unset Printing Implicit Defensive.
 Import Order.TTheory GRing.Theory Num.Theory.
 Local Open Scope ring_scope.
 
-(* NB: Coq 8.17.0 generalizes dependent_choice from Set to Type
-   making the following lemma redundant *)
-Section dependent_choice_Type.
-Context X (R : X -> X -> Prop).
-
-Lemma dependent_choice_Type : (forall x, {y | R x y}) ->
-  forall x0, {f | f 0%N = x0 /\ forall n, R (f n) (f n.+1)}.
-Proof.
-move=> h x0.
-set (f := fix f n := if n is n'.+1 then proj1_sig (h (f n')) else x0).
-exists f; split => //.
-intro n; induction n; simpl; apply: proj2_sig.
-Qed.
-End dependent_choice_Type.
-
 Section max_min.
 Variable R : realFieldType.
 
 Let nz2 : 2%:R != 0 :> R. Proof. by rewrite pnatr_eq0. Qed.
 
+(* NB: to appear in MathComp 2.5.0 (PR #1416) *)
 Lemma maxr_absE (x y : R) : Num.max x y = (x + y + `|x - y|) / 2%:R.
 Proof.
 apply: canRL (mulfK _) _ => //; rewrite ?pnatr_eq0//.
@@ -63,6 +49,7 @@ case: lerP => _; (* TODO: ring *) rewrite [2%:R]mulr2n mulrDr mulr1.
 by rewrite (addrC (x + y)) subrKA.
 Qed.
 
+(* NB: to appear in MathComp 2.5.0 (PR #1416) *)
 Lemma minr_absE (x y : R) : Num.min x y = (x + y - `|x - y|) / 2%:R.
 Proof.
 apply: (addrI (Num.max x y)); rewrite addr_max_min maxr_absE. (* TODO: ring *)
@@ -77,7 +64,8 @@ Section bigmax_seq.
 Context d {T : orderType d} {x : T} {I : eqType}.
 Variables (r : seq I) (i0 : I) (P : pred I).
 
-(* NB: as of [2023-08-28], bigop.leq_bigmax_seq already exists for nat *)
+(* NB: as of [2023-08-28], bigop.leq_bigmax_seq already exists for nat,
+   PRed to MathComp (PR #1449) *)
 Lemma le_bigmax_seq F :
   i0 \in r -> P i0 -> (F i0 <= \big[Order.max/x]_(i <- r | P i) F i)%O.
 Proof.
@@ -86,7 +74,8 @@ move=> /predU1P[<-|i0t]; first by rewrite Pi0 le_max// lexx.
 by case: ifPn => Ph; [rewrite le_max ih// orbT|rewrite ih].
 Qed.
 
-(* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat *)
+(* NB: as of [2023-08-28], bigop.bigmax_sup_seq already exists for nat,
+   PRed to MathComp (PR #1449) *)
 Lemma bigmax_sup_seq (m : T) (F : I -> T) :
   i0 \in r -> P i0 -> (m <= F i0)%O ->
   (m <= \big[Order.max/x]_(i <- r | P i) F i)%O.

theories/charge.v

@@ -711,7 +711,7 @@ rewrite setD0 => A0D.
 have [v [v0 Pv]] : {v : nat -> elt_type |
     v 0%N = exist _ (A0, d_ set0, A0) (And4 mA0 A0D (d_ge0 set0) A0d0) /\
     forall n, elt_rel (v n) (v n.+1)}.
-  apply: dependent_choice_Type => -[[[A' ?] U] [/= mA' A'D]].
+  apply: dependent_choice => -[[[A' ?] U] [/= mA' A'D]].
   have [A1 [mA1 A1DU A1t1]] := next_elt U.
   have A1D : A1 `<=` D by apply: (subset_trans A1DU); apply: subDsetl.
   by exists (exist _ (A1, d_ U, U `|` A1) (And4 mA1 A1D (d_ge0 U) A1t1)).
@@ -836,7 +836,7 @@ have [A0 [_ negA0 A0s0]] := next_elt set0.
 have [v [v0 Pv]] : {v |
     v 0%N = exist _ (A0, s_ set0, A0) (And3 (s_le0 set0) negA0 A0s0) /\
     forall n, elt_rel (v n) (v n.+1)}.
-  apply: dependent_choice_Type => -[[[A s] U] [/= s_le0' nsA]].
+  apply: dependent_choice => -[[[A s] U] [/= s_le0' nsA]].
   have [A' [? nsA' A's'] ] := next_elt U.
   by exists (exist _ (A', s_ U, U `|` A') (And3 (s_le0 U) nsA' A's')).
 have Ubig n : U_ (v n) = \big[setU/set0]_(i < n.+1) A_ (v i).

theories/normedtype_theory/vitali_lemma.v

@@ -443,7 +443,7 @@ have H0 : elt_prop (D0, 0%N, set0).
   - by move=> F D0F FH0; apply: maxD0 => // i Fi; exact: (FH0 _ Fi).1.
 have [v [Hv0 HvRel]] : {v : nat -> elt_type |
     v 0%N = exist _ _ H0 /\ forall n, Rel (v n) (v n.+1)}.
-  apply: dependent_choice_Type => -[[[Dn n] Un] Hn].
+  apply: dependent_choice => -[[[Dn n] Un] Hn].
   pose Hn1 := H_ n.+1 (Un `|` Dn).
   have [Dn1 maxDn1] :=
     ex_maximal_disjoint_subcollection (closure\o B) Hn1.

theories/probability.v

@@ -66,6 +66,8 @@ From mathcomp Require Import ftc gauss_integral hoelder.
 (*      normal_prob m s == normal probability measure                         *)
 (*    exponential_pdf r == pdf of the exponential distribution with rate r    *)
 (*   exponential_prob r == exponential probability measure                    *)
+(*      poisson_pmf r k == pmf of the Poisson distribution with parameter r   *)
+(*       poisson_prob r == Poisson probability measure                        *)
 (* ```                                                                        *)
 (*                                                                            *)
 (******************************************************************************)