hoeffding's inequality lemma definition

.github/workflows/generate_docs.yml

@@ -38,7 +38,7 @@ jobs:
         run: opam install -y --deps-only . && opam exec -- make -j 4
 
       - name: Install Rocqnavi
-        run: opam install -y rocq-navi
+        run: opam install -y rocq-navi.0.3.1
 
       - name: Generate Documents
         run: |

.nix/config.nix

@@ -45,21 +45,24 @@ in {
 
   ## select an entry to build in the following `bundles` set
   ## defaults to "default"
-  default-bundle = "8.20-2.4.0";
+  default-bundle = "9.0";
 
   ## write one `bundles.name` attribute set per
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
 
-  bundles."8.20-2.3.0".coqPackages = common-bundle // {
+  bundles."8.20-2.4.0".coqPackages = common-bundle // {
     coq.override.version = "8.20";
-    mathcomp.override.version = "2.3.0";
+    mathcomp.override.version = "2.4.0";
   };
 
-  bundles."8.20-2.4.0".coqPackages = common-bundle // {
+  bundles."8.20-master".coqPackages = common-bundle // {
     coq.override.version = "8.20";
-    mathcomp.override.version = "2.4.0";
+    mathcomp.override.version = "master";
+    mathcomp-bigenough.override.version = "master";
+    mathcomp-finmap.override.version = "master";
+    ssprove.job = false;
   };
 
   bundles."9.0" = {

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,92 +4,86 @@
 
 ### 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 `constructive_ereal.v`:
+  + lemma `ltgte_fin_num`
 
-- in `functions.v`:
-  + lemmas `fct_prodE`, `prodrfctE`
+- in `probability.v`:
+  + lemmas `cdf_fin_num`, `lebesgue_stieltjes_cdf_id`
 
-- in `exp.v`:
-  + lemma `norm_expR`
+- in `num_normedtype.v`:
+  + lemma `nbhs_infty_gtr`
+- in `function_spaces.v`:
+  + lemmas `cvg_big`, `continuous_big`
 
-- in `hoelder.v`
-  + lemma `hoelder_conj_ge1`
+- in `realfun.v`:
+  + lemma `cvg_addrl_Ny`
 
-- in `reals.v`:
-  + definition `irrational`
-  + lemmas `irrationalE`, `rationalP` 
+- in `constructive_ereal.v`:
+  + lemmas `mule_natr`, `dmule_natr`
+  + lemmas `inve_eqy`, `inve_eqNy`
 
-- in `topology_structure.v`:
-  + lemmas `denseI`, `dense0`
+- in `uniform_structure.v`:
+  + lemma `continuous_injective_withinNx`
 
+- in `constructive_ereal.v`:
+  + variants `Ione`, `Idummy_placeholder`
+  + inductives `Inatmul`, `IEFin`
+  + definition `parse`, `print`
+  + number notations in scopes `ereal_dual_scope` and `ereal_scope`
+  + notation `- 1` in scopes `ereal_dual_scope` and `ereal_scope`
 - 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`
+  + lemma `le0_ball0`
+- in `theories/landau.v`:
+  + lemma `littleoE0`
 
 - 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`
+  + lemma `lt0_adde`
 
-### Changed
+- in `unstable.v`
+  + lemmas `coprime_prodr`, `Gauss_dvd_prod`, `expn_prod`, `mono_leq_infl`,
+    `card_big_setU`
 
-- moved from `pi_irrational.v` to `reals.v` and changed
-  + definition `rational`
+- file `pnt.v`
+  + definitions `next_prime`, `prime_seq`
+  + lemmas `leq_prime_seq`, `mem_prime_seq`
+  + theorem `dvg_sum_inv_prime_seq`
 
-- 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`
+### Changed
 
-### Renamed
+- in `lebesgue_stieltjes_measure.v` specialized from `numFieldType` to `realFieldType`:
+  + lemma `nondecreasing_right_continuousP` 
+  + definition `CumulativeBounded`
 
-- in `lebesgue_stieltjes_measure.v`:
-  + `cumulativeNy0` -> `cumulativeNy`
-  + `cumulativey1` -> `cumulativey`
+- in `lebesgue_stieltjes_measure.v`, according to generalization of `Cumulative`, modified:
+  + lemmas `wlength_ge0`, `cumulative_content_sub_fsum`, `wlength_sigma_subadditive`, `lebesgue_stieltjes_measure_unique`
+  + definitions `lebesgue_stieltjes_measure`, `completed_lebesgue_stieltjes_measure`
 
-- in `exp.v`:
-  + `ltr_expeR` -> `lte_expeR`
-  + `ler_expeR` -> `lee_expeR`
+- moved from `vitali_lemma.v` to `pseudometric_normed_Zmodule.v` and renamed:
+  + `closure_ball` -> `closure_ballE`
 
-- in `derive.v`:
-  + `derivemxE` -> `deriveEjacobian`
+### Renamed
 
 ### Generalized
 
-- in `functions.v`
-  + lemma `fct_sumE` (from a pointwise equality to a functional one)
+- in `pseudometric_normed_Zmodule.v`:
+  + lemma `closed_ball0` (`realFieldType` -> `pseudoMetricNormedZmodType`)
+  + lemmas `closed_ball_closed`, `subset_closed_ball` (`realFieldType` -> `numDomainType`)
+  + lemma `subset_closure_half` (`realFieldType` -> `numFieldType`)
+  + lemma `le_closed_ball` (`pseudoMetricNormedZmodType` -> `pseudoMetricType`)
+
+- in `lebesgue_stieltjes_measure.v` generalized (codomain is now an `orderNbhsType`):
+  + lemma `right_continuousW`
+  + record `isCumulative`
+  + definition `Cumulative`
 
 ### Deprecated
 
 ### Removed
 
-- file `forms.v` (superseded by MathComp's `sesquilinear.v`)
+- file `interval_inference.v` (now in MathComp)
+
+- in file `all_reals.v`
+  + export of `interval_inference` (now in mathcomp-algebra, but not automatically exported)
 
 ### Infrastructure
 

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.4.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
 ```
@@ -73,7 +73,7 @@ using [proof general for emacs](https://github.com/ProofGeneral/PG)
 
 ## Break-down of phase 3 of the installation procedure step by step
 
-With the example of Coq 8.20.1 and MathComp 2.3.0. For other versions, update the
+With the example of Coq 8.20.1 and MathComp 2.4.0. For other versions, update the
 version numbers accordingly.
 
 1. Install Coq 8.20.1
@@ -82,11 +82,11 @@ $ opam install coq.8.20.1
 ```
 2. Install the Mathematical Components
 ```
-$ opam install coq-mathcomp-ssreflect.2.3.0
-$ opam install coq-mathcomp-fingroup.2.3.0
-$ opam install coq-mathcomp-algebra.2.3.0
-$ opam install coq-mathcomp-solvable.2.3.0
-$ opam install coq-mathcomp-field.2.3.0
+$ opam install coq-mathcomp-ssreflect.2.4.0
+$ opam install coq-mathcomp-fingroup.2.4.0
+$ opam install coq-mathcomp-algebra.2.4.0
+$ opam install coq-mathcomp-solvable.2.4.0
+$ opam install coq-mathcomp-field.2.4.0
 ```
 3. Install the Finite maps library
 ```