Commit 2021-10-16 18:01 3fe67d65

View on Github →

feat(analysis/special_functions/integrals): integral of |x - a| ^ n over Ι a b (#9752) Also use notation for interval a b and interval_oc a b.

Estimated changes

Modified src/analysis/special_functions/integrals.lean

modified theorem integral_inv

modified theorem integral_log

modified theorem integral_one_div

added theorem integral_pow_abs_sub_interval_oc

modified theorem interval_integral.interval_integrable_inv

modified theorem interval_integral.interval_integrable_log

modified theorem interval_integral.interval_integrable_one_div