Commit 2023-01-26 09:46 9b94375a

View on Github →

feat(data/real/pi): refactor Wallis formula for pi (#18280) This is preparation for adding Euler's sine product (whose proof is a generalisation of the proof of Wallis' formula)

Estimated changes

Modified src/analysis/special_functions/stirling.lean

deleted theorem stirling.tendsto_w_at_top:

Modified src/data/real/pi/wallis.lean

added theorem integral_sin_pow_even_le

added theorem integral_sin_pow_le

added theorem integral_sin_pow_odd_le

added theorem le_integral_sin_pow

deleted theorem real.integral_sin_pow_div_tendsto_one

modified theorem real.tendsto_prod_pi_div_two

added theorem real.wallis.W_eq_factorial_ratio

added theorem real.wallis.W_eq_integral_sin_pow_div_integral_sin_pow

added theorem real.wallis.W_eq_mul_sq

added theorem real.wallis.W_le

added theorem real.wallis.W_pos

added theorem real.wallis.W_succ

added theorem real.wallis.integral_sin_pow_even_sq_eq

added theorem real.wallis.integral_sin_pow_odd_sq_eq

added theorem real.wallis.le_W

added theorem real.wallis.tendsto_W_nhds_pi_div_two