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)

[Arend Mellendijk]

Got a bit distracted, but this is covered by #9984

[Terence Tao]

I have a personal project https://github.com/teorth/asymptotic which is aimed at proving bounds like this. A sample result is

lemma sum_approx_eq_integral_antitone_nat {a b:ℝ} (h0: 0 ≤ a) (h: a ≤ b) (f: ℝ → ℝ) (hf: AntitoneOn f (Set.Icc a b)) (hf': f b ≥ 0) : ∑ n in Finset.Ico ⌈ a ⌉₊ ⌈ b ⌉₊, f n =[1] ∫ t in Set.Ico a b, f t ∂ volume + O( f a )

where X =[C] Y + O( Z ) is my notation for |X-Y| ≤ C * Z; there will also be a similar result for Set.Icc that I plan to put in shortly. This would give a slight variant of your bounds, namely | ∑ d in Finset.Icc 1 n, (d:ℝ)⁻¹ - log n | ≤ 1. I plan to fold this code into a forthcoming project in analytic number theory, and perhaps at that point it might eventually be ported into Mathlib.