Commit 2020-05-11 09:42 e777d0b4

View on Github →

refactor(data/real/pi): add tactics for pi computation (#2641) Depends on #2589. Moves pi bounds from @fpvandoorn's gist to mathlib, and also adds a small tactic to uniformize the proofs (and also skip some unsqueezed proofs), making the compilation even faster (just around 1 second for the longest proofs).

Estimated changes

Modified src/data/real/pi.lean

added theorem real.pi_gt_3141592

added theorem real.pi_gt_31415

modified theorem real.pi_gt_314

modified theorem real.pi_gt_three

added theorem real.pi_lower_bound_start

added theorem real.pi_lt_3141593

added theorem real.pi_lt_31416

modified theorem real.pi_lt_315

added theorem real.pi_upper_bound_start

modified theorem real.sqrt_two_add_series_step_down

modified theorem real.sqrt_two_add_series_step_up