Harmonic numbers and the Euler–Mascheroni constant

TheoremLogarithm gap between a real number and its floor#✓fully proved

For every real \(x \ge 1\), the floor \(\lfloor x \rfloor\) of \(x\) satisfies \(\log x - \log \lfloor x \rfloor \le 1/\lfloor x \rfloor\).

theorem log_sub_log_floor_le {x : ℝ} (hx : 1 ≤ x) :
    Real.log x - Real.log (⌊x⌋₊ : ℝ) ≤ 1 / (⌊x⌋₊ : ℝ)

Used by 1

Used byExplicit harmonic error bound at real arguments

TheoremExplicit harmonic error bound at integers#✓fully proved

Let \(H_n = \sum_{k=1}^{n} 1/k\) be the \(n\)-th harmonic number and \(\gamma\) the Euler–Mascheroni constant. For every natural number \(n \ge 1\), \(|H_n - \log n - \gamma| \le 1/n\).

theorem abs_harmonic_sub_log_sub_eulerMascheroniConstant_le {n : ℕ} (hn : 1 ≤ n) :
    |(harmonic n : ℝ) - Real.log n - Real.eulerMascheroniConstant| ≤ 1 / n

Used by 1

Used byExplicit harmonic error bound at real arguments

TheoremExplicit harmonic error bound at real arguments#✓fully proved

Let \(H_n = \sum_{k=1}^{n} 1/k\) be the \(n\)-th harmonic number and \(\gamma\) the Euler–Mascheroni constant. For every real \(x \ge 2\), with \(\lfloor x \rfloor\) the floor of \(x\), \(|H_{\lfloor x \rfloor} - \log x - \gamma| \le 2/x\).

theorem abs_harmonic_floor_sub_log_sub_eulerMascheroniConstant_le {x : ℝ} (hx : 2 ≤ x) :
    |(harmonic ⌊x⌋₊ : ℝ) - Real.log x - Real.eulerMascheroniConstant| ≤ 2 / x

Uses 2

Proof usesExplicit harmonic error bound at integers · Logarithm gap between a real number and its floor

TheoremHarmonic numbers at the floor track the logarithm#✓fully proved

Let \(H_k\) denote the \(k\)-th harmonic number, \(\lfloor x \rfloor\) the floor of a real number \(x\), and \(\gamma\) the Euler–Mascheroni constant. Then \(H_{\lfloor x \rfloor} - \log x - \gamma = O(1/x)\) as \(x \to \infty\).

theorem isBigO_harmonic_floor_sub_log_sub_eulerMascheroniConstant :
    (fun x : ℝ => (harmonic ⌊x⌋₊ : ℝ) - Real.log x - Real.eulerMascheroniConstant)
      =O[atTop] (fun x : ℝ => x⁻¹)

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.