From ed7d91c286e253edd328c3c69ad3b87bd309ee3a Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 29 Jul 2020 17:50:37 +0900 Subject: [PATCH 1/2] minor fix, generalizations, cleaning --- theories/measure.v | 30 ++++++------------------------ theories/sequences.v | 23 +++++++++++++++++++++-- 2 files changed, 27 insertions(+), 26 deletions(-) diff --git a/theories/measure.v b/theories/measure.v index cc9125460f..066274b210 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -6,12 +6,13 @@ Require Import boolp reals ereal. Require Import classical_sets posnum topology normedtype sequences. (******************************************************************************) -(* This file provides basic elements of a theory of measure illustrated *) -(* by a formalization of Boole's inequality. *) +(* This file provides basic elements of a theory of measure. *) (* *) (* {measure set T -> {ereal R}} == type of a measure over sets of elements of *) (* type T where R is expected to be a *) (* a realFieldType or a realType *) +(* *) +(* Theorems: Boole_inequality, generalized_Boole_inequality *) (******************************************************************************) Set Implicit Arguments. @@ -24,7 +25,7 @@ Local Open Scope ring_scope. (* TODO: move to classical_sets *) Definition triviset T (U : nat -> set T) := - forall j i, (i != j)%nat -> U i `&` U j = set0. + forall i j, (i != j)%nat -> U i `&` U j = set0. Module Measurable. @@ -256,7 +257,7 @@ Definition B_of (A : (set T) ^nat) := Lemma triviset_B_of (A : (set T) ^nat) : {homo A : n m / (n <= m)%nat >-> n `<=` m} -> triviset (B_of A). Proof. -move=> ndA j i; wlog : j i / (i < j)%N. +move=> ndA i j; wlog : i j / (i < j)%N. move=> h; rewrite neq_ltn => /orP[|] ?; by [rewrite h // ltn_eqF|rewrite setIC h // ltn_eqF]. move=> ij _; move: j i ij; case => // j [_ /=|n]. @@ -362,25 +363,6 @@ Qed. End boole_inequality. Notation le_mu_bigsetU := Boole_inequality. -(* NB: see also nondecreasing_series *) -Lemma ereal_nondecreasing_series (R : realFieldType) (u_ : {ereal R} ^nat) : - (forall n, 0%:E <= u_ n)%E -> - nondecreasing_seq (fun n => \sum_(i < n) u_ i)%E. -Proof. -move=> u_ge0 n m nm; rewrite -(subnKC nm). -rewrite -[X in (_ <= X)%E](big_mkord xpredT) /index_iota subn0 iota_add. -rewrite big_cat -[in X in (_ <= X + _)%E](subn0 n) big_mkord lee_addl //=. -by rewrite sume_ge0. -Qed. - -Lemma series_nneg (R : realType) (u_ : {ereal R} ^nat) k : - (forall n, (0%:E <= u_ n)%E) -> - (\sum_(i < k.+1) u_ i <= lim (fun n : nat => \sum_(i < n) u_ i))%E. -Proof. -move/ereal_nondecreasing_series/nondecreasing_seq_ereal_cvg/cvg_lim => -> //. -by apply ereal_sup_ub; exists k.+1. -Qed. - Section generalized_boole_inequality. Variables (R : realType) (T : measurableType). Variable (mu : {measure set T -> {ereal R}}). @@ -409,7 +391,7 @@ have -> : lim (mu \o B) = ereal_sup ((mu \o B) @` setT). exact: subset_bigsetU. have BA : forall m, (mu (B m) <= lim (fun n : nat => \sum_(i < n) mu (A i)))%E. move=> m; rewrite (le_trans (le_mu_bigsetU mu mA m.+1)) // -/(B m). - by apply: (@series_nneg _ (mu \o A)) => n; exact: measure_ge0. + by apply: (@ereal_nneg_series_lim_ge _ (mu \o A)) => n; exact: measure_ge0. by apply ub_ereal_sup => /= x [n _ <-{x}]; apply BA. Qed. diff --git a/theories/sequences.v b/theories/sequences.v index 988e729a8d..35bd52b026 100644 --- a/theories/sequences.v +++ b/theories/sequences.v @@ -775,7 +775,7 @@ Qed. Section sequences_of_extended_real_numbers. -(* TODO: worth keeping in addition to cvgPpinfty? *) +(* NB: worth keeping in addition to cvgPpinfty? *) Lemma cvgPpinfty_lt (R : realFieldType) (u_ : R^o ^nat) : u_ --> +oo <-> forall A, A > 0 -> \forall n \near \oo, A < u_ n. Proof. @@ -786,7 +786,7 @@ exists n => // m nm; rewrite (@lt_le_trans _ _ (A *+ 2)) // ?mulr2n ?ltr_addr // exact: uoo. Qed. -Lemma dvg_ereal_cvg (R : realType) (u_ : (R^o) ^nat) : +Lemma dvg_ereal_cvg (R : realFieldType) (u_ : (R^o) ^nat) : u_ --> +oo -> (fun n => (u_ n)%:E) --> +oo%E. Proof. move/cvgPpinfty_lt => uoo; apply/cvg_ballP => _/posnumP[e]; rewrite near_map. @@ -909,4 +909,23 @@ rewrite ltr_subl_addr addrC -ltr_subl_addr (lt_le_trans leum) //. by rewrite le_contract nd_u_//; near: n; exists m. Grab Existential Variables. all: end_near. Qed. +(* NB: see also nondecreasing_series *) +Lemma ereal_nondecreasing_series (R : realDomainType) (u_ : {ereal R} ^nat) : + (forall n, 0%:E <= u_ n)%E -> + nondecreasing_seq (fun n => \sum_(i < n) u_ i)%E. +Proof. +move=> u_ge0 n m nm; rewrite -(subnKC nm). +rewrite -[X in (_ <= X)%E](big_mkord xpredT) /index_iota subn0 iota_add. +rewrite big_cat -[in X in (_ <= X + _)%E](subn0 n) big_mkord lee_addl //=. +by rewrite sume_ge0. +Qed. + +Lemma ereal_nneg_series_lim_ge (R : realType) (u_ : {ereal R} ^nat) k : + (forall n, (0%:E <= u_ n)%E) -> + (\sum_(i < k) u_ i <= lim (fun n : nat => \sum_(i < n) u_ i))%E. +Proof. +move/ereal_nondecreasing_series/nondecreasing_seq_ereal_cvg/cvg_lim => -> //. +by apply ereal_sup_ub; exists k. +Qed. + End sequences_of_extended_real_numbers. From bc0e4b2e602ccdf3d6d0318378557fb3caab6370 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 29 Jul 2020 17:54:11 +0900 Subject: [PATCH 2/2] update changelog --- CHANGELOG_UNRELEASED.md | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 0c8e77f6ff..fd68837e48 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -67,6 +67,9 @@ valid for a `uniformType` + moved `continuous_withinNx` from `normedType.v` to `topology.v` and generalised it to `uniformType` +- moved from `measure.v` to `sequences.v` + + `ereal_nondecreasing_series` + + `ereal_nneg_series_lim_ge` (renamed from `series_nneg`) ### Renamed