From e3796f3cd04b6e32f1b941a0d127906121a0d268 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 19 Feb 2021 11:51:07 +0900 Subject: [PATCH] generalize the defintion of trivIset Co-authored-by: Cyril Cohen --- CHANGELOG_UNRELEASED.md | 10 ++++ theories/classical_sets.v | 103 ++++++++++++++++++++++++++++++++------ theories/measure.v | 38 +++++++------- 3 files changed, 118 insertions(+), 33 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9206ee165..becf8ca15 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -16,6 +16,13 @@ - in `normedtype.v`, lemmas `nbhs0_lt`, `nbhs'0_lt`, `interior_closed_ballE`, open_nbhs_closed_ball` - in `classical_sets.v`, lemmas `subset_has_lbound`, `subset_has_ubound` +- in `classical_sets.v`, lemma `mksetE` + +- in `classical_sets.v`: + + definitions `cover`, `partition`, `pblock_index`, `pblock` + + lemmas `trivIsetP`, `trivIset_sets`, `trivIset_restr`, `perm_eq_trivIset` + + lemma `fdisjoint_cset` + - in `reals.v`, lemmas `sup_setU`, `inf_setU` - in `boolp.v`, lemmas `iff_notr`, `iff_not2` - in `reals.v`, lemmas `RtointN`, `floor_le0` @@ -44,6 +51,9 @@ + same change for `<` + change extended to notations `_ <= _ <= _`, `_ < _ <= _`, `_ <= _ < _`, `_ < _ < _` +- in `classical_sets.v`: + + generalization and change of `trivIset` (and thus lemmas `trivIset_bigUI` and `trivIset_setI`) + ### Renamed - in `normedtype.v`, `bounded_on` -> `bounded_near` diff --git a/theories/classical_sets.v b/theories/classical_sets.v index 5397dc1e4..c10d2d0f6 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -230,6 +230,9 @@ Definition setM T1 T2 (A1 : set T1) (A2 : set T2) := [set z | A1 z.1 /\ A2 z.2]. Definition fst_set T1 T2 (A : set (T1 * T2)) := [set x | exists y, A (x, y)]. Definition snd_set T1 T2 (A : set (T1 * T2)) := [set y | exists x, A (x, y)]. +Lemma mksetE (P : T -> Prop) x : [set x | P x] x = P x. +Proof. by []. Qed. + Definition bigsetI T I (P : set I) (F : I -> set T) := [set a | forall i, P i -> F i a]. Definition bigsetU T I (P : set I) (F : I -> set T) := @@ -567,6 +570,15 @@ Proof. by rewrite 2!setDE setCI setCK setIUr setICr set0U. Qed. End basic_lemmas. +(* TODO: other lemmas that relate fset and classical sets *) +Lemma fdisjoint_cset (T : choiceType) (A B : {fset T}) : + [disjoint A & B]%fset = ([set x | x \in A] `&` [set x | x \in B] == set0). +Proof. +rewrite -fsetI_eq0; apply/idP/idP; apply: contraLR. +by move=> /set0P[t [tA tB]]; apply/fset0Pn; exists t; rewrite inE; apply/andP. +by move=> /fset0Pn[t]; rewrite inE => /andP[tA tB]; apply/set0P; exists t. +Qed. + Section SetMonoids. Variable (T : Type). @@ -775,20 +787,6 @@ Lemma preimage_bigcap {aT rT I} (P : set I) (f : aT -> rT) F : f @^-1` (\bigcap_ (i in P) F i) = \bigcap_(i in P) (f @^-1` F i). Proof. exact/predeqP. Qed. -Definition trivIset T (F : nat -> set T) := - forall i j, i != j -> F i `&` F j = set0. - -Lemma trivIset_bigUI T (F : nat -> set T) : trivIset F -> - forall n m, n <= m -> \big[setU/set0]_(i < n) F i `&` F m = set0. -Proof. -move=> tF; elim => [|n ih m]; first by move=> m _; rewrite big_ord0 set0I. -by rewrite ltn_neqAle => /andP[? ?]; rewrite big_ord_recr setIUl tF ?setU0 ?ih. -Qed. - -Lemma trivIset_setI T (F : nat -> set T) : trivIset F -> - forall A, trivIset (fun n => A `&` F n). -Proof. by move=> tF A j i /tF; apply: subsetI_eq0; apply subIset; right. Qed. - Lemma setM0 T1 T2 (A1 : set T1) : A1 `*` set0 = set0 :> set (T1 * T2). Proof. by rewrite predeqE => -[t u]; split => // -[]. Qed. @@ -944,6 +942,83 @@ Proof. exact: (xgetPN point). Qed. End PointedTheory. +Section partitions. + +Definition trivIset T I (D : set I) (F : I -> set T) := + forall i j : I, D i -> D j -> F i `&` F j !=set0 -> i = j. + +Lemma trivIsetP {T} {I : eqType} {D : set I} {F : I -> set T} : + trivIset D F <-> + forall i j : I, D i -> D j -> i != j -> F i `&` F j = set0. +Proof. +split=> tDF i j Di Dj; first by apply: contraNeq => /set0P/tDF->. +by move=> /set0P; apply: contraNeq => /tDF->. +Qed. + +Lemma trivIset_bigUI T (D : {pred nat}) (F : nat -> set T) : trivIset D F -> + forall n m, D m -> n <= m -> \big[setU/set0]_(i < n | D i) F i `&` F m = set0. +Proof. +move=> /trivIsetP tA; elim => [|n IHn] m Dm. + by move=> _; rewrite big_ord0 set0I. +move=> lt_nm; rewrite big_mkcond/= big_ord_recr -big_mkcond/=. +rewrite setIUl IHn 1?ltnW// set0U. +by case: ifPn => [Dn|NDn]; rewrite ?set0I// tA// ltn_eqF. +Qed. + +Lemma trivIset_setI T I D (F : I -> set T) X : + trivIset D F -> trivIset D (fun i => X `&` F i). +Proof. +move=> tDF i j Di Dj; rewrite setIACA setIid => -[x [_ Fijx]]. +by apply: tDF => //; exists x. +Qed. + +Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i. + +Definition partition T I D (F : I -> set T) (A : set T) := + [/\ cover D F = A, trivIset D F & forall i, D i -> F i !=set0]. + +Definition pblock_index T (I : pointedType) D (F : I -> set T) (x : T) := + get (fun i => D i /\ F i x). + +Definition pblock T (I : pointedType) D (F : I -> set T) (x : T) := + F (pblock_index D F x). + +(* TODO: theory of trivIset, cover, partition, pblock_index and pblock *) + +Lemma trivIset_sets T I D (F : I -> set T) : + trivIset D F -> trivIset [set F i | i in D] id. +Proof. by move=> DF A B [i Di <-{A}] [j Dj <-{B}] /DF ->. Qed. + +Lemma trivIset_restr T I D' D (F : I -> set T) : +(* D `<=` D' -> (forall i, D i -> ~ D' i -> F i !=set0) ->*) + D `<=` D' -> (forall i, D' i -> ~ D i -> F i = set0) -> + trivIset D F = trivIset D' F. +Proof. +move=> DD' DD'F. +rewrite propeqE; split=> [DF i j D'i D'j FiFj0|D'F i j Di Dj FiFj0]. + have [Di|Di] := pselect (D i); last first. + by move: FiFj0; rewrite (DD'F i) // set0I => /set0P; rewrite eqxx. + have [Dj|Dj] := pselect (D j). + - exact: DF. + - by move: FiFj0; rewrite (DD'F j) // setI0 => /set0P; rewrite eqxx. +by apply D'F => //; apply DD'. +Qed. + +Lemma perm_eq_trivIset {T : eqType} (s1 s2 : seq (set T)) : perm_eq s1 s2 -> + trivIset setT (fun i => nth set0 s1 i) -> + trivIset setT (fun i => nth set0 s2 i). +Proof. +rewrite perm_sym => /(perm_iotaP set0)[s ss1 s12] /trivIsetP /(_ _ _ I I) ts1. +apply/trivIsetP => i j _ _ ij. +rewrite {}s12 {s2}; have [si|si] := ltnP i (size s); last first. + by rewrite (nth_default set0) ?size_map// set0I. +rewrite (nth_map O) //; have [sj|sj] := ltnP j (size s); last first. + by rewrite (nth_default set0) ?size_map// setI0. +by rewrite (nth_map O) // ts1 // nth_uniq // (perm_uniq ss1) iota_uniq. +Qed. + +End partitions. + Definition total_on T (A : set T) (R : T -> T -> Prop) := forall s t, A s -> A t -> R s t \/ R t s. diff --git a/theories/measure.v b/theories/measure.v index cc5010c2a..beed537ad 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -235,12 +235,12 @@ Definition semi_additive2 := forall A B, measurable A -> measurable B -> A `&` B = set0 -> mu (A `|` B) = (mu A + mu B)%E. Definition semi_additive := - forall A, (forall i, measurable (A i)) -> trivIset A -> + forall A, (forall i : nat, measurable (A i)) -> trivIset setT A -> (forall n, measurable (\big[setU/set0]_(i < n) A i)) -> forall n, mu (\big[setU/set0]_(i < n) A i) = (\sum_(i < n) mu (A i))%E. Definition semi_sigma_additive := - forall A, (forall i, measurable (A i)) -> trivIset A -> + forall A, (forall i : nat, measurable (A i)) -> trivIset setT A -> measurable (\bigcup_n A n) -> (fun n => (\sum_(i < n) mu (A i))%E) --> mu (\bigcup_n A n). @@ -248,18 +248,19 @@ Definition additive2 := forall A B, measurable A -> measurable B -> A `&` B = set0 -> mu (A `|` B) = (mu A + mu B)%E. Definition additive := - forall A, (forall i, measurable (A i)) -> trivIset A -> + forall A, (forall i : nat, measurable (A i)) -> trivIset setT A -> forall n, mu (\big[setU/set0]_(i < n) A i) = (\sum_(i < n) mu (A i))%E. Definition sigma_additive := - forall A, (forall i, measurable (A i)) -> trivIset A -> + forall A, (forall i : nat, measurable (A i)) -> trivIset setT A -> (fun n => (\sum_(i < n) mu (A i))%E) --> mu (\bigcup_n A n). Lemma semi_additive2P : mu set0 = 0%:E -> semi_additive <-> semi_additive2. Proof. -move=> mu0; split => [amx A B mA mB mAB AB|a2mx A mA ATI mbigA n]. +move=> mu0; split => [amx A B mA mB mAB AB|a2mx A mA /trivIsetP ATI mbigA n]. set C := bigcup2 A B. - have tC : trivIset C by move=> [|[|i]] [|[|j]]; rewrite ?set0I ?setI0// setIC. + have tC : trivIset setT C. + by apply/trivIsetP => -[|[|i]] [|[|j]]; rewrite ?set0I ?setI0// setIC. have mC : forall i, measurable (C i). by move=> [|[]] //= i; exact: measurable0. have := amx _ mC tC _ 2%N; rewrite !big_ord_recl !big_ord0 adde0/= setU0. @@ -272,12 +273,10 @@ move=> mu0; split => [amx A B mA mB mAB AB|a2mx A mA ATI mbigA n]. elim: n => [|n IHn] in A mA ATI mbigA *. by rewrite !big_ord0. rewrite big_ord_recr /= a2mx //; last 3 first. - exact: mbigA. - have := mbigA n.+1. - by rewrite big_ord_recr. - rewrite big_distrl /= big1 // => i _; apply: ATI; rewrite lt_eqF //. - exact: ltn_ord. -by rewrite IHn // [in RHS]big_ord_recr. +- exact: mbigA. +- by have := mbigA n.+1; rewrite big_ord_recr. +- by rewrite big_distrl /= big1 // => i _; rewrite ATI// ltn_eqF. +- by rewrite IHn // [in RHS]big_ord_recr. Qed. End semi_additivity. @@ -309,7 +308,8 @@ Lemma semi_sigma_additive_is_additive Proof. move=> mu0 samu; apply/semi_additive2P => // A B mA mB mAB AB_eq0. pose C := bigcup2 A B. -have tC : trivIset C by move=> [|[|i]] [|[|j]]; rewrite ?setI0 ?set0I// setIC. +have tC : trivIset setT C. + by apply/trivIsetP=> -[|[|i]] [|[|j]]; rewrite ?setI0 ?set0I// setIC. have -> : A `|` B = \bigcup_i C i. rewrite predeqE => x; split. by case=> [Ax|Bx]; by [exists 0%N|exists 1%N]. @@ -516,12 +516,12 @@ Definition B_of (A : (set T) ^nat) := fun n => if n isn't n'.+1 then A O else A n `\` A n'. Lemma trivIset_B_of (A : (set T) ^nat) : - {homo A : n m / (n <= m)%nat >-> n `<=` m} -> trivIset (B_of A). + {homo A : n m / (n <= m)%nat >-> n `<=` m} -> trivIset setT (B_of A). Proof. -move=> ndA i j; wlog : i j / (i < j)%N. - move=> h; rewrite neq_ltn => /orP[|] ?; by - [rewrite h // ltn_eqF|rewrite setIC h // ltn_eqF]. -move=> ij _; move: j i ij; case => // j [_ /=|n]. +move=> ndA i j _ _; wlog ij : i j / (i < j)%N => [/(_ _ _ _) tB|]. + by have [ij /tB->|ij|] := ltngtP i j; rewrite //setIC => /tB->. +move=> /set0P; apply: contraNeq => _; apply/eqP. +case: j i ij => // j [_ /=|n]. rewrite funeqE => x; rewrite propeqE; split => // -[A0 [Aj1 Aj]]. exact/Aj/(ndA O). rewrite ltnS => nj /=; rewrite funeqE => x; rewrite propeqE; split => //. @@ -586,7 +586,7 @@ Lemma cvg_mu_inc (A : (set T) ^nat) : mu \o A --> mu (\bigcup_n A n). Proof. move=> mA mbigcupA ndA. -have Binter : trivIset (B_of A) := trivIset_B_of ndA. +have Binter : trivIset setT (B_of A) := trivIset_B_of ndA. have ABE : forall n, A n.+1 = A n `|` B_of A n.+1 := UB_of ndA. have AE n : A n = \big[setU/set0]_(i < n.+1) (B_of A) i := eq_bigsetUB_of n ndA. have -> : \bigcup_n A n = \bigcup_n (B_of A) n := eq_bigcupB_of ndA.