feat(measure_theory/bochner_integration): linearity of the Bochner Integral

[aceg00]

This PR proves integral_zero integral_add integral_sub and integral_smul,

TO CONTRIBUTORS:

Make sure you have:

• reviewed and applied the coding style: coding, naming
• reviewed and applied the documentation requirements
• for tactics:
  • added or adapted documentation in tactics.md
  • write an example of use of the new feature in tactics.lean
• make sure definitions and lemmas are put in the right files
• make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

[sgouezel]

I imagine it would be a good idea to make integral irreducible at the end of this file, once the API is set up: otherwise, whenever Lean will see an integral (which will happen in a lot of different places), it might try to unfold everything all the way down to the uniform extension of a continuous linear map defined on the space of simple functions, and it might slow down things a bit. What do you think?

[sgouezel]

I know that Johan has requested simp attributes, but I am not so sure about this: I imagine that we will have complicated integrals and that we will want to make simplifications in the integrand. Splitting the integral into many integrals seems to go in the opposite direction -- it might be useful sometimes, especially when there is a formula for the integral of some part of the integrand, but not always. @jcommelin, what do you think?

[jcommelin]

@sgouezel Fair enough, that's a good point. So how about make the integrand-simp-lemmas high priority, and the ones in this PR low priority? Or maybe put these lemmas in a special simp-set, that doesn't get used by default. I think I like that best. It's better to err on the safe side (-;

[sgouezel]

Yes, a specific simp set is a good idea. Simp priorities don't work very well, as they only play a role when there are two lemmas to be applied at the same stage, but a low priority lemma can be applied earlier, deeper in the expression.

[aceg00]

How do I put lemmas into a simp-set?

[PatrickMassot]

See the very end of https://leanprover.github.io/theorem_proving_in_lean/tactics.html#using-the-simplifier