Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-01 07:41 980755c3

View on Github →

feat(analysis/special_functions/trigonometric): Euler's infinite product for sine (part b) (#18281)

Estimated changes

Modified src/analysis/special_functions/trigonometric/euler_sine_prod.lean

added theorem complex.tendsto_euler_sin_prod

added theorem euler_sine.tendsto_integral_cos_pow_mul_div

added theorem real.tendsto_euler_sin_prod

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

deleted theorem integral_sin_pow_even_le

deleted theorem integral_sin_pow_le

deleted theorem integral_sin_pow_odd_le

deleted theorem le_integral_sin_pow

deleted theorem real.wallis.W_eq_mul_sq

deleted theorem real.wallis.integral_sin_pow_even_sq_eq

deleted theorem real.wallis.integral_sin_pow_odd_sq_eq