continuity of the parameterized integral on the interval

CHANGELOG_UNRELEASED.md

@@ -24,6 +24,17 @@
   + lemmas `g_sigma_completed_algebra_genE`, `negligible_sub_caratheodory`,
     `completed_caratheodory_measurable`
 
+- in `set_interval.v`:
+  + lemmas `subset_itvl`, `subset_itvr`, `subset_itvS`
+
+- in `normedtype.v`:
+  + lemmas `nbhs_lt`, `nbhs_le`
+
+- in `lebesgue_integral.v`:
+  + lemmas `eq_Rintegral`, `Rintegral_mkcond`, `Rintegral_mkcondr`, `Rintegral_mkcondl`,
+    `le_normr_integral`, `Rintegral_setU_EFin`, `Rintegral_set0`, `Rintegral_itv_bndo_bndc`,
+    `Rintegral_itv_obnd_cbnd`, `Rintegral_set1`, `Rintegral_itvB`
+
 ### Changed
 
 - in `topology.v`:
@@ -66,9 +77,10 @@
   + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, `integral_normr_continuous`
 
 - in `ftc.v`:
-  + definition `indefinite_integral`
-  + lemmas `indefinite_integral_near_left`,
-    `indefinite_integral_cvg_left`, `indefinite_integral_cvg_at_left`
+  + definition `parameterized_integral`
+  + lemmas `parameterized_integral_near_left`,
+    `parameterized_integral_left`, `parameterized_integral_cvg_at_left`,
+    `parameterized_integral_continuous`
   + corollary `continuous_FTC2`
 
 ### Changed

classical/set_interval.v

@@ -70,6 +70,51 @@ by move: b0 b1 => [] [] /=; [exact: subset_itv_oo_co|exact: subset_itv_oo_cc|
   exact: subset_refl|exact: subset_itv_oo_oc].
 Qed.
 
+Lemma subset_itvl (a b c : itv_bound T) : (b <= c)%O ->
+  [set` Interval a b] `<=` [set` Interval a c].
+Proof.
+case: c => [[|] c bc x/=|[//|_] x/=].
+- rewrite !in_itv/= => /andP[->/=].
+  case: b bc => [[|]/=|[|]//] b bc.
+    by move=> /lt_le_trans; exact.
+  by move=> /le_lt_trans; exact.
+- rewrite !in_itv/= => /andP[->/=].
+  case: b bc => [[|]/=|[|]//] b bc.
+    by move=> /ltW /le_trans; apply.
+  by move=> /le_trans; apply.
+- by move: x; rewrite le_ninfty => /eqP ->.
+- by rewrite !in_itv/=; case: a => [[|]/=|[|]//] a /andP[->].
+Qed.
+
+Lemma subset_itvr (a b c : itv_bound T) : (c <= a)%O ->
+  [set` Interval a b] `<=` [set` Interval c b].
+Proof.
+move=> ac x/=; rewrite !in_itv/= => /andP[ax ->]; rewrite andbT.
+move: c a ax ac => [[|] c [[|]/= a ax|[|]//=]|[//|]]; rewrite ?bnd_simp.
+- by move=> /le_trans; exact.
+- by move=> /le_trans; apply; exact/ltW.
+- by move=> /lt_le_trans; exact.
+- by move=> /le_lt_trans; exact.
+- by move=> [[|]|[|]//].
+Qed.
+
+Lemma subset_itvS (a b : itv_bound T) (c e : T) :
+    (BLeft c <= a)%O -> (b <= BRight e)%O ->
+  [set` Interval a b] `<=` [set` `[c, e]].
+Proof.
+move=> ca be z/=; rewrite !in_itv/= => /andP[az zb].
+case: a ca az => [[|]/=|[|]//] a; rewrite bnd_simp => ca az.
+  rewrite (le_trans ca az)/=.
+  move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be.
+    by move=> /ltW/le_trans; exact.
+  by move=> /le_trans; exact.
+move/ltW in az.
+rewrite (le_trans ca az)/=.
+move: b be zb => [[|]/= b|[|]//]; rewrite bnd_simp => be.
+  by move=> /ltW/le_trans; exact.
+by move=> /le_trans; exact.
+Qed.
+
 Lemma interval_set1 x : `[x, x]%classic = [set x] :> set T.
 Proof.
 apply/seteqP; split => [y/=|y <-]; last by rewrite /= in_itv/= lexx.