Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-30 05:32 c7dd27d7

View on Github →

split(analysis/convex/jensen): split Jensen's inequalities off analysis.convex.function (#9445)

Estimated changes

Modified src/analysis/convex/function.lean

deleted theorem concave_on.exists_le_of_center_mass

deleted theorem concave_on.exists_le_of_mem_convex_hull

deleted theorem concave_on.le_map_center_mass

deleted theorem concave_on.le_map_sum

deleted theorem convex_on.exists_ge_of_center_mass

deleted theorem convex_on.exists_ge_of_mem_convex_hull

deleted theorem convex_on.map_center_mass_le

deleted theorem convex_on.map_sum_le

Created src/analysis/convex/jensen.lean

added theorem concave_on.exists_le_of_center_mass

added theorem concave_on.exists_le_of_mem_convex_hull

added theorem concave_on.le_map_center_mass

added theorem concave_on.le_map_sum

added theorem convex_on.exists_ge_of_center_mass

added theorem convex_on.exists_ge_of_mem_convex_hull

added theorem convex_on.map_center_mass_le

added theorem convex_on.map_sum_le

Modified src/analysis/convex/topology.lean