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

[Merged by Bors] - feat(probability/strong_law): Lp version of the strong law of large numbers #15392

Closed
wants to merge 16 commits into from

Conversation

JasonKYi
Copy link
Member

@JasonKYi JasonKYi commented Jul 15, 2022

This PR proves the Lp version of the strong law of large numbers which states that $\frac{1}{n}\sum_{i < n} X_i$ converges to $\mathbb{E}[X_0]$ in the Lp-norm where $(X_n)$ is iid. and Lp.


Open in Gitpod

@JasonKYi JasonKYi added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jul 15, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 15, 2022
@fpvandoorn fpvandoorn requested a review from sgouezel July 19, 2022 17:08
@sgouezel
Copy link
Collaborator

I disagree that it needs more measurability than the almost sure version: ae measurability is clearly enough for the statement to be true -- you can deduce it from the version where you add measurability, by doing modifications on a measure 0 set, but I'd rather see a direct proof if possible (should be change the definition of uniform integrability to replace strongly_measurable with ae_strongly_measurable? I'd say yes, probably).

@JasonKYi JasonKYi added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 22, 2022
@JasonKYi
Copy link
Member Author

should be change the definition of uniform integrability to replace strongly_measurable with ae_strongly_measurable? I'd say yes, probably.

I've opened #15623 for this

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 22, 2022
bors bot pushed a commit that referenced this pull request Jul 25, 2022
…_integrable` to only require `ae_strongly_measurable` (#15623)


The L¹ version of the strong LLN does not require `strongly_measurable` but the assumption in `uniform_integrable` forces it to have this condition if not requiring an extra step to relax the condition (see #15392). This PR relaxes the definition of `uniform_integrable` so it only requires `ae_strongly_measurable`.
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 25, 2022
@JasonKYi JasonKYi added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 26, 2022
src/probability/ident_distrib.lean Outdated Show resolved Hide resolved
src/probability/ident_distrib.lean Outdated Show resolved Hide resolved
src/probability/strong_law.lean Outdated Show resolved Hide resolved
src/probability/ident_distrib.lean Outdated Show resolved Hide resolved
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 26, 2022
@JasonKYi JasonKYi added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 27, 2022
@JasonKYi JasonKYi changed the title feat(probability/strong_law): L1 version of the strong law of large numbers feat(probability/strong_law): Lp version of the strong law of large numbers Jul 27, 2022
Copy link
Collaborator

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

LGTM, thanks!
bors d+

src/probability/ident_distrib.lean Outdated Show resolved Hide resolved
src/probability/ident_distrib.lean Outdated Show resolved Hide resolved
src/probability/strong_law.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Jul 28, 2022

✌️ JasonKYi can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jul 28, 2022
JasonKYi and others added 2 commits July 28, 2022 20:40
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
@JasonKYi
Copy link
Member Author

Thanks for the reviews!
bors r+

bors bot pushed a commit that referenced this pull request Jul 28, 2022
…umbers (#15392)

This PR proves the Lp version of the strong law of large numbers which states that $\frac{1}{n}\sum_{i < n} X_i$ converges to $\mathbb{E}[X_0]$ in the Lp-norm where $(X_n)$ is iid. and Lp.
@bors
Copy link

bors bot commented Jul 28, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(probability/strong_law): Lp version of the strong law of large numbers [Merged by Bors] - feat(probability/strong_law): Lp version of the strong law of large numbers Jul 28, 2022
@bors bors bot closed this Jul 28, 2022
@bors bors bot deleted the JasonKYi/strong_law_L1 branch July 28, 2022 21:09
bottine pushed a commit to bottine/mathlib that referenced this pull request Jul 30, 2022
…_integrable` to only require `ae_strongly_measurable` (leanprover-community#15623)


The L¹ version of the strong LLN does not require `strongly_measurable` but the assumption in `uniform_integrable` forces it to have this condition if not requiring an extra step to relax the condition (see leanprover-community#15392). This PR relaxes the definition of `uniform_integrable` so it only requires `ae_strongly_measurable`.
bottine pushed a commit to bottine/mathlib that referenced this pull request Jul 30, 2022
…umbers (leanprover-community#15392)

This PR proves the Lp version of the strong law of large numbers which states that $\frac{1}{n}\sum_{i < n} X_i$ converges to $\mathbb{E}[X_0]$ in the Lp-norm where $(X_n)$ is iid. and Lp.
robertylewis pushed a commit that referenced this pull request Aug 2, 2022
…_integrable` to only require `ae_strongly_measurable` (#15623)


The L¹ version of the strong LLN does not require `strongly_measurable` but the assumption in `uniform_integrable` forces it to have this condition if not requiring an extra step to relax the condition (see #15392). This PR relaxes the definition of `uniform_integrable` so it only requires `ae_strongly_measurable`.
robertylewis pushed a commit that referenced this pull request Aug 2, 2022
…umbers (#15392)

This PR proves the Lp version of the strong law of large numbers which states that $\frac{1}{n}\sum_{i < n} X_i$ converges to $\mathbb{E}[X_0]$ in the Lp-norm where $(X_n)$ is iid. and Lp.
khwilson pushed a commit that referenced this pull request Aug 2, 2022
…_integrable` to only require `ae_strongly_measurable` (#15623)


The L¹ version of the strong LLN does not require `strongly_measurable` but the assumption in `uniform_integrable` forces it to have this condition if not requiring an extra step to relax the condition (see #15392). This PR relaxes the definition of `uniform_integrable` so it only requires `ae_strongly_measurable`.
khwilson pushed a commit that referenced this pull request Aug 2, 2022
…umbers (#15392)

This PR proves the Lp version of the strong law of large numbers which states that $\frac{1}{n}\sum_{i < n} X_i$ converges to $\mathbb{E}[X_0]$ in the Lp-norm where $(X_n)$ is iid. and Lp.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

4 participants