FTC1 corollary

CHANGELOG_UNRELEASED.md

@@ -38,6 +38,16 @@
 
 - in `realfun.v`:
   + lemma `nondecreasing_at_left_is_cvgr`
+- 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`
 
 - in `constructive_ereal.v`:
   + lemmas `lteD2rE`, `leeD2rE`
@@ -46,13 +56,61 @@
 - in `mathcomp_extra.v`:
   + lemma `invf_ltp`
 
+- in `classical_sets.v`:
+  + lemmas `setC_I`, `bigcup_subset`
+
+- in `set_interval.v`:
+  + lemma `interval_set1`
+
+- in `normedtype.v`:
+  + lemma `nbhs_right_ltDr`
+
+- in `numfun.v`:
+  + lemma `epatch_indic`
+  + lemma `restrict_normr`
+  + lemmas `funepos_le`, `funeneg_le`
+
+- in `ereal.v`:
+  + lemmas `restrict_EFin`
+
+- in `measure.v`:
+  + definition `lim_sup_set`
+  + lemmas `lim_sup_set_ub`, `lim_sup_set_cvg`, `lim_sup_set_cvg0`
+
+- in `lebesgue_integral.v`:
+  + lemma `integral_Sset1`
+  + lemma `integralEpatch`
+  + lemma `integrable_restrict`
+  + lemma `le_integral`
+  + lemma `null_set_integral`
+  + lemma `EFin_normr_Rintegral`
+
+- in `charge.v`:
+  + definition `charge_variation`
+  + lemmas `abse_charge_variation`, `charge_variation_continuous`
+  + definition `induced`
+  + lemmas `semi_sigma_additive_nng_induced`, `dominates_induced`, `integral_normr_continuous`
+
+- in `ftc.v`:
+  + definition `parameterized_integral`
+  + lemmas `parameterized_integral_near_left`,
+    `parameterized_integral_left`, `parameterized_integral_cvg_at_left`,
+    `parameterized_integral_continuous`
+  + corollary `continuous_FTC2`
+
 ### Changed
 
 - in `topology.v`:
   + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
     `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
 	into local `Let`'s
 
+- in `lebesgue_integral.v`:
+  + lemma `measurable_int`: argument `mu` now explicit 
+
+- moved from `lebesgue_integral.v` to `ereal.v`:
+  + lemma `funID`
+
 - in `reals.v`:
   + definitions `Rceil`, `Rfloor`
 
@@ -94,6 +152,8 @@
   + `lee_ndivr_mull` -> `lee_ndivrMl`
   + `lee_ndivr_mulr` -> `lee_ndivrMr`
   + `eqe_pdivr_mull` -> `eqe_pdivrMl`
+- in `measure.v`:
+  + `measurable_restrict` -> `measurable_restrictT`
 
 - in `ftc.v`:
   + `FTC1` -> `FTC1_lebesgue_pt`
@@ -142,13 +202,17 @@
 
 - in `constructive_ereal.v`:
   + lemmas `leeN2`, `lteN2` generalized from `realDomainType` to `numDomainType`
+- in `measure.v`:
+  + lemma `measurable_restrict`
 
 ### Deprecated
 
 - in `reals.v`:
   + `floor_le` (use `ge_floor` instead)
   + `le_floor` (use `Num.Theory.floor_le` instead)
   + `le_ceil` (use `ceil_ge` instead)
+- in `lebesgue_integral.v`:
+  + lemmas `integralEindic`, `integral_setI_indic`
 
 - in `constructive_ereal.v`:
   + lemmas `lte_opp2`, `lee_opp2` (use `lteN2`, `leeN2` instead)

classical/classical_sets.v

@@ -248,18 +248,24 @@ Reserved Notation "A `\ b" (at level 50, left associativity).
 Reserved Notation "A `+` B"  (at level 54, left associativity).
 Reserved Notation "A +` B"  (at level 54, left associativity).
 *)
-Reserved Notation "\bigcup_ ( i 'in' P ) F"
-  (at level 41, F at level 41, i, P at level 50,
-           format "'[' \bigcup_ ( i  'in'  P ) '/  '  F ']'").
-Reserved Notation "\bigcup_ ( i : T ) F"
-  (at level 41, F at level 41, i at level 50,
-           format "'[' \bigcup_ ( i  :  T ) '/  '  F ']'").
 Reserved Notation "\bigcup_ ( i < n ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \bigcup_ ( i  <  n ) '/  '  F ']'").
 Reserved Notation "\bigcup_ ( i >= n ) F"
   (at level 41, F at level 41, i, n at level 50,
            format "'[' \bigcup_ ( i  >=  n ) '/  '  F ']'").
+Reserved Notation "\bigcap_ ( i < n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcap_ ( i  <  n ) '/  '  F ']'").
+Reserved Notation "\bigcap_ ( i >= n ) F"
+  (at level 41, F at level 41, i, n at level 50,
+           format "'[' \bigcap_ ( i  >=  n ) '/  '  F ']'").
+Reserved Notation "\bigcup_ ( i 'in' P ) F"
+  (at level 41, F at level 41, i, P at level 50,
+           format "'[' \bigcup_ ( i  'in'  P ) '/  '  F ']'").
+Reserved Notation "\bigcup_ ( i : T ) F"
+  (at level 41, F at level 41, i at level 50,
+           format "'[' \bigcup_ ( i  :  T ) '/  '  F ']'").
 Reserved Notation "\bigcup_ i F"
   (at level 41, F at level 41, i at level 0,
            format "'[' \bigcup_ i '/  '  F ']'").
@@ -269,12 +275,6 @@ Reserved Notation "\bigcap_ ( i 'in' P ) F"
 Reserved Notation "\bigcap_ ( i : T ) F"
   (at level 41, F at level 41, i at level 50,
            format "'[' \bigcap_ ( i  :  T ) '/  '  F ']'").
-Reserved Notation "\bigcap_ ( i < n ) F"
-  (at level 41, F at level 41, i, n at level 50,
-           format "'[' \bigcap_ ( i  <  n ) '/  '  F ']'").
-Reserved Notation "\bigcap_ ( i >= n ) F"
-  (at level 41, F at level 41, i, n at level 50,
-           format "'[' \bigcap_ ( i  >=  n ) '/  '  F ']'").
 Reserved Notation "\bigcap_ i F"
   (at level 41, F at level 41, i at level 0,
            format "'[' \bigcap_ i '/  '  F ']'").
@@ -1207,6 +1207,11 @@ Proof. by move=> k; apply/val_inj. Qed.
 Lemma IIordK {n} : cancel (@IIord n) ordII.
 Proof. by move=> k; apply/val_inj. Qed.
 
+Lemma setC_I n : ~` `I_n = [set k | n <= k].
+Proof.
+by apply/seteqP; split => [x /negP|x /= nx]; last apply/negP; rewrite -leqNgt.
+Qed.
+
 Lemma mem_not_I N n : (n \in ~` `I_N) = (N <= n).
 Proof. by rewrite in_setC /mkset /in_mem /mem /= /in_set asboolb -leqNgt. Qed.
 
@@ -1937,6 +1942,10 @@ Proof.
 by move=> FG; apply: bigcup_sub => i Pi + /(FG _ Pi); apply: bigcup_sup.
 Qed.
 
+Lemma bigcup_subset P Q F : P `<=` Q ->
+  \bigcup_(i in P) F i `<=` \bigcup_(i in Q) F i.
+Proof. by move=> PQ t [i /PQ Qi Fit]; exists i. Qed.
+
 Lemma subset_bigcap P F G : (forall i, P i -> F i `<=` G i) ->
   \bigcap_(i in P) F i `<=` \bigcap_(i in P) G i.
 Proof.

classical/set_interval.v

@@ -70,6 +70,57 @@ 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.
+by rewrite in_itv/= => /andP[yx xy]; apply/eqP; rewrite eq_le yx xy.
+Qed.
+
 Lemma set_itvoo x y : `]x, y[%classic = [set z | (x < z < y)%O].
 Proof. by []. Qed.