Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-05-18 13:54 8f9fea08

View on Github →

refactor(analysis/convex/specific_functions): split (#19031) Split analysis/convex/specific_function into a part which doesn't require differentiation (as of #19026) and a part which does. This removes the dependence of measure_theory/integral/bochner on differentiation, and decreases by 11 the length of the longest path in mathlib. See Zulip

Estimated changes

deleted theorem deriv2_sqrt_mul_log
deleted theorem deriv_sqrt_mul_log'
deleted theorem deriv_sqrt_mul_log
deleted theorem even.strict_convex_on_pow
deleted theorem has_deriv_at_sqrt_mul_log
deleted theorem int_prod_range_nonneg
deleted theorem int_prod_range_pos
deleted theorem strict_concave_on_cos_Icc
deleted theorem strict_concave_on_sin_Icc
deleted theorem strict_convex_on_pow
deleted theorem strict_convex_on_zpow
added theorem deriv2_sqrt_mul_log
added theorem deriv_sqrt_mul_log'
added theorem deriv_sqrt_mul_log
added theorem int_prod_range_nonneg
added theorem int_prod_range_pos
added theorem strict_convex_on_pow
added theorem strict_convex_on_zpow