BKLNW.row_bound_k5

theorem row_bound_k5 (b b' A₁ A₂ E T : ℝ)    (hbb' : b ≤ b') (hb20 : 20 ≤ b)    (hA1 : 0 ≤ A₁) (hA2 : 0 ≤ A₂) (hE : 0 ≤ E)    (ha1 : Inputs.default.a₁ b ≤ A₁) (ha2 : Inputs.default.a₂ b ≤ A₂) (heps : Inputs.default.ε b ≤ E)    (hGb : Gp A₁ A₂ E b ≤ T) (hGb' : Gp A₁ A₂ E b' ≤ T) :    B_8_exact 5 b b' ≤ T := by  unfold B_8_exact  refine B_le_of_forall_log _ _ _ _ hbb' ?_  intro y hy  have hy0 : (0 : ℝ) ≤ y := by have := hy.1; linarith  have hy5 : (0 : ℝ) ≤ y ^ 5 := pow_nonneg hy0 5  have hconv : Gp A₁ A₂ E y ≤ T :=    le_trans ((Gp_convexOn b b' hbb' hb20 hA1 hA2 hE).le_max_of_mem_Icc      (left_mem_Icc.mpr hbb') (right_mem_Icc.mpr hbb') hy) (max_le hGb hGb')  rw [show Finset.Icc 1 2 = {1, 2} from by decide, Finset.sum_insert (by decide), Finset.sum_singleton]  have hif1 : (if (1 : ℕ) = 1 then Inputs.default.a₁ b else if (1 : ℕ) = 2 then Inputs.default.a₂ b else 0)      = Inputs.default.a₁ b := by norm_num  have hif2 : (if (2 : ℕ) = 1 then Inputs.default.a₁ b else if (2 : ℕ) = 2 then Inputs.default.a₂ b else 0)      = Inputs.default.a₂ b := by norm_num  have ce1 : Real.exp (-(((1 : ℕ) : ℝ) / (((1 : ℕ) : ℝ) + 1) * y)) = Real.exp (-(1 / 2 * y)) := by    congr 1; push_cast; ring  have ce2 : Real.exp (-(((2 : ℕ) : ℝ) / (((2 : ℕ) : ℝ) + 1) * y)) = Real.exp (-(2 / 3 * y)) := by    congr 1; push_cast; ring  rw [hif1, hif2, ce1, ce2]  have e1 : (0 : ℝ) ≤ y ^ 5 * Real.exp (-(1 / 2 * y)) := mul_nonneg hy5 (Real.exp_pos _).le  have e2 : (0 : ℝ) ≤ y ^ 5 * Real.exp (-(2 / 3 * y)) := mul_nonneg hy5 (Real.exp_pos _).le  have h1 : Inputs.default.a₁ b * y ^ 5 * Real.exp (-(1 / 2 * y)) ≤ A₁ * (y ^ 5 * Real.exp (-(1 / 2 * y))) := by    rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha1 e1  have h2 : Inputs.default.a₂ b * y ^ 5 * Real.exp (-(2 / 3 * y)) ≤ A₂ * (y ^ 5 * Real.exp (-(2 / 3 * y))) := by    rw [mul_assoc]; exact mul_le_mul_of_nonneg_right ha2 e2  have h3 : Inputs.default.ε b * y ^ 5 ≤ E * y ^ 5 := mul_le_mul_of_nonneg_right heps hy5  have hGpy : Gp A₁ A₂ E y      = A₁ * (y ^ 5 * Real.exp (-(1 / 2 * y))) + A₂ * (y ^ 5 * Real.exp (-(2 / 3 * y))) + E * y ^ 5 := by    unfold Gp expT; ring  rw [hGpy] at hconv  linarith [h1, h2, h3, hconv]