FKS2.exists_larger_than_boundary_val

lemma exists_larger_than_boundary_val {x₁ : ℝ} (h : x₁ ≥ 14) :    ∃ t > x₁ * log x₁, (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2 >      (log (x₁ * log x₁) / (x₁ * log x₁)) * ∫ s in x₁..(x₁ * log x₁), 1 / (log s) ^ 2 := by  have h_deriv : deriv (fun t ↦ (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2) (x₁ * log x₁) > 0 :=    deriv_log_div_self_mul_integral_one_div_log_sq_pos h  have h_tendsto := hasDerivAt_iff_tendsto_slope.mp (hasDerivAt_log_div_self_mul_integral_one_div_log_sq h)  have h_slope_pos : ∀ᶠ t in nhdsWithin (x₁ * log x₁) (Set.Ioi (x₁ * log x₁)), slope (fun t ↦ (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2) (x₁ * log x₁) t > 0 :=    Filter.Eventually.filter_mono (nhdsWithin_mono (x₁ * log x₁) (fun _ h ↦ ne_of_gt h))      (Filter.Tendsto.eventually_const_lt h_deriv h_tendsto)  have h_exists : ∃ t > x₁ * log x₁, slope (fun t ↦ (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2) (x₁ * log x₁) t > 0 := by    haveI : Filter.NeBot (nhdsWithin (x₁ * log x₁) {x | (fun x ↦ x > x₁ * log x₁) x}) := nhdsWithin_Ioi_neBot le_rfl    exact Filter.Eventually.exists (Filter.Eventually.and self_mem_nhdsWithin h_slope_pos)  obtain ⟨t, ht_gt, ht_slope⟩ := h_exists  have h_val : (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2 >    (log (x₁ * log x₁) / (x₁ * log x₁)) * ∫ s in x₁..(x₁ * log x₁), 1 / (log s) ^ 2 :=    (slope_pos_iff_of_le ht_gt.le).mp ht_slope  exact ⟨t, ht_gt, h_val⟩