Merge pull request #1610 from affeldt-aist/changelog1110

changelog for version 1.11.0

Author: affeldt-aist

CHANGELOG.md

@@ -1,6 +1,159 @@
 # Changelog
 
-Latest releases: [[1.10.0] - 2025-04-21](#1100---2025-04-21), [[1.9.0] - 2025-02-20](#190---2025-02-20), and [[1.8.0] - 2024-12-19](#180---2024-12-19)
+Latest releases: [[1.11.0] - 2025-05-02](#1110---2025-05-02), [[1.10.0] - 2025-04-21](#1100---2025-04-21), and [[1.9.0] - 2025-02-20](#190---2025-02-20)
+
+## [1.11.0] - 2025-05-02
+
+### Added
+
+- in `unstable.v`:
+  + lemmas `eq_exists2l`, `eq_exists2r`
+  + module `ProperNotations` with notations `++>`, `==>`, `~~>`
+
+- in `mathcomp_extra.v`:
+  + lemmas `inr_inj`, `inl_inj`
+
+- in `boolp.v`:
+  + lemmas `orW`, `or3W`, `or4W`
+
+- in `classical_sets.v`:
+  + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
+  + lemmas `inr_in_set_inl`, `inl_in_set_inl`
+  + lemmas `set_cst`, `image_nonempty`
+
+- in `functions.v`:
+  + lemma `natmulfctE`
+
+- in `constructive_ereal.v`:
+  + lemma `EFin_bigmax`
+  + lemmas `expe_ge0`, `expe_eq0`, `expe_gt0`
+
+- in `ereal.v`:
+  + lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN`
+  + lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`,
+    `ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`,
+    `ereal_sup_real`, `ereal_inf_real`
+  + lemmas `ereal_sup_cst`, `ereal_inf_cst`,
+    `ereal_sup_pZl`, `ereal_supZl`, `ereal_inf_pZl`, `ereal_infZl`
+
+- in `sequences.v`:
+  + lemmas `ereal_inf_seq`, `ereal_sup_seq`
+
+- in `realfun.v`:
+  + lemma `cvge_ninftyP`
+
+- in `exp.v`:
+  + lemma `poweRE`
+  + lemmas `lnNy`, `powR_cvg0`, `derivable_powR`, `powR_derive1`
+  + Instance `is_derive1_powR`
+
+- in `measure.v`:
+  + lemmas `mnormalize_id`, `measurable_fun_eqP`
+
+- in `lebesgue_integral_approximation.v` (now `measurable_fun_approximation.v`):
+  + lemma `measurable_prod`
+  + lemma `measurable_fun_lte`
+  + lemma `measurable_fun_lee`
+  + lemma `measurable_fun_eqe`
+  + lemma `measurable_poweR`
+
+- in `ftc.v`:
+  + lemma `integrable_locally`
+
+- in `probability.v`:
+  + lemmas `eq_bernoulli`, `eq_bernoulliV2`
+
+### Changed
+
+- in `pi_irrational`:
+  + definition `rational`
+
+### Renamed
+
+- in `kernel.v`:
+  + `isFiniteTransition` -> `isFiniteTransitionKernel`
+
+- in `ereal.v`:
+  + `ereal_sup_le` -> `ereal_sup_ge`
+
+- in `pseudometric_normed_Zmodule.v`:
+  + `opp_continuous` -> `oppr_continuous`
+
+- in `lebesgue_integral_approximation.v` (now `measurable_fun_approximation.v`):
+  + `emeasurable_fun_lt` -> `measurable_lte`
+  + `emeasurable_fun_le` -> `measurable_lee`
+  + `emeasurable_fun_eq` -> `measurable_lee`
+  + `emeasurable_fun_neq` -> `measurable_neqe`
+
+- file `lebesgue_integral_approximation.v` -> `measurable_fun_approximation.v`
+
+### Generalized
+
+- in `functions.v`:
+  + `fct_sumE`, `addrfctE`, `sumrfctE` (from `zmodType` to `nmodType`)
+  + `scalerfctE` (from `pointedType` to `Type`)
+
+- in `normedtype.v`:
+  + lemmas `gt0_cvgMlNy`, `gt0_cvgMly`
+
+- in `measurable_realfun.v`
+  + lemma `measurable_ln`
+
+### Removed
+
+- in `functions.v`:
+  + definitions `fct_ringMixin`, `fct_ringMixin` (was only used in an `HB.instance`)
+
+- in `constructive_ereal.v`:
+  + notations `esum_ninftyP`, `esum_ninfty`, `esum_pinftyP`, `esum_pinfty` (deprecated since 0.6.0)
+
+- in `pseudometric_structure.v`:
+  + notations `cvg_ballPpos`, `app_cvg_locally` (deprecated since 0.6.0)
+
+- in `product_topology.v`:
+  + notation `compact_setM` (deprecated since 0.6.0)
+
+- in `separation_axioms.v`:
+  + notations `cvg_map_lim`, `cvgi_map_lim` (deprecated since 0.6.6)
+
+- in `sequences.v`:
+  + notation `nonincreasing_cvg_ge` (deprecated since 0.6.6)
+  + notation `nondecreasing_cvg_le` (deprecated since 0.6.6)
+  + notations `nonincreasing_cvg`, `nondecreasing_cvg`, `nonincreasing_is_cvg`,
+    `nondecreasing_is_cvg`, `nondecreasing_dvg_lt`, `near_nondecreasing_is_cvg`,
+    `near_nonincreasing_is_cvg` (deprecated since 0.6.6)
+  + notation `ereal_nondecreasing_opp` (deprecated since 0.6.6)
+  + notations `ereal_nondecreasing_cvg`, `ereal_nondecreasing_is_cvg`, `ereal_nonincreasing_cvg`,
+    `ereal_nonincreasing_is_cvg` (deprecated since 0.6.6)
+  + notations `lim_sup`, `lim_inf`, `lim_infN`, `lim_supE`, `lim_infE`, `lim_inf_le_lim_sup`,
+    `cvg_lim_infE`, `cvg_lim_supE`, `le_lim_supD`, `le_lim_infD`, `lim_supD`, `lim_infD`
+  + notations `lim_einf_shift`, `lim_esup_le_cvg`, `lim_einfN`, `lim_esupN`, `lim_einf_sup`,
+    `cvgNy_lim_einf_sup`, `cvg_lim_einf_sup`, `is_cvg_lim_einfE`, `is_cvg_lim_esupE`
+
+- in `exp.v`:
+  + notation `gt0_ler_powR` (deprecated since 0.6.5)
+
+- in `measure.v`:
+  + notation `measurable_fun_ext` (deprecated since 0.6.2)
+  + notations `measurable_fun_id`, `measurable_fun_cst`, `measurable_fun_comp` (deprecated since 0.6.3)
+  + notation `measurable_funT_comp` (deprecated since 0.6.3)
+
+- in `measurable_realfun.v`:
+  + notation `measurable_fun_ln` (deprecated since 0.6.3)
+  + notations `emeasurable_itv_bnd_pinfty`, `emeasurable_itv_ninfty_bnd` (deprecated since 0.6.2)
+  + notation `measurable_fun_lim_sup` (deprecated since 0.6.6)
+  + notation `measurable_fun_max` (deprecated since 0.6.3)
+  + notation `measurable_fun_er_map` (deprecated since 0.6.3)
+  + notations `emeasurable_funN`, `emeasurable_fun_max`, `emeasurable_fun_min`,
+    `emeasurable_fun_funepos`, `emeasurable_fun_funeneg` (deprecated since 0.6.3)
+  + notation `measurable_fun_lim_esup` (deprecated since 0.6.6)
+
+- in `lebesgue_integral_nonneg.v`:
+  + notations `ge0_integralM_EFin`, `ge0_integralM`, `integralM_indic`, `integralM_indic_nnsfun`
+    (deprecated since 0.6.4)
+
+- in `lebesgue_integrable.v`:
+  + notation `integralM` (deprecated since 0.6.4)
 
 ## [1.10.0] - 2025-04-21
 

CHANGELOG_UNRELEASED.md

@@ -4,125 +4,16 @@
 
 ### Added
 
-- in `probability.v`:
-  + lemmas `eq_bernoulli`, `eq_bernoulliV2`
-
-- in `measure.v`:
-  + lemmas `mnormalize_id`, `measurable_fun_eqP`
-
-- in `ftc.v`:
-  + lemma `integrable_locally`
-
-- in `constructive_ereal.v`:
-  + lemma `EFin_bigmax`
-
-- in `mathcomp_extra.v`:
-  + lemmas `inr_inj`, `inl_inj`
-
-- in `classical_sets.v`:
-  + lemmas `in_set1`, `inr_in_set_inr`, `inl_in_set_inr`, `mem_image`, `mem_range`, `image_f`
-  + lemmas `inr_in_set_inl`, `inl_in_set_inl`
-
-- in `lebesgue_integral_approximation.v` (now `measurable_fun_approximation.v`):
-  + lemma `measurable_prod`
-  + lemma `measurable_fun_lte`
-  + lemma `measurable_fun_lee`
-  + lemma `measurable_fun_eqe`
-  + lemma `measurable_poweR`
-
-- in `exp.v`:
-  + lemma `poweRE`
-
-- in `exp.v`:
-  + lemmas `lnNy`, `powR_cvg0`, `derivable_powR`, `powR_derive1`
-  + Instance `is_derive1_powR`
-- in `realfun.v`:
-  + lemma `cvge_ninftyP`
-
-- in `boolp.v`:
-  + lemmas `orW`, `or3W`, `or4W`
-  
-- in `classical_sets.v`:
-  + lemmas `set_cst`, `image_nonempty`
-
-- in `unstable.v`:
-  + lemmas `eq_exists2l`, `eq_exists2r`
-  + module `ProperNotations` with notations `++>`, `==>`, `~~>`
-- in `functions.v`:
-  + lemma `natmulfctE`
-
-- in `ereal.v`:
-  + lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN`
-  + lemmas `ereal_supP`, `ereal_infP`, `ereal_sup_gtP`, `ereal_inf_ltP`,
-    `ereal_inf_leP`, `ereal_sup_geP`, `lb_ereal_infNy_adherent`,
-    `ereal_sup_real`, `ereal_inf_real`
-- in `constructive_ereal.v`:
-  + lemmas `expe_ge0`, `expe_eq0`, `expe_gt0`
-
-- in `ereal.v`:
-  + lemmas `ereal_sup_cst`, `ereal_inf_cst`,
-    `ereal_sup_pZl`, `ereal_supZl`, `ereal_inf_pZl`, `ereal_infZl`
-
-- in `sequences.v`:
-  + lemmas `ereal_inf_seq`, `ereal_sup_seq`
-
 ### Changed
 
-- in `pi_irrational`:
-  + definition `rational`
-
 ### Renamed
 
-- in `kernel.v`:
-  + `isFiniteTransition` -> `isFiniteTransitionKernel`
-
-- in `lebesgue_integral_approximation.v`:
-  + `emeasurable_fun_lt` -> `measurable_lte`
-  + `emeasurable_fun_le` -> `measurable_lee`
-  + `emeasurable_fun_eq` -> `measurable_lee`
-  + `emeasurable_fun_neq` -> `measurable_neqe`
-
-- file `lebesgue_integral_approximation.v` -> `measurable_fun_approximation.v`
-
-- in `ereal.v`:
-  + `ereal_sup_le` -> `ereal_sup_ge`
-
-- in `pseudometric_normed_Zmodule.v`:
-  + `opp_continuous` -> `oppr_continuous`
-
 ### Generalized
 
-- in `normedtype.v`:
-  + lemmas `gt0_cvgMlNy`, `gt0_cvgMly`
-- in `functions.v`:
-  + `fct_sumE`, `addrfctE`, `sumrfctE` (from `zmodType` to `nmodType`)
-  + `scalerfctE` (from `pointedType` to `Type`)
-
-- in `measurable_realfun.v`
-  + lemma `measurable_ln`
-
 ### Deprecated
 
 ### Removed
 
-- in `functions.v`:
-  + definitions `fct_ringMixin`, `fct_ringMixin` (was only used in an `HB.instance`)
-
-- in `measurable_realfun.v`:
-  + notation `measurable_fun_ln` (deprecated since 0.6.3)
-  + notations `emeasurable_itv_bnd_pinfty`, `emeasurable_itv_ninfty_bnd` (deprecated since 0.6.2)
-  + notation `measurable_fun_lim_sup` (deprecated since 0.6.6)
-  + notation `measurable_fun_max` (deprecated since 0.6.3)
-  + notation `measurable_fun_er_map` (deprecated since 0.6.3)
-  + notations `emeasurable_funN`, `emeasurable_fun_max`, `emeasurable_fun_min`,
-    `emeasurable_fun_funepos`, `emeasurable_fun_funeneg` (deprecated since 0.6.3)
-  + notation `measurable_fun_lim_esup` (deprecated since 0.6.6)
-
-- in `measure.v`:
-  + notation `measurable_fun_ext` (deprecated since 0.6.2)
-  + notations `measurable_fun_id`, `measurable_fun_cst`, `measurable_fun_comp` (deprecated since 0.6.3)
-  + notation `measurable_funT_comp` (deprecated since 0.6.3)
-
 ### Infrastructure
 
 ### Misc

INSTALL.md

@@ -48,7 +48,7 @@ $ opam install coq-mathcomp-analysis
 ```
 To install a precise version, type, say
 ```
-$ opam install coq-mathcomp-analysis.1.9.0
+$ opam install coq-mathcomp-analysis.1.11.0
 ```
 4. Everytime you want to work in this same context, you need to type
 ```
@@ -88,7 +88,7 @@ $ opam install coq-mathcomp-field.2.3.0
 ```
 3. Install the Finite maps library
 ```
-$ opam install coq-mathcomp-finmap.2.1.0
+$ opam install coq-mathcomp-finmap.2.2.0
 ```
 4. Install the Hierarchy Builder
 ```

README.md

@@ -77,7 +77,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_10_0/index.html) (using a fork of [`coq2html`](https://github.com/xavierleroy/coq2html)).
+[HTML rendering of the source code](https://math-comp.github.io/analysis/htmldoc_1_11_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:
@@ -92,13 +92,16 @@ Publications about MathComp-Analysis:
 - [Measure Construction by Extension in Dependent Type Theory with Application to Integration](https://arxiv.org/pdf/2209.02345.pdf) (2023) doi:[10.1007/s10817-023-09671-5](https://doi.org/10.1007/s10817-023-09671-5)
 - [The Radon-Nikodým Theorem and the Lebesgue-Stieltjes Measure in Coq](https://www.jstage.jst.go.jp/article/jssst/41/2/41_2_41/_pdf/-char/en) (2024) doi:[10.11309/jssst.41.2_41](https://doi.org/10.11309/jssst.41.2_41)
 - [A Comprehensive Overview of the Lebesgue Differentiation Theorem in Coq](https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.5/LIPIcs.ITP.2024.5.pdf) (2024) doi:[10.4230/LIPIcs.ITP.2024.5](https://doi.org/10.4230/LIPIcs.ITP.2024.5)
+- [Prouver que pi est irrationnel avec MathComp-Analysis](https://hal.science/hal-04859455/document) (2025)
 
 Other work using MathComp-Analysis:
 - [A Formal Classical Proof of Hahn-Banach in Coq](https://lipn.univ-paris13.fr/~kerjean/slides/slidesTYPES19.pdf) (2019)
 - [Semantics of Probabilistic Programs using s-Finite Kernels in Coq](https://hal.inria.fr/hal-03917948/document) (2023)
 - [CoqQ: Foundational Verification of Quantum Programs](https://arxiv.org/pdf/2207.11350.pdf) (2023)
 - [Experimenting with an intrinsically-typed probabilistic programming language in Coq](https://staff.aist.go.jp/reynald.affeldt/documents/syntax-aplas2023.pdf) (2023)
 - [Taming Differentiable Logics with Coq Formalisation](https://drops.dagstuhl.de/storage/00lipics/lipics-vol309-itp2024/LIPIcs.ITP.2024.4/LIPIcs.ITP.2024.4.pdf) (2024)
+- [Décomposition Algébrique Cylindrique en Coq/Rocq](https://inria.hal.science/hal-04859512/document) (2025)
+- [Semantics of Probabilistic Programs using s-Finite Kernels in Dependent Type Theory](https://dl.acm.org/doi/pdf/10.1145/3732291) (2025)
 
 ## Development information
 

reals/constructive_ereal.v

@@ -1180,15 +1180,6 @@ move=> fio; apply/idP/existsP => [/eqP /=|[/= i /andP[Pi /eqP fi]]].
 by apply/eqP/esum_eqyP => //; exists i.
 Qed.
 
-#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNyP`")]
-Notation esum_ninftyP := esum_eqNyP (only parsing).
-#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqNy`")]
-Notation esum_ninfty := esum_eqNy (only parsing).
-#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqyP`")]
-Notation esum_pinftyP := esum_eqyP (only parsing).
-#[deprecated(since="mathcomp-analysis 0.6.0", note="renamed `esum_eqy`")]
-Notation esum_pinfty := esum_eqy (only parsing).
-
 Lemma adde_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
 Proof. by move: x y => [r0| |] [r1| |] // ? ?; rewrite !lee_fin addr_ge0. Qed.
 

theories/exp.v

@@ -1108,9 +1108,6 @@ Qed.
 End PowR.
 Notation "a `^ x" := (powR a x) : ring_scope.
 
-#[deprecated(since="mathcomp-analysis 0.6.5", note="renamed `ge0_ler_powR`")]
-Notation gt0_ler_powR := ge0_ler_powR.
-
 Section poweR.
 Local Open Scope ereal_scope.
 Context {R : realType}.

theories/ftc.v

@@ -1648,7 +1648,7 @@ rewrite (@increasing_ge0_integration_by_substitutiony (\- (F \o -%R))%R); last 8
   by apply: funext => r/=; rewrite fctE opprK.
 - apply/continuous_within_itvcyP; split.
     move=> x; rewrite in_itv/= opprK andbT => Fbx.
-    apply: continuous_comp; first exact: opp_continuous.
+    apply: continuous_comp; first exact: oppr_continuous.
     by apply: cG; rewrite in_itv/= ltrNl.
   by rewrite /= !opprK; exact/cvg_at_leftNP.
 - move=> z; rewrite in_itv/= opprK andbT => Fbz.

theories/lebesgue_integral_theory/lebesgue_integrable.v

@@ -519,8 +519,6 @@ Lemma integralZr r :
 Proof. by rewrite muleC -integralZl; under eq_integral do rewrite muleC. Qed.
 
 End integralZl.
-#[deprecated(since="mathcomp-analysis 0.6.4", note="use `integralZl` instead")]
-Notation integralM := integralZl (only parsing).
 
 Section integralD_EFin.
 Local Open Scope ereal_scope.