Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-12-16 10:20 de25b101

View on Github →

refactor(analysis/convex): simplify proofs, use implicit args and dot notation (#1804)

  • feat(data/set/intervals): add nonempty_Icc etc, image_(add/mul)_(left/right)_Icc
  • refactor(analysis/convex): simplify proofs, use implicit args and dot notation
  • Use dot notation.
  • Swap LHS and RHS of image_Icc_zero_one_eq_segment.
  • Introduce finset.center_mass, prove basic properties.
  • Deduce Jensen's inequality from the corresponding property of convex sets; rename corresponding lemmas.
  • Fix a typo Co-Authored-By: sgouezel sebastien.gouezel@univ-rennes1.fr
  • Update src/analysis/convex.lean

Estimated changes

added theorem finset.prod_pair
added theorem convex.add
added theorem convex.affinity
added theorem convex.center_mass_mem
added theorem convex.closure
added theorem convex.inter
added theorem convex.interior
added theorem convex.is_linear_image
added theorem convex.linear_image
added theorem convex.linear_preimage
added theorem convex.neg
added theorem convex.neg_preimage
added theorem convex.prod
added theorem convex.smul
added theorem convex.smul_preimage
added theorem convex.sub
added theorem convex.sum_mem
added theorem convex.translate
modified theorem convex_Inter
deleted theorem convex_add
deleted theorem convex_affinity
deleted theorem convex_closure
deleted theorem convex_halfplane
modified theorem convex_halfspace_ge
modified theorem convex_halfspace_gt
modified theorem convex_halfspace_le
modified theorem convex_halfspace_lt
added theorem convex_hyperplane
added theorem convex_iff_sum_mem
deleted theorem convex_inter
deleted theorem convex_interior
deleted theorem convex_le_of_convex_on
deleted theorem convex_linear_image'
deleted theorem convex_linear_image
deleted theorem convex_linear_preimage'
deleted theorem convex_linear_preimage
deleted theorem convex_lt_of_convex_on
deleted theorem convex_neg
deleted theorem convex_neg_preimage
added theorem convex_on.add
added theorem convex_on.convex_le
added theorem convex_on.convex_lt
added theorem convex_on.map_sum_le
added theorem convex_on.smul
added theorem convex_on.subset
deleted theorem convex_on_add
modified theorem convex_on_linorder
deleted theorem convex_on_smul
deleted theorem convex_on_subset
deleted theorem convex_on_sum
deleted theorem convex_prod
added theorem convex_real_iff
added theorem convex_sInter
deleted theorem convex_smul
deleted theorem convex_smul_preimage
deleted theorem convex_sub
deleted theorem convex_submodule
deleted theorem convex_subspace
deleted theorem convex_sum
deleted theorem convex_sum_iff
deleted theorem convex_translation
modified theorem left_mem_segment
modified theorem right_mem_segment
modified def segment
added theorem segment_eq_Icc'
modified theorem segment_translate
added theorem submodule.convex
added theorem subspace.convex