Skip to content

Instantly share code, notes, and snippets.

@fpvandoorn

fpvandoorn/pi2.lean

Created Mar 19, 2019
Embed
What would you like to do?
import data.real.pi
set_option profiler true
namespace real
lemma sqrt_two_add_series_step_up' {x z : ℝ} {n : ℕ} (y : ℝ) (hz : sqrt_two_add_series y n ≤ z)
(h : 2 + x ≤ y ^ 2) (h2 : 0 ≤ y) : sqrt_two_add_series x (n+1) ≤ z :=
begin
refine le_trans _ hz, rw [sqrt_two_add_series_succ], apply sqrt_two_add_series_monotone_left,
rw [sqrt_le_left], exact h, exact h2
end
lemma sqrt_two_add_series_step_down' {x z : ℝ} {n : ℕ} (y : ℝ) (hz : z ≤ sqrt_two_add_series y n)
(h : y ^ 22 + x) : z ≤ sqrt_two_add_series x (n+1) :=
begin
apply le_trans hz, rw [sqrt_two_add_series_succ],
apply sqrt_two_add_series_monotone_left, exact le_sqrt_of_sqr_le h
end
/- currently we use the "slow" certificates (using real computation instead of nat computation),
because the certificates for nat raise errors during type-checking -/
-- 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],
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],
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],
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],
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment