BKLNW.bklnw_corollary_9_1_explicit

@[blueprint  "bklnw-corollary-9-1-explicit"  (title := "BKLNW Corollary 9.1 explicit version")  (statement := /--  We have $\theta(x) - x \geq - C_{b,k} x / \log k$ for all $k=1,\dots, 5$, $e^b \leq x < 10^{19}$, and $C_{b,k}$ from Table 12. -/)  (proof := /-- Insert the above table into the previous corollary. -/)  (latexEnv := "corollary")]theorem bklnw_corollary_9_1_explicit (b c C M : ℝ) (Cb : ℕ → ℝ) (h : (b, Cb 1, Cb 2, Cb 3, Cb 4, Cb 5, c, C, M) ∈ BKLNW.table_12) :  ∀ x ∈ Set.Ico (exp b) (10 ^ 19), ∀ k ∈ Finset.Icc 1 5, θ x - x ≥ - Cb k * x / (log x)^k := by  obtain ⟨h_buthe, h_expb_le_M, h_10000_le_expb, h_ten_le_b, h_b_pos, h_M_vals⟩ :=    mem_table_from_buthe_and_bounds_of_mem_table_12 b c C M Cb h  have h_expb_lb : ∀ k : ℕ, k ∈ Finset.Icc 1 5 →      max (10000 : ℝ) (exp (2 * (k : ℝ))) ≤ exp b := fun k hk =>    max_le_iff.mpr ⟨h_10000_le_expb,                    le_trans (exp_two_k_le_exp_ten k hk) (Real.exp_le_exp.mpr h_ten_le_b)⟩  have h_cor_9_1 : ∀ k : ℕ, k ∈ Finset.Icc 1 5 →      ∀ x ∈ Set.Icc (exp b) M,      θ x ≥ x - C_bk b c C RS_prime.c₀ k * x / (log x) ^ k :=    fun k hk => bklnw_corollary_9_1 k M c C b h_buthe ⟨h_expb_lb k hk, h_expb_le_M⟩  have h_Cb_le : ∀ k ∈ Finset.Icc 1 5, C_bk b c C RS_prime.c₀ k ≤ Cb k :=    bklnw_table_12_verification b c C M Cb h  intro x hx k hk  rcases le_or_gt x M with hx_le | hx_gt  · have hx_in_Icc : x ∈ Set.Icc (exp b) M := ⟨hx.1, hx_le⟩    have hx_pos : (0 : ℝ) < x := (exp_pos b).trans_le hx_in_Icc.1    have h_log_pos : (0 : ℝ) < (log x) ^ k := by      apply pow_pos      calc 0 < b := h_b_pos        _ = log (exp b) := (Real.log_exp b).symm        _ ≤ log x := Real.log_le_log (exp_pos b) hx_in_Icc.1    exact theta_sub_ge_of_cbk_le x _ _ k hx_pos h_log_pos      (by linarith [h_cor_9_1 k hk x hx_in_Icc]) (h_Cb_le k hk)  · by_cases hM : M = 10 ^ 19    · subst hM; linarith [hx.2, hx_gt]    · by_cases hM5 : M = 5 * 10 ^ 10      · by_cases hx32 : x ≤ bklnw_M_row6        · have hx_in_Icc6 : x ∈ Set.Icc (exp bklnw_b_row6) bklnw_M_row6 := by            eval_table_12_at_all            rw [Real.exp_log (by norm_num)]; exact ⟨by linarith, hx32⟩          have h_cor_9_1_row6 := bklnw_corollary_9_1 k bklnw_M_row6 bklnw_c_row6 bklnw_C_row6 bklnw_b_row6            (by eval_table_12; simp [table_from_buthe]; norm_num)            (by eval_table_12                rw [Real.exp_log (by norm_num)]                try simp only [max_le_iff]                refine ⟨⟨by norm_num, le_trans (exp_two_k_le_exp_ten k hk) ?_⟩, by norm_num⟩                grw [← exp_one_rpow 10, Real.exp_one_lt_d9]; norm_num)          have hx_pos : (0 : ℝ) < x := by linarith          have h_log_pos : (0 : ℝ) < log x ^ k :=            pow_pos (Real.log_pos (by linarith : (1 : ℝ) < x)) k          exact theta_sub_ge_of_cbk_le x _ _ k hx_pos h_log_pos            (by linarith [h_cor_9_1_row6 x hx_in_Icc6])            (C_bk_le_Cb_of_M_eq_five_mul_ten_pow_ten b c C M Cb h k hk hM5)        · have hx_in_Icc14 : x ∈ Set.Icc (exp bklnw_b_row14) bklnw_M_row14 := by            eval_table_12_at_all            rw [Real.exp_log (by norm_num)]            exact ⟨(not_le.mp hx32).le, by linarith [hx.2]⟩          have h_cor_9_1_row14 := bklnw_corollary_9_1 k bklnw_M_row14 bklnw_c_row14 bklnw_C_row14 bklnw_b_row14            (by eval_table_12; simp [table_from_buthe]; norm_num)            (by eval_table_12                rw [Real.exp_log (by norm_num)]                try simp only [max_le_iff]                refine ⟨⟨by norm_num, le_trans (exp_two_k_le_exp_ten k hk) ?_⟩, by norm_num⟩                grw [← exp_one_rpow 10, Real.exp_one_lt_d9]; norm_num)          have hx_pos : (0 : ℝ) < x := by linarith          have h_log_pos : (0 : ℝ) < log x ^ k :=            pow_pos (Real.log_pos (by linarith : (1 : ℝ) < x)) k          exact theta_sub_ge_of_cbk_le x _ _ k hx_pos h_log_pos            (by linarith [h_cor_9_1_row14 x hx_in_Icc14])            (C_bk_le_Cb_of_M_ne_ten_pow_nineteen b c C M Cb h k hk (by rw [hM5]; norm_num))      · have h_M_eq : M = bklnw_M_row6 := by          eval_table_12          rcases h_M_vals with rfl | rfl | rfl          · exact absurd rfl hM5          · norm_num          · exact absurd rfl hM        have hx_gt32 : x > bklnw_M_row6 := h_M_eq ▸ hx_gt        have hx_in_Icc14 : x ∈ Set.Icc (exp bklnw_b_row14) bklnw_M_row14 := by          eval_table_12_at_all          rw [Real.exp_log (by norm_num)]          exact ⟨hx_gt32.le, by linarith [hx.2]⟩        have h_cor_9_1_row14 := bklnw_corollary_9_1 k bklnw_M_row14 bklnw_c_row14 bklnw_C_row14 bklnw_b_row14          (by eval_table_12; simp [table_from_buthe]; norm_num)          (by eval_table_12              rw [Real.exp_log (by norm_num)]              try simp only [max_le_iff]              refine ⟨⟨by norm_num, le_trans (exp_two_k_le_exp_ten k hk) ?_⟩, by norm_num⟩              grw [← exp_one_rpow 10, Real.exp_one_lt_d9]; norm_num)        have hx_pos : (0 : ℝ) < x := by linarith        have h_log_pos : (0 : ℝ) < log x ^ k :=          pow_pos (Real.log_pos (by linarith : (1 : ℝ) < x)) k        exact theta_sub_ge_of_cbk_le x _ _ k hx_pos h_log_pos          (by linarith [h_cor_9_1_row14 x hx_in_Icc14])          (C_bk_le_Cb_of_M_ne_ten_pow_nineteen b c C M Cb h k hk hM)