diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 9618c5235..4662b6c9b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -94,6 +94,16 @@ - in `lebesgue_measure.v`: + notation `_.-ocitv` + definition `ocitv_display` +- in `classical_sets.v`: + + lemmas `trivIset_image`, `trivIset_comp` + + notation `trivIsets` +- in `functions.v`: + + lemma `patch_pred`, `trivIset_restr` +- in `measure.v`: + + lemma `measure_semi_additive_ord`, `measure_semi_additive_ord_I` + + lemma `decomp_finite_set` +- in `esum.v`: + + lemma `fsbig_esum` ### Changed @@ -140,6 +150,13 @@ * `mem_factor_itv` - lemma `preimage_cst` generalized and moved from `lebesgue_integral.v` to `functions.v` +- in `fsbig.v`: + + generalize `exchange_fsum` ++ in `measure.v`: + + statement of lemmas `content_fin_bigcup`, `measure_fin_bigcup`, `ring_fsets`, + `decomp_triv`, `cover_decomp`, `decomp_set0`, `decompN0`, `Rmu_fin_bigcup` + + definitions `decomp`, `measure` ++ lemma `fset_set_image` moved from `measure.v` to `cardinality.v` ### Renamed @@ -156,6 +173,8 @@ - in `lebesgue_measure.v`: + `itvs` -> `ocitv_type` + `measurable_fun_sum` -> `emeasurable_fun_sum` +- in `classical_sets.v`: + + `trivIset_restr` -> `trivIset_widen` ### Removed diff --git a/theories/classical_sets.v b/theories/classical_sets.v index 7e3f05a8f..ba602409b 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -2346,6 +2346,22 @@ apply/trivIsetP => -[/=|]; rewrite /bigcup2 /=. by move=> [//|j _ _ _]; rewrite setI0. Qed. +Lemma trivIset_image (T I I' : Type) (D : set I) (f : I -> I') (F : I' -> set T) : + trivIset D (F \o f) -> trivIset (f @` D) F. +Proof. +by move=> trivF i j [{}i Di <-] [{}j Dj <-] Ffij; congr (f _); apply: trivF. +Qed. +Arguments trivIset_image {T I I'} D f F. + +Lemma trivIset_comp (T I I' : Type) (D : set I) (f : I -> I') (F : I' -> set T) : + {in D &, injective f} -> + trivIset D (F \o f) = trivIset (f @` D) F. +Proof. +move=> finj; apply/propext; split; first exact: trivIset_image. +move=> trivF i j Di Dj Ffij; apply: finj; rewrite ?in_setE//. +by apply: trivF => //=; [exists i| exists j]. +Qed. + Definition cover T I D (F : I -> set T) := \bigcup_(i in D) F i. Lemma cover_restr T I D' D (F : I -> set T) : @@ -2380,11 +2396,13 @@ Definition pblock T (I : pointedType) D (F : I -> set T) (x : T) := (* TODO: theory of trivIset, cover, partition, pblock_index and pblock *) +Notation trivIsets X := (trivIset X id). + 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. + trivIset D F -> trivIsets [set F i | i in D]. +Proof. exact: trivIset_image. Qed. -Lemma trivIset_restr T I D' D (F : I -> set T) : +Lemma trivIset_widen 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. diff --git a/theories/esum.v b/theories/esum.v index 36717403a..403a752be 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -1,7 +1,7 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From mathcomp Require Import all_ssreflect ssralg ssrnum finmap. Require Import boolp reals mathcomp_extra ereal classical_sets signed topology. -Require Import sequences functions cardinality normedtype numfun. +Require Import sequences functions cardinality normedtype numfun fsbigop. (******************************************************************************) (* Summation over classical sets *) @@ -105,6 +105,9 @@ move=> Afin a0; rewrite -esum_fset => [|i]; rewrite ?fset_setK//. by rewrite in_fset_set ?inE//; apply: a0. Qed. +Lemma fsbig_esum (A : set T) a : finite_set A -> (forall x, 0 <= a x) -> + \sum_(x \in A) (a x) = \esum_(x in A) a x. +Proof. by move=> *; rewrite fsbig_finite//= sum_fset_set. Qed. End esum_realType. Lemma esum_ge [R : realType] [T : choiceType] (I : set T) (a : T -> \bar R) x : diff --git a/theories/fsbigop.v b/theories/fsbigop.v index c40a05af8..c1f0ec728 100644 --- a/theories/fsbigop.v +++ b/theories/fsbigop.v @@ -522,12 +522,12 @@ move=> /andP[Pi Qi]; exists i; rewrite 2?inE ?andbT//. by exists j; rewrite 2?inE ?andbT. Qed. -Lemma exchange_fsum (T : choiceType) (R : realDomainType) (P Q : set T) - (f : T -> T -> \bar R) : +Lemma exchange_fsum (T1 T2 : choiceType) (R : realDomainType) (P : set T1) (Q : set T2) + (f : T1 -> T2 -> \bar R) : finite_set P -> finite_set Q -> (\sum_(i \in P) \sum_(j \in Q) f i j = \sum_(j \in Q) \sum_(i \in P) f i j)%E. Proof. -move=> Pfin Qfin; rewrite 2?pair_fsum//; pose swap (x : T * T) := (x.2, x.1). +move=> Pfin Qfin; rewrite 2?pair_fsum//; pose swap (x : T2 * T1) := (x.2, x.1). apply: (reindex_fsbig swap). split=> [? [? ?]//|[? ?] [? ?] /set_mem[? ?] /set_mem[? ?] [-> ->]//|]. by move=> [i j] [? ?]; exists (j, i). diff --git a/theories/functions.v b/theories/functions.v index 9ae1d2b8b..154ad8a65 100644 --- a/theories/functions.v +++ b/theories/functions.v @@ -1800,6 +1800,10 @@ End patch. Notation restrict := (patch (fun=> point)). Notation "f \_ D" := (restrict D f) : fun_scope. +Lemma patch_pred {I T} (D : {pred I}) (d f : I -> T) : + patch d D f = fun i => if D i then f i else d i. +Proof. by apply/funext => i; rewrite /patch mem_setE. Qed. + Lemma preimage_restrict (aT : Type) (rT : pointedType) (f : aT -> rT) (D : set aT) (B : set rT) : (f \_ D) @^-1` B = (if point \in B then ~` D else set0) `|` D `&` f @^-1` B. @@ -1835,6 +1839,18 @@ Lemma restrict_comp {aT} {rT sT : pointedType} (h : rT -> sT) (f : aT -> rT) D : Proof. by move=> hp; apply/funext => x; rewrite /patch/=; case: ifP. Qed. Arguments restrict_comp {aT rT sT} h f D. +Lemma trivIset_restr (T I : Type) (D D' : set I) (F : I -> set T) : + trivIset D' (F \_ D) = trivIset (D `&` D') F. +Proof. +apply/propext; split=> FDtriv i j. + move=> [Di D'i] [Dj D'j] [x [Fix Fjx]]; apply: FDtriv => //. + by exists x; split => /=; rewrite ?patchT ?in_setE. +move=> D'i D'j [x []]; rewrite /patch. +do 2![case: ifPn => //]; rewrite !in_setE => Di Dj Fix Fjx. +by apply: FDtriv => //; exists x. +Qed. + + (**************************************) (* Restriction of domain and codomain *) (**************************************) diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 83be5092b..c72d988d9 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -601,8 +601,8 @@ Lemma measure_fsbig (I : choiceType) (A : set I) (F : I -> set T) : (forall i, A i -> measurable (F i)) -> trivIset A F -> m (\big[setU/set0]_(i \in A) F i) = \sum_(i \in A) m (F i). Proof. -move=> Afin Fm Ft; rewrite !fsbig_finite//=. -by rewrite -!bigcup_fset_set// measure_fin_bigcup. +move=> Afin Fm Ft. +by rewrite fsbig_finite// -measure_fin_bigcup// bigcup_fset_set. Qed. Lemma additive_nnsfunr (g f : {nnsfun T >-> R}) x : diff --git a/theories/measure.v b/theories/measure.v index f34aaad19..6a0b0ee9c 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1263,40 +1263,49 @@ Hint Resolve measure_ge0 : core. Hint Resolve measure_semi_additive : core. +Lemma measure_semi_additive_ord (n : nat) (F : 'I_n -> set T) : + (forall (k : 'I_n), measurable (F k)) -> + trivIset setT F -> + measurable (\big[setU/set0]_(k < n) F k) -> + mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i). +Proof. +move=> mF tF mUF; pose F' (i : nat) := oapp F set0 (insub i). +have FE (i : 'I_n) : F i = (F' \o val) i by rewrite /F'/= valK/=. +rewrite (eq_bigr (F' \o val))// (eq_bigr (mu \o F' \o val))//; last first. + by move=> i _; rewrite FE. +rewrite -measure_semi_additive//. +- by move=> k; rewrite /F'; case: insubP => /=. +- apply/trivIsetP=> i j _ _; rewrite /F'. + do 2?[case: insubP; rewrite ?(set0I, setI0)//= => ? _ <-]. + by move/trivIsetP: tF; apply. +- by rewrite (eq_bigr (F' \o val)) in mUF. +Qed. + +Lemma measure_semi_additive_ord_I (F : nat -> set T) (n : nat) : + (forall k, (k < n)%N -> measurable (F k)) -> + trivIset `I_n F -> + measurable (\big[setU/set0]_(k < n) F k) -> + mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i). +Proof. +move=> mF tF; apply: measure_semi_additive_ord. + by move=> k; apply: mF. +by rewrite trivIset_comp// ?(image_eq [surjfun of val])//; apply: 'inj_val. +Qed. + Lemma content_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) : finite_set D -> trivIset D F -> (forall i, D i -> measurable (F i)) -> measurable (\bigcup_(i in D) F i) -> - mu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i). -Proof. -move=> Dfin Ftriv Fm UFm; pose G (i : option I) : set T := oapp (F \_ D) set0 i. -have UFG : \bigcup_(i in D) F i = \bigcup_(i in [set Some x | x in D]) G i. - apply/predeqP => x; split=> [[i Di Fix]|[[]// _ [i Di [<- /=]]]]. - by exists (Some i) => //=; rewrite ?patchT ?inE//; exists i. - by rewrite ?patchT ?inE// => Fix; exists i. -suff muG : mu (\bigcup_(i in some @` D) G i) = \sum_(i <- fset_set (some @` D)) mu (G i). - transitivity (mu (\bigcup_(i in some @` D) G i)); first by rewrite UFG. - rewrite muG fset_set_image// (big_imfset _ _ _ (in2W Some_inj))/=. - by apply: eq_big_seq => X; rewrite in_fset_set// => XD; rewrite patchT. -have oDfin: finite_set (Some @` D) by exact: finite_image. -rewrite bigcup_fset_set//= !(big_nth None) !big_mkord. -set s : seq (option I) := fset_set (some @` D). -rewrite (@measure_semi_additive _ _ _ mu (fun i => G (nth None s i)))//. -- move=> i; case: (ltnP i (size s)) => [/(mem_nth None)|/(nth_default _)->//=]. - rewrite in_fset_set// inE/= => -[j Dj <-]//=. - by rewrite patchT ?inE//; apply: Fm. -- move=> m n _ _. - case: (ltnP m (size s)) => [lt_ms|/(nth_default _)->]; last first. - by rewrite set0I => -[]. - case: (ltnP n (size s)) => [lt_ns|/(nth_default _)->]; last first. - by rewrite setI0 => -[]. - have := mem_nth None lt_ns; have := mem_nth None lt_ms. - rewrite !in_fset_set// !inE/= => -[i Di ieq]/= -[j Dj jeq]. - rewrite -ieq -jeq/= !patchT ?inE// => /(Ftriv _ _ Di Dj) eqij. - by have := jeq; rewrite -eqij ieq => /uniqP; apply => //; rewrite fset_uniq. -- rewrite -(big_mkord predT (fun i => G (nth None s i))) -(big_nth None xpredT). - by rewrite -bigcup_fset_set// -UFG. + mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i). +Proof. +elim/choicePpointed: I => I in D F *. + by rewrite !emptyE => *; rewrite fsbig_set0 bigcup0. +move=> [n /ppcard_eqP[f]] Ftriv Fm UFm. +rewrite -(image_eq [surjfun of f^-1%FUN])/= in UFm Ftriv *. +rewrite bigcup_image fsbig_image//= bigcup_mkord -fsbig_ord/= in UFm *. +rewrite (@measure_semi_additive_ord_I (F \o f^-1))//= 1?trivIset_comp//. +by move=> k kn; apply: Fm; exact: funS. Qed. Lemma measure_semi_additive2 : semi_additive2 mu. @@ -1327,7 +1336,7 @@ Lemma measure_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) : finite_set D -> trivIset D F -> (forall i, D i -> measurable (F i)) -> - mu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i). + mu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i). Proof. move=> Dfin Ftriv Fm; rewrite content_fin_bigcup//. exact: fin_bigcup_measurable. @@ -1337,14 +1346,11 @@ Lemma measure_bigsetU_ord_cond n (P : {pred 'I_n}) (F : 'I_n -> set T) : (forall i : 'I_n, P i -> measurable (F i)) -> trivIset P F -> mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E. Proof. -move=> mF tF; rewrite -bigcup_set_cond measure_fin_bigcup//=; last first. -- by move=> i /andP[_ /mF]. -- by apply: sub_trivIset tF => i /andP[]. -rewrite -[RHS]big_filter; apply: perm_big. -rewrite uniq_perm ?fset_uniq ?filter_uniq ?index_enum_uniq//=. -move=> i; rewrite in_fset_set// ?mem_filter. - by apply/idP/idP; rewrite ?inE/= andbC. -by rewrite set_andb/=; apply: finite_setIr. +move=> mF tF; rewrite !(big_mkcond P)/= measure_semi_additive_ord//. +- by apply: eq_bigr => i _; rewrite (fun_if mu) measure0. +- by move=> k; case: ifP => //; apply: mF. +- by rewrite -patch_pred trivIset_restr setIT. +- by apply: bigsetU_measurable=> k _; case: ifP => //; apply: mF. Qed. Lemma measure_bigsetU_ord n (P : {pred 'I_n}) (F : 'I_n -> set T) : @@ -1357,7 +1363,9 @@ Qed. Lemma measure_fbigsetU (I : choiceType) (A : {fset I}) (F : I -> set T) : (forall i, i \in A -> measurable (F i)) -> trivIset [set` A] F -> mu (\big[setU/set0]_(i <- A) F i) = (\sum_(i <- A) mu (F i))%E. -Proof. by move=> mF tF; rewrite -bigcup_fset measure_fin_bigcup// set_fsetK. Qed. +Proof. +by move=> mF tF; rewrite -bigcup_fset measure_fin_bigcup// -fsbig_seq. +Qed. End additive_measure_on_ring_of_sets. @@ -1959,82 +1967,87 @@ rewrite -bigcup2inE; apply: mdU => //; last by move=> [|[]]// _; apply: mdDI. by move=> [|[]]// [|[]]//= _ _ []; rewrite setDE ?setIA => X [] []//. Qed. -Lemma ring_fsets (A : set rT) : measurable A -> exists B : {fset set T}, - [/\ all [pred X | X != set0] B, - trivIset [set` B] id, +Lemma ring_fsets (A : set rT) : measurable A -> exists B : set (set T), + [/\ finite_set B, + (forall X, B X -> X !=set0), + trivIset B id, (forall X : set T, X \in B -> measurable X) & - A = \bigcup_(X in [set` B]) X]. + A = \bigcup_(X in B) X]. Proof. rewrite ring_measurableE => -[B [-> Bm Bfin Btriv]]. -exists [fset X in fset_set B | X != set0]%fset; split => //. -- by apply/allP => _ /imfsetP[/= X /andP[_ +] ->]. -- move=> _ _ /imfsetP[X /andP[+ _] ->] /imfsetP[Y/= /andP[+ _] ->]. - by rewrite !in_fset_set ?inE//; apply: Btriv. -- by move=> _ /imfsetP[X /andP[+ _] ->]; rewrite in_fset_set// inE; apply: Bm. -rewrite bigcup_fset big_imfset//= big_filter big_rmcond; last first. - by move=> X; rewrite negbK => /eqP. -by rewrite -bigcup_fset_set. +exists (B `&` [set X | X != set0]); split. +- by apply: sub_finite_set Bfin; exact: subIsetl. +- by move=> ?/= [_ /set0P]. +- by move=> X Y/= [XB _] [YB _]; exact: Btriv. +- by move=> X/= /[!inE] -[] /Bm. +rewrite bigcup_mkcondr; apply eq_bigcupr => X Bx; case: ifPn => //. +by rewrite notin_set/= => /negP/negPn/eqP. Qed. -Definition decomp (A : set rT) : {fset set T} := - if A == set0 then [fset set0]%fset else - if pselect (measurable A) is left mA then projT1 (cid (ring_fsets mA)) else [fset A]%fset. +Definition decomp (A : set rT) : set (set T) := + if A == set0 then [set set0] else + if pselect (measurable A) is left mA then projT1 (cid (ring_fsets mA)) else + [set A]. + +Lemma decomp_finite_set (A : set rT) : finite_set (decomp A). +Proof. +rewrite /decomp; case: ifPn => // A0; case: pselect => // X. +by case: cid => /= ? []. +Qed. -Lemma decomp_triv (A : set rT) : trivIset [set` decomp A] id. +Lemma decomp_triv (A : set rT) : trivIset (decomp A) id. Proof. -rewrite /decomp; case: ifP => _. - by move=> i j; rewrite /= !inE => -> ->. +rewrite /decomp; case: ifP => _; first by move=> i j/= -> ->. case: pselect => // Am; first by case: cid => //= ? []. -by move=> i j /=; rewrite !inE => -> ->. +by move=> i j /= -> ->. Qed. Hint Resolve decomp_triv : core. -Lemma all_decomp_neq0 (A : set rT) : A !=set0 -> all [pred X | X != set0] (decomp A). +Lemma all_decomp_neq0 (A : set rT) : + A !=set0 -> (forall X, decomp A X -> X !=set0). Proof. move=> /set0P AN0; rewrite /decomp/= (negPf AN0). case: pselect => //= Am; first by case: cid => //= ? []. -by apply/allP => X; rewrite !inE => ->. +by move=> X ->; exact/set0P. Qed. Lemma decomp_neq0 (A : set rT) X : A !=set0 -> X \in decomp A -> X !=set0. -Proof. by move=> /all_decomp_neq0/allP/[apply]/set0P. Qed. +Proof. by move=> /all_decomp_neq0/(_ X) /[!inE]. Qed. Lemma decomp_measurable (A : set rT) (X : set T) : measurable A -> X \in decomp A -> measurable X. Proof. -rewrite /decomp; case: ifP => _; first by rewrite inE => _ /eqP->. -by case: pselect => // Am _; case: cid => //= ? [_ _ + _]; apply. +rewrite /decomp; case: ifP => _; first by rewrite inE => _ ->. +by case: pselect => // Am _; case: cid => //= ? [_ _ _ + _]; apply. Qed. -Lemma cover_decomp (A : set rT) : \bigcup_(X in [set` decomp A]) X = A. +Lemma cover_decomp (A : set rT) : \bigcup_(X in decomp A) X = A. Proof. -rewrite /decomp; case: ifP => [/eqP->|_]. - by rewrite set_fset1 bigcup_set1. +rewrite /decomp; case: ifP => [/eqP->|_]; first by rewrite bigcup0. case: pselect => // Am; first by case: cid => //= ? []. -by rewrite set_fset1 bigcup_set1. +by rewrite bigcup_set1. Qed. Lemma decomp_sub (A : set rT) (X : set T) : X \in decomp A -> X `<=` A. Proof. -rewrite /decomp; case: ifP => _; first by rewrite !inE => ->. -case: pselect => //= Am; last by rewrite inE => /eqP->. -by case: cid => //= D [_ _ _ ->] XD; exact: bigcup_sup. +rewrite /decomp; case: ifP => _; first by rewrite inE/= => ->//. +case: pselect => //= Am; last by rewrite inE => ->. +by case: cid => //= D [_ _ _ _ ->] /[!inE] XD; apply: bigcup_sup. Qed. -Lemma decomp_set0 : decomp set0 = [fset set0]%fset. +Lemma decomp_set0 : decomp set0 = [set set0]. Proof. by rewrite /decomp eqxx. Qed. -Lemma decompN0 (A : set rT) : decomp A != fset0. +Lemma decompN0 (A : set rT) : decomp A != set0. Proof. -rewrite /decomp; case: ifPn => [_|AN0]. - by apply/fset0Pn; exists set0; rewrite inE. -case: pselect=> //= Am; last by apply/fset0Pn; exists A; rewrite inE. -case: cid=> //= D [_ _ _ Aeq]; apply: contra_neq AN0; rewrite Aeq => ->. -by rewrite set_fset0 bigcup_set0. +rewrite /decomp; case: ifPn => [_|AN0]; first by apply/set0P; exists set0. +case: pselect=> //= Am; last by apply/set0P; exists A. +case: cid=> //= D [_ _ _ _ Aeq]; apply: contra_neq AN0; rewrite Aeq => ->. +by rewrite bigcup_set0. Qed. Definition measure (R : numDomainType) (mu : set T -> \bar R) - (A : set rT) : \bar R := \sum_(X <- decomp A) mu X. + (A : set rT) : \bar R := \sum_(X \in decomp A) mu X. Section additive_measure. Context {R : realFieldType} (mu : {additive_measure set T -> \bar R}). @@ -2042,41 +2055,41 @@ Local Notation Rmu := (measure mu). Arguments big_trivIset {I D T R idx op} A F. Lemma Rmu_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) : - finite_set D -> trivIset D F -> (forall i, D i -> measurable (F i)) -> - Rmu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i). + finite_set D -> trivIset D F -> (forall i, i \in D -> measurable (F i)) -> + Rmu (\bigcup_(i in D) F i) = \sum_(i \in D) mu (F i). Proof. move=> Dfin Ftriv Fm; rewrite /measure. have mUD : measurable (\bigcup_(i in D) F i : set rT). - apply: fin_bigcup_measurable => // i Di. - by apply: sub_gen_smallest; apply: Fm. + apply: fin_bigcup_measurable => // *; apply: sub_gen_smallest. + exact/Fm/mem_set. have [->|/set0P[i0 Di0]] := eqVneq D set0. - by rewrite bigcup_set0 decomp_set0 big_seq_fset1 fset_set0 big_seq_fset0. -set E := (decomp _); have Em X := decomp_measurable mUD X. -transitivity (\sum_(X <- E) \sum_(i <- fset_set D) mu (X `&` F i)). - apply: eq_big_seq => /= X XE. - have Xeq : X = \bigcup_(i in D) (X `&` F i). - by rewrite -setI_bigcupr setIidl//; apply: decomp_sub. - rewrite -content_fin_bigcup// -?Xeq//; last exact: Em. - exact: trivIset_setI. - by move=> i Di; apply: measurableI; [apply: Em| apply: Fm]. -rewrite exchange_big; apply: eq_big_seq => i; rewrite in_fset_set ?inE//= => Di. -have Feq : F i = \bigcup_(X in [set` E]) (X `&` F i). - by rewrite -setI_bigcupl setIidr// cover_decomp; apply: bigcup_sup. -rewrite -[E]set_fsetK -content_fin_bigcup -?Feq//; last exact: Fm. - exact/trivIset_setIr/decomp_triv. -by move=> X /= XE; apply: measurableI; [apply: Em | apply: Fm]. + by rewrite bigcup_set0 decomp_set0 fsbig_set0 fsbig_set1. +set E := decomp _; have Em X := decomp_measurable mUD X. +transitivity (\sum_(X \in E) \sum_(i \in D) mu (X `&` F i)). + apply eq_fsbigr => /= X XE; have XDF : X = \bigcup_(i in D) (X `&` F i). + by rewrite -setI_bigcupr setIidl//; exact: decomp_sub. + rewrite [in LHS]XDF content_fin_bigcup//; first exact: trivIset_setI. + - by move=> i /mem_set Di; apply: measurableI; [exact: Em|exact: Fm]. + - by rewrite -XDF; exact: Em. +rewrite exchange_fsum //; last exact: decomp_finite_set. +apply eq_fsbigr => i Di; have Feq : F i = \bigcup_(X in E) (X `&` F i). + rewrite -setI_bigcupl setIidr// cover_decomp. + by apply/bigcup_sup; exact: set_mem. +rewrite -content_fin_bigcup -?Feq//; [exact/decomp_finite_set| | |exact/Fm]. +- exact/trivIset_setIr/decomp_triv. +- by move=> X /= XE; apply: measurableI; [apply: Em; rewrite inE | exact: Fm]. Qed. Lemma RmuE (A : set T) : measurable A -> Rmu A = mu A. Proof. move=> Am; rewrite -[A in LHS](@bigcup_set1 _ unit _ tt). -by rewrite Rmu_fin_bigcup// ?fset_set1// ?big_seq_fset1// => -[]. +by rewrite Rmu_fin_bigcup// ?fsbig_set1// => -[]. Qed. Let Rmu0 : Rmu set0 = 0. Proof. rewrite -(bigcup_set0 (fun _ : void => set0)). -by rewrite Rmu_fin_bigcup// fset_set0 big_seq_fset0. +by rewrite Rmu_fin_bigcup// fsbig_set0. Qed. Lemma Rmu_ge0 A : Rmu A >= 0. @@ -2085,17 +2098,17 @@ Proof. by rewrite sume_ge0. Qed. Lemma Rmu_additive : semi_additive Rmu. Proof. apply/(additive2P Rmu0) => // A B. -move=> /ring_fsets[/= {}A [_ Atriv Am ->]] /ring_fsets[/= {}B [_ Btriv Bm ->]]. +move=> /ring_fsets[/= {}A [? _ Atriv Am ->]] /ring_fsets[/= {}B [? _ Btriv Bm ->]]. rewrite -subset0 => coverAB0. -have AUBfin : finite_set ([set` A] `|` [set` B]) by rewrite finite_setU. -have AUBtriv : trivIset ([set` A] `|` [set` B]) id. - move=> X Y [] ABX [] ABY; do ?by [apply: Atriv|apply: Btriv]. +have AUBfin : finite_set (A `|` B) by rewrite finite_setU. +have AUBtriv : trivIset (A `|` B) id. + move=> X Y [] ABX [] ABY; do ?by [exact: Atriv|exact: Btriv]. by move=> [u [Xu Yu]]; case: (coverAB0 u); split; [exists X|exists Y]. by move=> [u [Xu Yu]]; case: (coverAB0 u); split; [exists Y|exists X]. -rewrite -bigcup_setU !Rmu_fin_bigcup//=; last by move=> X [/Am|/Bm]. -rewrite -!fsbig_finite//= fsbigU//= => [X /= [XA XB]]. -have [->//|/set0P[x Xx]] := eqVneq X set0. -by case: (coverAB0 x); split; [exists X|exists X]. +rewrite -bigcup_setU !Rmu_fin_bigcup//=. +- rewrite fsbigU//= => [X /= [XA XB]]; have [->//|/set0P[x Xx]] := eqVneq X set0. + by case: (coverAB0 x); split; exists X. +- by move=> X /set_mem [|] /mem_set ?; [exact: Am|exact: Bm]. Qed. #[export] @@ -2243,13 +2256,15 @@ Import SetRing. Lemma ring_sigma_sub_additive : sigma_sub_additive mu -> sigma_sub_additive Rmu. Proof. move=> muS; move=> /= D A Am Dm Dsub. -rewrite /Rmu -(eq_nneseries (fun _ _ => esum_fset _))//. +rewrite /Rmu (eq_nneseries (fun _ _ => fsbig_esum _ _))//; last first. + by move=> *; exact: decomp_finite_set. rewrite nneseries_esum ?esum_esum//=; last by move=> *; rewrite esum_ge0. set K := _ `*`` _. have /ppcard_eqP[f] : (K #= [set: nat])%card. apply: cardMR_eq_nat => [|i]. by rewrite (_ : [set _ | true] = setT)//; exact/predeqP. - by split=> //; apply/set0P; rewrite set_fset_eq0 decompN0. + split; first by apply/finite_set_countable; exact: decomp_finite_set. + exact/set0P/decompN0. have {Dsub} : D `<=` \bigcup_(k in K) k.2. apply: (subset_trans Dsub); apply: bigcup_sub => i _. rewrite -[A i]cover_decomp; apply: bigcup_sub => X/= XAi. @@ -2259,27 +2274,34 @@ rewrite (esum_set_image _ f^-1)//= bigcup_image => Dsub. have DXsub X : X \in decomp D -> X `<=` \bigcup_i ((f^-1%FUN i).2 `&` X). move=> XD; rewrite -setI_bigcupl -[Y in Y `<=` _](setIidr (decomp_sub XD)). by apply: setSI. -have mf i : measurable (((f^-1)%function i).2). - by have [_ /decomp_measurable] := 'invS_f (I : setT i); apply; apply: Am. +have mf i : measurable ((f^-1)%function i).2. + have [_ /mem_set/decomp_measurable] := 'invS_f (I : setT i). + by apply; exact: Am. have mfD i X : X \in decomp D -> measurable (((f^-1)%FUN i).2 `&` X : set T). - by move=> XD; apply: measurableI; [apply: mf|apply: (decomp_measurable _ XD)]. + by move=> XD; apply: measurableI; [exact: mf|exact: (decomp_measurable _ XD)]. apply: (@le_trans _ _ - (\sum_(i X; rewrite andbT => XD. - have Xm : measurable X by exact: decomp_measurable XD. - by apply: muS => // [i|]; [apply: mfD | apply: DXsub]. + (\sum_(i X /[!(andbT,in_fset_set)]; last exact: decomp_finite_set. + move=> XD; have Xm := decomp_measurable Dm XD. + by apply: muS => // [i|]; [exact: mfD|exact: DXsub]. apply: lee_lim => /=; do ?apply: is_cvg_nneseries=> //. by move=> n _; exact: sume_ge0. near=> n; rewrite [n in _ <= n]big_mkcond; apply: lee_sum => i _. rewrite ifT ?inE//. -under eq_big_seq do [rewrite -RmuE//; last exact: mfD]. -rewrite -[decomp _]set_fsetK -measure_fin_bigcup//=; last 2 first. +under eq_big_seq. + move=> x; rewrite in_fset_set=> [xD|]; last exact: decomp_finite_set. + rewrite -RmuE//; last exact: mfD. + over. +rewrite -fsbig_finite/=; last exact: decomp_finite_set. +rewrite -measure_fin_bigcup//=. +- rewrite -setI_bigcupr (cover_decomp D) -[leRHS]RmuE// ?le_measure ?inE//. + by apply: measurableI => //; apply: sub_gen_smallest; apply: mf. + by apply: sub_gen_smallest; apply: mf. +- exact: decomp_finite_set. - by apply: trivIset_setI; apply: decomp_triv. -- by move=> X /= XD; apply: sub_gen_smallest; apply: mfD. -rewrite -setI_bigcupr (cover_decomp D) -[leRHS]RmuE// ?le_measure ?inE//. - by apply: measurableI => //; apply: sub_gen_smallest; apply: mf. -by apply: sub_gen_smallest; apply: mf. +- by move=> X /= XD; apply: sub_gen_smallest; apply: mfD; rewrite inE. Unshelve. all: by end_near. Qed. Lemma ring_sigma_additive : sigma_sub_additive mu -> semi_sigma_additive Rmu. @@ -2309,12 +2331,10 @@ rewrite XE; move: (XE); rewrite seqDU_bigcup_eq. under eq_bigcupr do rewrite -[seqDU B _]cover_decomp//. rewrite bigcup_bigcup_dep; set K := _ `*`` _. have /ppcard_eqP[f] : (K #= [set: nat])%card. - apply: cardMR_eq_nat=> // i; split=> //. - by apply/set0P; rewrite set_fset_eq0 decompN0. -pose f' := f^-1%FUN. -rewrite -(image_eq [bij of f'])/= bigcup_image/=. -pose g n := (f' n).2. -have fVtriv : trivIset [set: nat] g. + apply: cardMR_eq_nat=> // i; split; last by apply/set0P; rewrite decompN0. + exact/finite_set_countable/decomp_finite_set. +pose f' := f^-1%FUN; rewrite -(image_eq [bij of f'])/= bigcup_image/=. +pose g n := (f' n).2; have fVtriv : trivIset [set: nat] g. move=> i j _ _; rewrite /g. have [/= _ f'iB] : K (f' i) by apply: funS. have [/= _ f'jB] : K (f' j) by apply: funS. @@ -2324,55 +2344,57 @@ have fVtriv : trivIset [set: nat] g. by case: (f' i) (f' j) => [? ?] [? ?]//= -> ->. move=> [x [f'ix f'jx]]; have Bij := @trivIset_seqDU _ B (f' i).1 (f' j).1 I I. rewrite Bij ?eqxx// in f'ij; exists x; split. - exact: (decomp_sub f'iB). - exact: (decomp_sub f'jB). + - by move/mem_set : f'iB => /decomp_sub; apply. + - by move/mem_set : f'jB => /decomp_sub; apply. have g_inj : set_inj [set i | g i != set0] g. - apply: trivIset_inj=> [i /set0P//|]. - by apply: sub_trivIset fVtriv. + by apply: trivIset_inj=> [i /set0P//|]; apply: sub_trivIset fVtriv. move=> XEbig; rewrite measure_semi_bigcup//= -?XEbig//; last first. - move=> i; have [/= _ f'iB] : K (f' i) by apply: funS. - by apply: decomp_measurable f'iB. + move=> i; have [/= _ /mem_set] : K (f' i) by apply: funS. + exact: decomp_measurable. rewrite [leLHS](_ : _ = \sum_(i i _; rewrite ifT ?inE//=; case: ifPn => //. by rewrite notin_set /= -/(g _) => /negP/negPn/eqP ->. rewrite -(esum_pred_image mu g)//. -rewrite [esum _ _](_ : _ = \esum_(X in range g) mu X); last first. +rewrite [leLHS](_ : _ = \esum_(X in range g) mu X); last first. rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum. move=> Y _; case: ifPn; rewrite ?(inE, notin_set)/=. by move=> [i giN0 giY]; rewrite ifT// ?inE//=; exists i. move=> Ngx; case: ifPn; rewrite ?(inE, notin_set)//=. move=> [i _ giY]; apply: contra_not_eq Ngx; rewrite -giY => mugi. by exists i => //; apply: contra_neq mugi => ->; rewrite measure0. -have -> : range g = \bigcup_i [set` decomp (seqDU B i)]. +have -> : range g = \bigcup_i (decomp (seqDU B i)). apply/predeqP => /= Y; split => [[n _ gnY]|[n _ /= YBn]]. have [/= _ f'nB] : K (f' n) by apply: funS. by exists (f' n).1 => //=; rewrite -gnY. - by exists (f (n, Y)) => //; rewrite /g /f' funK//= inE; split. + by exists (f (n, Y)) => //; rewrite /g /f' funK//= inE. rewrite esum_bigcup//; last first. move=> i j /=. have [->|/set0P DUBiN0] := eqVneq (seqDU B i) set0. rewrite decomp_set0 ?set_fset1 => /negP[]. - apply/eqP/predeqP=> x; split=> [[Y ->]|->]//=; first by rewrite measure0. + apply/eqP/predeqP=> x; split=> [[Y/=->]|->]//; first by rewrite measure0. by exists set0. have [->|/set0P DUBjN0] := eqVneq (seqDU B j) set0. rewrite decomp_set0 ?set_fset1 => _ /negP[]. - apply/eqP/predeqP=> x; split=> [[Y ->]|->]//=; first by rewrite measure0. + apply/eqP/predeqP=> x; split=> [[Y/=->]|->]//=; first by rewrite measure0. by exists set0. - move=> _ _ [Y /= [/[dup]+ /decomp_sub YBi /decomp_sub YBj]]. + move=> _ _ [Y /= [/[dup] +]]. + move=> /mem_set /decomp_sub YBi /mem_set + /mem_set /decomp_sub YBj. move=> /(decomp_neq0 DUBiN0) [y Yy]. apply: (@trivIset_seqDU _ B) => //; exists y. by split => //; [exact: YBi|exact: YBj]. rewrite nneseries_esum// set_true le_esum// => i _. -rewrite esum_fset// -[decomp _]set_fsetK. -rewrite -SetRing.Rmu_fin_bigcup//=; last 2 first. +rewrite [leLHS](_ : _ = \sum_(j \in decomp (seqDU B i)) mu j); last first. + by rewrite fsbig_esum//; exact: decomp_finite_set. +rewrite -SetRing.Rmu_fin_bigcup//=; last 3 first. + exact: decomp_finite_set. exact: decomp_triv. - by move=> ?; apply: decomp_measurable. -rewrite -[leRHS]SetRing.RmuE// le_measure ?inE//=. -- apply: fin_bigcup_measurable=> // j /= jdec. - by apply: sub_gen_smallest; exact: decomp_measurable jdec. -- exact: sub_gen_smallest. -- by rewrite cover_decomp. + by move=> ?; exact: decomp_measurable. +rewrite -[leRHS]SetRing.RmuE// le_measure//; last by rewrite cover_decomp. +- rewrite inE; apply: fin_bigcup_measurable; first exact: decomp_finite_set. + move=> j /mem_set jdec; apply: sub_gen_smallest. + exact: decomp_measurable jdec. +- by rewrite inE; apply: sub_gen_smallest; exact: Am. Qed. End more_premeasure_ring_lemmas. @@ -3236,20 +3258,22 @@ apply/funeqP => /= X; rewrite /mu_ext/=; apply/eqP; rewrite eq_le. rewrite ?lb_ereal_inf// => _ [F [Fm XS] <-]; rewrite ereal_inf_lb//; last first. exists F; first by split=> // i; apply: sub_gen_smallest. by rewrite (eq_nneseries (fun _ _ => RmuE _ (Fm _))). -pose K := [set: nat] `*`` fun i => [set` decomp (F i)]. +pose K := [set: nat] `*`` fun i => decomp (F i). have /ppcard_eqP[f] : (K #= [set: nat])%card. - apply: cardMR_eq_nat => // i. - by split=> //; apply/set0P; rewrite set_fset_eq0 decompN0. -pose g i := (f^-1%FUN i).2. -exists g; first split. -- move=> k; have [/= _] : K (f^-1%FUN k) by apply: funS. + apply: cardMR_eq_nat => // i; split; last by apply/set0P; rewrite decompN0. + by apply: finite_set_countable => //; exact: decomp_finite_set. +pose g i := (f^-1%FUN i).2; exists g; first split. +- move=> k; have [/= _ /mem_set] : K (f^-1%FUN k) by apply: funS. exact: decomp_measurable. - move=> i /XS [k _]; rewrite -[F k]cover_decomp => -[D /= DFk Di]. by exists (f (k, D)) => //; rewrite /g invK// inE. rewrite !nneseries_esum//= /measure ?set_true. -rewrite -[RHS](eq_esum (fun _ _ => esum_fset _))// esum_esum//=. -rewrite (reindex_esum K setT f) => //=; apply: eq_esum => i Ki. -by rewrite /g funK ?inE. +transitivity (\esum_(i in setT) \sum_(X0 \in decomp (F i)) mu X0); last first. + by apply eq_esum => /= k _; rewrite fsbig_finite//; exact: decomp_finite_set. +rewrite (eq_esum (fun _ _ => fsbig_esum _ _))//; last first. + by move=> ? _; exact: decomp_finite_set. +rewrite esum_esum//= (reindex_esum K setT f) => //=. +by apply: eq_esum => i Ki; rewrite /g funK ?inE. Qed. End Rmu_ext.