Files

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 ```

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 counting
Used by
  • mathcomp.analysis.hoelder
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.counting_lebesgue
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable
Source code (TSource code : choiceType) (RSource code : realType) (XSource code : 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 dSource code (TSource code : sigmaRingType d) (RSource code : realType).
Variables (DSource code : set T) (mDSource code : measurable D).

Local Notation countingUsed by
  • mathcomp.analysis.hoelder
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral_nonneg
  • mathcomp.analysis.lebesgue_integral_theory.counting_lebesgue
  • mathcomp.analysis.lebesgue_integral_theory.lebesgue_integrable
Source code := (@counting T R).

Let counting0Source code : counting set0 = 0.
Proof.
by rewrite /counting asboolT// fset_set0. Qed.

Let counting_ge0Source code (ASource code : set T) : 0 <= counting A.
Proof.
by rewrite /counting; case: ifPn; rewrite ?lee_fin// lee_pinfty. Qed.

Let counting_sigma_additiveSource code : semi_sigma_additive counting.
Proof.
move=> F mF tF mU.
have [[i Fi]|infinF] := pselect (exists kSource code, infinite_set (F k)).
  have -> : counting (\bigcup_nSource code 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 iSource code, finite_set (F i) by exact/not_forallP.
pose u : nat^nat := fun nSource code => #|` fset_set (F n) |.
have sumFE n : \sum_(iSource code < n) counting (F i) =
               #|` fset_set (\big[setU/set0]_(kSource code < 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 nSource code \near \oo, u n = 0%N by apply: cvg_nseries_near.
  rewrite [X in _ --> X](_ : _ = \sum_(iSource code < N) counting (F i)).
    have -> : \bigcup_iSource code (F i) = \big[setU/set0]_(iSource code < 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 nSource code => \sum_(iSource code < n) counting (F i)) @ \oo --> +oo.
  rewrite (_ : (fun nSource code => _) = [sequence (\sum_(0 <= iSource code < n) (u i))%:R%:E]_nSource code); 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_nSource code 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_nSource code 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.

HBSource code.instanceSource code DefinitionSource code _Source code :=Source code isMeasureSource code.Build _ _ _ counting
  counting0 counting_ge0 counting_sigma_additive.

End measure_count.

Lemma sigma_finite_countingSource code (RSource code : realType) :
  sigma_finite [set: nat] (@counting _ R).
Proof.
exists (fun nSource code => `I_n.+1); first by apply/seteqP; split=> //x _; exists x => /=.
by move=> k; split => //; rewrite /counting/= asboolT// ltry.
Qed.
HBSource code.instanceSource code DefinitionSource code _Source code RSource code :=Source code
  @isSigmaFiniteSource code.Build _ _ _ (@counting _ R) (sigma_finite_counting R).
Generated by rocqnavi
Source
Uses
Used By