Commit 2021-06-04 19:29 8b5ff9ce

View on Github →

feat(analysis/special_functions/integrals): integral_log (#7732) The integral of the (real) logarithmic function over the interval [a, b], provided that 0 ∉ interval a b.

Estimated changes

Modified src/analysis/special_functions/integrals.lean

added theorem integral_log

added theorem integral_log_of_neg

added theorem integral_log_of_pos

Modified test/integration.lean