Module infotheo.information_theory.aep

From mathcomp Require Import all_ssreflect ssralg ssrnum matrix.
From mathcomp Require boolp.
From mathcomp Require Import reals exp.
Require Import realType_ext ssr_ext bigop_ext ssralg_ext realType_ln.
Require Import fdist proba entropy.


Set Implicit Arguments.
Set SsrOldRewriteGoalsOrder.
Unset Strict Implicit.
Import Prenex Implicits.

Local Open Scope fdist_scope.
Local Open Scope proba_scope.
Local Open Scope entropy_scope.
Local Open Scope ring_scope.
Local Open Scope vec_ext_scope.

Import Order.POrderTheory GRing.Theory Num.Theory.

From mathcomp Require Import normedtype.
Import numFieldNormedType.Exports.

Section mlog_prop.
Context {R : realType}.
Variables (A : finType) (P : R.-fdist A).

Definition

aep_sigma2

aep_sigma2 not a defined object.

: R := `E ((`-- (`log P)) `^2) - (`H P)^+2.

Lemma aep_sigma2E : aep_sigma2 = \sum_(a in A) P a * (log (P a))^+2 - (`H P)^+2.

Proof.

rewrite /aep_sigma2 /Ex [in LHS]/log_RV !RV_fctE/=.
by under eq_bigr do rewrite /ambient_dist expr2 mulrNN -expr2.
Qed.

Lemma V_mlog : `V (`-- (`log P)) = aep_sigma2.

Proof.

by rewrite /aep_sigma2 VarE entropy_Ex. Qed.

Lemma aep_sigma2_ge0 : 0 <= aep_sigma2.

Proof.

by rewrite -V_mlog /Var; apply: Ex_ge0 => ?; exact: sq_RV_ge0. Qed.

End mlog_prop.

Definition

sum_mlog_prod

sum_mlog_prod not a defined object.

{R : realType} (A : finType) (P : R.-fdist A) n :
    {RV ((P `^ n)%fdist)-> R} :=
  (fun t => \sum_(i < n) - log (P (t ``_ i)))%R.

Arguments sum_mlog_prod {R} {A} _ _.

Lemma sum_mlog_prod_sum_map_mlog {R : realType} (A : finType) (P : R.-fdist A) n :
  sum_mlog_prod P n.+1 \=sum (\row_(i < n.+1) `-- (`log P)).

Proof.

elim : n => [|n IH].
- move: (@sum_n_1 _ A P (\row_i `-- (`log P))).
  set mlogP := cast_fun_rV10 _.
  move => HmlogP.
  set mlogprodP := @sum_mlog_prod _ _ _ 1.
  suff -> : mlogprodP = mlogP by [].
  rewrite /mlogprodP /mlogP /sum_mlog_prod /cast_fun_rV10 /= mxE /=.
  by rewrite boolp.funeqE => ta; rewrite big_ord_recl big_ord0 addr0.
- rewrite [X in _ \=sum X](_ : _ =
      row_mx (\row_(i < 1) (`-- (`log P))) (\row_(i < n.+1) `-- (`log P))); last first.
    apply/rowP => b; rewrite !mxE; case: splitP.
      by move=> a; rewrite {a}(ord1 a) => _; rewrite mxE.
    by move=> k _; rewrite mxE.
  apply: (sum_n_cons IH _) => /= ta.
  rewrite /sum_mlog_prod /= big_ord_recl /=; congr (_ + _)%R.
  by apply: eq_bigr => i _; rewrite mxE.
Qed.

Section aep_k0_constant.
Context {R : realType}.
Variables (A : finType) (P : R.-fdist A).

Definition

aep_bound

aep_bound not a defined object.

epsilon : R := (aep_sigma2 P / epsilon ^+ 3)%R.

Lemma aep_bound_ge0 e (_ : 0 < e) : 0 <= aep_bound e.

Proof.

by apply: divr_ge0; [exact: aep_sigma2_ge0 | apply/exprn_ge0/ltW]. Qed.

Lemma aep_bound_decreasing e e' : 0 < e' <= e -> aep_bound e <= aep_bound e'.

Proof.

case/andP=> Oe' e'e.
apply: ler_wpM2l; first exact: aep_sigma2_ge0.
rewrite lef_pV2 ?posrE; [|apply/exprn_gt0..] => //; last first.
  by rewrite (lt_le_trans _ e'e).
by rewrite lerXn2r// ?nnegrE ltW// (lt_le_trans _ e'e).
Qed.

End aep_k0_constant.

Section AEP.
Context {R : realType}.
Variables (A : finType) (P : R.-fdist A) (n : nat) (epsilon : R).
Hypothesis Hepsilon : 0 < epsilon.

Lemma aep : aep_bound P epsilon <= n.+1%:R ->
  Pr (P `^ n.+1)%fdist [set t | (0 < (P `^ n.+1)%fdist t) &&
    (`| (`-- (`log (P `^ n.+1)%fdist) `/ n.+1) t - `H P | >= epsilon) ] <= epsilon.

Proof.

move=> Hbound.
apply: (@le_trans _ _ (aep_sigma2 P / (n.+1%:R * epsilon ^+ 2))); last first.
  rewrite invfM mulrCA -ler_pdivlMl// ?invr_gt0// invrK.
  by rewrite -ler_pdivrMr// -mulrA -invfM (mulrC _ epsilon) -exprS.
have Hsum := sum_mlog_prod_sum_map_mlog P n.
have H1 k i : `E ((\row_(i < k.+1) `-- (`log P)) ``_ i) = `H P.
  by rewrite mxE entropy_Ex.
have H2 k i : `V ((\row_(i < k.+1) `-- (`log P)) ``_ i) = aep_sigma2 P.
  by rewrite mxE V_mlog.
have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon).
move/(le_trans _); apply.
apply/subset_Pr/subsetP => ta; rewrite 2!inE => /andP[H1].
rewrite /sum_mlog_prod [`-- (`log _)]lock /= -lock /scale_RV /log_RV !RV_fctE/=.
rewrite fdist_rVE log_prodr_sumr_mlog //.
apply/prod_gt0_inv.
  by move=> x; exact: FDist.ge0.
by move: H1; rewrite fdist_rVE.
Qed.

End AEP.