Commit 2023-08-24 13:32 7bd54f65

feat: MeasureTheory.Integral.Bochner: integral_fintype and similar (#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.