IntegralLogSqOverTSqBound

lemma IntegralLogSqOverTSqBound : ∃ C > 0, ∀ T, 3 < T →  ∫ t in Set.Ici T, (Real.log t)^2 / t^2 ≤ C / Real.sqrt T := by    have h_log_sq_le_t_fourth_pow :        ∃ C > 0, ∀ t : ℝ, 3 ≤ t → (Real.log t)^2 / t^2 ≤ C / t^(3/2 : ℝ) := by      have h_log_sq_le_sqrt :          ∃ C > 0, ∀ t : ℝ, 3 ≤ t → Real.log t ^ 2 ≤ C * t ^ (1 / 2 : ℝ) := by        have h_log_sq_le_sqrt : ∃ C > 0, ∀ t : ℝ, 3 ≤ t → Real.log t ≤ C * t ^ (1 / 4 : ℝ) := by          use 4, by grind, fun t ht ↦ ?_          have := Real.log_le_sub_one_of_pos (by positivity : 0 < t ^ (1 / 4 : ℝ))          rw [Real.log_rpow (by positivity)] at this; linarith        obtain ⟨C, hC₀, hC⟩ := h_log_sq_le_sqrt; use C^2        exact ⟨sq_pos_of_pos hC₀, fun t ht ↦          (pow_le_pow_left₀ (Real.log_nonneg <| by linarith) (hC t ht) 2).trans <| by            rw [mul_pow, ← Real.rpow_natCast, ← Real.rpow_natCast, ← Real.rpow_mul (by linarith)]            grind⟩      obtain ⟨C, hC_pos, hC⟩ := h_log_sq_le_sqrt; use C      refine ⟨hC_pos, fun t ht ↦ ?_⟩; rw [div_le_div_iff₀] <;> try positivity      convert mul_le_mul_of_nonneg_right (hC t ht)        (Real.rpow_nonneg (by linarith : 0 ≤ t) (3 / 2)) using 1      rw [mul_assoc, ← Real.rpow_natCast, ← Real.rpow_add (by linarith)]; grind    obtain ⟨C, hC_pos, hC_bound⟩ := h_log_sq_le_t_fourth_pow    use C * 2    have h_integral_bound :        ∀ T : ℝ, 3 < T → ∫ t in Set.Ici T, C / t^(3/2 : ℝ) = C * 2 / Real.sqrt T := by      have h_integral_eval :          ∀ T : ℝ, 3 < T → ∫ t in Set.Ici T, t ^ (-3 / 2 : ℝ) = 2 / Real.sqrt T := by        intro T hT        rw [MeasureTheory.integral_Ici_eq_integral_Ioi, integral_Ioi_rpow_of_lt] <;> norm_num        · rw [Real.sqrt_eq_rpow, Real.rpow_neg] <;> ring_nf; linarith        · linarith      intro T hT; convert congr_arg (fun x ↦ C * x) (h_integral_eval T hT) using 1 <;> ring_nf      rw [← MeasureTheory.integral_const_mul]      refine MeasureTheory.setIntegral_congr_fun measurableSet_Ici fun x hx ↦ ?_      rw [← Real.rpow_neg (by linarith [Set.mem_Ici.mp hx])]; ring_nf    refine ⟨by positivity, fun T hT ↦ (MeasureTheory.setIntegral_mono_on ?_ ?_ measurableSet_Ici        fun t ht ↦ hC_bound t <| by linarith [ht.out]).trans (h_integral_bound T hT |> le_of_eq)⟩    · have hInteg : IntegrableOn (fun t ↦ C / t ^ (3 / 2 : ℝ)) (Set.Ici T) := by        have := h_integral_bound T hT        contrapose! this; rw [MeasureTheory.integral_undef this]; positivity      have hMeas : AEStronglyMeasurable (fun t ↦ Real.log t ^ 2 / t ^ 2)          (MeasureTheory.volume.restrict (Set.Ici T)) :=        Measurable.aestronglyMeasurable <| Measurable.mul          (Measurable.pow_const Real.measurable_log _)          (Measurable.inv (measurable_id.pow_const _))      have hBound : ∀ᵐ t ∂MeasureTheory.volume.restrict (Set.Ici T),          ‖Real.log t ^ 2 / t ^ 2‖ ≤ C / t ^ (3 / 2 : ℝ) := by        filter_upwards [MeasureTheory.ae_restrict_mem measurableSet_Ici] with t ht        rw [Real.norm_of_nonneg (by positivity)]        exact hC_bound t (by linarith [ht.out])      exact MeasureTheory.Integrable.mono' hInteg hMeas hBound    · have := h_integral_bound T hT      contrapose! this; rw [MeasureTheory.integral_undef this]; positivity