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

Probabilistic convergence #769

Draft
wants to merge 26 commits into
base: probability
Choose a base branch
from

Conversation

hoheinzollern
Copy link
Collaborator

@hoheinzollern hoheinzollern commented Oct 11, 2022

Motivation for this change

Introduces probabilistic convergence

Things done/to do
  • add weak law of large numbers
  • prove Markov's and Chebyshev's inequality
  • check proofs for probabilistic convergence

Co-authors: @affeldt-aist @t6s

@zstone1
Copy link
Contributor

zstone1 commented Oct 11, 2022

I'm very happy to see more specialized convergences. I will propose an alternate approach: to build a topology on {RV P >-> R} that induces this convergence. This is the approach I took for relating uniform, pointwise, and compact convergence on function spaces in topology.v, and I think it turned out pretty well.

The benefit of the approach is access to the wealth of general topology lemmas and notations. For example, you need a topology to even state that "expected value is continuous from {RV P >-> R} to R". The main downside of the approach is it takes extra effort, and sometimes the topologies are arcane (in this case it appears to be a simple metric, not too bad). I see three options
A. Define the convergence as above, and prove it's backed by a topology
B. Define the topology, and prove the above property as a lemma
C. Not build underlying topology at all (you never actually need it to prove law of large numbers, CLT, etc).

To be concrete, wikipedia claims the metric d(x,y) := E(min(x => |X(x) - Y(x)|, 1) induces "convergence in probability". Also according to wikipedia, the "vague topology" should induce "convergence in distribution".

@zstone1
Copy link
Contributor

zstone1 commented Oct 12, 2022

As an aside, today I was quite surprised to learn that "almost everywhere convergence" is not topological. So while it looks like we could define a "filteredType" for it, we certainly cannot define a topologicalType for it.

@affeldt-aist affeldt-aist marked this pull request as draft October 20, 2022 10:21
@affeldt-aist affeldt-aist mentioned this pull request Oct 28, 2022
2 tasks
@t6s
Copy link
Member

t6s commented Nov 17, 2022

As an aside, today I was quite surprised to learn that "almost everywhere convergence" is not topological. So while it looks like we could define a "filteredType" for it, we certainly cannot define a topologicalType for it.

The notion of convergence spaces might be useful?
https://ncatlab.org/nlab/show/convergence+space

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>
Co-authored-by: Alessandro Bruni <alessandro.bruni@gmail.com>
hoheinzollern and others added 2 commits December 1, 2022 08:31
Lemma expectation_le

Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>
Co-authored-by: Reynald Affeldt <reynald.affeldt@aist.go.jp>
@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

affeldt-aist commented Jan 12, 2023

@hoheinzollern I have updated PR #516 so that we should be able to rebase and only keep the Section cvg_random_variable.

affeldt-aist and others added 5 commits March 17, 2023 15:58
Co-authored-by: Takafumi Saikawa <tscompor@gmail.com>
Co-authored-by: Alessandro Bruni <alessandro.bruni@gmail.com>
@affeldt-aist affeldt-aist force-pushed the probability branch 3 times, most recently from 1377f94 to 06adee5 Compare April 14, 2023 08:35
@affeldt-aist
Copy link
Member

@hoheinzollern I have updated PR #516 so that we should be able to rebase and only keep the Section cvg_random_variable.

This might be still worth doing it, though after one year a copy-paste might be more effective than a rebase.

@proux01 proux01 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 Jan 25, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
TODO: MC2 port This PR must be ported to mathcomp 2 now that the. Remove this label when the port is done.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

5 participants