From 3587d5d9d9a5666c335b8e5cad8418d160536662 Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Fri, 24 Feb 2023 16:14:49 +0900 Subject: [PATCH] fixes (#843) * fixes - fixes #828 - fixes #835 - fixes #838 --- CHANGELOG_UNRELEASED.md | 5 +++++ classical/functions.v | 2 +- theories/esum.v | 24 ++++++++++-------------- theories/lebesgue_integral.v | 12 ++++++------ theories/topology.v | 2 ++ 5 files changed, 24 insertions(+), 21 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index daa31011a..d10e505a8 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -118,6 +118,8 @@ - in file `topology.v`, + lemma `compact_near_coveringP` +- in `functions.v`: + + notation `mem_fun_` ### Renamed - in `measurable.v`: @@ -146,6 +148,9 @@ + `finSubCover` -> `finite_subset_cover` - in `sequences.v`: + `eq_eseries` -> `eq_eseriesr` +- in `esum.v`: + + `summable_nneseries_esum` -> `summable_eseries_esum` + + `summable_nneseries` -> `summable_eseries` ### Generalized diff --git a/classical/functions.v b/classical/functions.v index e8a79c8d1..2931ea4c1 100644 --- a/classical/functions.v +++ b/classical/functions.v @@ -389,7 +389,7 @@ Definition mem_fun aT rT (A : set aT) (B : set rT) (f : {fun A >-> B}) := Definition phant_mem_fun aT rT (A : set aT) (B : set rT) (f : {fun A >-> B}) of phantom (_ -> _) f := homo_setP.2 (@funS _ _ _ _ f). -Notation "'mem_fun_ f" := (phant_funS (Phantom (_ -> _) f)) +Notation "'mem_fun_ f" := (phant_mem_fun (Phantom (_ -> _) f)) (at level 8, f at level 2) : form_scope. Lemma some_inv {aT rT} (f : {inv aT >-> rT}) x : Some (f^-1 x) = 'oinv_f x. diff --git a/theories/esum.v b/theories/esum.v index 17eaa80db..608ae4d23 100644 --- a/theories/esum.v +++ b/theories/esum.v @@ -545,7 +545,7 @@ transitivity (lim (EFin \o A_)). by rewrite EFin_lim//; apply: summable_cvg. Qed. -Lemma summable_nneseries (f : nat -> \bar R) (P : pred nat) : summable P f -> +Lemma summable_eseries (f : nat -> \bar R) (P : pred nat) : summable P f -> \sum_(i C_ n - (A - B)) --> (0 : R^o))%R. move=> CAB. rewrite [X in X - _]summable_nneseries_lim//; last exact/summable_funepos. rewrite [X in _ - X]summable_nneseries_lim//; last exact/summable_funeneg. - rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split. - apply: nearW => n. - rewrite fin_num_abs; apply: le_lt_trans Pf => /=. - by rewrite -nneseries_esum// (le_trans (lee_abs_sum _ _ _))// nneseries_lim_ge. - by apply: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB) => //; exact: cvg_cst. + rewrite -EFinB; apply/cvg_lim => //; apply/fine_cvgP; split; last first. + apply: (@cvg_sub0 _ _ _ _ _ _ (cst (A - B)%R) _ CAB); exact: cvg_cst. + apply: nearW => n; rewrite fin_num_abs; apply: le_lt_trans Pf => /=. + by rewrite -nneseries_esum ?(le_trans (lee_abs_sum _ _ _)) ?nneseries_lim_ge. have : ((fun x => A_ x - B_ x) --> A - B)%R. apply: cvgD. - by apply: summable_cvg => //; exact/summable_funepos. @@ -575,23 +574,20 @@ rewrite distrC subr0. have -> : (C_ = A_ \- B_)%R. apply/funext => k. rewrite /= /A_ /C_ /B_ -sumrN -big_split/= -summable_fine_sum//. - apply eq_bigr => i Pi. - rewrite -fineB//. + apply eq_bigr => i Pi; rewrite -fineB//. - by rewrite [in LHS](funeposneg f). - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funepos. - by rewrite fin_num_abs (@summable_pinfty _ _ P) //; exact/summable_funeneg. by rewrite distrC; apply: hN; near: n; exists N. Unshelve. all: by end_near. Qed. -Lemma summable_nneseries_esum (f : nat -> \bar R) (P : pred nat) : +Lemma summable_eseries_esum (f : nat -> \bar R) (P : pred nat) : summable P f -> \sum_(i Pfoo. -rewrite -nneseries_esum; last first. +move=> Pfoo; rewrite -nneseries_esum; last first. by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite -leNgt. -rewrite -nneseries_esum; last first. - by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt. -by rewrite [LHS]summable_nneseries. +rewrite -nneseries_esum ?[LHS]summable_eseries//. +by move=> n Pn; rewrite /maxe; case: ifPn => //; rewrite leNgt. Qed. End summable_nat. diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v index 877c2379b..7fe90dcf8 100644 --- a/theories/lebesgue_integral.v +++ b/theories/lebesgue_integral.v @@ -2864,15 +2864,15 @@ rewrite -esumB//; last 4 first. - by rewrite /summable /= -nneseries_esum// -fineKn; exact: fmoo. - by move=> n _; exact/fine_ge0/integral_ge0. - by move=> n _; exact/fine_ge0/integral_ge0. -rewrite -summable_nneseries_esum; last first. - rewrite /summable. +rewrite -summable_eseries_esum; last first. apply: (@le_lt_trans _ _ (\esum_(i in (fun=> true)) `|(fine (\int[m_ i]_(x in D) f x))%:E|)). - apply: le_esum => k _; rewrite -EFinB -fineB// -?integralE//; + by apply: le_esum => k _; rewrite -EFinB -fineB// -?integralE//; [exact: integrable_pos_fin_num|exact: integrable_neg_fin_num]. rewrite -nneseries_esum; last by []. - apply: (@le_lt_trans _ _ (\sum_(n // n _. rewrite integralE fineB// ?EFinB. - exact: (le_trans (lee_abs_sub _ _)). @@ -3841,7 +3841,7 @@ rewrite set_true -esumB//=; last 4 first. - exact: integrableN. - by move=> n _; exact: integral_ge0. - by move=> n _; exact: integral_ge0. -rewrite summable_nneseries; last first. +rewrite summable_eseries; last first. under [X in summable _ X]eq_fun do rewrite -integralE. by rewrite fun_true; exact: integrable_summable. by congr (_ - _)%E; rewrite nneseries_esum// set_true. diff --git a/theories/topology.v b/theories/topology.v index 887e92ed3..7be480d51 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -188,6 +188,8 @@ Require Import reals signed. (* a pointedType, as well as the carrier. *) (* nbhs_of_open \o open_from must be *) (* used to declare a filterType *) +(* finI_from D f == set of \bigcap_(i in E) f i where E is *) +(* a finite subset of D *) (* topologyOfSubbaseMixin D b == builds the mixin for a topological *) (* space from a subbase of open sets b *) (* indexed on domain D; the type of *)