Skip to content
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.

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

use topology.fct_comRingType for RVs #67

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

use topology.fct_comRingType for RVs #67

wants to merge 3 commits into from

Conversation

t6s
Copy link
Collaborator

@t6s t6s commented Oct 20, 2021

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_RV to rewrite sq_RV_pow2.

@t6s
Copy link
Collaborator Author

t6s commented Oct 20, 2021

One concern is that I could not use generic lemmas not so much I originally expected.
I am afraid that the usefulness of the ring structure needs to be more clearly shown for this draft to be turned into a proper PR.

@t6s
Copy link
Collaborator Author

t6s commented Oct 21, 2021

Oops, inv is indeed wrong. I have renamed it E_opp_RV.
(I would rather keep neg for boolean negation.)

@@ -30,36 +30,23 @@ Section mlog_prop.

Variables (A : finType) (P : fdist A).

Lemma E_mlog : `E (--log P) = `H P.
Copy link
Owner

Choose a reason for hiding this comment

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

Well spotted!

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

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.

@@ -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.
Copy link
Owner

Choose a reason for hiding this comment

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

This should go to ssrR.v.

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.
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 could be shorter by using ltR0n

@affeldt-aist
Copy link
Owner

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!

@t6s
Copy link
Collaborator Author

t6s commented Oct 21, 2021

I have noticed that this change imports the axiom of choice in proba.v, which I expect cause some controversy.
I am now changing my mind to define the ring structure in a separate file and let a user import it when needed.

@hoheinzollern
Copy link
Collaborator

This is useful to have in robustmean, could you revive this and put it in the next release?

@t6s
Copy link
Collaborator Author

t6s commented Dec 5, 2023

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,
since completing it will require some experiments to settle some design choices.

Uses in robustmean will help this process, and so I suggest using a development branch for a while, not waiting for a release.

@t6s
Copy link
Collaborator Author

t6s commented Dec 5, 2023

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

@affeldt-aist
Copy link
Owner

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).
Once this is done in a branch of infotheo, we just need to compile against this branch.

@affeldt-aist
Copy link
Owner

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).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants