summable_inv_mul_log_sq

lemma summable_inv_mul_log_sq : Summable (fun n : ℕ => (n * (Real.log n) ^ 2)⁻¹) := by  let u (n : ℕ) := (n * (Real.log n) ^ 2)⁻¹  have l7 : ∀ᶠ n : ℕ in atTop, 1 ≤ Real.log n :=    tendsto_atTop.mp (tendsto_log_atTop.comp tendsto_natCast_atTop_atTop) 1  have l8 : ∀ᶠ n : ℕ in atTop, 1 ≤ n := eventually_ge_atTop 1  have l9 : ∀ᶠ n in atTop, u (n + 1) ≤ u n := by    filter_upwards [l7, l8] with n l2 l8; dsimp [u]; gcongr <;> simp  obtain ⟨v, l1, l2, l3⟩ := exists_antitone_of_eventually l9  rw [summable_congr_ae l3.symm]  have l4 (n : ℕ) : 0 ≤ v n := by obtain ⟨k, hk⟩ := l1 ⟨n, rfl⟩ ; rw [← hk] ; positivity  apply (summable_condensed_iff_of_nonneg l4 (fun _ _ _ a ↦ l2 a)).mp  suffices this : ∀ᶠ k : ℕ in atTop, 2 ^ k * v (2 ^ k) = ((k : ℝ) ^ 2)⁻¹ * ((Real.log 2) ^ 2)⁻¹ by    exact (summable_congr_ae this).mpr <| (Real.summable_nat_pow_inv.mpr one_lt_two).mul_right _  have l5 : ∀ᶠ k in atTop, v (2 ^ k) = u (2 ^ k) :=    l3.comp_tendsto <| tendsto_pow_atTop_atTop_of_one_lt Nat.le.refl  filter_upwards [l5, l8] with k l5 l8  simp only [l5, mul_inv_rev, Nat.cast_pow, Nat.cast_ofNat, log_pow, u]  field_simp