basic log bounds on harmonic sums

Stream: Is there code for X?

[Arend Mellendijk]

I have the following bounds lying around:

import Mathlib.Analysis.SumIntegralComparisons
open BigOperators

theorem log_add_one_le_sum_inv (n : ℕ) :
    Real.log ↑(n+1) ≤ ∑ d in Finset.Icc 1 n, (d:ℝ)⁻¹ := sorry

theorem sum_inv_le_log (n : ℕ) (hn : 1 ≤ n) :
    ∑ d in Finset.Icc 1 n, (d : ℝ)⁻¹ ≤ 1 + Real.log ↑n := sorry

-- and corollaries
theorem log_le_sum_one_div (y : ℝ) (hy : 1 ≤ y) :
    Real.log y ≤ ∑ d in Finset.Icc 1 (⌊y⌋₊), (d:ℝ)⁻¹ := sorry

theorem sum_inv_le_log_real (y : ℝ) (hy : 1 ≤ y) :
    ∑ d in Finset.Icc 1 (⌊y⌋₊), (d:ℝ)⁻¹ ≤ 1 + Real.log y := sorry

Am I right to say we don't have any results of this form in mathlib? And if so where should these go?

[Arend Mellendijk]

I was also surprised I couldn't find anything like

theorem inv_sub_antitoneOn_gt {R : Type*} [LinearOrderedField R] (c : R) :
    AntitoneOn (fun x:R ↦ (x-c)⁻¹) (Set.Ioi c) := sorry

[Alex J. Best]

@Koundinya Vajjha recently added Mathlib/NumberTheory/Padics/Harmonic.lean I think the basic definition there should be factored out into a new file with some basic properties, including yours

[Yury G. Kudryashov]

Do you use integrals or induction/estimates on Real.log?

[Arend Mellendijk]

Integrals. (note the import)