Commit 2023-06-08 19:16 840194b6

View on Github →

feat: port Analysis.SpecialFunctions.Integrals (#4860)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/SpecialFunctions/Integrals.lean

added theorem IntervalIntegrable.log

added theorem integral_const_on_unit_interval

added theorem integral_cos

added theorem integral_cos_mul_complex

added theorem integral_cos_pow

added theorem integral_cos_pow_aux

added theorem integral_cos_pow_three

added theorem integral_cos_sq

added theorem integral_cos_sq_sub_sin_sq

added theorem integral_cpow

added theorem integral_exp

added theorem integral_exp_mul_complex

added theorem integral_id

added theorem integral_inv

added theorem integral_inv_of_neg

added theorem integral_inv_of_pos

added theorem integral_inv_one_add_sq

added theorem integral_log

added theorem integral_log_of_neg

added theorem integral_log_of_pos

added theorem integral_mul_cpow_one_add_sq

added theorem integral_mul_rpow_one_add_sq

added theorem integral_one

added theorem integral_one_div

added theorem integral_one_div_of_neg

added theorem integral_one_div_of_pos

added theorem integral_one_div_one_add_sq

added theorem integral_pow

added theorem integral_pow_abs_sub_uIoc

added theorem integral_rpow

added theorem integral_sin

added theorem integral_sin_mul_cos_sq

added theorem integral_sin_mul_cos₁

added theorem integral_sin_mul_cos₂

added theorem integral_sin_pow

added theorem integral_sin_pow_antitone

added theorem integral_sin_pow_aux

added theorem integral_sin_pow_even

added theorem integral_sin_pow_even_mul_cos_pow_even

added theorem integral_sin_pow_mul_cos_pow_odd

added theorem integral_sin_pow_odd

added theorem integral_sin_pow_odd_mul_cos_pow

added theorem integral_sin_pow_pos

added theorem integral_sin_pow_succ_le

added theorem integral_sin_pow_three

added theorem integral_sin_sq

added theorem integral_sin_sq_mul_cos

added theorem integral_sin_sq_mul_cos_sq

added theorem integral_zpow

added theorem intervalIntegral.intervalIntegrable_const

added theorem intervalIntegral.intervalIntegrable_cos

added theorem intervalIntegral.intervalIntegrable_cpow'

added theorem intervalIntegral.intervalIntegrable_cpow

added theorem intervalIntegral.intervalIntegrable_exp

added theorem intervalIntegral.intervalIntegrable_id

added theorem intervalIntegral.intervalIntegrable_inv

added theorem intervalIntegral.intervalIntegrable_inv_one_add_sq

added theorem intervalIntegral.intervalIntegrable_log

added theorem intervalIntegral.intervalIntegrable_one_div

added theorem intervalIntegral.intervalIntegrable_one_div_one_add_sq

added theorem intervalIntegral.intervalIntegrable_pow

added theorem intervalIntegral.intervalIntegrable_rpow'

added theorem intervalIntegral.intervalIntegrable_rpow

added theorem intervalIntegral.intervalIntegrable_sin

added theorem intervalIntegral.intervalIntegrable_zpow

added theorem intervalIntegral.inv_mul_integral_comp_add_div

added theorem intervalIntegral.inv_mul_integral_comp_div

added theorem intervalIntegral.inv_mul_integral_comp_div_add

added theorem intervalIntegral.inv_mul_integral_comp_div_sub

added theorem intervalIntegral.inv_mul_integral_comp_sub_div

added theorem intervalIntegral.mul_integral_comp_add_mul

added theorem intervalIntegral.mul_integral_comp_mul_add

added theorem intervalIntegral.mul_integral_comp_mul_left

added theorem intervalIntegral.mul_integral_comp_mul_right

added theorem intervalIntegral.mul_integral_comp_mul_sub

added theorem intervalIntegral.mul_integral_comp_sub_mul