pi2_error.lean

import data.real.pi

set_option profiler true

set_option timeout 1000000
namespace real
-- the following lemma takes about 9 seconds
lemma pi_gt_31415 : pi > 3.1415 :=
begin
  refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 6), rw [mul_comm],
  apply le_mul_of_div_le, norm_num, apply le_sqrt_of_sqr_le, 
  rw [le_sub, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
  apply sqrt_two_add_series_step_up 11482 8119,
  apply sqrt_two_add_series_step_up 5401 2923,
  apply sqrt_two_add_series_step_up 2348 1197,
  apply sqrt_two_add_series_step_up 11367 5711,
  apply sqrt_two_add_series_step_up 25705 12868,
  apply sqrt_two_add_series_step_up 23235 11621,
  all_goals {norm_num}
end

-- the following lemma takes about 14 seconds
lemma pi_lt_31416 : pi < 3.1416 :=
begin
  refine lt_of_lt_of_le (pi_lt_sqrt_two_add_series 9) _,
  apply add_le_of_le_sub_right, rw [mul_comm], apply mul_le_of_le_div, apply pow_pos, norm_num,
  rw [sqrt_le_left, sub_le, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
  apply sqrt_two_add_series_step_down 4756 3363,
  apply sqrt_two_add_series_step_down 101211 54775,
  apply sqrt_two_add_series_step_down 505534 257719,
  apply sqrt_two_add_series_step_down 83289 41846,
  apply sqrt_two_add_series_step_down 411278 205887,
  apply sqrt_two_add_series_step_down 438142 219137,
  apply sqrt_two_add_series_step_down 451504 225769,
  apply sqrt_two_add_series_step_down 265603 132804,
  apply sqrt_two_add_series_step_down 849938 424971,
  all_goals {norm_num}
end

-- the following lemma takes about 15 seconds
lemma pi_gt_3141592 : pi > 3.141592  :=
begin
  refine lt_of_le_of_lt _ (pi_gt_sqrt_two_add_series 10), rw [mul_comm],
  apply le_mul_of_div_le, norm_num, apply le_sqrt_of_sqr_le,
  rw [le_sub, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
  apply sqrt_two_add_series_step_up 11482 8119,
  apply sqrt_two_add_series_step_up 7792 4217,
  apply sqrt_two_add_series_step_up 54055 27557,
  apply sqrt_two_add_series_step_up 949247 476920,
  apply sqrt_two_add_series_step_up 3310126 1657059,
  apply sqrt_two_add_series_step_up 2635492 1318143,
  apply sqrt_two_add_series_step_up 1580265 790192,
  apply sqrt_two_add_series_step_up 1221775 610899,
  apply sqrt_two_add_series_step_up 3612247 1806132,
  apply sqrt_two_add_series_step_up 849943 424972,
  all_goals {norm_num}
end

-- the following lemma takes about 19 seconds
lemma pi_lt_3141593 : pi < 3.141593 :=
begin
  refine lt_of_lt_of_le (pi_lt_sqrt_two_add_series 11) _,
  apply add_le_of_le_sub_right, rw [mul_comm], apply mul_le_of_le_div, apply pow_pos, norm_num,
  rw [sqrt_le_left, sub_le, show (0:ℝ) = (0:ℕ)/(1:ℕ), by rw [nat.cast_zero, zero_div]],
  apply sqrt_two_add_series_step_down 27720 19601,
  apply sqrt_two_add_series_step_down 56935 30813,
  apply sqrt_two_add_series_step_down 49359 25163,
  apply sqrt_two_add_series_step_down 258754 130003,
  apply sqrt_two_add_series_step_down 113599 56868,
  apply sqrt_two_add_series_step_down 1101994 551163,
  apply sqrt_two_add_series_step_down 8671537 4336095,
  apply sqrt_two_add_series_step_down 3877807 1938940,
  apply sqrt_two_add_series_step_down 52483813 26242030,
  apply sqrt_two_add_series_step_down 56946167 28473117,
  apply sqrt_two_add_series_step_down 23798415 11899211,
  all_goals {norm_num},
end

end real