FKS2.exists_isMaxOn_Ici_log_div_self_mul_integral_one_div_log_sq

lemma exists_isMaxOn_Ici_log_div_self_mul_integral_one_div_log_sq {x₁ : ℝ} (h : x₁ ≥ 14) : ∃ xm > x₁, xm > x₁ * log x₁ ∧  ∀ y ≥ x₁, (log y / y) * ∫ t in x₁..y, 1 / (log t) ^ 2 ≤ 1 / (log xm - 1) := by  obtain ⟨t₁, ht₁_gt, ht₁_val⟩ := exists_larger_than_boundary_val h  have ht₁_ge : x₁ ≤ t₁ := (x1_le_x1_log_x1 h).trans ht₁_gt.le  have h_exists_max : ∃ xm ≥ x₁, ∀ y ≥ x₁,    (log y / y) * ∫ t in x₁..y, 1 / (log t) ^ 2 ≤ (log xm / xm) * ∫ t in x₁..xm, 1 / (log t) ^ 2 := by    have hc_pos : 0 < (log t₁ / t₁) * ∫ s in x₁..t₁, 1 / (log s) ^ 2 :=      (log_div_self_mul_integral_nonneg h (x1_le_x1_log_x1 h)).trans_lt ht₁_val    have h_eventually : ∀ᶠ y in Filter.atTop,        (log y / y) * ∫ s in x₁..y, 1 / (log s) ^ 2 <        (log t₁ / t₁) * ∫ s in x₁..t₁, 1 / (log s) ^ 2 := by      filter_upwards [tendsto_log_div_self_mul_integral_atTop_zero h          (Metric.ball_mem_nhds 0 hc_pos),        Filter.eventually_ge_atTop x₁] with y hy hy_ge      rwa [Set.mem_preimage, Metric.mem_ball, Real.dist_0_eq_abs,           abs_of_nonneg (log_div_self_mul_integral_nonneg h hy_ge)] at hy    obtain ⟨M, hM_prop⟩ := Filter.eventually_atTop.mp h_eventually    set M' := max (max M t₁) x₁    have hM'_ge_x₁ : x₁ ≤ M' := le_max_right (max M t₁) x₁    have hM'_ge_t₁ : t₁ ≤ M' := (le_max_right M t₁).trans (le_max_left (max M t₁) x₁)    have hM'_ge_M  : M ≤ M'  := (le_max_left M t₁).trans (le_max_left (max M t₁) x₁)    have h_int_M' : IntervalIntegrable (fun s ↦ 1 / (Real.log s) ^ 2) volume x₁ M' := by      apply ContinuousOn.intervalIntegrable      rw [Set.uIcc_of_le hM'_ge_x₁]      intro s hs      have hs0 : s ≠ 0 := ne_of_gt (by linarith [hs.1] : 0 < s)      have hlog_ne : Real.log s ≠ 0 :=        ne_of_gt (Real.log_pos (by linarith [hs.1] : 1 < s))      exact (ContinuousAt.div continuousAt_const        (ContinuousAt.pow (Real.continuousAt_log hs0) 2)        (pow_ne_zero 2 hlog_ne)).continuousWithinAt    have h_cont_f : ContinuousOn        (fun y ↦ (Real.log y / y) * ∫ t in x₁..y, 1 / (Real.log t) ^ 2) (Set.Icc x₁ M') := by      apply ContinuousOn.mul      · intro y hy        exact (ContinuousAt.div (Real.continuousAt_log (ne_of_gt (by linarith [hy.1] : 0 < y)))          continuousAt_id (by simp; linarith [hy.1])).continuousWithinAt      · rw [← Set.uIcc_of_le hM'_ge_x₁]        exact intervalIntegral.continuousOn_primitive_interval' h_int_M' Set.left_mem_uIcc    obtain ⟨xm, hxm_mem, hxm_max⟩ :=      isCompact_Icc.exists_isMaxOn (Set.nonempty_Icc.mpr hM'_ge_x₁) h_cont_f    exact ⟨xm, hxm_mem.1, fun y hy_ge ↦ by      by_cases hy_le : y ≤ M'      · exact hxm_max ⟨hy_ge, hy_le⟩      · have hy_ge_M : M ≤ y := by linarith [hM'_ge_M, not_le.mp hy_le]        exact ((hM_prop y hy_ge_M).trans_le (hxm_max ⟨ht₁_ge, hM'_ge_t₁⟩)).le⟩  obtain ⟨xm, hxm_ge, hxm_max⟩ := h_exists_max  have h_xm_gt : xm > x₁ * log x₁ := by    by_contra hle    push Not at hle    linarith [h_monotoneOn h ⟨hxm_ge, hle⟩ ⟨x1_le_x1_log_x1 h, le_refl _⟩ hle,              hxm_max t₁ ((x1_lt_x1_log_x1 h).trans ht₁_gt |>.le)]  have h_max_val : (log xm / xm) * ∫ t in x₁..xm, 1 / (log t) ^ 2 = 1 / (log xm - 1) := by    have hxm_gt : x₁ < xm := (x1_lt_x1_log_x1 h).trans h_xm_gt    have h_local_max : IsLocalMax (fun t ↦ (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2) xm := by      filter_upwards [eventually_ge_nhds hxm_gt] with y hy using hxm_max y hy    have h_deriv_xm : HasDerivAt (fun t ↦ (log t / t) * ∫ s in x₁..t, 1 / (log s) ^ 2)        ((xm / log xm - (log xm - 1) * ∫ s in x₁..xm, 1 / (log s) ^ 2) / xm ^ 2) xm :=      hasDerivAt_log_div_self_mul_integral (by linarith : 1 < x₁) hxm_gt    have h_num_eq_zero : xm / log xm - (log xm - 1) * ∫ s in x₁..xm, 1 / (log s) ^ 2 = 0 :=      div_eq_zero_iff.mp (h_deriv_xm.deriv ▸ h_local_max.deriv_eq_zero)        |>.resolve_right (pow_ne_zero 2 (by linarith : xm ≠ 0))    have h_logxm_gt : log xm > 1 := by      have h1 : log x₁ > 1 := log_gt_one_of_ge_14 h      linarith [Real.log_le_log (by positivity) h_xm_gt.le, Real.log_pos h1,                Real.log_mul (by linarith : x₁ ≠ 0) (by linarith : log x₁ ≠ 0)]    have h_logxm_sub_ne : log xm - 1 ≠ 0 := by linarith    have h_logxm_ne : log xm ≠ 0 := by linarith    have h_xm_ne : xm ≠ 0 := by linarith    rw [show (log xm / xm) * ∫ s in x₁..xm, 1 / (log s) ^ 2 =        ((log xm - 1) * ∫ s in x₁..xm, 1 / (log s) ^ 2) * (log xm / (xm * (log xm - 1)))        from by field_simp,      show (log xm - 1) * ∫ s in x₁..xm, 1 / (log s) ^ 2 = xm / log xm        from by linarith [h_num_eq_zero]]    field_simp [h_logxm_sub_ne, h_logxm_ne, h_xm_ne]  exact ⟨xm, (x1_lt_x1_log_x1 h).trans h_xm_gt, h_xm_gt,    fun y hy ↦ (hxm_max y hy).trans h_max_val.le⟩