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.

Sign up for GitHub

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

Jump to bottom

Weaken measurability assumptions in `Probability/Moments` #20367

Open

Vilin97 opened this issue Dec 31, 2024 · 1 comment

Collaborator

Vilin97 commented Dec 31, 2024

Weaken measurability assumptions from Measurable to AEMeasurable in iIndepFun.mgf_sum and other theorems.

https://github.com/leanprover-community/mathlib4/pull/19886/files/9d4de646114bf5ea72f2020b96bc2c57eff77460#diff-9baadefbb1a705ec3c606ff4bcdb8c4d2888985c99ee05eefc987312770ecbaeR265

Suggested by @YaelDillies.

The text was updated successfully, but these errors were encountered:

Vilin97 mentioned this issue

[Merged by Bors] - feat(Probability/Moments): add lemmas about moment generating functions #19886

Closed

Collaborator Author

Vilin97 commented Dec 31, 2024

@YaelDillies started on this branch: https://github.com/leanprover-community/mathlib4/tree/mgf_sum_ae_measurable

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment