Module mathcomp.analysis.measure_theory.counting_measure

From HB Require Import structures.
From mathcomp Require Import boot order algebra finmap.
From mathcomp Require Import boolp classical_sets functions cardinality reals.
From mathcomp Require Import interval_inference ereal topology normedtype.
From mathcomp Require Import sequences measurable_structure measure_function.

# The Counting Measure ``` counting T R == counting measure ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Definition ( : choiceType) ( : realType) ( : set T) : \bar R :=
if `[< finite_set X >] then (#|` fset_set X |)%:R%:E else +oo%E.
Arguments counting {T R}.

Section measure_count.
Local Open Scope ereal_scope.
Context ( : sigmaRingType d) ( : realType).
Variables ( : set T) ( : measurable D).

Local Notation := (@counting T R).

Let : counting set0 = 0.

Proof.

by rewrite /counting asboolT// fset_set0. Qed.

Let ( : set T) : 0 <= counting A.

Proof.

by rewrite /counting; case: ifPn; rewrite ?lee_fin// lee_pinfty. Qed.

Let : semi_sigma_additive counting.

Proof.

move=> F mF tF mU.
have [[i Fi]|infinF] := pselect (exists , infinite_set (F k)).
  have -> : counting (\bigcup_ F n) = +oo.
    rewrite /counting asboolF//.
    by apply: contra_not Fi; exact/sub_finite_set/bigcup_sup.
  apply/cvgeyPge => M; 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 + _]/(counting _) asboolF// addye ?leey//.
  by rewrite gt_eqF// (@lt_le_trans _ _ 0)//; exact: sume_ge0.
have {infinF}finF : forall , finite_set (F i) by exact/not_forallP.
pose u : nat^nat := fun => #|` fset_set (F n) |.
have sumFE n : \sum_( < n) counting (F i) =
               #|` fset_set (\big[setU/set0]_( < n) F k) |%:R%:E.
  rewrite -trivIset_sum_card// natr_sum -sumEFin.
  by apply: eq_bigr => // i _; rewrite /counting asboolT.
have [cvg_u|dvg_u] := pselect (cvg (nseries u @ \oo)).
  have [N _ Nu] : \forall \near \oo, u n = 0%N by apply: cvg_nseries_near.
  rewrite [X in _ --> X](_ : _ = \sum_( < N) counting (F i)).
    have -> : \bigcup_ (F i) = \big[setU/set0]_( < 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 ->.
    by rewrite /counting /= asboolT ?sumFE// -bigcup_mkord; exact: bigcup_finite.
  set l := (X in _ --> X); rewrite -(cvg_shiftn N)/= -[X in _ --> X]/(nbhs l).
  rewrite [X in X @ _](_ : _ = cst l)//.
  apply/funext => n; rewrite /index_iota subn0 (addnC n) iotaD big_cat/=.
  rewrite [X in _ + X](_ : _ = 0) ?adde0; last first.
    by rewrite -{1}(subn0 N) big_mkord.
  rewrite add0n big_seq big1// => i /[!mem_iota] => /andP[NI iNn].
  by rewrite /counting asboolT//= -/(u _) Nu.
have {dvg_u}cvg_F : (fun => \sum_( < n) counting (F i)) @ \oo --> +oo.
  rewrite (_ : (fun => _) = [sequence (\sum_(0 <= < n) (u i))%:R%:E]_); last first.
    exact/cvgenyP/dvg_nseries.
  apply/funext => n /=; under eq_bigr.
    by rewrite /counting => i _; rewrite asboolT//; over.
  by rewrite sumEFin natr_sum big_mkord.
have [UFoo|/contrapT[k UFk]] := pselect (infinite_set (\bigcup_ F n)).
  rewrite /counting asboolF//.
  by under eq_fun do rewrite big_mkord.
suff: false by [].
move: cvg_F =>/cvgeyPge/(_ k.+1%:R) [K _] /(_ K (leqnn _)) /=; apply: contra_leT => _.
rewrite sumFE lte_fin ltr_nat ltnS.
have -> : k = #|` fset_set (\bigcup_ F n) |.
  by apply/esym/card_eq_fsetP; rewrite fset_setK//; exists k.
apply/fsubset_leq_card; rewrite -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.

..Build _ _ _ counting
counting0 counting_ge0 counting_sigma_additive.

End measure_count.

Lemma ( : realType) :
sigma_finite [set: nat] (@counting _ R).

Proof.

exists (fun => `I_n.+1); first by apply/seteqP; split=> //x _; exists x => /=.
by move=> k; split => //; rewrite /counting/= asboolT// ltry.
Qed.

.
.Build _ _ _ (@counting _ R) (sigma_finite_counting R).

Files

Module mathcomp.analysis.measure_theory.counting_measure