diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 39442747b..b55a55209 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -3,7 +3,7 @@ ## [Unreleased] ### Added - + - in `ereal.v`: + lemmas `big_nat_widenl`, `big_geq_mkord` + lemmas `lee_sum_nneg_natr`, `lee_sum_nneg_natl` @@ -12,6 +12,18 @@ + lemmas `ereal_pseries_sum_nat`, `lte_lim` + lemmas `is_cvg_ereal_nneg_natsum_cond`, `is_cvg_ereal_nneg_natsum` + lemma `ereal_pseriesD`, `ereal_pseries0`, `eq_ereal_pseries` +- in `classical_sets.v`, lemma `subset_bigsetU_cond` +- in `measure.v`: + + lemma `eq_bigcupB_of_bigsetU` + + definitions `caratheodory_type` + + definition `caratheodory_measure` and lemma `caratheodory_measure_complete` + + internal definitions and lemmas that may be deprecated and hidden in the future: + * `caratheodory_measurable`, notation `... .-measurable`, + * `le_caratheodory_measurable`, `outer_measure_bigcup_lim`, + `caratheodory_measurable_{set0,setC,setU_le,setU,bigsetU,setI,setD}` + `disjoint_caratheodoryIU`, `caratheodory_additive`, + `caratheodory_lim_lee`, `caratheodory_measurable_trivIset_bigcup`, + `caratheodory_measurable_bigcup` ### Changed @@ -24,7 +36,7 @@ * lemmas `ereal_nondecreasing_series`, `ereal_nneg_series_lim_ge` * lemmas `is_cvg_ereal_nneg_series_cond`, `is_cvg_ereal_nneg_series` * lemmas `ereal_nneg_series_lim_ge0`, `ereal_nneg_series_pinfty` - +- in `classical_sets.v`, lemma `subset_bigsetU` ### Renamed diff --git a/theories/classical_sets.v b/theories/classical_sets.v index a5fa2719b..dbbbf138a 100644 --- a/theories/classical_sets.v +++ b/theories/classical_sets.v @@ -822,11 +822,19 @@ rewrite big_ord_recl /= (IHn (fun i => F i.+1)) predeqE => x; split. by move=> [[|i] Fi]; [left|right; exists i]. Qed. -Lemma subset_bigsetU m n F : (m <= n)%N -> - \big[setU/set0]_(i < m) F i `<=` \big[setU/set0]_(i < n) F i. +Lemma subset_bigsetU F : + {homo (fun n => \big[setU/set0]_(i < n) F i) : n m / (n <= m)%N >-> n `<=` m}. Proof. -rewrite !bigcup_ord => mn x [i im ?]; exists i => //. -by rewrite /mkset (leq_trans im). +move=> m n mn; rewrite !bigcup_ord => x [i im Fix]. +by exists i => //=; rewrite (leq_trans im). +Qed. + +Lemma subset_bigsetU_cond (P : pred nat) F : + {homo (fun n => \big[setU/set0]_(i < n | P i) F i) + : n m / (n <= m)%N >-> n `<=` m}. +Proof. +move=> n m nm; rewrite big_mkcond [in X in _ `<=` X]big_mkcond/=. +exact: (@subset_bigsetU (fun i => if P i then F i else _)). Qed. Lemma bigcap_ord n F : diff --git a/theories/measure.v b/theories/measure.v index 315298311..6d91e38ee 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -9,8 +9,6 @@ From HB Require Import structures. (******************************************************************************) (* Measure Theory *) (* *) -(* WIP. *) -(* *) (* semiRingOfSetsType == the type of semirings of sets *) (* ringOfSetsType == the type of rings of sets *) (* measurableType == the type of sigma-algebras *) @@ -35,6 +33,18 @@ From HB Require Import structures. (* of elements of type T where R is expected *) (* to be a numFieldType *) (* *) +(* mu.-measurable X == X is Caratheodory measurable for the outer measure mu, *) +(* i.e., forall Y, mu X = mu (X `&` Y) + mu (X `&` ~` Y) *) +(* *) +(* Caratheodory theorem: *) +(* caratheodory_type mu := T, where mu : {outer_measure set T -> {ereal R}} *) +(* it is a canonical mesurableType copy of T. *) +(* caratheodory_measure mu == the restriction of the outer measure mu to the *) +(* sigma algebra of Caratheodory measurable sets is a *) +(* measure *) +(* Remark: sets that are negligible for *) +(* caratheodory_measure are Caratheodory measurable *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -42,7 +52,9 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Reserved Notation "mu .-negligible" (at level 2, format "mu .-negligible"). Reserved Notation "{ 'ae' m , P }" (at level 0, format "{ 'ae' m , P }"). +Reserved Notation "mu .-measurable" (at level 2, format "mu .-measurable"). Local Open Scope classical_set_scope. Local Open Scope ring_scope. @@ -569,6 +581,16 @@ move=> -[m _] myBAmx; exists m => //=. by rewrite (eq_bigsetUB_of _ ndA) bigcup_ord; exists m => /=. Qed. +Lemma eq_bigcupB_of_bigsetU (A : (set T) ^nat) : + \bigcup_n (B_of (fun n => \big[setU/set0]_(i < n.+1) A i) n) = \bigcup_n A n. +Proof. +rewrite -(@eq_bigcupB_of (fun n => \big[setU/set0]_(i < n.+1) A i)) //. + rewrite eqEsubset; split => [t [i _]|t [i _ Ait]]. + by rewrite -bigcup_mkset => -[/= j _ Ajt]; exists j. + by exists i => //; rewrite big_ord_recr /=; right. +by move=> m n; rewrite -ltnS; exact/(@subset_bigsetU _ A). +Qed. + End trivIfy. (* 401,p.43 measure is continuous from below *) @@ -631,32 +653,32 @@ Variable (mu : {measure set T -> {ereal R}}). (* 404,p.44 measure satisfies generalized Boole's inequality *) Theorem generalized_Boole_inequality (A : (set T) ^nat) : - (forall i : nat, measurable (A i)) -> measurable (\bigcup_n A n) -> + (forall i, measurable (A i)) -> measurable (\bigcup_n A n) -> (mu (\bigcup_n A n) <= \sum_(i mA mbigcupA; set B := fun n => \big[setU/set0]_(i < n.+1) (A i). have AB : \bigcup_k A k = \bigcup_n B n. - rewrite predeqE => x; split. - by move=> -[k _ Akx]; exists k => //; rewrite /B big_ord_recr /=; right. - move=> -[m _]. - rewrite /B big_ord_recr /= => -[]. - by rewrite bigcup_ord => -[k km Akx]; exists k. - by move=> Amx; exists m. + rewrite predeqE => x; split => [[k _ ?]|[m _]]. + by exists k => //; rewrite /B big_ord_recr /=; right. + rewrite /B big_ord_recr /= => -[|Amx]; last by exists m. + by rewrite bigcup_ord => -[k ? ?]; exists k. have ndB : {homo B : n m / (n <= m)%N >-> n `<=` m}. - by move=> n m nm; apply subset_bigsetU. + by move=> n m; rewrite -ltnS; exact/subset_bigsetU. have mB : forall i, measurable (B i) by move=> i; exact: bigsetU_measurable. rewrite AB. -move/(@cvg_mu_inc _ _ mu _ mB _) : ndB => /(_ _)/cvg_lim <- //; last first. +move/(@cvg_mu_inc _ _ mu _ mB) : ndB => /(_ _)/cvg_lim <- //; last first. by rewrite -AB. have -> : lim (mu \o B) = ereal_sup ((mu \o B) @` setT). suff : nondecreasing_seq (mu \o B). - by move/nondecreasing_seq_ereal_cvg; apply/cvg_lim. + by move/nondecreasing_seq_ereal_cvg; exact/cvg_lim. move=> n m nm; apply: le_measure => //; try by rewrite inE; apply mB. - exact: subset_bigsetU. -have BA : forall m, (mu (B m) <= \sum_(i m; rewrite (le_trans (le_mu_bigsetU (measure_additive_measure mu) mA m.+1)) //. + by move: nm; rewrite -ltnS; exact/subset_bigsetU. +have BA : forall m, (mu (B m) <= \sum_(i m. + rewrite (le_trans (le_mu_bigsetU (measure_additive_measure mu) mA m.+1)) //. rewrite -(big_mkord xpredT (mu \o A)). - by apply: (@ereal_nneg_series_lim_ge _ (mu \o A) xpredT) => n _; exact: measure_ge0. + apply: (@ereal_nneg_series_lim_ge _ (mu \o A) xpredT) => n _. + exact: measure_ge0. by apply ub_ereal_sup => /= x [n _ <-{x}]; apply BA. Qed. @@ -669,8 +691,7 @@ Variables (R : realFieldType) (T : ringOfSetsType). Definition negligible (mu : set T -> {ereal R}) (N : set T) := exists A : set T, [/\ measurable A, mu A = 0%:E & N `<=` A]. -Local Notation "mu .-negligible" := (negligible mu) - (at level 2, format "mu .-negligible"). +Local Notation "mu .-negligible" := (negligible mu). Lemma negligibleP (mu : {measure _ -> _}) A : measurable A -> mu.-negligible A <-> mu A = 0%:E. @@ -699,15 +720,13 @@ Qed. End negligible. -Notation "mu .-negligible" := (negligible mu) - (at level 2, format "mu .-negligible"). +Notation "mu .-negligible" := (negligible mu) : type_scope. -Notation "{ 'ae' m , P }" := (almost_everywhere m (inPhantom P)) - (at level 0, format "{ 'ae' m , P }") : type_scope. +Notation "{ 'ae' m , P }" := (almost_everywhere m (inPhantom P)) : type_scope. Definition sigma_subadditive (R : numFieldType) (T : Type) (mu : set T -> {ereal R}) := forall (A : (set T) ^nat), - (mu (\bigcup_n (A n)) <= lim (fun n => \sum_(i < n) mu (A i)))%E. + (mu (\bigcup_n (A n)) <= \sum_(i (\sum_(i < n) mu (B i))%E) --> (mu (B 0%N) + mu (B 1%N))%E. + (fun n => \sum_(i < n) mu (B i))%E --> (mu (B 0%N) + mu (B 1%N))%E. rewrite -2!cvg_shiftS /=. rewrite [X in X --> _](_ : _ = (fun=> mu (B 0%N) + mu (B 1%N)))%E; last first. rewrite funeqE => i; rewrite 2!big_ord_recl /= big1 ?adde0 // => j _. @@ -783,9 +802,263 @@ have cvg_mu : exact: cvg_cst. have := outer_measure_sigma_subadditive mu B. suff : \bigcup_n B n = X. - by move=> -> /le_trans; apply; rewrite (cvg_lim _ cvg_mu). + move=> -> /le_trans; apply; under eq_fun do rewrite big_mkord. + by rewrite (cvg_lim _ cvg_mu). transitivity (\big[setU/set0]_(i < 2) B i). rewrite (bigcup_recl 2) // bigcup_ord [X in _ `|` X](_ : _ = set0) ?setU0 //. by rewrite predeqE => t; split => // -[]. by rewrite 2!big_ord_recl big_ord0 setU0 /= -setIUr setUCr setIT. Grab Existential Variables. all: end_near. Qed. + +Definition caratheodory_measurable (R : realType) (T : Type) + (mu : {outer_measure set T -> {ereal R}}) (A : set T) := forall X, + (mu X = mu (X `&` A) + mu (X `&` ~` A))%E. + +Notation "mu .-measurable" := (caratheodory_measurable mu) + (at level 2, format "mu .-measurable") : type_scope. + +Lemma le_caratheodory_measurable (R : realType) T + (mu : {outer_measure set T -> {ereal R}}) (A : set T) : + (forall X, (mu (X `&` A) + mu (X `&` ~` A) <= mu X)%E) -> + mu.-measurable A. +Proof. +move=> suf X; apply/eqP; rewrite eq_le; apply/andP; split; + [exact: le_outer_measureIC | exact: suf]. +Qed. + +Section caratheodory_theorem_sigma_algebra. + +Variables (R : realType) (T : Type) + (mu : {outer_measure set T -> {ereal R}}). + +Lemma outer_measure_bigcup_lim (A : (set T) ^nat) X : + (mu (X `&` \bigcup_k A k) <= \sum_(k X `&` A n))). +by apply/le_outer_measure; rewrite bigcup_distrr. +Qed. + +Let M := mu.-measurable. + +Lemma caratheodory_measurable_set0 : M set0. +Proof. by move=> X /=; rewrite setI0 outer_measure0 add0e setC0 setIT. Qed. + +Lemma caratheodory_measurable_setC A : M A -> M (~` A). +Proof. by move=> MA X; rewrite setCK addeC -MA. Qed. + +Lemma caratheodory_measurable_setU_le (X A B : set T) : + mu.-measurable A -> mu.-measurable B -> + (mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <= mu X)%E. +Proof. +move=> mA mB; pose Y := X `&` A `|` X `&` B `&` ~` A. +have /(lee_add2r (mu (X `&` ~` (A `|` B)))) : + (mu Y <= mu (X `&` A) + mu (X `&` B `&` ~` A))%E. + pose Z := bigcup2 (X `&` A) (X `&` B `&` ~` A). + have -> : Y = \bigcup_k Z k. + rewrite predeqE => t; split=> [[?|?]|[]]; [by exists O|by exists 1%N|]. + by move=> [_ ?|[_ ?|//]]; [left|right]. + rewrite (le_trans (outer_measure_sigma_subadditive mu Z)) //. + suff : ((fun n => \sum_(i < n) mu (Z i)) --> + mu (X `&` A) + mu (X `&` B `&` ~` A))%E. + move/cvg_lim => /=; under [in X in (X <= _)%E]eq_fun do rewrite big_mkord. + by move=> ->. + rewrite -(cvg_shiftn 2) /=; set l := (X in _ --> X). + rewrite [X in X --> _](_ : _ = cst l); first exact: cvg_cst. + rewrite funeqE => i; rewrite addn2 2!big_ord_recl big1 ?adde0 //. + by move=> ? _; exact: outer_measure0. +have /le_trans : (mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) <= + mu Y + mu (X `&` ~` (A `|` B)))%E. + rewrite setIUr (_ : X `&` A `|` X `&` B = Y) //. + rewrite /Y -[in LHS](setIT B) -(setUCr A) 2!setIUr setUC -[in RHS]setIA. + rewrite setUC setUA; congr (_ `|` _). + by rewrite setUidPl setICA; apply subIset; right. +suff -> : (mu (X `&` A) + mu (X `&` B `&` ~` A) + + mu (X `&` (~` (A `|` B))) = mu X)%E by exact. +by rewrite setCU setIA -(setIA X) setICA (setIC B) -addeA -mB -mA. +Qed. + +Lemma caratheodory_measurable_setU A B : M A -> M B -> M (A `|` B). +Proof. +move=> mA mB X; apply/eqP; rewrite eq_le. +by rewrite le_outer_measureIC andTb caratheodory_measurable_setU_le. +Qed. + +Lemma caratheodory_measurable_bigsetU (A : (set T) ^nat) : (forall n, M (A n)) -> + forall n, M (\big[setU/set0]_(i < n) A i). +Proof. +move=> MA; elim=> [|n ih]; first by rewrite big_ord0; exact: caratheodory_measurable_set0. +by rewrite big_ord_recr; apply caratheodory_measurable_setU. +Qed. + +Lemma caratheodory_measurable_setI A B : M A -> M B -> M (A `&` B). +Proof. +move=> mA mB; rewrite -(setCK A) -(setCK B) -setCU. +by apply/caratheodory_measurable_setC/caratheodory_measurable_setU; + exact/caratheodory_measurable_setC. +Qed. + +Lemma caratheodory_measurable_setD A B : M A -> M B -> M (A `\` B). +Proof. +move=> mA mB; rewrite setDE; apply caratheodory_measurable_setI => //. +exact: caratheodory_measurable_setC. +Qed. + +Section additive_ext_lemmas. +Variable A B : set T. +Hypothesis (mA : M A) (mB : M B). + +Let caratheodory_decomp X : + mu X = (mu (X `&` A `&` B) + mu (X `&` A `&` ~` B) + + mu (X `&` ~` A `&` B) + mu (X `&` ~` A `&` ~` B))%E. +Proof. by rewrite mA mB [X in (_ + _ + X)%E = _]mB addeA. Qed. + +Let caratheorody_decompIU X : mu (X `&` (A `|` B)) = + (mu (X `&` A `&` B) + mu (X `&` ~` A `&` B) + mu (X `&` A `&` ~` B))%E. +Proof. +rewrite caratheodory_decomp -!addeA; congr (mu _ + _)%E. + rewrite -!setIA; congr (_ `&` _). + by rewrite setIC; apply/setIidPl; apply subIset; left; left. +rewrite addeA addeC [X in (mu X + _)%E](_ : _ = set0); last first. + by rewrite -setIA -setCU -setIA setICr setI0. +rewrite outer_measure0 add0e addeC -!setIA; congr (mu (X `&` _) + mu (X `&` _))%E. +by rewrite setIC; apply/setIidPl; apply subIset; right; right. +by rewrite setIC; apply/setIidPl; apply subIset; left; left. +Qed. + +Lemma disjoint_caratheodoryIU X : [disjoint A & B] -> + (mu (X `&` (A `|` B)) = mu (X `&` A) + mu (X `&` B))%E. +Proof. +move=> /eqP AB; rewrite caratheodory_decomp -setIA AB setI0 outer_measure0. +rewrite add0e addeC -setIA -setCU -setIA setICr setI0 outer_measure0 add0e. +rewrite -!setIA; congr (mu (X `&` _ ) + mu (X `&` _))%E. +rewrite (setIC A) setIA setIC; apply/setIidPl. +- by rewrite setIUl setICr setU0 subsetI; move/disjoints_subset in AB; split. +- rewrite setIA setIC; apply/setIidPl; rewrite setIUl setICr set0U. + by move: AB; rewrite setIC => /disjoints_subset => AB; rewrite subsetI; split. +Qed. +End additive_ext_lemmas. + +Lemma caratheodory_additive (A : (set T) ^nat) : (forall n, M (A n)) -> + trivIset setT A -> forall n X, + mu (X `&` \big[setU/set0]_(i < n) A i) = (\sum_(i < n) mu (X `&` A i))%E. +Proof. +move=> MA ta; elim=> [|n ih] X; first by rewrite !big_ord0 setI0 outer_measure0. +rewrite big_ord_recr /= disjoint_caratheodoryIU // ?ih ?big_ord_recr //. +- exact: caratheodory_measurable_bigsetU. +- by apply/eqP/(@trivIset_bigUI _ predT) => //; rewrite /predT /= trueE. +Qed. + +Lemma caratheodory_lim_lee (A : (set T) ^nat) : (forall n, M (A n)) -> + trivIset setT A -> forall X, + (\sum_(k MA tA X. +set A' := \bigcup_k A k; set B := fun n => \big[setU/set0]_(k < n) (A k). +suff : forall n, (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` A') <= mu X)%E. + move=> XA; rewrite (_ : lim _ = ereal_sup + ((fun n => \sum_(k < n) mu (X `&` A k))%E @` setT)); last first. + under eq_fun do rewrite big_mkord. + apply/cvg_lim => //; apply/nondecreasing_seq_ereal_cvg. + apply: (lee_sum_nneg_ord (fun n => mu (X `&` A n)) xpredT) => n _. + exact: outer_measure_ge0. + move XAx : (mu (X `&` ~` A')) => [x| |]. + - rewrite -lee_subr_addr; apply ub_ereal_sup => /= _ [n _] <-. + by rewrite lee_subr_addr -XAx XA. + - suff : mu X = +oo%E by move=> ->; rewrite lee_pinfty. + apply/eqP; rewrite -lee_pinfty_eq -XAx le_outer_measure //. + by apply subIset; left. + - by rewrite addeC /= lee_ninfty. +move=> n. +apply (@le_trans _ _ (\sum_(k < n) mu (X `&` A k) + mu (X `&` ~` B n))%E). + apply/lee_add2l/le_outer_measure; apply: setIS; apply: subsetC => t. + by rewrite /B bigcup_ord => -[i ? ?]; exists i. +rewrite [in X in (_ <= X)%E](caratheodory_measurable_bigsetU MA n) lee_add2r //. +by rewrite caratheodory_additive. +Qed. + +Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) : + (forall n, M (A n)) -> trivIset setT A -> M (\bigcup_k (A k)). +Proof. +move=> MA tA; apply le_caratheodory_measurable => X /=. +have /(lee_add2r (mu (X `&` ~` \bigcup_k A k))) := outer_measure_bigcup_lim A X. +by move/le_trans; apply; exact: caratheodory_lim_lee. +Qed. + +Lemma caratheodory_measurable_bigcup (A : (set T) ^nat) : (forall n, M (A n)) -> + M (\bigcup_k (A k)). +Proof. +set C_of := B_of (fun n => \big[setU/set0]_(i < n.+1) A i). +move=> MA; rewrite -eq_bigcupB_of_bigsetU. +apply/caratheodory_measurable_trivIset_bigcup; last first. + apply: (@trivIset_B_of _ (fun n => \big[setU/set0]_(i < n.+1) A i)). + by move=> n m; rewrite -ltnS; exact/subset_bigsetU. +by case=> [|n /=]; [| apply/caratheodory_measurable_setD => //]; + exact/caratheodory_measurable_bigsetU. +Qed. + +End caratheodory_theorem_sigma_algebra. + +Definition caratheodory_type (R : realType) (T : Type) + (mu : {outer_measure set T -> {ereal R}}) := T. + +Section caratheodory_sigma_algebra. +Variables (R : realType) (T : Type) (mu : {outer_measure set T -> {ereal R}}). + +HB.instance Definition caratheodory_mixin := @isMeasurable.Build + (caratheodory_type mu) mu.-measurable + (caratheodory_measurable_set0 mu) + (@caratheodory_measurable_setC _ _ mu) + (@caratheodory_measurable_bigcup _ _ mu). + +End caratheodory_sigma_algebra. + +Section caratheodory_measure. +Variables (R : realType) (T : Type) (mu : {outer_measure set T -> {ereal R}}). +Local Notation U := (caratheodory_type mu). + +Lemma caratheodory_measure0 : mu (set0 : set U) = 0%:E. +Proof. exact: outer_measure0. Qed. + +Lemma caratheodory_measure_ge0 (A : set U) : + measurable A -> (0%:E <= mu A)%E. +Proof. by move=> mx; apply outer_measure_ge0. Qed. + +Lemma caratheodory_measure_sigma_additive : semi_sigma_additive (mu : set U -> _). +Proof. +move=> A mA tA mbigcupA; set B := \bigcup_k A k. +suff : forall X, (mu X = \sum_(k _) = (fun n => (\sum_(k < n) mu (A k))%E)); last first. + rewrite funeqE => n; rewrite big_mkord; apply eq_bigr => i _; congr (mu _). + by rewrite setIC; apply/setIidPl => t Ait; exists i. + move=> ->; have := fun n (_ : xpredT n) => outer_measure_ge0 mu (A n). + move/(@is_cvg_ereal_nneg_series _ _) => /cvg_ex[l] hl. + under eq_fun do rewrite -(big_mkord xpredT (mu \o A)). + by move/(@cvg_lim _ (@ereal_hausdorff R)) : (hl) => ->. +move=> X. +have mB : mu.-measurable B := caratheodory_measurable_bigcup mA. +apply/eqP; rewrite eq_le (caratheodory_lim_lee mA tA X) andbT. +have /(lee_add2r (mu (X `&` ~` B))) := outer_measure_bigcup_lim mu A X. +by rewrite -le_caratheodory_measurable // => ?; rewrite -mB. +Qed. + +Definition caratheodory_measure_mixin := Measure.Axioms caratheodory_measure0 + caratheodory_measure_ge0 caratheodory_measure_sigma_additive. +Definition caratheodory_measure : {measure set U -> {ereal R}} := + Measure caratheodory_measure_mixin. + +Lemma caratheodory_measure_complete (B : set U) : + caratheodory_measure.-negligible B -> measurable B. +Proof. +move=> [A [mA muA0 BA]]; apply le_caratheodory_measurable => X. +suff -> : mu (X `&` B) = 0%:E. + by rewrite add0e le_outer_measure //; apply subIset; left. +have muB0 : mu B = 0%:E. + apply/eqP; rewrite eq_le outer_measure_ge0 andbT. + by apply: (le_trans (le_outer_measure mu BA)); rewrite -muA0. +apply/eqP; rewrite eq_le outer_measure_ge0 andbT. +have : X `&` B `<=` B by apply subIset; right. +by move/(le_outer_measure mu); rewrite muB0 => ->. +Qed. + +End caratheodory_measure. diff --git a/theories/sequences.v b/theories/sequences.v index 74188c480..5adf61962 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -810,7 +810,6 @@ Notation "\sum_ ( i