Merge pull request #1540 from IshiguroYoshihiro/continuousT_under_integral_20250326

add continuous_under_integral

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -58,6 +58,11 @@
 
 - in `mathcomp_extra.v`:
   + lemmas `intrN`, `real_floor_itv`, `real_ge_floor`, `real_ceil_itv`
+- in `lebesgue_integral.v`:
+  + lemma `dominated_cvg` (was previous `Local`)
+
+- in `ftc.v`:
+  + lemma `continuity_under_integral`
 
 - in `set_interval.v`:
   + lemma `subset_itv`
@@ -77,6 +82,20 @@
     `ceil_le_int_tmp`, `ceil_gt_int`, `ceil_eq`, `ceil_ge0`,
     `ceil_le0`, `natr_int`
 
+- new directory `lebesgue_integral_theory` with new files:
+  + `simple_functions.v`
+  + `lebesgue_integral_definition.v`
+  + `lebesgue_integral_approximation.v`
+  + `lebesgue_integral_monotone_convergence.v`
+  + `lebesgue_integral_nonneg.v`
+  + `lebesgue_integrable.v`
+  + `lebesgue_integral_dominated_convergence.v`
+  + `lebesgue_integral_under.v`
+  + `lebesgue_Rintegral.v`
+  + `lebesgue_integral_fubini.v`
+  + `lebesgue_integral_differentiation.v`
+  + `lebesgue_integral.v`
+
 ### Changed
 
 - file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package
@@ -92,6 +111,18 @@
     `Instances.num_spec_intmul`, `Instances.num_itv_bound_exprn_le1`
   + canonical instance `Instances.succn_inum`
 
+- in `lebesgue_integral_properties.v`
+  (new file with contents moved from `lebesgue_integral.v`)
+  + `le_normr_integral` renamed to `le_normr_Rintegral`
+
+- moved to `lebesgue_measure.v` (from old `lebesgue_integral.v`)
+  + `compact_finite_measure`
+
+- moved from `ftc.v` to `lebesgue_integral_under.v` (new file)
+  + notation `'d1`, definition `partial1of2`, lemmas `partial1of2E`,
+    `cvg_differentiation_under_integral`, `differentiation_under_integral`,
+    `derivable_under_integral`
+
 ### Renamed
 
 - in `lebesgue_integral.v`:
@@ -153,6 +184,9 @@
 - in `reals.v`:
   + lemmas `floor_le`, `le_floor` (deprecated since 1.3.0)
 
+- file `lebesgue_integral.v` (split in several files in the directory
+  `lebesgue_integral_theory`)
+
 ### Infrastructure
 
 ### Misc

_CoqProject

@@ -86,7 +86,20 @@ theories/forms.v
 theories/derive.v
 theories/measure.v
 theories/numfun.v
-theories/lebesgue_integral.v
+
+theories/lebesgue_integral_theory/simple_functions.v
+theories/lebesgue_integral_theory/lebesgue_integral_definition.v
+theories/lebesgue_integral_theory/lebesgue_integral_approximation.v
+theories/lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
+theories/lebesgue_integral_theory/lebesgue_integral_nonneg.v
+theories/lebesgue_integral_theory/lebesgue_integrable.v
+theories/lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
+theories/lebesgue_integral_theory/lebesgue_integral_under.v
+theories/lebesgue_integral_theory/lebesgue_Rintegral.v
+theories/lebesgue_integral_theory/lebesgue_integral_fubini.v
+theories/lebesgue_integral_theory/lebesgue_integral_differentiation.v
+theories/lebesgue_integral_theory/lebesgue_integral.v
+
 theories/ftc.v
 theories/hoelder.v
 theories/probability.v

classical/mathcomp_extra.v

@@ -238,13 +238,13 @@ Notation comparable_max_le_max := comparable_le_max2.
 
 Lemma le_min2 d (T : orderType d) (x y z t : T) :
   (x <= z)%O -> (y <= t)%O -> (Order.min x y <= Order.min z t)%O.
-Proof. exact: comparable_min_le_min. Qed.
+Proof. exact: comparable_le_min2. Qed.
 #[deprecated(since="mathcomp-analysis 1.10.0", note="use `le_min2` instead")]
 Notation min_le_min := le_min2.
 
 Lemma le_max2 d (T : orderType d) (x y z t : T) :
   (x <= z)%O -> (y <= t)%O -> (Order.max x y <= Order.max z t)%O.
-Proof. exact: comparable_max_le_max. Qed.
+Proof. exact: comparable_le_max2. Qed.
 #[deprecated(since="mathcomp-analysis 1.10.0", note="use `le_max2` instead")]
 Notation max_le_max := le_max2.
 

reals/interval_inference.v

@@ -1057,9 +1057,9 @@ apply: Itv.spec_real2 (Itv.P x) (Itv.P y).
 case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
 move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
 apply/and3P; split; rewrite ?min_real//= num_itv_bound_min real_BSide_min//.
-- apply: (comparable_min_le_min (comparable_num_itv_bound _ _)) => //.
+- apply: (comparable_le_min2 (comparable_num_itv_bound _ _)) => //.
   exact: real_comparable.
-- apply: (comparable_min_le_min _ (comparable_num_itv_bound _ _)) => //.
+- apply: (comparable_le_min2 _ (comparable_num_itv_bound _ _)) => //.
   exact: real_comparable.
 Qed.
 
@@ -1071,9 +1071,9 @@ apply: Itv.spec_real2 (Itv.P x) (Itv.P y).
 case: x y => [x /= _] [y /= _] => {xi yi r} -[lx ux] [ly uy]/=.
 move=> /andP[xr /=/andP[lxx xux]] /andP[yr /=/andP[lyy yuy]].
 apply/and3P; split; rewrite ?max_real//= num_itv_bound_max real_BSide_max//.
-- apply: (comparable_max_le_max (comparable_num_itv_bound _ _)) => //.
+- apply: (comparable_le_max2 (comparable_num_itv_bound _ _)) => //.
   exact: real_comparable.
-- apply: (comparable_max_le_max _ (comparable_num_itv_bound _ _)) => //.
+- apply: (comparable_le_max2 _ (comparable_num_itv_bound _ _)) => //.
   exact: real_comparable.
 Qed.
 
@@ -1325,7 +1325,7 @@ Lemma num_spec_sqrtC (i : Itv.t) (x : num_def R i) (r := sqrtC_itv i) :
 Proof.
 rewrite {}/r; case: i x => [//| [l u] [x /=/and3P[xr /= lx xu]]].
 case: l lx => [bl [l |//] |[]//] lx; apply/and3P; split=> //=.
-  by apply: real_sqrtC; case: bl lx => /[!bnd_simp] [|/ltW]; apply: le_trans.
+  by apply: sqrtC_real; case: bl lx => /[!bnd_simp] [|/ltW]; apply: le_trans.
 case: bl lx => /[!bnd_simp] lx.
 - by rewrite sqrtC_ge0; apply: le_trans lx.
 - by rewrite sqrtC_gt0; apply: le_lt_trans lx.

theories/Make

@@ -50,7 +50,20 @@ forms.v
 derive.v
 measure.v
 numfun.v
-lebesgue_integral.v
+
+lebesgue_integral_theory/simple_functions.v
+lebesgue_integral_theory/lebesgue_integral_definition.v
+lebesgue_integral_theory/lebesgue_integral_approximation.v
+lebesgue_integral_theory/lebesgue_integral_monotone_convergence.v
+lebesgue_integral_theory/lebesgue_integral_nonneg.v
+lebesgue_integral_theory/lebesgue_integrable.v
+lebesgue_integral_theory/lebesgue_integral_dominated_convergence.v
+lebesgue_integral_theory/lebesgue_integral_under.v
+lebesgue_integral_theory/lebesgue_Rintegral.v
+lebesgue_integral_theory/lebesgue_integral_fubini.v
+lebesgue_integral_theory/lebesgue_integral_differentiation.v
+lebesgue_integral_theory/lebesgue_integral.v
+
 ftc.v
 hoelder.v
 probability.v