Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-09 15:38 48f557d5

View on Github →

chore(analysis/convex/integral): use variables (#14592)

Move some implicit arguments to variables.
Move ae_eq_const_or_exists_average_ne_compl to the root namespace.
Add ae_eq_const_or_norm_set_integral_lt_of_norm_le_const.

Estimated changes

Modified src/analysis/convex/integral.lean

added theorem ae_eq_const_or_exists_average_ne_compl

added theorem ae_eq_const_or_norm_set_integral_lt_of_norm_le_const

modified theorem concave_on.average_mem_hypograph

modified theorem concave_on.le_map_average

modified theorem concave_on.le_map_integral

modified theorem concave_on.le_map_set_average

modified theorem concave_on.set_average_mem_hypograph

modified theorem convex.average_mem

modified theorem convex.average_mem_interior_of_set

modified theorem convex.integral_mem

modified theorem convex.set_average_mem

modified theorem convex.set_average_mem_closure

modified theorem convex_on.average_mem_epigraph

modified theorem convex_on.map_average_le

modified theorem convex_on.map_integral_le

modified theorem convex_on.map_set_average_le

modified theorem convex_on.set_average_mem_epigraph

deleted theorem measure_theory.integrable.ae_eq_const_or_exists_average_ne_compl

modified theorem strict_concave_on.ae_eq_const_or_lt_map_average

modified theorem strict_convex.ae_eq_const_or_average_mem_interior

modified theorem strict_convex_on.ae_eq_const_or_map_average_lt