From ca199a0212e5fe5b5d0b97d25f6afd5f04b44a2b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 4 Mar 2026 15:27:56 +0900 Subject: [PATCH 1/3] mv function_spaces - fixes #1844 --- CHANGELOG_UNRELEASED.md | 2 ++ _CoqProject | 2 +- theories/Make | 2 +- theories/{ => topology_theory}/function_spaces.v | 6 +++++- theories/topology_theory/topology.v | 1 + 5 files changed, 10 insertions(+), 3 deletions(-) rename theories/{ => topology_theory}/function_spaces.v (99%) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f4a1cc4dfd..4790799c00 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -204,6 +204,8 @@ - moved from `measurable_structure.v` to `classical_sets.v`: + definitions `setI_closed`, `setU_closed` +- moved from `theories` to `theories/topology_theory` + ### Renamed - in `topology_structure.v` diff --git a/_CoqProject b/_CoqProject index fdbf17db9c..44d0d98520 100644 --- a/_CoqProject +++ b/_CoqProject @@ -67,13 +67,13 @@ theories/topology_theory/sigT_topology.v theories/topology_theory/discrete_topology.v theories/topology_theory/separation_axioms.v theories/topology_theory/metric_structure.v +theories/topology_theory/function_spaces.v theories/homotopy_theory/homotopy.v theories/homotopy_theory/wedge_sigT.v theories/homotopy_theory/continuous_path.v theories/ess_sup_inf.v -theories/function_spaces.v theories/cantor.v theories/tvs.v diff --git a/theories/Make b/theories/Make index ea73a4022f..9c1128c724 100644 --- a/theories/Make +++ b/theories/Make @@ -33,13 +33,13 @@ topology_theory/sigT_topology.v topology_theory/discrete_topology.v topology_theory/separation_axioms.v topology_theory/metric_structure.v +topology_theory/function_spaces.v homotopy_theory/homotopy.v homotopy_theory/wedge_sigT.v homotopy_theory/continuous_path.v ess_sup_inf.v -function_spaces.v cantor.v tvs.v diff --git a/theories/function_spaces.v b/theories/topology_theory/function_spaces.v similarity index 99% rename from theories/function_spaces.v rename to theories/topology_theory/function_spaces.v index dabd225b1d..d8605bc443 100644 --- a/theories/function_spaces.v +++ b/theories/topology_theory/function_spaces.v @@ -6,7 +6,11 @@ From mathcomp Require Import generic_quotient. From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals interval_inference. -From mathcomp Require Import topology. +From mathcomp Require Import topology_structure uniform_structure. +From mathcomp Require Import supremum_topology initial_topology. +From mathcomp Require Import pseudometric_structure separation_axioms. +From mathcomp Require Import compact connected subspace_topology. +From mathcomp Require Import product_topology. (**md**************************************************************************) (* # The topology of functions spaces *) diff --git a/theories/topology_theory/topology.v b/theories/topology_theory/topology.v index aae6eab62d..066275d4e7 100644 --- a/theories/topology_theory/topology.v +++ b/theories/topology_theory/topology.v @@ -20,3 +20,4 @@ From mathcomp Require Export sigT_topology. From mathcomp Require Export discrete_topology. From mathcomp Require Export separation_axioms. From mathcomp Require Export metric_structure. +From mathcomp Require Export function_spaces. From 775fdbd30555648ab347ed217fb4077ad523a4d9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 4 Mar 2026 16:59:30 +0900 Subject: [PATCH 2/3] fix --- theories/all_analysis.v | 1 - theories/borel_hierarchy.v | 3 ++- theories/cantor.v | 7 +++---- theories/charge.v | 8 ++++---- theories/ess_sup_inf.v | 3 ++- theories/ftc.v | 10 +++++----- theories/gauss_integral.v | 10 ++++++---- theories/hoelder.v | 13 +++++++------ theories/homotopy_theory/continuous_path.v | 6 +++--- theories/homotopy_theory/wedge_sigT.v | 5 +++-- theories/kernel.v | 11 ++++++----- .../lebesgue_Rintegral.v | 16 +++++++--------- .../lebesgue_integrable.v | 11 +++++------ .../lebesgue_integral_definition.v | 11 ++++++----- .../lebesgue_integral_differentiation.v | 16 +++++++--------- .../lebesgue_integral_dominated_convergence.v | 16 +++++++--------- .../lebesgue_integral_fubini.v | 13 ++++++------- .../lebesgue_integral_monotone_convergence.v | 11 +++++------ .../lebesgue_integral_nonneg.v | 11 +++++------ .../lebesgue_integral_under.v | 15 +++++++-------- .../measurable_fun_approximation.v | 11 +++++------ .../lebesgue_integral_theory/simple_functions.v | 11 +++++------ theories/lebesgue_measure.v | 15 +++++++-------- theories/measurable_realfun.v | 12 +++++------- theories/normedtype_theory/matrix_normedtype.v | 9 +++++---- theories/normedtype_theory/normed_module.v | 5 ++--- theories/normedtype_theory/num_normedtype.v | 9 ++++----- .../pseudometric_normed_Zmodule.v | 7 +++---- theories/normedtype_theory/urysohn.v | 10 +++++----- theories/normedtype_theory/vitali_lemma.v | 10 +++++----- theories/numfun.v | 8 ++++---- theories/pi_irrational.v | 8 +++++--- .../probability_theory/bernoulli_distribution.v | 4 ++-- theories/probability_theory/beta_distribution.v | 10 +++++----- .../probability_theory/binomial_distribution.v | 4 ++-- .../exponential_distribution.v | 4 ++-- .../probability_theory/normal_distribution.v | 3 ++- .../probability_theory/poisson_distribution.v | 3 ++- theories/probability_theory/random_variable.v | 8 ++++---- .../probability_theory/uniform_distribution.v | 8 ++++---- theories/tvs.v | 4 ++-- 41 files changed, 176 insertions(+), 184 deletions(-) diff --git a/theories/all_analysis.v b/theories/all_analysis.v index 9043f05ae0..cc3cf0470c 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -1,7 +1,6 @@ From mathcomp Require Export ereal. From mathcomp Require Export landau. From mathcomp Require Export topology. -From mathcomp Require Export function_spaces. From mathcomp Require Export cantor. From mathcomp Require Export prodnormedzmodule. From mathcomp Require Export normedtype. diff --git a/theories/borel_hierarchy.v b/theories/borel_hierarchy.v index 943d564a30..d77658a42a 100644 --- a/theories/borel_hierarchy.v +++ b/theories/borel_hierarchy.v @@ -1,7 +1,8 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals topology normedtype sequences. -From mathcomp Require Import measure lebesgue_measure. +From mathcomp Require Import measure lebesgue_measure measurable_realfun. (**md**************************************************************************) (* # Basic facts about G-delta and F-sigma sets *) diff --git a/theories/cantor.v b/theories/cantor.v index 6c1b71b4fb..eee56e3f02 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -1,10 +1,9 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum interval rat. -From mathcomp Require Import finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrint ssrnum interval. +From mathcomp Require Import rat finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals. -From mathcomp Require Import topology function_spaces. +From mathcomp Require Import cardinality reals topology. (**md**************************************************************************) (* # The Cantor Space and Applications *) diff --git a/theories/charge.v b/theories/charge.v index 6d0327c0d1..30e2018070 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1,13 +1,13 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. -From mathcomp Require Import finmap fingroup perm rat. +From mathcomp Require Import interval_inference finmap fingroup perm rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality. -From mathcomp Require Import functions fsbigop set_interval reals. -From mathcomp Require Import interval_inference ereal topology numfun. -From mathcomp Require Import normedtype derive sequences esum measure realfun. +From mathcomp Require Import functions fsbigop set_interval reals ereal. +From mathcomp Require Import topology numfun normedtype derive sequences esum. +From mathcomp Require Import measure realfun measurable_realfun. From mathcomp Require Import lebesgue_measure lebesgue_integral. (**md**************************************************************************) diff --git a/theories/ess_sup_inf.v b/theories/ess_sup_inf.v index 9a59ef894e..b6d3354f61 100644 --- a/theories/ess_sup_inf.v +++ b/theories/ess_sup_inf.v @@ -1,8 +1,9 @@ +(* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat all_algebra. From mathcomp Require Import boolp classical_sets functions cardinality. From mathcomp Require Import reals ereal topology normedtype sequences. -From mathcomp Require Import measure lebesgue_measure. +From mathcomp Require Import measure lebesgue_measure measurable_realfun. (**md**************************************************************************) (* # Essential infimum and essential supremum *) diff --git a/theories/ftc.v b/theories/ftc.v index b05e71287c..7b916e2efc 100644 --- a/theories/ftc.v +++ b/theories/ftc.v @@ -1,13 +1,13 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference finmap archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. -From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import esum measure lebesgue_measure numfun realfun. +From mathcomp Require Import cardinality fsbigop reals ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. From mathcomp Require Import interval_inference real_interval lebesgue_integral. From mathcomp Require Import derive charge. diff --git a/theories/gauss_integral.v b/theories/gauss_integral.v index 6fe6eea0f0..a5ef8500ff 100644 --- a/theories/gauss_integral.v +++ b/theories/gauss_integral.v @@ -1,11 +1,13 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import esum measure lebesgue_measure numfun realfun. -From mathcomp Require Import exp trigo lebesgue_integral derive charge ftc. +From mathcomp Require Import esum measure measurable_realfun numfun realfun. +From mathcomp Require Import exp trigo lebesgue_measure lebesgue_integral. +From mathcomp Require Import derive ftc. (**md**************************************************************************) (* # Gauss integral *) @@ -384,7 +386,7 @@ rewrite ge0_symfun_integralT//=. - by move=> x/=; rewrite /gauss_fun sqrrN. Qed. -Lemma integrableT_gauss : mu.-integrable setT (EFin \o gauss_fun). +Lemma integrableT_gauss : mu.-integrable [set: R] (EFin \o gauss_fun). Proof. apply/integrableP; split. by apply/measurable_EFinP/measurable_funTS; exact: measurable_gauss_fun. diff --git a/theories/hoelder.v b/theories/hoelder.v index 49597c32e4..096f55960b 100644 --- a/theories/hoelder.v +++ b/theories/hoelder.v @@ -1,13 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp interval_inference. -From mathcomp Require Import classical_sets functions cardinality fsbigop reals. -From mathcomp Require Import ereal topology normedtype sequences real_interval. -From mathcomp Require Import esum measure ess_sup_inf lebesgue_measure. -From mathcomp Require Import lebesgue_integral numfun exp convex. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality convex fsbigop reals ereal topology. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import ess_sup_inf measurable_realfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral numfun exp. (**md**************************************************************************) (* # Hoelder's Inequality *) diff --git a/theories/homotopy_theory/continuous_path.v b/theories/homotopy_theory/continuous_path.v index c52f68bf52..5cf26c8d56 100644 --- a/theories/homotopy_theory/continuous_path.v +++ b/theories/homotopy_theory/continuous_path.v @@ -1,9 +1,9 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra finmap generic_quotient. +From mathcomp Require Import all_ssreflect_compat generic_quotient all_algebra. +From mathcomp Require Import finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals topology. -From mathcomp Require Import function_spaces wedge_sigT. +From mathcomp Require Import cardinality fsbigop reals topology wedge_sigT. (**md**************************************************************************) (* # Paths *) diff --git a/theories/homotopy_theory/wedge_sigT.v b/theories/homotopy_theory/wedge_sigT.v index 698ea5c6ef..1864434e50 100644 --- a/theories/homotopy_theory/wedge_sigT.v +++ b/theories/homotopy_theory/wedge_sigT.v @@ -1,10 +1,11 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat all_algebra finmap generic_quotient. +From mathcomp Require Import all_ssreflect_compat all_algebra generic_quotient. +From mathcomp Require Import finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals topology function_spaces. +From mathcomp Require Import cardinality fsbigop reals topology. (**md**************************************************************************) (* # wedge sum for sigT *) diff --git a/theories/kernel.v b/theories/kernel.v index 6e066bcf6f..777a5f90a3 100644 --- a/theories/kernel.v +++ b/theories/kernel.v @@ -1,11 +1,12 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality fsbigop reals interval_inference ereal. -From mathcomp Require Import topology normedtype sequences esum measure. -From mathcomp Require Import numfun lebesgue_measure lebesgue_integral. +From mathcomp Require Import cardinality fsbigop reals ereal topology. +From mathcomp Require Import normedtype sequences esum measure. +From mathcomp Require Import measurable_realfun numfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral. (**md**************************************************************************) (* # Kernels *) diff --git a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v index f6bb55a805..a01b70628f 100644 --- a/theories/lebesgue_integral_theory/lebesgue_Rintegral.v +++ b/theories/lebesgue_integral_theory/lebesgue_Rintegral.v @@ -1,17 +1,15 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. -From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import function_spaces esum measure lebesgue_measure. -From mathcomp Require Import numfun realfun simple_functions. -From mathcomp Require Import measurable_fun_approximation. +From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. +From mathcomp Require Import simple_functions measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. -From mathcomp Require Import lebesgue_integral_nonneg. -From mathcomp Require Import lebesgue_integrable. +From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. From mathcomp Require Import lebesgue_integral_dominated_convergence. (**md**************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_integrable.v b/theories/lebesgue_integral_theory/lebesgue_integrable.v index 4946a51a3b..06f888196c 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integrable.v +++ b/theories/lebesgue_integral_theory/lebesgue_integrable.v @@ -1,15 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import archimedean interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference. -From mathcomp Require Import topology ereal tvs normedtype sequences. -From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. -From mathcomp Require Import measurable_fun_approximation. +From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. From mathcomp Require Import lebesgue_integral_nonneg. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v index 75158186fa..4ac6ad27de 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_definition.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_definition.v @@ -1,13 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference. -From mathcomp Require Import ereal topology tvs normedtype sequences. -From mathcomp Require Import real_interval esum measure lebesgue_measure numfun. -From mathcomp Require Import realfun function_spaces simple_functions. +From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. +From mathcomp Require Import measurable_realfun. (**md**************************************************************************) (* # Definition of the Lebesgue integral *) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v index 0973c75e07..40a6e076d0 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v @@ -1,17 +1,15 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. -From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import esum function_spaces measure lebesgue_measure. -From mathcomp Require Import numfun realfun simple_functions. -From mathcomp Require Import measurable_fun_approximation. +From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. +From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. -From mathcomp Require Import lebesgue_integral_nonneg. -From mathcomp Require Import lebesgue_integrable. +From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. From mathcomp Require Import lebesgue_integral_dominated_convergence. From mathcomp Require Import lebesgue_Rintegral. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v index 7857df2ea7..b261fbd1da 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v @@ -1,17 +1,15 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. -From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import function_spaces esum measure lebesgue_measure. -From mathcomp Require Import numfun realfun simple_functions. -From mathcomp Require Import measurable_fun_approximation. +From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. +From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. -From mathcomp Require Import lebesgue_integral_nonneg. -From mathcomp Require Import lebesgue_integrable. +From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. (**md**************************************************************************) (* # Dominated Convergence Theorem for the Lebesgue Integral *) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v index 199f1def82..a6fa005408 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_fubini.v @@ -1,13 +1,12 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. -From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import esum measure lebesgue_measure numfun realfun. -From mathcomp Require Import function_spaces simple_functions. -From mathcomp Require Import measurable_fun_approximation. +From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. +From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. From mathcomp Require Import lebesgue_integral_nonneg lebesgue_integrable. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v index c12faf50e1..a6d8685ad7 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v @@ -1,15 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference. -From mathcomp Require Import topology ereal tvs normedtype sequences. -From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. -From mathcomp Require Import measurable_fun_approximation. +From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. (**md**************************************************************************) diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v index 6a49ab6495..8a583075cc 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v @@ -1,15 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference finmap archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference. -From mathcomp Require Import topology ereal tvs normedtype sequences. -From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. -From mathcomp Require Import measurable_fun_approximation. +From mathcomp Require Import measurable_realfun measurable_fun_approximation. From mathcomp Require Import lebesgue_integral_definition. From mathcomp Require Import lebesgue_integral_monotone_convergence. diff --git a/theories/lebesgue_integral_theory/lebesgue_integral_under.v b/theories/lebesgue_integral_theory/lebesgue_integral_under.v index 12f5c93df1..7e4cd77b8e 100644 --- a/theories/lebesgue_integral_theory/lebesgue_integral_under.v +++ b/theories/lebesgue_integral_theory/lebesgue_integral_under.v @@ -1,14 +1,13 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. -From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import function_spaces derive esum measure. -From mathcomp Require Import lebesgue_measure numfun realfun simple_functions. -From mathcomp Require Import lebesgue_integral_definition. -From mathcomp Require Import lebesgue_integral_nonneg. +From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval derive esum. +From mathcomp Require Import measure lebesgue_measure numfun realfun. +From mathcomp Require Import measurable_realfun simple_functions. +From mathcomp Require Import lebesgue_integral_definition lebesgue_integral_nonneg. From mathcomp Require Import lebesgue_integrable lebesgue_Rintegral. From mathcomp Require Import lebesgue_integral_dominated_convergence. diff --git a/theories/lebesgue_integral_theory/measurable_fun_approximation.v b/theories/lebesgue_integral_theory/measurable_fun_approximation.v index 5c21a1dc26..a1754685ac 100644 --- a/theories/lebesgue_integral_theory/measurable_fun_approximation.v +++ b/theories/lebesgue_integral_theory/measurable_fun_approximation.v @@ -1,15 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference. -From mathcomp Require Import topology ereal tvs normedtype sequences. -From mathcomp Require Import real_interval function_spaces esum measure. +From mathcomp Require Import cardinality reals fsbigop topology ereal tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. From mathcomp Require Import lebesgue_measure numfun realfun exp. -From mathcomp Require Import simple_functions. +From mathcomp Require Import measurable_realfun simple_functions. (**md**************************************************************************) (* # Approximation theorem for measurable functions *) diff --git a/theories/lebesgue_integral_theory/simple_functions.v b/theories/lebesgue_integral_theory/simple_functions.v index 96573b7b5c..c40790c1fb 100644 --- a/theories/lebesgue_integral_theory/simple_functions.v +++ b/theories/lebesgue_integral_theory/simple_functions.v @@ -1,12 +1,11 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality reals fsbigop interval_inference ereal. -From mathcomp Require Import topology tvs normedtype sequences real_interval. -From mathcomp Require Import esum measure lebesgue_measure numfun realfun. -From mathcomp Require Import function_spaces. +From mathcomp Require Import cardinality reals fsbigop ereal topology tvs. +From mathcomp Require Import normedtype sequences real_interval esum measure. +From mathcomp Require Import lebesgue_measure numfun realfun measurable_realfun. (**md**************************************************************************) (* # Simple functions *) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index d97457ae71..e7f4a782d1 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -1,15 +1,14 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. -From mathcomp Require Import archimedean rat. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. +From mathcomp Require Import interval interval_inference archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import mathcomp_extra boolp classical_sets. -From mathcomp Require Import functions cardinality fsbigop reals. -From mathcomp Require Import interval_inference ereal topology numfun tvs. -From mathcomp Require Import normedtype function_spaces sequences esum measure. -From mathcomp Require Import real_interval realfun exp. -From mathcomp Require Export measurable_realfun lebesgue_stieltjes_measure. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop reals ereal topology numfun. +From mathcomp Require Import tvs normedtype sequences esum measure. +From mathcomp Require Import real_interval realfun exp measurable_realfun. +From mathcomp Require Export lebesgue_stieltjes_measure. (**md**************************************************************************) (* # Lebesgue Measure *) diff --git a/theories/measurable_realfun.v b/theories/measurable_realfun.v index 05d0608393..92e62fc232 100644 --- a/theories/measurable_realfun.v +++ b/theories/measurable_realfun.v @@ -1,15 +1,13 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. -From mathcomp Require Import interval archimedean rat. +From mathcomp Require Import interval interval_inference archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. -From mathcomp Require Import boolp classical_sets. -From mathcomp Require Import functions cardinality fsbigop reals ereal. -From mathcomp Require Import interval_inference topology numfun tvs normedtype. -From mathcomp Require Import function_spaces sequences esum measure. -From mathcomp Require Import real_interval realfun exp. -From mathcomp Require Export lebesgue_stieltjes_measure. +From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. +From mathcomp Require Import reals ereal topology numfun tvs normedtype. +From mathcomp Require Import real_interval sequences esum measure realfun exp. +From mathcomp Require Import lebesgue_stieltjes_measure. (**md**************************************************************************) (* # Measurable Functions over $\mathbb{R}$ and $\overline{\mathbb{R}}$ *) diff --git a/theories/normedtype_theory/matrix_normedtype.v b/theories/normedtype_theory/matrix_normedtype.v index d4194e5d14..7e40862fc6 100644 --- a/theories/normedtype_theory/matrix_normedtype.v +++ b/theories/normedtype_theory/matrix_normedtype.v @@ -1,9 +1,10 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum matrix interval. -From mathcomp Require Import boolp classical_sets interval_inference reals. -From mathcomp Require Import topology function_spaces prodnormedzmodule tvs. -From mathcomp Require Import pseudometric_normed_Zmodule normed_module. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum matrix. +From mathcomp Require Import interval interval_inference. +From mathcomp Require Import boolp classical_sets reals topology. +From mathcomp Require Import prodnormedzmodule tvs pseudometric_normed_Zmodule. +From mathcomp Require Import normed_module. (**md**************************************************************************) (* # Normed topological Abelian group of matrices *) diff --git a/theories/normedtype_theory/normed_module.v b/theories/normedtype_theory/normed_module.v index 8ebdee3787..3e5b5d4826 100644 --- a/theories/normedtype_theory/normed_module.v +++ b/theories/normedtype_theory/normed_module.v @@ -2,12 +2,11 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. From mathcomp Require Import archimedean rat interval zmodp vector. -From mathcomp Require Import fieldext falgebra. +From mathcomp Require Import interval_inference fieldext falgebra. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets filter functions cardinality. -From mathcomp Require Import set_interval interval_inference ereal reals. -From mathcomp Require Import topology function_spaces real_interval. +From mathcomp Require Import set_interval ereal reals topology real_interval. From mathcomp Require Import prodnormedzmodule tvs num_normedtype. From mathcomp Require Import ereal_normedtype pseudometric_normed_Zmodule. diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 5ef7c3e869..38b10494c7 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -1,12 +1,11 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) -From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. -From mathcomp Require Import archimedean rat. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. +From mathcomp Require Import interval interval_inference archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. -From mathcomp Require Import cardinality set_interval interval_inference reals. -From mathcomp Require Import topology function_spaces real_interval. -From mathcomp Require Import prodnormedzmodule tvs. +From mathcomp Require Import cardinality set_interval reals real_interval. +From mathcomp Require Import topology prodnormedzmodule tvs. (**md**************************************************************************) (* # Preliminaries for norm-related notions *) diff --git a/theories/normedtype_theory/pseudometric_normed_Zmodule.v b/theories/normedtype_theory/pseudometric_normed_Zmodule.v index 6b5f948182..dd4ed670d3 100644 --- a/theories/normedtype_theory/pseudometric_normed_Zmodule.v +++ b/theories/normedtype_theory/pseudometric_normed_Zmodule.v @@ -1,11 +1,10 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. -From mathcomp Require Import interval archimedean. +From mathcomp Require Import interval interval_inference archimedean. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import set_interval interval_inference ereal reals. -From mathcomp Require Import topology function_spaces prodnormedzmodule tvs. -From mathcomp Require Import num_normedtype. +From mathcomp Require Import set_interval ereal reals topology. +From mathcomp Require Import prodnormedzmodule tvs num_normedtype. (**md**************************************************************************) (* # Normed topological abelian groups *) diff --git a/theories/normedtype_theory/urysohn.v b/theories/normedtype_theory/urysohn.v index c1c9ef3b97..a9e9e1f364 100644 --- a/theories/normedtype_theory/urysohn.v +++ b/theories/normedtype_theory/urysohn.v @@ -1,13 +1,13 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. -From mathcomp Require Import archimedean. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. +From mathcomp Require Import interval interval_inference archimedean. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import set_interval interval_inference ereal reals. -From mathcomp Require Import topology function_spaces tvs num_normedtype. -From mathcomp Require Import pseudometric_normed_Zmodule normed_module. +From mathcomp Require Import set_interval ereal reals topology tvs. +From mathcomp Require Import num_normedtype pseudometric_normed_Zmodule. +From mathcomp Require Import normed_module. (**md**************************************************************************) (* # Urysohn's lemma *) diff --git a/theories/normedtype_theory/vitali_lemma.v b/theories/normedtype_theory/vitali_lemma.v index 286a1c02c0..491e955a00 100644 --- a/theories/normedtype_theory/vitali_lemma.v +++ b/theories/normedtype_theory/vitali_lemma.v @@ -1,13 +1,13 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint interval. -From mathcomp Require Import archimedean rat. +From mathcomp Require Import all_ssreflect_compat finmap ssralg ssrnum ssrint. +From mathcomp Require Import interval_inference interval archimedean rat. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import set_interval interval_inference ereal reals. -From mathcomp Require Import topology function_spaces tvs num_normedtype. -From mathcomp Require Import pseudometric_normed_Zmodule normed_module. +From mathcomp Require Import set_interval ereal reals topology tvs. +From mathcomp Require Import num_normedtype pseudometric_normed_Zmodule. +From mathcomp Require Import normed_module. (**md**************************************************************************) (* # Vitali's covering lemmas *) diff --git a/theories/numfun.v b/theories/numfun.v index f75aa5b76d..d56e400fbf 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1,12 +1,12 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval finmap. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. +From mathcomp Require Import interval_inference finmap. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop. -From mathcomp Require Import functions cardinality set_interval. -From mathcomp Require Import interval_inference reals ereal topology normedtype. -From mathcomp Require Import sequences function_spaces. +From mathcomp Require Import functions cardinality set_interval reals ereal. +From mathcomp Require Import topology normedtype sequences. (**md**************************************************************************) (* # Numerical functions *) diff --git a/theories/pi_irrational.v b/theories/pi_irrational.v index 1ccb5494e1..d55cea90d4 100644 --- a/theories/pi_irrational.v +++ b/theories/pi_irrational.v @@ -1,10 +1,12 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect_compat all_algebra. +From mathcomp Require Import interval_inference. From mathcomp Require Import mathcomp_extra boolp classical_sets. -From mathcomp Require Import functions cardinality fsbigop interval_inference. +From mathcomp Require Import functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences. -From mathcomp Require Import real_interval esum measure lebesgue_measure numfun. -From mathcomp Require Import realfun lebesgue_integral derive charge ftc trigo. +From mathcomp Require Import real_interval esum measure measurable_realfun. +From mathcomp Require Import numfun realfun lebesgue_measure lebesgue_integral. +From mathcomp Require Import derive charge ftc trigo. (**md**************************************************************************) (* # Formalisation of A simple proof that pi is irrational by Ivan Niven *) diff --git a/theories/probability_theory/bernoulli_distribution.v b/theories/probability_theory/bernoulli_distribution.v index b785f167ad..3abe1ee546 100644 --- a/theories/probability_theory/bernoulli_distribution.v +++ b/theories/probability_theory/bernoulli_distribution.v @@ -7,8 +7,8 @@ From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences esum. -From mathcomp Require Import measure numfun lebesgue_measure lebesgue_integral. -From mathcomp Require Import kernel. +From mathcomp Require Import measure numfun measurable_realfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral kernel. (**md**************************************************************************) (* # Bernoulli distribution *) diff --git a/theories/probability_theory/beta_distribution.v b/theories/probability_theory/beta_distribution.v index e1de1f3ca7..be915da53b 100644 --- a/theories/probability_theory/beta_distribution.v +++ b/theories/probability_theory/beta_distribution.v @@ -1,15 +1,15 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg poly ssrnum ssrint interval. -From mathcomp Require Import archimedean finmap interval_inference. +From mathcomp Require Import all_ssreflect_compat ssralg poly ssrnum ssrint. +From mathcomp Require Import archimedean finmap interval interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences derive. -From mathcomp Require Import measure exp numfun realfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral charge ftc uniform_distribution. -From mathcomp Require Import bernoulli_distribution. +From mathcomp Require Import measure exp numfun realfun measurable_realfun. +From mathcomp Require Import lebesgue_measure lebesgue_integral charge ftc. +From mathcomp Require Import uniform_distribution bernoulli_distribution. (**md**************************************************************************) (* # Beta distribution *) diff --git a/theories/probability_theory/binomial_distribution.v b/theories/probability_theory/binomial_distribution.v index 458d7ee351..01c41b99c8 100644 --- a/theories/probability_theory/binomial_distribution.v +++ b/theories/probability_theory/binomial_distribution.v @@ -7,8 +7,8 @@ From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences esum. -From mathcomp Require Import measure lebesgue_measure lebesgue_integral. -From mathcomp Require Import bernoulli_distribution. +From mathcomp Require Import measure measurable_realfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral bernoulli_distribution. (**md**************************************************************************) (* # Binomial distribution *) diff --git a/theories/probability_theory/exponential_distribution.v b/theories/probability_theory/exponential_distribution.v index b099443017..0206c08f40 100644 --- a/theories/probability_theory/exponential_distribution.v +++ b/theories/probability_theory/exponential_distribution.v @@ -4,8 +4,8 @@ From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences derive. -From mathcomp Require Import measure exp realfun numfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral ftc. +From mathcomp Require Import measure exp realfun measurable_realfun numfun. +From mathcomp Require Import lebesgue_measure lebesgue_integral ftc. (**md**************************************************************************) (* # Exponential distribution *) diff --git a/theories/probability_theory/normal_distribution.v b/theories/probability_theory/normal_distribution.v index c8dfbabb05..89e1e89703 100644 --- a/theories/probability_theory/normal_distribution.v +++ b/theories/probability_theory/normal_distribution.v @@ -4,7 +4,8 @@ From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences derive. -From mathcomp Require Import measure exp trigo numfun realfun lebesgue_measure. +From mathcomp Require Import measure exp trigo numfun realfun. +From mathcomp Require Import measurable_realfun lebesgue_measure. From mathcomp Require Import lebesgue_integral ftc gauss_integral. (**md**************************************************************************) diff --git a/theories/probability_theory/poisson_distribution.v b/theories/probability_theory/poisson_distribution.v index 4a4deeed68..d120ff9811 100644 --- a/theories/probability_theory/poisson_distribution.v +++ b/theories/probability_theory/poisson_distribution.v @@ -4,7 +4,8 @@ From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. From mathcomp Require Import archimedean finmap interval_inference. From mathcomp Require Import boolp classical_sets reals ereal topology. From mathcomp Require Import normedtype sequences exp esum measure. -From mathcomp Require Import lebesgue_measure lebesgue_integral. +From mathcomp Require Import measurable_realfun lebesgue_measure. +From mathcomp Require Import lebesgue_integral. (**md**************************************************************************) (* # Poisson distribution *) diff --git a/theories/probability_theory/random_variable.v b/theories/probability_theory/random_variable.v index 631f2c7a7e..e46c95a887 100644 --- a/theories/probability_theory/random_variable.v +++ b/theories/probability_theory/random_variable.v @@ -1,13 +1,13 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. -From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint poly interval. -From mathcomp Require Import archimedean finmap interval_inference. +From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint poly. +From mathcomp Require Import interval archimedean finmap interval_inference. #[warning="-warn-library-file-internal-analysis"] From mathcomp Require Import unstable. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. From mathcomp Require Import reals ereal topology normedtype sequences measure. -From mathcomp Require Import exp numfun realfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral hoelder. +From mathcomp Require Import exp numfun realfun measurable_realfun. +From mathcomp Require Import lebesgue_measure lebesgue_integral hoelder. (**md**************************************************************************) (* # Probability *) diff --git a/theories/probability_theory/uniform_distribution.v b/theories/probability_theory/uniform_distribution.v index 75486c5eac..91e2f1289e 100644 --- a/theories/probability_theory/uniform_distribution.v +++ b/theories/probability_theory/uniform_distribution.v @@ -1,11 +1,11 @@ (* mathcomp analysis (c) 2026 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum ssrint interval. -From mathcomp Require Import archimedean finmap. +From mathcomp Require Import interval_inference archimedean finmap. From mathcomp Require Import boolp classical_sets functions cardinality fsbigop. -From mathcomp Require Import reals interval_inference ereal topology normedtype. -From mathcomp Require Import sequences measure numfun lebesgue_measure. -From mathcomp Require Import lebesgue_integral. +From mathcomp Require Import reals ereal topology normedtype. +From mathcomp Require Import sequences measure measurable_realfun numfun. +From mathcomp Require Import lebesgue_measure lebesgue_integral. (**md**************************************************************************) (* # Uniform distribution *) diff --git a/theories/tvs.v b/theories/tvs.v index a22206fcd9..bd6f428b19 100644 --- a/theories/tvs.v +++ b/theories/tvs.v @@ -1,9 +1,9 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum vector. +From mathcomp Require Import interval_inference. From mathcomp Require Import boolp classical_sets functions cardinality. -From mathcomp Require Import set_interval reals interval_inference. -From mathcomp Require Import topology function_spaces. +From mathcomp Require Import set_interval reals topology. (**md**************************************************************************) (* # Topological vector spaces *) From a013eff71b75d21271be2759cd88225ff44743de Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 4 Mar 2026 17:29:13 +0900 Subject: [PATCH 3/3] fix changelog --- CHANGELOG_UNRELEASED.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4790799c00..5b7f660af6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -204,7 +204,8 @@ - moved from `measurable_structure.v` to `classical_sets.v`: + definitions `setI_closed`, `setU_closed` -- moved from `theories` to `theories/topology_theory` +- moved from `theories` to `theories/topology_theory`: + + file `function_spaces.v` ### Renamed