[Merged by Bors] - feat: MeasureTheory.Integral.Bochner: integral_fintype and similar #6446
Conversation
nomeata
force-pushed
the
joachim/integral_fintype
branch
from
058f1cb
to
9ad7fc5
Compare
nomeata
added
awaiting-review
t-measure-probability
|
The motivation of the present PR is to be able to do #6454 |
|
I’ll be traveling without a laptop for week, and will address review comments afterwards. Should anyone want to adopt this PR and see it through, that’s fine with me as well. |
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
|
@RemyDegenne, what is your preferred etiquette: Should I re-request a review from you after addressing your initial one? |
|
Usually I would simply have seen that you had pushed modifications to the branch and I would have come back to this PR without you needing to ping me, but I was on vacation recently and I lost track of those reviews. Sorry about the long delay. I'll review it shortly. |
leanprover-community-mathlib4-bot
added
ready-to-merge
|
Sorry, typo: |
|
✌️ nomeata can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Canceled. |
Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
|
bors r+ |
…6446) This adds some lemmas about `integral` where we already have the corresponding lemmas for `lintegral`. The goal is `integral_fintype`, which rewrites an integral over a finite type as a finite sum over the elements, with singleton measures (these singleton measures can then further be simplified when the measure comes from a `Pmf`, but that will follow some other time.). Also fixes lemma name `integral_eq_lintegral_pos_part_sub_lintegral_neg_part` in the module comments.
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
bors
bot
changed the title
This adds some lemmas about
integralwhere we already have the correspondinglemmas for
lintegral. The goal isintegral_fintype, which rewrites anintegral over a finite type as a finite sum over the elements, with singleton
measures (these singleton measures can then further be simplified when the
measure comes from a
Pmf, but that will follow some other time.).Also fixes lemma name
integral_eq_lintegral_pos_part_sub_lintegral_neg_partinthe module comments.