From 9a516236dce472264d098b6b81cb34a272373bcb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 4 Jul 2021 13:07:44 +0900 Subject: [PATCH] using a modified version of epsilon_trick - from PR #395 (in progress) --- theories/measure_wip.v | 165 +++++++++++++++++++++-------------------- 1 file changed, 85 insertions(+), 80 deletions(-) diff --git a/theories/measure_wip.v b/theories/measure_wip.v index 6af9d73055..e517396d5c 100644 --- a/theories/measure_wip.v +++ b/theories/measure_wip.v @@ -94,13 +94,28 @@ move=> f0 g0; rewrite /adde_def !negb_and; apply/andP; split. by have := ereal_nneg_series_lim_ge0 f0; rewrite Pf. Qed. +(* PR 395 in progress *) +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%E <= 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 => //. @@ -110,24 +125,22 @@ 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%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_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. +(* /PR 395 in progress *) Section measurable_cover. Variable T : ringOfSetsType. @@ -183,13 +196,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. @@ -198,8 +211,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%E by move/lb_ereal_inf; rewrite Soo. move=> /= _ [B [mB AnB] <-]. @@ -3941,8 +3953,8 @@ have a'b'i : {subset `[a', b'] <= i}. by rewrite (le_lt_trans rb') // /b' ltr_subl_addl ltr_addr. set a_ := fun k => real_of_extended (j k).1. set b_ := fun k => real_of_extended (j k).2. -set a'_ := fun k => ((a_ k) - e%:num / (2 ^ k.+3)%:R)%R. -set b'_ := fun k => ((b_ k) + e%:num / (2 ^ k.+3)%:R)%R. +set a'_ := (fun k => a_ k - e%:num / (2 ^ k.+3)%:R)%R. +set b'_ := (fun k => b_ k + e%:num / (2 ^ k.+3)%:R)%R. have ia_b_ : set_of_itv i `<=` \bigcup_(k in P) set_of_itv `] (a'_ k) , (b'_ k) [. move/subset_trans : ij; apply => r [k Pk]. have [/eqP ->//|jk0 /set_of_itv_mem] := boolP (set_of_itv (j k) == set0). @@ -3959,16 +3971,16 @@ have ia_b_ : set_of_itv i `<=` \bigcup_(k in P) set_of_itv `] (a'_ k) , (b'_ k) have a'b'a'_b'_ : [set x | x \in `[a', b']] `<=` \bigcup_(k in P) (set_of_itv `](a'_ k), (b'_ k)[). by move/subset_of_itvP : a'b'i => /subset_trans; apply. have [F [HF HF_]] : exists F : {fset nat}, - (set_of_itv `[a', b'] `<=` \bigcup_(k in [set x | (x \in F) && (P x)]) set_of_itv `] (a'_ k), (b'_ k) [) /\ [set x | x \in F] `<=` P. + (set_of_itv `[a', b'] `<=` \bigcup_(k in [set x | (x \in F) && (P x)]) set_of_itv `] (a'_ k), (b'_ k) [) /\ + [set x | x \in F] `<=` P. have h : forall j, P j -> @open [topologicalType of R^o] (set_of_itv `](a'_ j), (b'_ j)[). by move=> k _; exact: interval_open. have := @segment_compact _ a' b'. (* NB: Borel-Lebesgue theorem *) - rewrite compact_cover => /(_ _ _ _ h a'b'a'_b'_) => -[F H1 H2]; exists F. - split; last first. - by move=> x /H1; rewrite inE. - move=> r /H2[k Fk kr]; exists k => //=. - by rewrite Fk /=; move/H1 : Fk; rewrite inE. + rewrite compact_cover => /(_ _ _ _ h a'b'a'_b'_) => -[F FP a'b'F]; exists F. + split; last by move=> x /FP; rewrite inE. + move=> r /a'b'F[k Fk kr]; exists k => //=. + by rewrite Fk /=; move/FP : Fk; rewrite inE. set F' := [fset k in F | neitv `](a'_ k), (b'_ k)[]%fset. have HF' : set_of_itv `[a', b'] `<=` \bigcup_(k in [set x | x \in F']) set_of_itv `](a'_ k), (b'_ k)[. move/subset_trans : HF; apply. @@ -3996,9 +4008,7 @@ have : (b'%:E - a'%:E <= \sum_(k k. rewrite /neitv /= lte_bnd => a'b'k0. by rewrite slength_itv hlength_itv /= lte_fin a'b'k0. - rewrite (_ : e%:num / 2 = 2 * (e%:num / 4%:R)); last first. - by rewrite (@natrM _ 2 2) mulrA -mulf_div divff // mul1r. - apply: (le_trans _ (@epsilon_trick _ (slength \o set_of_itv \o j) (Nonneg.NngNum (e%:num / 4%:R) _) P _)) => //; last first. + apply: (le_trans _ (@epsilon_trick _ (slength \o set_of_itv \o j) _ P _)) => //; last first. by move=> n; apply/slength_ge0. rewrite [X in (X <= _)%E](_ : _ = (\sum_(k <- F') ((b_ k - a_ k) + (e%:num / (2 ^ k.+2)%:R))%:E)%E); last first. apply eq_bigr => /= k ?. @@ -4007,83 +4017,78 @@ have : (b'%:E - a'%:E <= \sum_(k (\sum_(i < n) (e%:num / 4%:R / (2 ^ i)%:R)%:E)%E) --> (e%:num / 2)%:E. - rewrite (_ : (fun n => _) = (@EFin _) \o series (geometric (e%:num / 4%:R) (2^-1)%R)); last first. + (* TODO: lemma *) + have cvggeo : (fun n => \sum_(i < n) (e%:num / (2 ^ i.+2)%:R)%:E)%E --> (e%:num / 2)%:E. + rewrite (_ : (fun n => _) = (@EFin _) \o series (fun k => e%:num / (2 ^ (k + 2))%:R)); last first. + rewrite funeqE => n; rewrite /series /=. + rewrite (@big_morph _ _ (@EFin _) 0%:E adde) // big_mkord. + by under eq_bigr do rewrite -[in X in (_ ^X)%:R]addn2. + apply: cvg_comp; last apply cvg_refl. + have := @cvg_geometric_series_half _ e%:num 1. + by rewrite expr1. +(* have cvggeo : (fun n => \sum_(i < n) (e%:num / (2 ^ i.+2)%:R)%:E)%E --> (e%:num / 2)%:E. + rewrite (_ : (fun n => _) = (@EFin _) \o series (geometric (e%:num / 4%:R) 2^-1%R)); last first. rewrite funeqE => n; rewrite /series /=. rewrite (@big_morph _ _ (@EFin _) 0%:E adde) // big_mkord. - by apply eq_bigr => k _; rewrite natrX exprVn. + by apply eq_bigr => ? _; rewrite 2!expnS mulnA natrM invfM mulrA exprVn natrX. apply: cvg_comp. apply: cvg_geometric_series. by rewrite ger0_norm // invr_lt1 // ?ltr1n // unitfE. rewrite (_ : [filter of _] = [filter of e%:num / 2 : R^o]) // !filter_of_filterE. congr ([filter of _]); rewrite -mulrA; congr (_ * _)%R. - rewrite (_ : 1 - _ = 2^-1); last first. - by apply/eqP; rewrite subr_eq [in X in X == _](splitr 1) div1r. - by rewrite (natrM _ 2 2) invfM // mulrAC divff // div1r. - have ? : cvg (fun n : nat => (\sum_(k < n | P k) (e%:num / 4%:R / (2 ^ k)%:R)%:E)%E). - under eq_fun do rewrite -(big_mkord P (fun k => (e%:num / 4%:R / (2 ^ k)%:R)%:E)). - by apply: is_cvg_ereal_nneg_series => n _; rewrite lee_fin divr_ge0 // ler0n. + rewrite [X in X - _](splitr 1) div1r addrK. + by rewrite (natrM _ 2 2) invfM // mulrAC divff // div1r.*) + have ? : cvg (fun n => \sum_(k < n | P k) (e%:num / (2 ^ k.+2)%:R)%:E)%E. + under eq_fun do rewrite -(big_mkord P (fun k => (e%:num / (2 ^ k.+2)%:R)%:E)). + by apply: is_cvg_ereal_nneg_series => n _; rewrite lee_fin divr_ge0// ler0n. apply (@le_trans _ _ (\sum_(k k Pk; exact/Sset.is_sset_itv. + by apply: is_cvg_sum_slength => k Pk; exact/measurable_itv. by under eq_fun do rewrite big_mkord. - have /andP[l0 le2] : (0%:E <= \sum_(k (e%:num / 4%:R / (2 ^ k)%:R)%:E)) // => n _. + rewrite (@ereal_nneg_series_lim_ge0 _ (fun k => (e%:num / (2 ^ k.+2)%:R)%:E)) // => n _. by apply divr_ge0 => //; rewrite ler0n. move/cvg_lim : (cvggeo) => <- //=. apply lee_lim => //. by under eq_fun do rewrite big_mkord. - under eq_fun do rewrite -(big_mkord xpredT (fun k => ((e)%:num / 4%:R / (2 ^ k)%:R)%:E)). + under eq_fun do rewrite -(big_mkord xpredT (fun k => (e%:num / (2 ^ k.+2)%:R)%:E)). by apply: is_cvg_ereal_nneg_series => n _; rewrite lee_fin divr_ge0 // ler0n. near=> n. - rewrite (big_mkord P (fun k => ((e)%:num / 4%:R / (2 ^ k)%:R)%:E)). - move: (@lee_sum_nneg R _ (enum 'I_n) xpredT P (fun k => (e%:num / 4%:R / (2 ^ k)%:R)%:E)). + rewrite (big_mkord P (fun k => (e%:num / (2 ^ k.+2)%:R)%:E)). + move: (@lee_sum_nneg R _ (enum 'I_n) xpredT P (fun k => (e%:num / (2 ^ k.+2)%:R)%:E)). rewrite big_enum big_enum_cond; apply => k _ _. by apply divr_ge0 => //; rewrite ler0n. apply: fin_num_adde_def => //. rewrite fin_numE gt_eqF /=; last by rewrite (lt_le_trans _ l0) // lte_ninfty. by rewrite lt_eqF // (le_lt_trans le2) // lte_pinfty. - rewrite (_ : (fun x : nat => _) = (fun x => \sum_(0 <= k < x | P k) (slength (set_of_itv (j k)) + (e%:num / 4%:R / (2 ^ k)%:R)%:E))%E) //. - by rewrite funeqE => n; rewrite big_split. - have sum_F'_P : forall f : nat -> \bar R, (\sum_(i1 <- F') (f i1) = \sum_(i1 <- F' | P i1) (f i1))%E. - move=> f; apply eq_fbigl_cond => //. - move=> k; apply/idP/idP => /=. + rewrite (_ : (fun x => _) = (fun x => \sum_(0 <= k < x | P k) (slength (set_of_itv (j k)) + (e%:num / 2 / (2 ^ k.+1)%:R)%:E)))%E //. + rewrite funeqE => n; rewrite big_split => /=; congr (_ + _)%E. + by apply eq_bigr => m Pm; rewrite expnS natrM invfM -mulrA. + have sum_F'_P : forall f : nat -> \bar R, (\sum_(k <- F') f k = \sum_(k <- F' | P k) f k)%E. + move=> f; apply eq_fbigl_cond => // k; apply/idP/idP => /=. rewrite !inE andbT => /andP[/= kF -> /=]. - rewrite andbT; apply/andP; split => //. - by apply/HF_. - by rewrite !inE andbT => /andP[/=]. + by rewrite andbT kF /=; apply/HF_. + by rewrite !inE andbT => /andP[]. apply: lee_add; last first. - set f := (fun i : nat => \sum_(k < i | P k) (e%:num / 4%:R / (2 ^ i)%:R)%:E)%E. + set f := (fun i : nat => \sum_(k < i | P k) (e%:num / (2 ^ i.+2)%:R)%:E)%E. rewrite (@le_trans _ _ (\sum_(k n _; apply divr_ge0 => //; rewrite ler0n. - apply lee_lim => //. - by apply: is_cvg_ereal_nneg_series => n _; rewrite lee_fin divr_ge0 // ler0n. - by under eq_fun do rewrite big_mkord. - near=> n. - apply: lee_sum. - move=> /= k _. - rewrite le_eqVlt; apply/orP; left; apply/eqP; congr (_%:E). - by rewrite -mulrA; congr (_ * _); rewrite 2!expnS mulnA natrM invfM. + rewrite sum_F'_P. + by apply: lee_sum_lim => n _; apply divr_ge0 => //; rewrite ler0n. rewrite [X in (X <= _)%E](_ : _ = (\sum_(k <- F') slength (set_of_itv (j k)))%E); last first. apply eq_fbigr => k /imfsetP[/= p]; rewrite !inE => /andP[pF a'b'p0 ->{k} ?]. - rewrite /b_ /a_. - rewrite slength_itv hlength_itv. + rewrite /b_ /a_ slength_itv hlength_itv. have [? ?] : (((j p).1 : \bar R) \is a fin_num) /\ (((j p).2 : \bar R) \is a fin_num). apply hlength_finite_fin_num. - apply: jne => //. - by move/HF_ : pF. - apply j_finite => //. - by move/HF_ : pF. + by apply: jne => //; exact: (HF_ _ pF). + by apply j_finite => //; exact: (HF_ _ pF). rewrite subEFin -EFin_real_of_extended // -EFin_real_of_extended //. - have /jne : P p by move/HF_ : pF. + have /jne : P p := HF_ _ pF. rewrite /neitv => /ltW/le_bnd_er. rewrite le_eqVlt => /orP[/eqP ->|->//]. by rewrite ltxx subee. - rewrite sum_F'_P. - by apply: lee_sum_lim => k _; exact/slength_ge0. + by rewrite sum_F'_P; apply: lee_sum_lim => k _; exact/slength_ge0. have -> : (b'%:E - a'%:E = (b%:E - a%:E) - (e%:num / 2)%:E)%E. rewrite /a' /b' (addEFin a) oppeD (subEFin b) -addeA. rewrite (addeCA (- (e%:num / 4%:R)%:E)%E) addeA; congr (_ + _)%E.