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

Probability #516

Merged
merged 17 commits into from
Apr 14, 2023
Merged

Probability #516

merged 17 commits into from
Apr 14, 2023

Conversation

affeldt-aist
Copy link
Member

@affeldt-aist affeldt-aist commented Jan 17, 2022

Tentative definition of expectation, discrete random variables, and a few basic lemmas about probability.

@affeldt-aist affeldt-aist changed the base branch from master to simple_function January 17, 2022 09:33
@affeldt-aist affeldt-aist marked this pull request as draft January 20, 2022 03:47
@affeldt-aist affeldt-aist changed the base branch from simple_function to lebesgue_measure February 16, 2022 09:39
@affeldt-aist affeldt-aist force-pushed the probability branch 3 times, most recently from 932adeb to ef65b12 Compare March 10, 2022 08:02
@affeldt-aist affeldt-aist changed the base branch from lebesgue_measure to master April 4, 2022 09:59
@affeldt-aist affeldt-aist force-pushed the probability branch 2 times, most recently from 9c6172a to 4c25cda Compare August 9, 2022 08:07
@affeldt-aist affeldt-aist marked this pull request as ready for review August 9, 2022 08:07
@affeldt-aist affeldt-aist requested a review from t6s August 9, 2022 08:07
@affeldt-aist affeldt-aist mentioned this pull request Aug 26, 2022
2 tasks
@affeldt-aist affeldt-aist force-pushed the probability branch 5 times, most recently from bb6bc24 to fcbf458 Compare September 8, 2022 01:44
@affeldt-aist affeldt-aist force-pushed the probability branch 2 times, most recently from 5724d89 to 896ae2f Compare January 12, 2023 10:23
@affeldt-aist
Copy link
Member Author

(In particular, expectation_le should be AE and Lspace should be quotiented.)

The last commits (kind of) address these two issues.

@affeldt-aist affeldt-aist force-pushed the probability branch 2 times, most recently from c9140fa to 1377f94 Compare April 10, 2023 09:56
@affeldt-aist
Copy link
Member Author

What is left to do with this PR is to make sure that the coercion LfunType_of_LType of Lp spaces works as intended. This might amount to transport correctly the eq_quot structure of LspaceType to LType which I haven't figured out yet.

@affeldt-aist
Copy link
Member Author

What is left to do with this PR is to make sure that the coercion LfunType_of_LType of Lp spaces works as intended. This might amount to transport correctly the eq_quot structure of LspaceType to LType which I haven't figured out yet.

I have therefore removed the Lp-spaces for the time being and will merge only the basic definitions.

@affeldt-aist affeldt-aist added the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Apr 14, 2023
@affeldt-aist affeldt-aist merged commit 59b23e0 into master Apr 14, 2023
affeldt-aist added a commit that referenced this pull request Apr 15, 2023
* first take at probability theory

Co-authored-by: Takafumi Saikawa <[email protected]>
Co-authored-by: Alessandro Bruni <[email protected]>
Co-authored-by: Pierre Roux <[email protected]>
@proux01 proux01 removed the TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done. label Apr 29, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement ✨ This issue/PR is about adding new features enhancing the library
Projects
None yet
Development

Successfully merging this pull request may close these issues.

6 participants