From b05674c58d3a9960f4382d2fcdceaf0e156abf84 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 17 Jun 2021 23:54:30 +0900 Subject: [PATCH 1/4] extension theorem - build an outer measure out of a measure over a ring of sets --- CHANGELOG_UNRELEASED.md | 9 ++ theories/measure.v | 177 +++++++++++++++++++++++++++++++++++++++- theories/sequences.v | 12 +++ 3 files changed, 196 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f5c58612c..3b3d37542 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,6 +21,15 @@ + lemmas `bigcupD1`, `bigcapD1` - in `measure.v`: + definition `measurable_fun` + + lemma `adde_undef_nneg_series` +- in `measure.v`: + + lemmas `epsilon_trick`, + + definition `measurable_cover` + + lemmas `cover_measurable`, `cover_subset` + + definition `mu_ext` + + lemmas `le_mu_ext`, `mu_ext_ge0`, `mu_ext0`, `measurable_uncurry`, + `mu_ext_sigma_subadditive` + + canonical `outer_measure_of_measure` ### Changed diff --git a/theories/measure.v b/theories/measure.v index 001838ce0..d97514220 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -2,8 +2,8 @@ From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice seq fintype order bigop. From mathcomp Require Import ssralg ssrnum finmap. -Require Import boolp classical_sets reals ereal posnum topology normedtype. -Require Import sequences. +Require Import boolp classical_sets reals ereal posnum nngnum topology. +Require Import normedtype sequences cardinality csum. From HB Require Import structures. (******************************************************************************) @@ -52,6 +52,15 @@ From HB Require Import structures. (* Remark: sets that are negligible for *) (* caratheodory_measure are Caratheodory measurable *) (* *) +(* Extension theorem: *) +(* measurable_cover X == the set of sequences F such that *) +(* - forall i, F i is measurable *) +(* - X `<=` \bigcup_i (F i) *) +(* mu_ext mu == the extension of the measure mu, a measure over a *) +(* ring of sets; it is an outer measure, declared as *) +(* canonical (i.e., we have the notation *) +(* [outer_measure of mu_ext mu]) *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -1088,3 +1097,167 @@ by move/(le_outer_measure mu); rewrite muB0 => ->. Qed. End caratheodory_measure. + +Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) (e : {nonneg R}) + (P : pred nat) : (forall n, 0%E <= A n) -> + \sum_(i A0; rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) + + \sum_(0 <= i < n) (e%:nngnum / (2 ^ i)%:R)%:E))) //. + rewrite ereal_pseriesD //; last by move=> n _; apply: divr_ge0. + rewrite ereal_limD //. + - rewrite lee_add2l //; apply: lee_lim => //. + + by apply: is_cvg_ereal_nneg_series => n _; apply: divr_ge0. + + by apply: is_cvg_ereal_nneg_series => n _; apply: divr_ge0. + + by near=> n; apply: lee_sum_nneg_subset => // i _; apply divr_ge0. + - exact: is_cvg_ereal_nneg_series. + - by apply: is_cvg_ereal_nneg_series => n _; apply: divr_ge0. + - by apply: adde_undef_nneg_series => // n _; apply: divr_ge0. +have cvggeo : (fun n => \sum_(0 <= i < n) (e%:nngnum / (2 ^ i)%:R)%:E) --> + (2 * e%:nngnum)%:E. + rewrite (_ : (fun n => _) = @EFin _ \o series (geometric e%:nngnum 2^-1)). + apply: cvg_comp. + - by apply: cvg_geometric_series; rewrite ger0_norm // invf_lt1 // ltr1n. + - rewrite (_ : [filter of _] = [filter of (2 * e%:nngnum)%R : R^o]) //. + rewrite filter_of_filterE; congr ([filter of _]); rewrite mulrC. + congr (_ * _)%R; apply mulr1_eq. + by rewrite mulrBl mulVr ?unitfE// mul1r (_ : 1%R = 1%:R)// -natrB. + rewrite funeqE => n /=. + rewrite /series (@big_morph _ _ (@EFin _) 0%E adde) //=. + by apply eq_bigr => i _; rewrite natrX exprVn. +rewrite ereal_limD //. +- by rewrite lee_add2l // (cvg_lim _ cvggeo). +- exact: is_cvg_ereal_nneg_series. +- by apply: is_cvg_ereal_nneg_series => ?; rewrite lee_fin divr_ge0. +- by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_undef. +Grab Existential Variables. all: end_near. Qed. + +Section measurable_cover. +Variable T : ringOfSetsType. +Implicit Types (X : set T) (F : (set T)^nat). + +Definition measurable_cover X := [set F : (set T)^nat | + (forall i, measurable (F i)) /\ X `<=` \bigcup_k (F k)]. + +Lemma cover_measurable X F : measurable_cover X F -> forall k, measurable (F k). +Proof. by move=> + k; rewrite /measurable_cover => -[] /(_ k). Qed. + +Lemma cover_subset X F : measurable_cover X F -> X `<=` \bigcup_k (F k). +Proof. by case. Qed. + +End measurable_cover. + +Section measure_extension. +Variables (R : realType) (T : ringOfSetsType) (mu : {measure set T -> \bar R}). + +Definition mu_ext (X : set T) : \bar R := + ereal_inf [set \sum_(i -> A <= B}. +Proof. +move=> A B AB; apply/le_ereal_inf => x [B' [mB' BB']]. +by move=> <-{x}; exists B' => //; split => //; apply: subset_trans AB BB'. +Qed. + +Lemma mu_ext_ge0 A : 0%:E <= mu_ext A. +Proof. +apply: lb_ereal_inf => x [B [mB AB] <-{x}]; rewrite ereal_lim_ge //=. + by apply: is_cvg_ereal_nneg_series => // n _; exact: measure_ge0. +by near=> n; rewrite sume_ge0 // => i _; apply: measure_ge0. +Grab Existential Variables. all: end_near. Qed. + +Lemma mu_ext0 : mu_ext set0 = 0%:E. +Proof. +apply/eqP; rewrite eq_le; apply/andP; split; last first. + by apply: mu_ext_ge0; exact: measurable0. +rewrite /mu_ext; apply ereal_inf_lb; exists (fun _ => set0). + by split => // _; exact: measurable0. +by apply: (@lim_near_cst _ _ _ _ _ 0%:E) => //; near=> n => /=; rewrite big1. +Grab Existential Variables. all: end_near. Qed. + +Lemma measurable_uncurry (G : ((set T)^nat)^nat) (x : nat * nat) : + measurable (G x.1 x.2) -> measurable (uncurry G x). +Proof. by case: x. Qed. + +Lemma mu_ext_sigma_subadditive : sigma_subadditive mu_ext. +Proof. +move=> A; have [[i ioo]|] := pselect (exists i, mu_ext (A i) = +oo). + rewrite (ereal_nneg_series_pinfty _ _ ioo)// ?lee_pinfty// => n _. + exact: mu_ext_ge0. +rewrite -forallNE => Aoo. +suff add2e : forall e : {posnum R}, + mu_ext (\bigcup_n A n) <= \sum_(i e. + by rewrite -(mul1r e%:num) -(@divff _ 2%:R)// -mulrAC -mulrA add2e. +move=> e; rewrite (le_trans _ (epsilon_trick _ _ _))//; last first. + by move=> n; apply: mu_ext_ge0. +pose P n (B : (set T)^nat) := measurable_cover (A n) B /\ + \sum_(k n; rewrite /P /mu_ext. + set S := (X in ereal_inf X); move infS : (ereal_inf S) => iS. + case: iS infS => [r Sr|Soo|Soo]. + - have en1 : (0 < e%:num / (2 ^ n.+1)%:R)%R. + by rewrite divr_gt0 // ltr0n expn_gt0. + have [x [[B [mB AnB muBx]] xS]] := lb_ereal_inf_adherent (PosNum en1) Sr. + exists B; split => //; rewrite muBx -Sr; apply/ltW. + rewrite (lt_le_trans xS) // lee_add2l //= lee_fin ler_pmul //=. + by rewrite lef_pinv // ?(posrE,ltr0n,expn_gt0) // ler_nat leq_exp2l. + - by have := Aoo n; rewrite /mu_ext Soo. + - suff : lbound S 0%E by move/lb_ereal_inf; rewrite Soo. + move=> /= _ [B [mB AnB] <-]. + by apply: ereal_nneg_series_lim_ge0 => ? _; exact: measure_ge0. +have muG_ge0 : forall x, 0%E <= (mu \o uncurry G) x. + by move=> x; apply/measure_ge0/measurable_uncurry/(PG x.1).1.1. +apply (@le_trans _ _ (\csum_(i in setT) (mu \o uncurry G) i)). + rewrite /mu_ext; apply ereal_inf_lb. + have [f [Tf fi]] : exists e, enumeration (@setT (nat * nat)) e /\ injective e. + have /countable_enumeration [|[f ef]] := countable_prod_nat. + by rewrite predeqE => /(_ (0%N, 0%N)) [] /(_ Logic.I). + by exists (enum_wo_rep infinite_prod_nat ef); split; + [exact: enumeration_enum_wo_rep | exact: injective_enum_wo_rep]. + exists (uncurry G \o f). + split => [i|]; first exact/measurable_uncurry/(PG (f i).1).1.1. + apply: (@subset_trans _ (\bigcup_n \bigcup_k G n k)) => [t [i _]|]. + by move=> /(cover_subset (PG i).1) -[j _ ?]; exists i => //; exists j. + move=> t [i _ [j _ Bijt]]. + have [k fkij] : exists k, f k = (i, j). + by have : setT (i, j) by []; rewrite Tf => -[k _ fkij]; exists k. + by exists k => //=; rewrite fkij. + rewrite -(@csum_image _ _ (mu \o uncurry G) _ xpredT) //; congr csum. + by rewrite Tf predeqE=> -[a b]; split=> -[n _ <-]; exists n. +rewrite (_ : csum _ _ = \sum_(i set (nat * nat) := fun i => [set (i, j) | j in setT]. + rewrite (_ : setT = \bigcup_k J k); last first. + by rewrite predeqE => -[a b]; split => // _; exists a => //; exists b. + rewrite csum_bigcup /=; last 3 first. + - by move=> k; exists (k, O), O. + - apply/trivIsetP => i j _ _ ij. + rewrite predeqE => -[n m] /=; split => //= -[] [_] _ [<-{n} _]. + by move=> [m' _] [] /esym/eqP; rewrite (negbTE ij). + - by move=> /= [n m]; apply/measure_ge0; exact: (cover_measurable (PG n).1). + rewrite (_ : setT = id @` xpredT); last first. + by rewrite image_id funeqE => x; rewrite trueE. + rewrite csum_image //; last by move=> n _; apply: csum_ge0. + apply eq_ereal_pseries => /= j. + pose x_j : nat -> nat * nat := fun y => (j, y). + have [enux injx] : enumeration (J j) x_j /\ injective x_j. + by split => [|x y [] //]; rewrite /enumeration predeqE=> -[? ?]; split. + rewrite -(@csum_image R _ (mu \o uncurry G) x_j predT) //=; last first. + by move=> x _; move: (muG_ge0 (j, x)). + by congr csum; rewrite predeqE => -[a b]; split; move=> [i _ <-]; exists i. +apply lee_lim. +- apply: is_cvg_ereal_nneg_series => n _. + by apply: ereal_nneg_series_lim_ge0 => m _; exact: (muG_ge0 (n, m)). +- by apply: is_cvg_ereal_nneg_series => n _; apply: adde_ge0 => //; + [exact: mu_ext_ge0 | rewrite lee_fin // divr_ge0 // ler0n]. +- by near=> n; apply: lee_sum => i _; exact: (PG i).2. +Grab Existential Variables. all: end_near. Qed. + +End measure_extension. + +Canonical outer_measure_of_measure (R : realType) (T : ringOfSetsType) + (mu : {measure set T -> \bar R}) : {outer_measure set T -> \bar R} := + OuterMeasure (OuterMeasure.Axioms (mu_ext0 mu) (mu_ext_ge0 mu) + (le_mu_ext mu) (mu_ext_sigma_subadditive mu)). diff --git a/theories/sequences.v b/theories/sequences.v index fa8c130ce..011431258 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1259,6 +1259,18 @@ move=> u0; apply: (ereal_lim_ge (is_cvg_ereal_nneg_series _ _ u0)). by near=> k; rewrite sume_ge0 // => i; apply: u0. Grab Existential Variables. all: end_near. Qed. +Lemma adde_undef_nneg_series (R : realType) (f g : (\bar R)^nat) + (P Q : pred nat) : + (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) -> + ~~ adde_undef (\sum_(i f0 g0; rewrite /adde_undef negb_or !negb_and; apply/andP; split. +- apply/orP; right; apply/eqP => Qg. + by have := ereal_nneg_series_lim_ge0 g0; rewrite Qg. +- apply/orP; left; apply/eqP => Pf. + by have := ereal_nneg_series_lim_ge0 f0; rewrite Pf. +Qed. + Lemma ereal_nneg_series_pinfty (R : realType) (u_ : (\bar R)^nat) (P : pred nat) k : (forall n, P n -> 0 <= u_ n) -> P k -> u_ k = +oo -> \sum_(i Date: Fri, 18 Jun 2021 00:03:29 +0900 Subject: [PATCH 2/4] add temporary definition of uncurry - for the CI --- theories/measure.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/theories/measure.v b/theories/measure.v index d97514220..cc0b29685 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -75,6 +75,11 @@ Reserved Notation "mu .-measurable" (at level 2, format "mu .-measurable"). Local Open Scope classical_set_scope. Local Open Scope ring_scope. +(* TODO: remove when available in all the Coq versions supported by the CI + (as of today, only in Coq 8.13) *) +Definition uncurry {A B C : Type} (f : A -> B -> C) + (p : A * B) : C := match p with (x, y) => f x y end. + Definition bigcup2 T (A B : set T) : nat -> set T := fun i => if i == 0%N then A else if i == 1%N then B else set0. From 865ea0af98b747ce069f52d6c25f4a46fe777367 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 18 Jun 2021 01:35:09 +0900 Subject: [PATCH 3/4] nitpicking and rebase --- CHANGELOG_UNRELEASED.md | 1 + theories/measure.v | 22 +++++++++++----------- theories/sequences.v | 6 +++--- 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 3b3d37542..c4704c4c6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -22,6 +22,7 @@ - in `measure.v`: + definition `measurable_fun` + lemma `adde_undef_nneg_series` + + lemma `adde_def_nneg_series` - in `measure.v`: + lemmas `epsilon_trick`, + definition `measurable_cover` diff --git a/theories/measure.v b/theories/measure.v index cc0b29685..aada2b69b 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1104,9 +1104,9 @@ Qed. End caratheodory_measure. Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) (e : {nonneg R}) - (P : pred nat) : (forall n, 0%E <= A n) -> + (P : pred nat) : (forall n, 0 <= A n) -> \sum_(i A0; rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) + \sum_(0 <= i < n) (e%:nngnum / (2 ^ i)%:R)%:E))) //. @@ -1118,7 +1118,7 @@ move=> A0; rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) + + by near=> n; apply: lee_sum_nneg_subset => // i _; apply divr_ge0. - exact: is_cvg_ereal_nneg_series. - by apply: is_cvg_ereal_nneg_series => n _; apply: divr_ge0. - - by apply: adde_undef_nneg_series => // n _; apply: divr_ge0. + - by apply: adde_def_nneg_series => // n _; apply: divr_ge0. have cvggeo : (fun n => \sum_(0 <= i < n) (e%:nngnum / (2 ^ i)%:R)%:E) --> (2 * e%:nngnum)%:E. rewrite (_ : (fun n => _) = @EFin _ \o series (geometric e%:nngnum 2^-1)). @@ -1129,13 +1129,13 @@ have cvggeo : (fun n => \sum_(0 <= i < n) (e%:nngnum / (2 ^ i)%:R)%:E) --> congr (_ * _)%R; apply mulr1_eq. by rewrite mulrBl mulVr ?unitfE// mul1r (_ : 1%R = 1%:R)// -natrB. rewrite funeqE => n /=. - rewrite /series (@big_morph _ _ (@EFin _) 0%E adde) //=. + rewrite /series (@big_morph _ _ (@EFin _) 0 adde) //=. by apply eq_bigr => i _; rewrite natrX exprVn. rewrite ereal_limD //. - by rewrite lee_add2l // (cvg_lim _ cvggeo). - exact: is_cvg_ereal_nneg_series. - by apply: is_cvg_ereal_nneg_series => ?; rewrite lee_fin divr_ge0. -- by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_undef. +- by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_def. Grab Existential Variables. all: end_near. Qed. Section measurable_cover. @@ -1165,20 +1165,20 @@ move=> A B AB; apply/le_ereal_inf => x [B' [mB' BB']]. by move=> <-{x}; exists B' => //; split => //; apply: subset_trans AB BB'. Qed. -Lemma mu_ext_ge0 A : 0%:E <= mu_ext A. +Lemma mu_ext_ge0 A : 0 <= mu_ext A. Proof. apply: lb_ereal_inf => x [B [mB AB] <-{x}]; rewrite ereal_lim_ge //=. by apply: is_cvg_ereal_nneg_series => // n _; exact: measure_ge0. by near=> n; rewrite sume_ge0 // => i _; apply: measure_ge0. Grab Existential Variables. all: end_near. Qed. -Lemma mu_ext0 : mu_ext set0 = 0%:E. +Lemma mu_ext0 : mu_ext set0 = 0. Proof. apply/eqP; rewrite eq_le; apply/andP; split; last first. by apply: mu_ext_ge0; exact: measurable0. rewrite /mu_ext; apply ereal_inf_lb; exists (fun _ => set0). by split => // _; exact: measurable0. -by apply: (@lim_near_cst _ _ _ _ _ 0%:E) => //; near=> n => /=; rewrite big1. +by apply: (@lim_near_cst _ _ _ _ _ 0) => //; near=> n => /=; rewrite big1. Grab Existential Variables. all: end_near. Qed. Lemma measurable_uncurry (G : ((set T)^nat)^nat) (x : nat * nat) : @@ -1210,10 +1210,10 @@ have [G PG] : {G : ((set T)^nat)^nat & forall n, P n (G n)}. rewrite (lt_le_trans xS) // lee_add2l //= lee_fin ler_pmul //=. by rewrite lef_pinv // ?(posrE,ltr0n,expn_gt0) // ler_nat leq_exp2l. - by have := Aoo n; rewrite /mu_ext Soo. - - suff : lbound S 0%E by move/lb_ereal_inf; rewrite Soo. + - suff : lbound S 0 by move/lb_ereal_inf; rewrite Soo. move=> /= _ [B [mB AnB] <-]. by apply: ereal_nneg_series_lim_ge0 => ? _; exact: measure_ge0. -have muG_ge0 : forall x, 0%E <= (mu \o uncurry G) x. +have muG_ge0 : forall x, 0 <= (mu \o uncurry G) x. by move=> x; apply/measure_ge0/measurable_uncurry/(PG x.1).1.1. apply (@le_trans _ _ (\csum_(i in setT) (mu \o uncurry G) i)). rewrite /mu_ext; apply ereal_inf_lb. @@ -1256,7 +1256,7 @@ apply lee_lim. - apply: is_cvg_ereal_nneg_series => n _. by apply: ereal_nneg_series_lim_ge0 => m _; exact: (muG_ge0 (n, m)). - by apply: is_cvg_ereal_nneg_series => n _; apply: adde_ge0 => //; - [exact: mu_ext_ge0 | rewrite lee_fin // divr_ge0 // ler0n]. + [exact: mu_ext_ge0 | rewrite lee_fin // divr_ge0]. - by near=> n; apply: lee_sum => i _; exact: (PG i).2. Grab Existential Variables. all: end_near. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 011431258..bdfddc56a 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -1259,12 +1259,12 @@ move=> u0; apply: (ereal_lim_ge (is_cvg_ereal_nneg_series _ _ u0)). by near=> k; rewrite sume_ge0 // => i; apply: u0. Grab Existential Variables. all: end_near. Qed. -Lemma adde_undef_nneg_series (R : realType) (f g : (\bar R)^nat) +Lemma adde_def_nneg_series (R : realType) (f g : (\bar R)^nat) (P Q : pred nat) : (forall n, P n -> 0 <= f n) -> (forall n, Q n -> 0 <= g n) -> - ~~ adde_undef (\sum_(i f0 g0; rewrite /adde_undef negb_or !negb_and; apply/andP; split. +move=> f0 g0; rewrite /adde_def !negb_and; apply/andP; split. - apply/orP; right; apply/eqP => Qg. by have := ereal_nneg_series_lim_ge0 g0; rewrite Qg. - apply/orP; left; apply/eqP => Pf. From 57425d5a056eb22f4af970d94603650a6de4dd1b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 19 Jul 2021 13:21:46 +0900 Subject: [PATCH 4/4] simpler `epsilon_trick` statement --- CHANGELOG_UNRELEASED.md | 2 +- theories/measure.v | 61 ++++++++++++++++++++++++----------------- 2 files changed, 37 insertions(+), 26 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index c4704c4c6..4b5460602 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -24,7 +24,7 @@ + lemma `adde_undef_nneg_series` + lemma `adde_def_nneg_series` - in `measure.v`: - + lemmas `epsilon_trick`, + + lemmas `cvg_geometric_series_half`, `epsilon_trick` + definition `measurable_cover` + lemmas `cover_measurable`, `cover_subset` + definition `mu_ext` diff --git a/theories/measure.v b/theories/measure.v index aada2b69b..86027fc38 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1103,13 +1103,28 @@ Qed. End caratheodory_measure. +(* TODO: move? *) +Lemma cvg_geometric_series_half (R : archiFieldType) (r : R) n : + series (fun k => r / (2 ^ (k + n.+1))%:R : R^o) --> (r / 2 ^+ n : R^o). +Proof. +rewrite (_ : series _ = series (geometric (r / (2 ^ n.+1)%:R) 2^-1%R)); last first. + rewrite funeqE => m; rewrite /series /=; apply eq_bigr => k _. + by rewrite expnD natrM (mulrC (2 ^ k)%:R) invfM exprVn (natrX _ 2 k) mulrA. +apply: cvg_trans. + apply: cvg_geometric_series. + by rewrite ger0_norm // invr_lt1 // ?ltr1n // unitfE. +rewrite [X in (X - _)%R](splitr 1) div1r addrK. +by rewrite -mulrA -invfM expnSr natrM -mulrA divff// mulr1 natrX. +Qed. +Arguments cvg_geometric_series_half {R} _ _. + Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) (e : {nonneg R}) - (P : pred nat) : (forall n, 0 <= A n) -> - \sum_(i + \sum_(i A0; rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) + - \sum_(0 <= i < n) (e%:nngnum / (2 ^ i)%:R)%:E))) //. + \sum_(0 <= i < n) (e%:nngnum / (2 ^ i.+1)%:R)%:E))) //. rewrite ereal_pseriesD //; last by move=> n _; apply: divr_ge0. rewrite ereal_limD //. - rewrite lee_add2l //; apply: lee_lim => //. @@ -1119,23 +1134,20 @@ move=> A0; rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) + - exact: is_cvg_ereal_nneg_series. - by apply: is_cvg_ereal_nneg_series => n _; apply: divr_ge0. - by apply: adde_def_nneg_series => // n _; apply: divr_ge0. -have cvggeo : (fun n => \sum_(0 <= i < n) (e%:nngnum / (2 ^ i)%:R)%:E) --> - (2 * e%:nngnum)%:E. - rewrite (_ : (fun n => _) = @EFin _ \o series (geometric e%:nngnum 2^-1)). - apply: cvg_comp. - - by apply: cvg_geometric_series; rewrite ger0_norm // invf_lt1 // ltr1n. - - rewrite (_ : [filter of _] = [filter of (2 * e%:nngnum)%R : R^o]) //. - rewrite filter_of_filterE; congr ([filter of _]); rewrite mulrC. - congr (_ * _)%R; apply mulr1_eq. - by rewrite mulrBl mulVr ?unitfE// mul1r (_ : 1%R = 1%:R)// -natrB. - rewrite funeqE => n /=. - rewrite /series (@big_morph _ _ (@EFin _) 0 adde) //=. - by apply eq_bigr => i _; rewrite natrX exprVn. -rewrite ereal_limD //. -- by rewrite lee_add2l // (cvg_lim _ cvggeo). -- exact: is_cvg_ereal_nneg_series. -- by apply: is_cvg_ereal_nneg_series => ?; rewrite lee_fin divr_ge0. -- by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_def. +suff cvggeo : (fun n => \sum_(0 <= i < n) (e%:nngnum / (2 ^ i.+1)%:R)%:E) --> + e%:nngnum%:E. + rewrite ereal_limD //. + - by rewrite lee_add2l // (cvg_lim _ cvggeo). + - exact: is_cvg_ereal_nneg_series. + - by apply: is_cvg_ereal_nneg_series => ?; rewrite lee_fin divr_ge0. + - by rewrite (cvg_lim _ cvggeo) //= fin_num_adde_def. +rewrite (_ : (fun n => _) = @EFin _ \o + (fun n => \sum_(0 <= i < n) (e%:nngnum / (2 ^ (i + 1))%:R))%R); last first. + rewrite funeqE => n /=; rewrite (@big_morph _ _ (@EFin _) 0 adde)//. + by under [in RHS]eq_bigr do rewrite addn1. +apply: cvg_comp; last apply cvg_refl. +have := cvg_geometric_series_half e%:nngnum O. +by rewrite expr0 divr1; apply: cvg_trans. Grab Existential Variables. all: end_near. Qed. Section measurable_cover. @@ -1192,13 +1204,13 @@ move=> A; have [[i ioo]|] := pselect (exists i, mu_ext (A i) = +oo). exact: mu_ext_ge0. rewrite -forallNE => Aoo. suff add2e : forall e : {posnum R}, - mu_ext (\bigcup_n A n) <= \sum_(i e. by rewrite -(mul1r e%:num) -(@divff _ 2%:R)// -mulrAC -mulrA add2e. move=> e; rewrite (le_trans _ (epsilon_trick _ _ _))//; last first. by move=> n; apply: mu_ext_ge0. pose P n (B : (set T)^nat) := measurable_cover (A n) B /\ - \sum_(k n; rewrite /P /mu_ext. set S := (X in ereal_inf X); move infS : (ereal_inf S) => iS. @@ -1207,8 +1219,7 @@ have [G PG] : {G : ((set T)^nat)^nat & forall n, P n (G n)}. by rewrite divr_gt0 // ltr0n expn_gt0. have [x [[B [mB AnB muBx]] xS]] := lb_ereal_inf_adherent (PosNum en1) Sr. exists B; split => //; rewrite muBx -Sr; apply/ltW. - rewrite (lt_le_trans xS) // lee_add2l //= lee_fin ler_pmul //=. - by rewrite lef_pinv // ?(posrE,ltr0n,expn_gt0) // ler_nat leq_exp2l. + by rewrite (lt_le_trans xS) // lee_add2l //= lee_fin ler_pmul. - by have := Aoo n; rewrite /mu_ext Soo. - suff : lbound S 0 by move/lb_ereal_inf; rewrite Soo. move=> /= _ [B [mB AnB] <-].