Ramanujan.log_8_bound

theorem log_8_bound (x : ℝ) (hx : 2 ≤ x) :    ∫ t in Set.Icc 2 x, 1 / log t ^ 8 <      sqrt x / log 2 ^ 8 + 2 ^ 8 * x / log x ^ 8 := by  by_cases h : x < 4  · refine lt_of_le_of_lt (MeasureTheory.setIntegral_mono_on ?_ ?_ measurableSet_Icc fun t ht =>      one_div_le_one_div_of_le ?_ <| pow_le_pow_left₀ (log_nonneg <| by linarith [ht.1])        (log_le_log (by linarith [ht.1]) ht.1) 8) ?_    · exact ContinuousOn.integrableOn_Icc (continuousOn_const.div (ContinuousOn.pow        (continuousOn_log.mono <| by norm_num) _) fun t ht ↦ pow_ne_zero _ <| ne_of_gt <|        log_pos <| by linarith [ht.1])    · norm_num    · positivity    · norm_num [← div_eq_mul_inv]      exact lt_add_of_le_of_pos (by        gcongr; cases max_cases (x - 2) 0 <;>          nlinarith [sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)]) (        div_pos (by positivity) (pow_pos (log_pos (by linarith)) _))  · have h_split : ∫ t in Set.Icc 2 x, 1 / log t ^ 8 =        (∫ t in Set.Icc 2 (sqrt x), 1 / log t ^ 8) +          (∫ t in Set.Icc (sqrt x) x, 1 / log t ^ 8) := by      norm_num [MeasureTheory.integral_Icc_eq_integral_Ioc,        ← intervalIntegral.integral_of_le, sqrt_le_iff, hx]      rw [← intervalIntegral.integral_of_le (by            nlinarith [sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)]),        ← intervalIntegral.integral_of_le (by          nlinarith [sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)]),        intervalIntegral.integral_add_adjacent_intervals]        <;> apply_rules [ContinuousOn.intervalIntegrable]      · exact continuousOn_of_forall_continuousAt fun y hy =>          ContinuousAt.inv₀ (ContinuousAt.pow (continuousAt_log (by            cases Set.mem_uIcc.mp hy <;>              nlinarith [sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)])) _)            (pow_ne_zero _ <| ne_of_gt <| log_pos <| by              cases Set.mem_uIcc.mp hy <;>                nlinarith [sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)])      · exact continuousOn_of_forall_continuousAt fun y hy =>          ContinuousAt.inv₀ (ContinuousAt.pow (continuousAt_log (by            cases Set.mem_uIcc.mp hy <;>              nlinarith [sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)])) _)            (pow_ne_zero _ <| ne_of_gt <| log_pos <| by              cases Set.mem_uIcc.mp hy <;>                nlinarith [sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)])    have h_first : ∫ t in Set.Icc 2 (sqrt x), 1 / log t ^ 8 ≤        sqrt x / (log 2) ^ 8 := by      have h_mono : ∫ t in Set.Icc 2 (sqrt x), 1 / log t ^ 8 ≤          ∫ t in Set.Icc 2 (sqrt x), 1 / log 2 ^ 8 := by        refine MeasureTheory.setIntegral_mono_on ?_ ?_ ?_ ?_ <;> norm_num        · exact ContinuousOn.integrableOn_Icc (continuousOn_of_forall_continuousAt fun t ht =>            ContinuousAt.inv₀              ((Real.continuousAt_log (show t ≠ 0 from ne_of_gt (by linarith [ht.1]))).pow _)              (ne_of_gt (pow_pos (log_pos (show 1 < t by linarith [ht.1])) _)))        · exact fun t ht₁ ht₂ ↦ inv_anti₀ (pow_pos (log_pos (by linarith)) _)            (pow_le_pow_left₀ (log_nonneg (by linarith)) (log_le_log (by linarith) (by linarith)) _)      refine le_trans h_mono ?_; norm_num      rw [max_eq_left (sub_nonneg.mpr <| le_sqrt_of_sq_le <| by linarith)]      ring_nf; norm_num; positivity    have h_second : ∫ t in Set.Icc (sqrt x) x, 1 / log t ^ 8 ≤        (x - sqrt x) * (2 ^ 8 / (log x) ^ 8) := by      have hbd : ∀ t ∈ Set.Icc (sqrt x) x,          1 / log t ^ 8 ≤ 2 ^ 8 / (log x) ^ 8 := by        intro t ht        have hlog_half : log t ≥ log (sqrt x) := log_le_log (by positivity) ht.1        rw [log_sqrt (by positivity)] at hlog_half        rw [div_le_div_iff₀] <;>          nlinarith [pow_pos (log_pos (by linarith : 1 < x)) 8,            pow_le_pow_left₀ (by linarith [log_pos (by linarith : 1 < x)]) hlog_half 8]      convert! MeasureTheory.setIntegral_mono_on _ _ _ hbd <;> norm_num      · exact Or.inl <| Or.inr <| by linarith      · exact ContinuousOn.integrableOn_Icc (continuousOn_of_forall_continuousAt fun t ht =>          ContinuousAt.inv₀ (ContinuousAt.pow (continuousAt_log (by            nlinarith [ht.1, sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)])) _)            (pow_ne_zero _ <| ne_of_gt <| log_pos <| by              nlinarith [ht.1, sqrt_nonneg x, sq_sqrt (show 0 ≤ x by linarith)]))    refine h_split.symm ▸ lt_of_le_of_lt (add_le_add h_first h_second) ?_    ring_nf    nlinarith [show 0 < sqrt x * (log x)⁻¹ ^ 8 from      mul_pos (sqrt_pos.mpr (by linarith))        (pow_pos (inv_pos.mpr (log_pos (by linarith))) _)]