Documentation
Mathlib
.
NumberTheory
.
Harmonic
.
Bounds
Search
Google site search
return to top
source
Imports
Init
Mathlib.Analysis.SumIntegralComparisons
Mathlib.Analysis.SpecialFunctions.Integrals
Mathlib.NumberTheory.Harmonic.Defs
Imported by
log_add_one_le_harmonic
harmonic_le_one_add_log
log_le_harmonic_floor
harmonic_floor_le_one_add_log
This file proves
log
(
n
+
1
)
≤
H
n
≤
1
+
log
(
n
)
for all natural numbers
n
.
source
theorem
log_add_one_le_harmonic
(n :
ℕ
)
:
Real.log
↑
(
n
+
1
)
≤
↑
(
harmonic
n
)
source
theorem
harmonic_le_one_add_log
(n :
ℕ
)
:
↑
(
harmonic
n
)
≤
1
+
Real.log
↑
n
source
theorem
log_le_harmonic_floor
(y :
ℝ
)
(hy :
0
≤
y
)
:
Real.log
y
≤
↑
(
harmonic
⌊
y
⌋₊
)
source
theorem
harmonic_floor_le_one_add_log
(y :
ℝ
)
(hy :
1
≤
y
)
:
↑
(
harmonic
⌊
y
⌋₊
)
≤
1
+
Real.log
y