cleaning (to be cont'd)

- move definitions and lemmas to more appropriate locations
- changelog, doc

CHANGELOG_UNRELEASED.md

@@ -64,6 +64,39 @@
 - in `classical_sets.v`:
   + lemma `Zorn_bigcup`
 
+- in `nomedtype.v`:
+  + lemmas `ball0`, `ball_itv`,
+  + lemmas `closed_ball0`, `closed_ball_itv`
+
+- in `mathcomp_extra.v`:
+  + lemma `leq_ltn_expn`
+
+- in `classical_sets.v`:
+  + lemma `set_cons1`, `trivIset_bigcup`
+  + definition `maximal_disjoint_subcollection`
+  + lemma `ex_maximal_disjoint_subcollection`
+
+- in `topology.v`:
+  + lemma `separated_open_countable`
+
+- in `normedtype.v`:
+  + definitions `scale_ball`, `scale_cball`
+  + lemmas `scale_ball1`, `scale_ball_neq0`, `sub_scale_ball`
+  + lemmas `scale_cball1`, `scale_cball_neq0`, `scale_cball_itv`
+  + lemmas `separated_open_countable`, `separated_closed_ball_countable`
+  + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover`
+  + definition `vitali_collection_partition`
+  + lemmas `vitali_collection_partition_ub_gt0`,
+    `ex_vitali_collection_partition`, `cover_vitali_collection_partition`,
+    `disjoint_vitali_collection_partition`
+  + lemma `separated_closed_ball_countable`
+  + lemmas `vitali_lemma`, `vitali_lemma_cover`
+
+- in `lebesgue_measure.v`:
+  + lemmas `measurable_ball`, `lebesgue_measure_ball`,
+    `measurable_closed_ball`, `lebesgue_measure_closed_ball`,
+    `measurable_scale_cball`
+
 ### Changed
 
 - moved from `lebesgue_measure.v` to `real_interval.v`:
@@ -161,6 +194,9 @@
     (from measure to content)
   + lemma `subset_measure0` (from `realType` to `realFieldType`)
 
+- in `classical_sets.v`:
+  + `set_nil` from `choiceType` to `eqType`
+
 ### Deprecated
 
 ### Removed

classical/classical_sets.v

@@ -121,6 +121,10 @@ From mathcomp Require Import mathcomp_extra boolp.
 (*          pblock_index D F x == index i such that i \in D and x \in F i     *)
 (*                pblock D F x := F (pblock_index D F x)                      *)
 (*                                                                            *)
+(*   maximal_disjoint_subcollection F A B == A is a maximal (for inclusion)   *)
+(*                                   disjoint subcollection of the collection *)
+(*                                   B of elements in F : I -> set T          *)
+(*                                                                            *)
 (* * Upper and lower bounds:                                                  *)
 (*              ubound A == the set of upper bounds of the set A              *)
 (*              lbound A == the set of lower bounds of the set A              *)
@@ -1049,9 +1053,12 @@ apply/predeqP => x; split=> [[a ? [b ? <-]]|[[a b] [? ? <-]]]/=;
 by [exists (a, b) | exists a => //; exists b].
 Qed.
 
-Lemma set_nil (T : choiceType) : [set` [::]] = @set0 T.
+Lemma set_nil (T : eqType) : [set` [::]] = @set0 T.
 Proof. by rewrite predeqP. Qed.
 
+Lemma set_cons1 (T : eqType) (x : T) : [set` [:: x]] = [set x].
+Proof. by apply/seteqP; split => y /=; rewrite ?inE => /eqP. Qed.
+
 Lemma set_seq_eq0 (T : eqType) (S : seq T) : ([set` S] == set0) = (S == [::]).
 Proof.
 apply/eqP/eqP=> [|->]; rewrite predeqE //; case: S => // h t /(_ h).
@@ -2519,6 +2526,16 @@ Lemma trivIset_preimage1_in {aT} {rT : choiceType} (D : set rT) (A : set aT)
   (f : aT -> rT) : trivIset D (fun x => A `&` f @^-1` [set x]).
 Proof. by move=> y z _ _ [x [[_ <-] [_ <-]]]. Qed.
 
+Lemma trivIset_bigcup (I T : Type) (J : eqType) (D : J -> set I) (F : I -> set T) :
+  (forall n, trivIset (D n) F) ->
+  (forall n m i j, n != m -> D n i -> D m j -> F i `&` F j !=set0 -> i = j) ->
+  trivIset (\bigcup_k D k) F.
+Proof.
+move=> tB H; move=> i j [n _ Dni] [m _ Dmi] ij.
+have [nm|nm] := eqVneq n m; first by apply: (tB m) => //; rewrite -nm.
+exact: (H _ _ _ _ nm).
+Qed.
+
 Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i.
 
 Lemma coverE T I D (F : I -> set T) : cover D F = \bigcup_(i in D) F i.
@@ -2746,6 +2763,34 @@ Qed.
 
 End Zorn_subset.
 
+Definition maximal_disjoint_subcollection T I (F : I -> set T) (A B : set I) :=
+  [/\ A `<=` B, trivIset A F & forall C,
+      A `<` C -> C `<=` B -> ~ trivIset C F ].
+
+Section maximal_disjoint_subcollection.
+Context {I T : Type}.
+Variables (B : I -> set T) (D : set I).
+
+Let P := fun X => X `<=` D /\ trivIset X B.
+
+Let maxP (A : set (set I)) :
+  A `<=` P -> total_on A (fun x y => x `<=` y) -> P (\bigcup_(x in A) x).
+Proof.
+move=> AP h; split; first by apply: bigcup_sub => E /AP [].
+move=> i j [x Ax] xi [y Ay] yj ij; have [xy|yx] := h _ _ Ax Ay.
+- by apply: (AP _ Ay).2 => //; exact: xy.
+- by apply: (AP _ Ax).2 => //; exact: yx.
+Qed.
+
+Lemma ex_maximal_disjoint_subcollection :
+  { E | maximal_disjoint_subcollection B E D }.
+Proof.
+have /cid[E [[ED tEB] maxE]] := Zorn_bigcup maxP.
+by exists E; split => // F /maxE + FD; exact: contra_not.
+Qed.
+
+End maximal_disjoint_subcollection.
+
 Definition premaximal T (R : T -> T -> Prop) (t : T) :=
   forall s, R t s -> R s t.
 

classical/mathcomp_extra.v

@@ -1392,3 +1392,13 @@ exists f; split => //.
 intro n; induction n; simpl; apply: proj2_sig.
 Qed.
 End dependent_choice_Type.
+
+Lemma leq_ltn_expn m : exists n, (2 ^ n <= m.+1 < 2 ^ n.+1)%N.
+Proof.
+elim: m => [|m [n /andP[h1 h2]]]; first by exists O.
+have [m2n|nm2] := ltnP m.+2 (2 ^ n.+1)%N.
+  by exists n; rewrite m2n andbT (leq_trans h1).
+exists n.+1; rewrite nm2/= -addn1.
+rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r.
+by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
+Qed.

theories/lebesgue_integral.v

@@ -1,4 +1,3 @@
-
 (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C.              *)
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.