Commit 2021-09-20 13:42 3703ab2a

View on Github →

chore(data/real/pi): split into three files (#9295) This is the last file to finish compilation in mathlib, and it naturally splits into three chunks, two of which have simpler dependencies.

Estimated changes

Modified src/analysis/special_functions/trigonometric.lean

Deleted src/data/real/pi.lean

deleted theorem real.integral_sin_pow_div_tendsto_one

deleted theorem real.pi_gt_3141592

deleted theorem real.pi_gt_31415

deleted theorem real.pi_gt_314

deleted theorem real.pi_gt_sqrt_two_add_series

deleted theorem real.pi_gt_three

deleted theorem real.pi_lower_bound_start

deleted theorem real.pi_lt_3141593

deleted theorem real.pi_lt_31416

deleted theorem real.pi_lt_315

deleted theorem real.pi_lt_sqrt_two_add_series

deleted theorem real.pi_upper_bound_start

deleted theorem real.sqrt_two_add_series_step_down

deleted theorem real.sqrt_two_add_series_step_up

deleted theorem real.tendsto_prod_pi_div_two

deleted theorem real.tendsto_sum_pi_div_four

Created src/data/real/pi/bounds.lean

added theorem real.pi_gt_3141592

added theorem real.pi_gt_31415

added theorem real.pi_gt_314

added theorem real.pi_gt_sqrt_two_add_series

added theorem real.pi_gt_three

added theorem real.pi_lower_bound_start

added theorem real.pi_lt_3141593

added theorem real.pi_lt_31416

added theorem real.pi_lt_315

added theorem real.pi_lt_sqrt_two_add_series

added theorem real.pi_upper_bound_start

added theorem real.sqrt_two_add_series_step_down

added theorem real.sqrt_two_add_series_step_up

Created src/data/real/pi/leibniz.lean

added theorem real.tendsto_sum_pi_div_four

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

added theorem real.integral_sin_pow_div_tendsto_one

added theorem real.tendsto_prod_pi_div_two