Skip to content

use topology.fct_comRingType for RVs #67

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

use topology.fct_comRingType for RVs #67

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
80b6dcd
use topology.fct_comRingType for RVs
t6s Oct 20, 2021
f784f12
shorten some lemmas
t6s Oct 20, 2021
57c7f19
E_inv_RV -> E_opp_RV
t6s Oct 21, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 18 additions & 24 deletions information_theory/aep.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,34 +34,24 @@ Definition aep_sigma2 := `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]/mlog_RV /sq_RV /comp_RV.
by under eq_bigr do rewrite mulRC /ambient_dist -mulRR Rmult_opp_opp mulRR.
rewrite /aep_sigma2 /Ex [in LHS]/mlog_RV /comp_RV.
by under eq_bigr do rewrite mulRC /ambient_dist sq_RV_pow2-mulRR Rmult_opp_opp mulRR.
Qed.

Lemma V_mlog : `V (--log P) = aep_sigma2.
Proof.
rewrite aep_sigma2E /Var E_trans_RV_id_rem -entropy_Ex.
transitivity
(\sum_(a in A) ((- log (P a))^2 * P a - 2 * `H P * - log (P a) * P a +
`H P ^ 2 * P a))%R.
apply eq_bigr => a _.
rewrite /scalel_RV /mlog_RV /trans_add_RV /sq_RV /comp_RV /= /sub_RV.
by rewrite /ambient_dist; field.
rewrite big_split /= big_split /= -big_distrr /= (FDist.f1 P) mulR1.
rewrite (_ : \sum_(a in A) - _ = - (2 * `H P ^ 2))%R; last first.
rewrite -{1}big_morph_oppR; congr (- _)%R.
rewrite [X in X = _](_ : _ =
\sum_(a in A) (2 * `H P) * (- (P a * log (P a))))%R; last first.
apply eq_bigr => a _; by rewrite -!mulRA (mulRC (P a)) mulNR.
rewrite -big_distrr [in LHS]/= -{1}big_morph_oppR.
by rewrite -/(entropy P) -mulRA /= mulR1.
set s := ((\sum_(a in A ) _)%R in LHS).
rewrite (_ : \sum_(a in A) _ = s)%R; last by apply eq_bigr => a _; field.
field.
rewrite aep_sigma2E /Var E_trans_RV_id_rem -entropy_Ex E_trans_add_RV E_sub_RV -scaler_RV_natr.
rewrite !E_scaler_RV -INRE !entropy_Ex mulRC mulRR -addRR -addR_opp oppRD.
rewrite -!addRA -(addRC (`E --log P ^ 2)) addR_opp subRR addR0 addR_opp.
under eq_bigr=> i do rewrite mulRC -mulRR -(Rmult_opp_opp (log (P i)) (log (P i))) mulRR.
rewrite -/(Ex _ _) /mlog_RV.
congr (`E _ - _); apply boolp.funext=> u /=.
by rewrite sq_RV_pow2.
Qed.

Lemma aep_sigma2_ge0 : 0 <= aep_sigma2.
Proof. rewrite -V_mlog /Var; apply Ex_ge0 => ?; exact: pow_even_ge0. Qed.
Proof.
by rewrite -V_mlog /Var; apply Ex_ge0 => ?; rewrite sq_RV_pow2; exact: pow_even_ge0.
Qed.

End mlog_prop.

Expand Down Expand Up @@ -135,8 +125,12 @@ have H2 : forall k i, `V ((\row_(i < k.+1) --log P) ``_ i) = aep_sigma2 P.
have {H1 H2} := (wlln (H1 n) (H2 n) Hsum Hepsilon).
move/(leR_trans _); apply.
apply/Pr_incl/subsetP => ta; rewrite 2!inE => /andP[H1].
rewrite /sum_mlog_prod [--log _]lock /= -lock /= /scalel_RV /mlog_RV.
rewrite TupleFDist.dE log_prodR_sumR_mlog //.
set X := (X in X >b= _); set Y := (Y in ((_ <= Y)%O)).
suff -> : X = Y by move/leRP/RleP.
rewrite /X /Y /comp_RV /trans_min_RV.
rewrite /scalel_RV /GRing.add /GRing.mul /topology.cst /=.
congr `| _ * _ + _ |.
rewrite /sum_mlog_prod /mlog_RV TupleFDist.dE log_prodR_sumR_mlog //.
apply: (prodR_gt0_inv (FDist.ge0 P)).
by move: H1; rewrite TupleFDist.dE => /ltRP.
Qed.
Expand Down
10 changes: 8 additions & 2 deletions information_theory/typ_seq.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -177,8 +177,14 @@ have -> : Pr P `^ n.+1 (~: p) =
rewrite {1}/Pr (eq_bigr (fun=> 0)); last by move=> /= v; rewrite inE => /eqP.
rewrite big_const iter_addR mulR0 add0R.
apply/(leR_trans _ (aep He k0_k))/Pr_incl/subsetP => /= t.
rewrite !inE /= => /andP[-> /= H3]; apply/ltRW'.
by rewrite /mlog_RV /= /scalel_RV /= mulRN -mulNR.
rewrite !inE /= => /andP[-> /= /ltRP H3]; apply/ltRW'.
Copy link
Owner

@affeldt-aist affeldt-aist Oct 21, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe this should not get longer.

suff <- : `|- (1 / n.+1%:R) * log (P `^ n.+1 t) - `H P|
= `|(--log (P `^ n.+1) `/ n.+1) t - `H P| by apply/ltRP.
congr `| _ - _ |.
rewrite /mlog_RV /scalel_RV /topology.cst /= div1R.
rewrite -RinvE -?INRE -?lt0n_neqR0' ?ltR0Sn //.
rewrite /GRing.mul /= mul1R mulNR -mulRN.
by congr (_ * _)%R.
Qed.

Variable He1 : epsilon < 1.
Expand Down
Loading