counting measure

CHANGELOG_UNRELEASED.md

@@ -34,6 +34,13 @@
   + lemma `fset_set_image`, `card_fset_set`, `geq_card_fset_set`,
     `leq_card_fset_set`, `infinite_set_fset`, `infinite_set_fsetP` and
     `fcard_eq`.
+- in file `cardinality.v`:
+  + lemmas `trivIset_sum_card`, `fset_set_sub`, `fset_set_set0`
+- in file `sequences.v`:
+  + lemmas `nat_dvg_real`, `nat_cvgPpinfty`, `nat_nondecreasing_is_cvg`
+  + definition `nseries`, lemmas `le_nseries`, `cvg_nseries_near`, `dvg_nseries`
+- in file `measure.v`:
+  + defintion `measure_count`, lemma `measure_countE`
 
 ### Changed
 

theories/cardinality.v

@@ -711,6 +711,20 @@ Proof.
 by move=> fA x; rewrite -[A in RHS]fset_setK//; apply/idP/idP; rewrite ?inE.
 Qed.
 
+Lemma fset_set_sub (T : choiceType) (A B : set T) :
+  finite_set A -> finite_set B -> A `<=` B -> (fset_set A `<=` fset_set B)%fset.
+Proof.
+move=> finA finB AB; apply/fsubsetP => t.
+by rewrite in_fset_set// in_fset_set// 2!inE => /AB.
+Qed.
+
+Lemma fset_set_set0 (T : choiceType) (A : set T) : finite_set A ->
+  fset_set A = fset0 -> A = set0.
+Proof.
+move=> finA; rewrite /fset_set; case: pselect => // {}finA.
+by case: cid => _/= -> ->; rewrite set_fset0.
+Qed.
+
 Lemma fset_set0 {T : choiceType} : fset_set (set0 : set T) = fset0.
 Proof.
 by apply/fsetP=> x; rewrite in_fset_set ?inE//; apply/negP; rewrite inE.
@@ -808,6 +822,21 @@ have Gy : y \in G k by rewrite in_fset_set ?inE//; apply: Ffin.
 by exists (Tagged G [` Gy]%fset).
 Qed.
 
+Lemma trivIset_sum_card (T : choiceType) (F : nat -> set T) n :
+  (forall n, finite_set (F n)) -> trivIset [set: nat] F ->
+  (\sum_(i < n) #|` fset_set (F i)| =
+   #|` fset_set (\big[setU/set0]_(k < n) F k)|)%N.
+Proof.
+move=> finF tF; elim: n => [|n ih]; first by rewrite !big_ord0 fset_set0.
+rewrite big_ord_recr//= ih big_ord_recr/= fset_setU//; last first.
+  by rewrite -bigcup_mkord; exact: bigcup_finite.
+rewrite cardfsU [X in (_ - X)%N](_ : _  = O) ?subn0// ?EFinD ?natrD//.
+apply/eqP; rewrite cardfs_eq0 -fset_setI//; last first.
+  by rewrite -bigcup_mkord; exact: bigcup_finite.
+rewrite (@trivIset_bigsetUI _ xpredT)// ?fset_set0//.
+by rewrite [X in trivIset X F](_ : _ = [set: nat])//; exact/seteqP.
+Qed.
+
 Lemma finite_setMR (T T' : choiceType) (A : set T) (B : T -> set T') :
   finite_set A -> (forall x, A x -> finite_set (B x)) -> finite_set (A `*`` B).
 Proof.

theories/lebesgue_integral.v

@@ -1989,7 +1989,7 @@ apply/eqP; rewrite eq_le; apply/andP; split; last first.
     apply: ge0_le_integral => //.
     - by move=> x _; apply: ereal_lim_ge => //; apply: nearW => k; exact/g0.
     - apply: emeasurable_fun_cvg mg _ => x _.
-      by apply: ereal_nondecreasing_is_cvg.
+      exact: ereal_nondecreasing_is_cvg.
     - move=> x Dx; apply: ereal_lim_ge => //.
       near=> m; have nm : (n <= m)%N by near: m; exists n.
       exact/nd_g.

theories/measure.v

@@ -62,6 +62,9 @@ From HB Require Import structures.
 (*                   measurable sets and is semi-sigma-additive               *)
 (*   sigma_finite A f == the measure f is sigma-finite on A : set T with      *)
 (*                   T : ringOfSetsType.                                      *)
+(*   measure_restr mu mD == restriction of the measure mu to a set D;         *)
+(*                   mD is a proof that D is measurable                       *)
+(*   measure_count T R == counting measure                                    *)
 (*   mu.-negligible A == A is mu negligible                                   *)
 (* 　{ae mu, forall x, P x} == P holds almost everywhere for the measure mu   *)
 (*                                                                            *)
@@ -1349,17 +1352,16 @@ End measure_is_additive_measure.
 
 Coercion measure_additive_measure : Measure.map >-> AdditiveMeasure.map.
 
-
 Section measure_restr.
 Variables (T : measurableType) (R : realType) (mu : {measure set T -> \bar R}).
 Variables (D : set T) (mD : measurable D).
 
 Let measure_restr' (X : set _) : \bar R := mu (X `&` D).
 
-Let measure_restr'0 : measure_restr' set0 = 0%E.
+Let measure_restr'0 : measure_restr' set0 = 0.
 Proof. by rewrite /measure_restr' set0I measure0. Qed.
 
-Let measure_restr'_ge0 (A : set _) : (0 <= measure_restr' A)%E.
+Let measure_restr'_ge0 (A : set _) : 0 <= measure_restr' A.
 Proof.
 by rewrite /measure_restr'; apply: measure_ge0; exact: measurableI.
 Qed.
@@ -1384,6 +1386,87 @@ Proof. by []. Qed.
 
 End measure_restr.
 
+Section measure_count.
+Variables (T : measurableType) (R : realType).
+Variables (D : set T) (mD : measurable D).
+
+Let measure_count' (X : set T) : \bar R :=
+  if `[< finite_set X >] then (#|` fset_set X |)%:R%:E else +oo.
+
+Let measure_count'0 : measure_count' set0 = 0.
+Proof. by rewrite /measure_count' asboolT// fset_set0. Qed.
+
+Let measure_count'_ge0 (A : set _) : 0 <= measure_count' A.
+Proof.
+by rewrite /measure_count'; case: ifPn; rewrite ?lee_fin// lee_pinfty.
+Qed.
+
+Let measure_count'_sigma_additive : semi_sigma_additive measure_count'.
+Proof.
+move=> F mF tF mU.
+have [[i Fi]|infinF] := pselect (exists k, infinite_set (F k)).
+  have -> : measure_count' (\bigcup_n F n) = +oo.
+    rewrite /measure_count' asboolF//.
+    by apply: contra_not Fi; exact/sub_finite_set/bigcup_sup.
+  apply/ereal_cvgPpinfty => M M0; near=> n.
+  have ni : (i < n)%N by near: n; exists i.+1.
+  rewrite (bigID (xpred1 i))/= big_mkord (big_pred1 (Ordinal ni))//=.
+  rewrite [X in X + _]/measure_count' asboolF// addooe ?lee_pinfty//.
+  by rewrite gt_eqF// (@lt_le_trans _ _ 0) ?lte_ninfty//; exact: sume_ge0.
+have {infinF}finF : forall i, finite_set (F i) by exact/not_forallP.
+pose u : nat^nat := fun n => #|` fset_set (F n) |.
+have sumFE n : \sum_(i < n) measure_count' (F i) =
+               #|` fset_set (\big[setU/set0]_(k < n) F k) |%:R%:E.
+  rewrite -trivIset_sum_card// natr_sum -sumEFin.
+  by apply eq_bigr => // i _; rewrite /measure_count' asboolT.
+have [cvg_u|dvg_u] := pselect (cvg (nseries u)).
+  have [N _ Nu] : \forall n \near \oo, u n = 0%N by apply: cvg_nseries_near.
+  rewrite [X in _ --> X](_ : _ = \sum_(i < N) measure_count' (F i)); last first.
+    have -> : \bigcup_i (F i) = \big[setU/set0]_(i < N) F i.
+      rewrite (bigcupID (`I_N)) setTI bigcup_mkord.
+      rewrite [X in _ `|` X](_ : _ = set0) ?setU0// bigcup0// => i [_ /negP].
+      by rewrite -leqNgt => /Nu/eqP/[!cardfs_eq0]/eqP/fset_set_set0 ->.
+    rewrite /measure_count' /= asboolT// ?sumFE//.
+    by rewrite -bigcup_mkord; exact: bigcup_finite.
+  rewrite -(cvg_shiftn N)/=.
+  rewrite (_ : (fun n => _) = (fun=> \sum_(i < N) measure_count' (F i))).
+    exact: cvg_cst.
+  apply/funext => n; rewrite /index_iota subn0 (addnC n) iotaD big_cat/=.
+  rewrite [X in _ + X](_ : _ = 0) ?adde0.
+    by rewrite -{1}(subn0 N) big_mkord.
+  rewrite add0n big_seq big1// => i /[!mem_iota] => /andP[NI iNn].
+  by rewrite /measure_count' asboolT//= -/(u _) Nu.
+have {dvg_u}cvg_F : (fun n => \sum_(i < n) measure_count' (F i)) --> +oo.
+  rewrite (_ : (fun n => _) = [sequence (\sum_(0 <= i < n) (u i))%:R%:E]_n).
+    exact/dvg_ereal_cvg/nat_dvg_real/dvg_nseries.
+  apply/funext => n /=; under eq_bigr.
+    by rewrite /measure_count' => i _; rewrite asboolT//; over.
+  by rewrite sumEFin natr_sum big_mkord.
+have [UFoo|/contrapT[k UFk]] := pselect (infinite_set (\bigcup_n F n)).
+  rewrite /measure_count' asboolF//.
+  by under eq_fun do rewrite big_mkord.
+exfalso.
+move: cvg_F =>/ereal_cvgPpinfty/(_ k.+1%:R)/[!ltr0n]/(_ erefl)[K _].
+move=> /(_ K (leqnn _)); rewrite leNgt => /negP; apply.
+rewrite sumFE lte_fin ltr_nat ltnS.
+have -> : k = #|` fset_set (\bigcup_n F n) |.
+  by apply/esym/card_eq_fsetP; rewrite fset_setK//; exists k.
+apply/fsubset_leq_card/fset_set_sub => //.
+- by rewrite -bigcup_mkord; exact: bigcup_finite.
+- by exists k.
+- by move=> /= t; rewrite -bigcup_mkord => -[m _ Fmt]; exists m.
+Unshelve. all: by end_near. Qed.
+
+Definition measure_count : {measure set _ -> \bar R} :=
+  Measure.Pack _ (Measure.Axioms
+    measure_count'0 measure_count'_ge0 measure_count'_sigma_additive).
+
+Lemma measure_countE A : measure_count A =
+  if `[< finite_set A >] then #|` fset_set A|%:R%:E else +oo.
+Proof. by []. Qed.
+
+End measure_count.
+
 Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R)
    (op : Monoid.com_law idx) (A : I -> set T) (F : set T -> R) :
     finite_set D -> trivIset D A -> F set0 = idx ->

theories/sequences.v

@@ -52,6 +52,9 @@ Require Import topology normedtype landau.
 (*                adjacent == adjacent sequences lemma                        *)
 (*                  cesaro == Cesaro's lemma                                  *)
 (*                                                                            *)
+(* * About sequences of natural numbers:                                      *)
+(*   nseries                                                                  *)
+(*                                                                            *)
 (* * About sequences of extended real numbers:                                *)
 (*   eseries, etelescope, etc.                                                *)
 (*                                                                            *)
@@ -627,7 +630,7 @@ apply: cvg_distW => _/posnumP[e]; rewrite near_map.
 have [p /andP[Mu_p u_pM]] : exists p, M - e%:num <= u_ p <= M.
   have [_ -[p _] <- /ltW Mu_p] := sup_adherent su_ (gt0 e).
   by exists p; rewrite Mu_p; have /ubP := sup_upper_bound su_; apply; exists p.
-near=> n; have pn : (p <= n)%N by near: n; apply: nbhs_infty_ge.
+near=> n; have pn : (p <= n)%N by near: n; exact: nbhs_infty_ge.
 rewrite distrC ler_norml ler_sub_addl (le_trans Mu_p (u_nd _ _ pn)) /=.
 rewrite ler_subl_addr (@le_trans _ _ M) ?ler_addr //.
 by have /ubP := sup_upper_bound su_; apply; exists n.
@@ -872,10 +875,9 @@ Lemma cvg_series_cvg_0 (K : numFieldType) (V : normedModType K) (u_ : V ^nat) :
   cvg (series u_) -> u_ --> (0 : V).
 Proof.
 move=> cvg_series.
-rewrite (_ : u_ = fun n => series u_ (n + 1)%nat - series u_ n); last first.
-  by rewrite funeqE => i; rewrite addn1 seriesSB.
-rewrite -(subrr (lim (series u_))).
-by apply: cvgB => //; rewrite ?cvg_shiftn.
+rewrite (_ : u_ = fun n => series u_ n.+1 - series u_ n); last first.
+  by rewrite funeqE => i; rewrite seriesSB.
+by rewrite -(subrr (lim (series u_))); apply: cvgB => //; rewrite ?cvg_shiftS.
 Qed.
 
 Lemma nondecreasing_series (R : numFieldType) (u_ : R ^nat) :
@@ -1186,6 +1188,89 @@ End exponential_series.
 (* TODO: generalize *)
 Definition expR {R : realType} (x : R) : R := lim (series (exp_coeff x)).
 
+(********************************)
+(* Sequences of natural numbers *)
+(********************************)
+
+Lemma nat_dvg_real (R : realType) (u_ : nat ^nat) : u_ --> \oo ->
+  ([sequence (u_ n)%:R : R^o]_n --> +oo)%R.
+Proof.
+move=> uoo; apply/cvgPpinfty => A /=.
+have /uoo[N _ NuA] : \oo [set m | `|ceil A|.+1 <= m]%N by exists `|ceil A|.+1.
+near=> n; have /NuA : (N <= n)%N by near: n; exact: nbhs_infty_ge.
+rewrite /= -(ler_nat R); apply: le_trans.
+have [A0|A0] := leP 0%R A; last by rewrite (le_trans (ltW A0)).
+by rewrite -addn1 natrD natr_absz ger0_norm// ?ceil_ge0// ler_paddr// ceil_ge.
+Unshelve. all: by end_near. Qed.
+
+Lemma nat_cvgPpinfty (u : nat^nat) :
+  u --> \oo <-> forall A, \forall n \near \oo, (A <= u n)%N.
+Proof.
+split => [uoo A|oou X [N _ NX]].
+  by rewrite -(near_map u \oo (leq A)); apply: uoo; exists A.
+rewrite !near_simpl [\near u, X _](near_map u \oo); near=> n.
+apply: NX => /=; rewrite (@leq_trans N.+1) //.
+by near: n; apply: oou; rewrite ltr_spaddr // le_maxr lexx.
+Unshelve. all: by end_near. Qed.
+
+Lemma nat_nondecreasing_is_cvg (u_ : nat^nat) :
+  nondecreasing_seq u_ -> has_ubound (range u_) -> cvg u_.
+Proof.
+move=> u_nd [l ul].
+suff [N Nu] : exists N, forall n, (n >= N)%N -> u_ n = u_ N.
+  apply/cvg_ex; exists (u_ N); rewrite -(cvg_shiftn N).
+  rewrite [X in X --> _](_ : _ = cst (u_ N))//; first exact: cvg_cst.
+  by apply/funext => n /=; rewrite Nu// leq_addl.
+apply/not_existsP => hu.
+have {hu}/choice[f Hf] : forall x, (exists n, x <= n /\ u_ n > u_ x)%N.
+  move=> x; have /existsNP[N /not_implyP[xN Nx]] := hu x.
+  exists N; split => //; move/eqP : Nx; rewrite neq_lt => /orP[|//].
+  by move/u_nd : xN; rewrite le_eqVlt => /predU1P[->|//].
+have uf : forall x, (x < u_ (iter x.+1 f O))%N.
+  elim=> /= [|i ih]; first by have := Hf O => -[_]; exact: leq_trans.
+  by have := Hf (f (iter i f O)) => -[_]; exact: leq_trans.
+have /ul : range u_ (u_ (iter l.+1 f O)) by exists (iter l.+1 f O).
+by rewrite leNgt => /negP; apply; rewrite ltEnat //=; exact: uf.
+Qed.
+
+Definition nseries (u : nat^nat) := (fun n => \sum_(0 <= k < n) u k)%N.
+
+Lemma le_nseries (u : nat^nat) : {homo nseries u : a b / (a <= b)%N}.
+Proof.
+move=> a b ab; rewrite /nseries [in X in (_ <= X)%N]/index_iota subn0.
+rewrite -[in X in (_ <= X)%N](subnKC ab) iotaD big_cat/= add0n.
+by rewrite /index_iota subn0 leq_addr.
+Qed.
+
+Lemma cvg_nseries_near (u : nat^nat) : cvg (nseries u) ->
+  \forall n \near \oo, u n = 0%N.
+Proof.
+move=> /cvg_ex[l ul]; have /ul[a _ aul] : nbhs l [set l].
+  exists [set l]; split; last by split.
+  by exists [set l] => //; rewrite bigcup_set1.
+have /ul[b _ bul] : nbhs l [set l.-1; l].
+  by exists [set l]; split => //; exists [set l] => //; rewrite bigcup_set1.
+exists (maxn a b) => // n /= abn.
+rewrite (_ : u = fun n => nseries u n.+1 - nseries u n)%N; last first.
+  by rewrite funeqE => i; rewrite /nseries big_nat_recr//= addnC addnK.
+have /aul -> : (a <= n)%N by rewrite (leq_trans _ abn) // leq_max leqnn.
+have /bul[->|->] : (b <= n.+1)%N by rewrite leqW// (leq_trans _ abn)// leq_maxr.
+- by apply/eqP; rewrite subn_eq0// leq_pred.
+- by rewrite subnn.
+Qed.
+
+Lemma dvg_nseries (u : nat^nat) : ~ cvg (nseries u) -> nseries u --> \oo.
+Proof.
+move=> du; apply: contrapT => /nat_cvgPpinfty/existsNP[l lu]; apply: du.
+apply: nat_nondecreasing_is_cvg => //; first exact: le_nseries.
+exists l => _ [n _ <-]; rewrite leNgt; apply/negP => lun; apply: lu; near=> m.
+by rewrite (leq_trans (ltW lun)) // le_nseries//; near: m; exists n.
+Unshelve. all: by end_near. Qed.
+
+(**************************************)
+(* Sequences of extended real numbers *)
+(**************************************)
+
 Notation "\big [ op / idx ]_ ( m <= i <oo | P ) F" :=
   (lim (fun n => (\big[ op / idx ]_(m <= i < n | P) F))) : big_scope.
 Notation "\big [ op / idx ]_ ( m <= i <oo ) F" :=

theories/topology.v

@@ -1064,7 +1064,7 @@ Ltac done :=
    | match goal with |- ?x \is_near _ => near: x; apply: prop_ofP end ].
 
 Lemma have_near (U : Type) (fT : filteredType U) (x : fT) (P : Prop) :
-   ProperFilter (nbhs x) -> (\forall x \near x, P) -> P.
+  ProperFilter (nbhs x) -> (\forall x \near x, P) -> P.
 Proof. by move=> FF nP; have [] := @filter_ex _ _ FF (fun=> P). Qed.
 Arguments have_near {U fT} x.
 
@@ -1114,7 +1114,7 @@ Lemma filter_const {T : Type} {F} {FF: @ProperFilter T F} (P : Prop) :
 Proof. by move=> FP; case: (filter_ex FP). Qed.
 
 Lemma in_filter_from {I T : Type} (D : set I) (B : I -> set T) (i : I) :
-   D i -> filter_from D B (B i).
+  D i -> filter_from D B (B i).
 Proof. by exists i. Qed.
 
 Lemma near_andP {T : Type} F (b1 b2 : T -> Prop) : Filter F ->
@@ -1147,7 +1147,7 @@ Qed.
 
 Lemma filter_ex2 {T U : Type} (F : set (set T)) (G : set (set U))
   {FF : ProperFilter F} {FG : ProperFilter G} (P : set T) (Q : set U) :
-   F P -> G Q -> exists x : T, exists2 y : U, P x & Q y.
+    F P -> G Q -> exists x : T, exists2 y : U, P x & Q y.
 Proof. by move=> /filter_ex [x Px] /filter_ex [y Qy]; exists x, y. Qed.
 Arguments filter_ex2 {T U F G FF FG _ _}.
 
@@ -2001,7 +2001,7 @@ Proof. by move=> ?; exists D. Qed.
 Variable (I : pointedType) (T : Type) (D : set I) (b : I -> (set T)).
 Hypothesis (b_cover : \bigcup_(i in D) b i = setT).
 Hypothesis (b_join : forall i j t, D i -> D j -> b i t -> b j t ->
-  exists k, D k /\ b k t /\ b k `<=` b i `&` b j).
+  exists k, [/\ D k, b k t & b k `<=` b i `&` b j]).
 
 Program Definition topologyOfBaseMixin :=
   @topologyOfOpenMixin _ (open_from D b) (open_fromT b_cover) _ _.
@@ -2016,7 +2016,7 @@ have ABU : forall t, (A `&` B) t ->
   have [iB [DiB [biBt sbiB]]] : exists i, D i /\ b i t /\ b i `<=` B.
     move: Bt; rewrite -BeUbB => - [i DBi bit]; exists i.
     by split; [apply: sDBD|split=> // ?; exists i].
-  have [i [Di [bit sbiAB]]] := b_join DiA DiB biAt biBt.
+  have [i [Di bit sbiAB]] := b_join DiA DiB biAt biBt.
   by exists i; split=> //; split=> // s /sbiAB [/sbiA ? /sbiB].
 set Dt := fun t => [set it | D it /\ b it t /\ b it `<=` A `&` B].
 exists [set get (Dt t) | t in A `&` B].
@@ -2071,7 +2071,7 @@ Program Definition topologyOfSubbaseMixin :=
   @topologyOfBaseMixin _ _ (finI_from D b) id (finI_from_cover D b) _.
 Next Obligation.
 move=> A B t [DA sDAD AeIbA] [DB sDBD BeIbB] At Bt.
-exists (A `&` B); split; last by split.
+exists (A `&` B); split => //.
 exists (DA `|` DB)%fset; first by move=> i /fsetUP [/sDAD|/sDBD].
 rewrite predeqE => s; split=> [Ifs|[As Bs] i /fsetUP].
   split; first by rewrite -AeIbA => i DAi; apply: Ifs; rewrite /= inE DAi.
@@ -2092,7 +2092,7 @@ Let bT : \bigcup_(i in D) b i = setT.
 Proof. by rewrite predeqE => i; split => // _; exists i. Qed.
 
 Let bD : forall i j t, D i -> D j -> b i t -> b j t ->
-  exists k, D k /\ b k t /\ b k `<=` b i `&` b j.
+  exists k, [/\ D k, b k t & b k `<=` b i `&` b j].
 Proof. by move=> i j t _ _ -> ->; exists j. Qed.
 
 Definition nat_topologicalTypeMixin := topologyOfBaseMixin bT bD.