Commit 2022-07-05 10:10 676e7725

View on Github →

refactor(analysis/convex/specific_functions): Remove hypothesis from deriv_sqrt_mul_log (#15015) This PR removes the hx : 0 < x hypothesis from deriv_sqrt_mul_log.

Estimated changes

Modified src/analysis/calculus/deriv.lean

added theorem has_deriv_within_at.congr_of_mem

added theorem has_deriv_within_at.deriv_eq_zero

Modified src/analysis/convex/specific_functions.lean

modified theorem deriv2_sqrt_mul_log

added theorem deriv_sqrt_mul_log'

modified theorem deriv_sqrt_mul_log

added theorem has_deriv_at_sqrt_mul_log

Modified src/topology/continuous_on.lean

added theorem eventually_mem_nhds_within