Skip to content

Commit 57e3f1d

Browse files
FLDutchmannFLDutchmann
committed
feat: explicit logarithmic bounds on the harmonic numbers (#9984)
Prove $\log(n+1) \le H_n \le 1 + \log(n)$ for all natural numbers $n$. There is an existing proof that $H_n$ is not an integer which uses p-adics. Since the new result uses some heavy machinery that is disjoint from the existing proof, the file is split into three parts to keep the dependencies lighter. See [zulip](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/basic.20log.20bounds.20on.20harmonic.20sums) Co-authored-by: Arend Mellendijk <FLDutchmann@users.noreply.github.com>
1 parent 92c93d7 commit 57e3f1d

File tree

5 files changed

+162
-19
lines changed

5 files changed

+162
-19
lines changed

‎Mathlib.lean‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2907,6 +2907,9 @@ import Mathlib.NumberTheory.FLT.Four
29072907
import Mathlib.NumberTheory.FermatPsp
29082908
import Mathlib.NumberTheory.FrobeniusNumber
29092909
import Mathlib.NumberTheory.FunctionField
2910+
import Mathlib.NumberTheory.Harmonic.Bounds
2911+
import Mathlib.NumberTheory.Harmonic.Defs
2912+
import Mathlib.NumberTheory.Harmonic.Int
29102913
import Mathlib.NumberTheory.KummerDedekind
29112914
import Mathlib.NumberTheory.LSeries.Basic
29122915
import Mathlib.NumberTheory.LSeries.Convergence
@@ -2946,7 +2949,6 @@ import Mathlib.NumberTheory.NumberField.Embeddings
29462949
import Mathlib.NumberTheory.NumberField.FractionalIdeal
29472950
import Mathlib.NumberTheory.NumberField.Norm
29482951
import Mathlib.NumberTheory.NumberField.Units
2949-
import Mathlib.NumberTheory.Padics.Harmonic
29502952
import Mathlib.NumberTheory.Padics.Hensel
29512953
import Mathlib.NumberTheory.Padics.PadicIntegers
29522954
import Mathlib.NumberTheory.Padics.PadicNorm

‎Mathlib/Algebra/Order/Field/Basic.lean‎

Lines changed: 47 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -791,6 +791,53 @@ theorem lt_inv_of_neg (ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹ :=
791791
lt_iff_lt_of_le_iff_le (inv_le_of_neg hb ha)
792792
#align lt_inv_of_neg lt_inv_of_neg
793793

794+
/-!
795+
### Monotonicity results involving inversion
796+
-/
797+
798+
799+
theorem sub_inv_antitoneOn_Ioi :
800+
AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Ioi c) :=
801+
antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
802+
inv_le_inv (sub_pos.mpr hb) (sub_pos.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl
803+
804+
theorem sub_inv_antitoneOn_Iio :
805+
AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Iio c) :=
806+
antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦
807+
inv_le_inv_of_neg (sub_neg.mpr hb) (sub_neg.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl
808+
809+
theorem sub_inv_antitoneOn_Icc_right (ha : c < a) :
810+
AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b) := by
811+
by_cases hab : a ≤ b
812+
· exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha
813+
· simp [hab, Set.Subsingleton.antitoneOn]
814+
815+
theorem sub_inv_antitoneOn_Icc_left (ha : b < c) :
816+
AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b) := by
817+
by_cases hab : a ≤ b
818+
· exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha
819+
· simp [hab, Set.Subsingleton.antitoneOn]
820+
821+
theorem inv_antitoneOn_Ioi :
822+
AntitoneOn (fun x:α ↦ x⁻¹) (Set.Ioi 0) := by
823+
convert sub_inv_antitoneOn_Ioi
824+
exact (sub_zero _).symm
825+
826+
theorem inv_antitoneOn_Iio :
827+
AntitoneOn (fun x:α ↦ x⁻¹) (Set.Iio 0) := by
828+
convert sub_inv_antitoneOn_Iio
829+
exact (sub_zero _).symm
830+
831+
theorem inv_antitoneOn_Icc_right (ha : 0 < a) :
832+
AntitoneOn (fun x:α ↦ x⁻¹) (Set.Icc a b) := by
833+
convert sub_inv_antitoneOn_Icc_right ha
834+
exact (sub_zero _).symm
835+
836+
theorem inv_antitoneOn_Icc_left (hb : b < 0) :
837+
AntitoneOn (fun x:α ↦ x⁻¹) (Set.Icc a b) := by
838+
convert sub_inv_antitoneOn_Icc_left hb
839+
exact (sub_zero _).symm
840+
794841
/-! ### Relating two divisions -/
795842

796843

‎Mathlib/NumberTheory/Harmonic/Bounds.lean‎

Lines changed: 71 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,71 @@
1+
/-
2+
Copyright (c) 2024 Arend Mellendijk. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Arend Mellendijk
5+
-/
6+
7+
import Mathlib.Analysis.SpecialFunctions.Integrals
8+
import Mathlib.Analysis.SumIntegralComparisons
9+
import Mathlib.NumberTheory.Harmonic.Defs
10+
11+
/-!
12+
13+
This file proves $\log(n+1) \le H_n \le 1 + \log(n)$ for all natural numbers $n$.
14+
15+
-/
16+
17+
open BigOperators
18+
19+
theorem log_add_one_le_harmonic (n : ℕ) :
20+
Real.log ↑(n+1) ≤ harmonic n := by
21+
calc _ = ∫ x in (1:ℕ)..↑(n+1), x⁻¹ := ?_
22+
_ ≤ ∑ d in Finset.Icc 1 n, (d:ℝ)⁻¹ := ?_
23+
_ = harmonic n := ?_
24+
· rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by norm_num)]), div_one]
25+
· exact (inv_antitoneOn_Icc_right <| by norm_num).integral_le_sum_Ico (Nat.le_add_left 1 n)
26+
· simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_coe_nat]
27+
28+
theorem harmonic_le_one_add_log (n : ℕ) :
29+
harmonic n ≤ 1 + Real.log n := by
30+
by_cases hn0 : n = 0
31+
· simp [hn0]
32+
have hn : 1 ≤ n := Nat.one_le_iff_ne_zero.mpr hn0
33+
simp_rw [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_coe_nat]
34+
rw [← Finset.sum_erase_add (Finset.Icc 1 n) _ (Finset.left_mem_Icc.mpr hn), add_comm,
35+
Nat.cast_one, inv_one]
36+
refine add_le_add_left ?_ 1
37+
simp only [Nat.lt_one_iff, Finset.mem_Icc, Finset.Icc_erase_left]
38+
calc ∑ d : ℕ in .Ico 2 (n + 1), (d : ℝ)⁻¹
39+
_ = ∑ d in .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_
40+
_ ≤ ∫ x in (2).. ↑(n + 1), (x - 1)⁻¹ := ?_
41+
_ = ∫ x in (1)..n, x⁻¹ := ?_
42+
_ = Real.log ↑n := ?_
43+
· simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel]
44+
· exact @AntitoneOn.sum_le_integral_Ico 2 (n + 1) (fun x : ℝ ↦ (x - 1)⁻¹) (by linarith [hn]) <|
45+
sub_inv_antitoneOn_Icc_right (by norm_num)
46+
· convert intervalIntegral.integral_comp_sub_right _ 1
47+
· norm_num
48+
· simp only [Nat.cast_add, Nat.cast_one, add_sub_cancel]
49+
· convert integral_inv _
50+
· rw [div_one]
51+
· simp only [Nat.one_le_cast, hn, Set.uIcc_of_le, Set.mem_Icc, Nat.cast_nonneg,
52+
and_true, not_le, zero_lt_one]
53+
54+
theorem log_le_harmonic_floor (y : ℝ) (hy : 0 ≤ y) :
55+
Real.log y ≤ harmonic ⌊y⌋₊ := by
56+
by_cases h0 : y = 0
57+
· simp [h0]
58+
· calc
59+
_ ≤ Real.log ↑(Nat.floor y + 1) := ?_
60+
_ ≤ _ := log_add_one_le_harmonic _
61+
gcongr
62+
apply (Nat.le_ceil y).trans
63+
norm_cast
64+
exact Nat.ceil_le_floor_add_one y
65+
66+
theorem harmonic_floor_le_one_add_log (y : ℝ) (hy : 1 ≤ y) :
67+
harmonic ⌊y⌋₊ ≤ 1 + Real.log y := by
68+
refine (harmonic_le_one_add_log _).trans ?_
69+
gcongr
70+
· exact_mod_cast Nat.floor_pos.mpr hy
71+
· exact Nat.floor_le <| zero_le_one.trans hy

‎Mathlib/NumberTheory/Harmonic/Defs.lean‎

Lines changed: 40 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,40 @@
1+
/-
2+
Copyright (c) 2023 Koundinya Vajjha. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Koundinya Vajjha, Thomas Browning
5+
-/
6+
7+
import Mathlib.Algebra.BigOperators.Order
8+
import Mathlib.Algebra.BigOperators.Intervals
9+
import Mathlib.Tactic.Linarith
10+
import Mathlib.Data.Nat.Interval
11+
12+
/-!
13+
14+
This file defines the harmonic numbers.
15+
16+
* `Mathilb/NumberTheory/Harmonic/Int.lean` proves that the `n`th harmonic number is not an integer.
17+
* `Mathlib/NumberTheory/Harmonic/Bounds.lean` provides basic log bounds.
18+
19+
-/
20+
21+
open BigOperators
22+
23+
/-- The nth-harmonic number defined as a finset sum of consecutive reciprocals. -/
24+
def harmonic : ℕ → ℚ := fun n => ∑ i in Finset.range n, (↑(i + 1))⁻¹
25+
26+
@[simp]
27+
lemma harmonic_zero : harmonic 0 = 0 :=
28+
rfl
29+
30+
@[simp]
31+
lemma harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹ :=
32+
Finset.sum_range_succ ..
33+
34+
lemma harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n :=
35+
Finset.sum_pos (fun _ _ => inv_pos.mpr (by norm_cast; linarith)) <|
36+
Finset.nonempty_range_iff.mpr Hn
37+
38+
lemma harmonic_eq_sum_Icc {n : ℕ} : harmonic n = ∑ i in Finset.Icc 1 n, (↑i)⁻¹ := by
39+
rw [harmonic, Finset.range_eq_Ico, Finset.sum_Ico_add' (fun (i : ℕ) ↦ (i : ℚ)⁻¹) 0 n (c := 1),
40+
Nat.Ico_succ_right]

‎Mathlib/NumberTheory/Padics/Harmonic.lean‎ renamed to ‎Mathlib/NumberTheory/Harmonic/Int.lean‎

Lines changed: 1 addition & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ Authors: Koundinya Vajjha, Thomas Browning
55
-/
66

77
import Mathlib.Algebra.CharP.Basic
8+
import Mathlib.NumberTheory.Harmonic.Defs
89
import Mathlib.NumberTheory.Padics.PadicNumbers
910

10-
1111
/-!
1212
1313
The nth Harmonic number is not an integer. We formalize the proof using
@@ -18,23 +18,6 @@ https://kconrad.math.uconn.edu/blurbs/gradnumthy/padicharmonicsum.pdf
1818
1919
-/
2020

21-
open BigOperators
22-
23-
/-- The nth-harmonic number defined as a finset sum of consecutive reciprocals. -/
24-
def harmonic : ℕ → ℚ := fun n => ∑ i in Finset.range n, (↑(i + 1))⁻¹
25-
26-
@[simp]
27-
lemma harmonic_zero : harmonic 0 = 0 :=
28-
rfl
29-
30-
@[simp]
31-
lemma harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹ := by
32-
apply Finset.sum_range_succ
33-
34-
lemma harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n :=
35-
Finset.sum_pos (fun _ _ => inv_pos.mpr (by norm_cast; linarith))
36-
(by rwa [Finset.nonempty_range_iff])
37-
3821
/-- The 2-adic valuation of the n-th harmonic number is the negative of the logarithm
3922
of n. -/
4023
theorem padicValRat_two_harmonic (n : ℕ) : padicValRat 2 (harmonic n) = -Nat.log 2 n := by

0 commit comments

Comments
 (0)