FTC1 corollary

Co-authored-by: Zachary Stone <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -30,6 +30,54 @@
   + lemmas `subspace_pm_ball_center`, `subspace_pm_ball_sym`,
     `subspace_pm_ball_triangle`, `subspace_pm_entourage` turned
 	into local `Let`'s
+- 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 `indefinite_integral`
+  + lemmas `indefinite_integral_near_left`,
+    `indefinite_integral_cvg_left`, `indefinite_integral_cvg_at_left`
+  + corollary `continuous_FTC2`
+
+### Changed
+
+- in `lebesgue_integral.v`:
+  + lemma `measurable_int`: argument `mu` now explicit 
+
+- moved from `lebesgue_integral.v` to `ereal.v`:
+  + lemma `funID`
 
 ### Renamed
 
@@ -51,11 +99,19 @@
   + `lee_ndivr_mull` -> `lee_ndivrMl`
   + `lee_ndivr_mulr` -> `lee_ndivrMr`
   + `eqe_pdivr_mull` -> `eqe_pdivrMl`
+- in `measure.v`:
+  + `measurable_restrict` -> `measurable_restrictT`
 
 ### Generalized
 
+- in `measure.v`:
+  + lemma `measurable_restrict`
+
 ### Deprecated
 
+- in `lebesgue_integral.v`:
+  + lemmas `integralEindic`, `integral_setI_indic`
+
 ### Removed
 
 ### Infrastructure

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,12 @@ by move: b0 b1 => [] [] /=; [exact: subset_itv_oo_co|exact: subset_itv_oo_cc|
   exact: subset_refl|exact: subset_itv_oo_oc].
 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.