FKS2.Floor.etheta_integrand_intble

theorem etheta_integrand_intble {x : ℝ} (hx : 2 ≤ x) :    IntervalIntegrable (fun t => Eθ t / log t ^ 2) volume 2 x := by  have log_t_ne_zero : ∀ t ∈ Set.uIcc (2:ℝ) x, log t ≠ 0 := fun t ht ↦ by    rw [Set.uIcc_of_le hx, Set.mem_Icc] at ht    exact ne_of_gt (log_pos (by linarith [ht.1]))  have t_ne_zero : ∀ t ∈ Set.uIcc (2:ℝ) x, t ≠ 0 := fun t ht ↦ by    rw [Set.uIcc_of_le hx, Set.mem_Icc] at ht; exact ne_of_gt (by linarith [ht.1])  refine IntervalIntegrable.mul_continuousOn ?_ (by fun_prop (disch := grind))  unfold Eθ  refine IntervalIntegrable.mul_continuousOn ?_ (by fun_prop (disch := grind))  refine IntervalIntegrable.abs <| IntervalIntegrable.sub ?_ intervalIntegral.intervalIntegrable_id  apply (intervalIntegrable_iff_integrableOn_Icc_of_le hx).mpr  conv => arg 1; ext y; rw [← one_mul (θ y), theta_eq_sum_Icc, Finset.sum_filter]  apply integrableOn_mul_sum_Icc _ (by linarith)  apply ContinuousOn.integrableOn_Icc; fun_prop