diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index f5c58612c..4b5460602 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -21,6 +21,16 @@ + lemmas `bigcupD1`, `bigcapD1` - in `measure.v`: + definition `measurable_fun` + + lemma `adde_undef_nneg_series` + + lemma `adde_def_nneg_series` +- in `measure.v`: + + lemmas `cvg_geometric_series_half`, `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..86027fc38 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. @@ -66,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. @@ -1088,3 +1102,178 @@ by move/(le_outer_measure mu); rewrite muB0 => ->. 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 A0; rewrite (@le_trans _ _ (lim (fun n => (\sum_(0 <= i < n | P i) A i) + + \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 => //. + + 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_def_nneg_series => // n _; apply: divr_ge0. +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. +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 <= 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. +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) => //; 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. + 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] <-]. + by apply: ereal_nneg_series_lim_ge0 => ? _; exact: measure_ge0. +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. + 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]. +- 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..bdfddc56a 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_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_def (\sum_(i 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. + 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