mv function_spaces

CHANGELOG_UNRELEASED.md

@@ -204,6 +204,9 @@
 - moved from `measurable_structure.v` to `classical_sets.v`:
   + definitions `setI_closed`, `setU_closed`
 
+- moved from `theories` to `theories/topology_theory`:
+  + file `function_spaces.v`
+
 ### Renamed
 
 - in `topology_structure.v`

_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
 

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
 

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.

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                               *)

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                                        *)

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**************************************************************************)

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                                 *)

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.
 

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.

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                                                     *)

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                                                                    *)

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                                                       *)

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                                                                  *)

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**************************************************************************)

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.

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                                      *)

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.
 

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                  *)

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.