[Merged by Bors] - feat(MeasureTheory): integral is monotone/convex if the integrand is monotone/convex

[dupuisf]

This PR shows that the function fun b => ∫ x, f x b ∂μ is monotone/antitone/convex/concave whenever the integrand f x is monotone/antitone/convex/concave ae.

This will be needed to show that various functions are operator monotone or convex.

---

[github-actions]

PR summary 4b70dd6b74

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ Integrable.fun_smul
+ convex_iff_add_mem
+ integral_antitoneOn_of_integrand_ae
+ integral_concaveOn_of_integrand_ae
+ integral_convexOn_of_integrand_ae
+ integral_monotoneOn_of_integrand_ae

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[j-loreaux]

To make the fun_prop calls you need to add this variant next to Integrable.smul:

@[fun_prop]
theorem Integrable.fun_smul {α β : Type*} {m : MeasurableSpace α} {μ : Measure α}
    [NormedAddCommGroup β] {𝕜 : Type u_6} [NormedAddCommGroup 𝕜] [SMulZeroClass 𝕜 β]
    [IsBoundedSMul 𝕜 β] (c : 𝕜) {f : α → β} (hf : Integrable f μ) :
    Integrable (fun x ↦ c • f x) μ :=
  hf.smul c

bors d+

[mathlib-bors]

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

[dupuisf]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style