Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-19 22:17 eba4829b

View on Github →

feat(data/real/pi): Wallis product for pi (#6568)

Estimated changes

Modified src/analysis/special_functions/integrals.lean

deleted theorem integral_cos

deleted theorem integral_exp

deleted theorem integral_id

deleted theorem integral_inv

deleted theorem integral_inv_of_neg

deleted theorem integral_inv_of_pos

deleted theorem integral_inv_one_add_sq

deleted theorem integral_one

deleted theorem integral_one_div

deleted theorem integral_one_div_of_neg

deleted theorem integral_one_div_of_pos

deleted theorem integral_one_div_one_add_sq

deleted theorem integral_pow

deleted theorem integral_sin

added theorem interval_integral.integral_cos

added theorem interval_integral.integral_exp

added theorem interval_integral.integral_id

added theorem interval_integral.integral_inv

added theorem interval_integral.integral_inv_of_neg

added theorem interval_integral.integral_inv_of_pos

added theorem interval_integral.integral_inv_one_add_sq

added theorem interval_integral.integral_one

added theorem interval_integral.integral_one_div

added theorem interval_integral.integral_one_div_of_neg

added theorem interval_integral.integral_one_div_of_pos

added theorem interval_integral.integral_one_div_one_add_sq

added theorem interval_integral.integral_pow

added theorem interval_integral.integral_sin

added theorem interval_integral.integral_sin_pow_aux

added theorem interval_integral.integral_sin_pow_even

added theorem interval_integral.integral_sin_pow_odd

added theorem interval_integral.integral_sin_pow_pos

added theorem interval_integral.integral_sin_pow_succ_succ

Modified src/data/real/pi.lean

added theorem real.integral_sin_pow_antimono

added theorem real.integral_sin_pow_div_tendsto_one

added theorem real.tendsto_prod_pi_div_two