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/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/lebesgue_integral.v b/theories/lebesgue_integral.v index a5ce1ac3e..c72d988d9 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -601,9 +601,9 @@ 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. -Qed.*) Admitted. +move=> Afin Fm Ft. +by rewrite fsbig_finite// -measure_fin_bigcup// bigcup_fset_set. +Qed. Lemma additive_nnsfunr (g f : {nnsfun T >-> R}) x : \sum_(i \in range g) m (f @^-1` [set x] `&` (g @^-1` [set i])) = diff --git a/theories/measure.v b/theories/measure.v index 4e802ed0e..6a0b0ee9c 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1263,7 +1263,7 @@ Hint Resolve measure_ge0 : core. Hint Resolve measure_semi_additive : core. -Lemma measure_semi_additive' (n : nat) (F : 'I_n -> set T) : +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) -> @@ -1281,13 +1281,13 @@ rewrite -measure_semi_additive//. - by rewrite (eq_bigr (F' \o val)) in mUF. Qed. -Lemma measure_semi_additive'' (F : nat -> set T) (n : nat) : +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'. +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. @@ -1304,7 +1304,7 @@ elim/choicePpointed: I => I in D F *. 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'' (F \o f^-1))//= 1?trivIset_comp//. +rewrite (@measure_semi_additive_ord_I (F \o f^-1))//= 1?trivIset_comp//. by move=> k kn; apply: Fm; exact: funS. Qed. @@ -1346,7 +1346,7 @@ 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 !(big_mkcond P)/= measure_semi_additive'//. +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. @@ -2060,28 +2060,22 @@ Lemma Rmu_fin_bigcup (I : choiceType) (D : set I) (F : I -> set T) : Proof. move=> Dfin Ftriv Fm; rewrite /measure. have mUD : measurable (\bigcup_(i in D) F i : set rT). - apply: fin_bigcup_measurable => // ? ?; apply: sub_gen_smallest. + 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 fsbig_set0 fsbig_set1. -set E := (decomp _); have Em X := decomp_measurable mUD X. +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 {1}-> : X = \bigcup_(i in D) (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 content_fin_bigcup//. - - exact: trivIset_setI. - - by move=> i /mem_set Di; apply: measurableI; [exact: Em| exact: Fm]. - - have <- : X = \bigcup_(i in D) (X `&` F i). - by rewrite -setI_bigcupr setIidl//; exact: decomp_sub. - exact: Em. + 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). +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//; last exact: Fm. -- exact/decomp_finite_set. +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. @@ -2112,8 +2106,7 @@ have AUBtriv : trivIset (A `|` B) id. 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//=. -- rewrite fsbigU//= => [X /= [XA XB]]. - have [->//|/set0P[x Xx]] := eqVneq X set0. +- 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. @@ -2263,55 +2256,53 @@ 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. - split=> //; apply/set0P. - (*by rewrite fset_setK ?decompN0//; exact: decomp_finite_set.*) admit. + 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. - move=> x Xx; exists (i, X) => //=. - (*rewrite /K/= in_fset_set ?inE//; exact: decomp_finite_set.*) admit. + by move=> x Xx; exists (i, X). rewrite -(image_eq [bij of f^-1%FUN])/=. 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. - have [_] := 'invS_f (I : setT i). - (*rewrite fset_setK; last exact: decomp_finite_set. - by move=> /mem_set/decomp_measurable; apply; exact: Am.*) admit. + 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 in_fset_set; last first. - exact: decomp_finite_set. - move=> XD. - have Xm : measurable X by exact: decomp_measurable XD. - by apply: muS => // [i|]; [apply: mfD | apply: DXsub].*)admit. + rewrite nneseries_sum// fsbig_finite/=; last exact: decomp_finite_set. + rewrite [leLHS]big_seq_cond [leRHS]big_seq_cond. + rewrite lee_sum// => 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. - move=> x; rewrite in_fset_set; last exact: decomp_finite_set. - move=> xD. - rewrite -RmuE//; last by exact: mfD. + move=> x; rewrite in_fset_set=> [xD|]; last exact: decomp_finite_set. + rewrite -RmuE//; last exact: mfD. over. -(*rewrite -measure_fin_bigcup//=. +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 inE.*) admit. -Unshelve. all: by end_near. Admitted. +- 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. Proof. @@ -2340,14 +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. - rewrite -(fset_setK (decomp_finite_set _))//. - exact: countable_fset. - by apply/set0P; rewrite 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. @@ -2357,11 +2344,10 @@ 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. - by move/mem_set : f'iB => /decomp_sub; apply. - by move/mem_set : f'jB => /decomp_sub; apply. + - 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 [/= _ /mem_set] : K (f' i) by apply: funS. exact: decomp_measurable. @@ -2370,7 +2356,7 @@ 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. @@ -2398,21 +2384,18 @@ rewrite esum_bigcup//; last first. apply: (@trivIset_seqDU _ B) => //; exists y. by split => //; [exact: YBi|exact: YBj]. rewrite nneseries_esum// set_true le_esum// => i _. -rewrite [X in X <= _](_ : _ = \sum_(j <- fset_set (decomp (seqDU B i))) mu j); last first. - by rewrite -esum_fset// fset_setK//; exact: decomp_finite_set. -(*rewrite -SetRing.Rmu_fin_bigcup//=; last 3 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=> ?; exact: decomp_measurable. -rewrite -[leRHS]SetRing.RmuE// le_measure //. -- rewrite inE; apply: fin_bigcup_measurable. - exact: decomp_finite_set. +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. -- by rewrite cover_decomp. -Qed.*) admit. -Admitted. +Qed. End more_premeasure_ring_lemmas. @@ -3277,26 +3260,21 @@ rewrite ?lb_ereal_inf// => _ [F [Fm XS] <-]; rewrite ereal_inf_lb//; last first. by rewrite (eq_nneseries (fun _ _ => RmuE _ (Fm _))). pose K := [set: nat] `*`` fun i => decomp (F i). have /ppcard_eqP[f] : (K #= [set: nat])%card. - apply: cardMR_eq_nat => // i. - split. - by apply: finite_set_countable => //; exact: decomp_finite_set. - by apply/set0P; rewrite decompN0. -pose g i := (f^-1%FUN i).2. -exists g; first split. + 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 _))//. -rewrite esum_esum//=. -rewrite (reindex_esum K setT f) => //=. -rewrite [X in _ `*`` X](_ : _ = decomp \o F); last first. - apply/funext => n/=. - (*rewrite fset_setK//. - exact: decomp_finite_set.*) admit. +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. -Admitted. +Qed. End Rmu_ext.