average): define `measure_theory.average` (#12128)

Commit

3 years ago

feat(measure_theory/integral/average): define `measure_theory.average` (#12128) And use it to formulate Jensen's inequality. Also add Jensen's inequality for concave functions.

Author

urkud

Parents

f3ee4628

mathlib3 f6a7ad9e - feat(measure_theory/integral/average): define `measure_theory.average` (#12128)

mathlib3
f6a7ad9e - feat(measure_theory/integral/average): define `measure_theory.average` (#12128)