use topology.fct_comRingType for RVs #67
Conversation
|
One concern is that I could not use generic lemmas not so much I originally expected. |
|
Oops, |
information_theory/aep.v
Outdated
| @@ -30,36 +30,23 @@ Section mlog_prop. | |||
|
|
|||
| Variables (A : finType) (P : fdist A). | |||
|
|
|||
| Lemma E_mlog : `E (--log P) = `H P. | |||
| @@ -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'. | |||
There was a problem hiding this comment.
Maybe this should not get longer.
| @@ -164,6 +167,21 @@ Proof. by apply/setP => -[a b]; rewrite !inE. Qed. | |||
|
|
|||
| End TsetT. | |||
|
|
|||
| Section Rstruct_ext. | |||
| Lemma ltR0Sn n : 0 < n.+1%:R. | |||
| Section Rstruct_ext. | ||
| Lemma ltR0Sn n : 0 < n.+1%:R. | ||
| Proof. by move/ltR_nat:(ltn0Sn n). Qed. | ||
| Lemma lt0n_neqR0 n : (0 < n)%nat <-> n%:R != 0. |
There was a problem hiding this comment.
Maybe this could be shorter by using ltR0n
|
Could you put some information in the changelog? (At least about the potentially breaking changes.) In any case, good to see things get little bit tidier. Thanks! |
|
I have noticed that this change imports the axiom of choice in proba.v, which I expect cause some controversy. |
|
This is useful to have in robustmean, could you revive this and put it in the next release? |
Let's do it! I think I can look at this after completing the current batch of cleaning in infotheo (removal of R). I am afraid a release including this work will not be that quick, Uses in robustmean will help this process, and so I suggest using a development branch for a while, not waiting for a release. |
|
The proper way for RVs to behave like fct_ringType will be to definene them in the hierarchy, inheriting definitions from functions.v. I would really like to use HB for such an extension. What is the current status of the compatibility between infotheo and HB-based analysis? @affeldt-aist |
|
I didn't try but according to https://hal.science/hal-04225130/document (see page 2) and since we are not building any deep hierarchy using canonicals in infotheo (indeed we are now using HB for convex and scaled convex) this should almost be transparent (unless we try to get rid of our ordered structure, in which case there is a bit of work but maybe not much). |
|
I am not saying that we should do it asap though, on the contrary, considering practical aspects, it is maybe more reasonable to clean up infotheo for robustmean as much as possible first and then do the port once MathComp-Analysis 1.0 is released (the plan is January 2024, beginning of the month at the latest). |
This is an experiment to switch algebraic operations on random variables to the generic ones on
ringType.Some lemmas in proba.v, aep.v, typ_seq.v needed rather big modifications, while the proofs in other files could be accommodated
just by changing
rewrite /sq_RV /comp_RVtorewrite sq_RV_pow2.