Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-27 00:33 5c957ec8

View on Github →

feat(analysis/convex/integral): Jensen's inequality for integrals (#4225)

Estimated changes

Created src/analysis/convex/integral.lean

added theorem convex.integral_mem

added theorem convex.smul_integral_mem

added theorem convex_on.map_integral_le

added theorem convex_on.map_smul_integral_le

Modified src/analysis/normed_space/basic.lean

added theorem prod.nnnorm_def

Modified src/measure_theory/integration.lean

added theorem measure_theory.simple_func.sum_range_measure_preimage_singleton

Modified src/measure_theory/l1_space.lean

added theorem measure_theory.integrable.prod_mk

Modified src/measure_theory/measure_space.lean

added theorem measure_theory.probability_measure.ne_zero

Modified src/measure_theory/set_integral.lean

added theorem fst_integral

added theorem integral_pair

added theorem snd_integral