From 8cdccc200ce043dca884d789c9a5936f804be58e Mon Sep 17 00:00:00 2001 From: Arend Mellendijk Date: Fri, 1 Mar 2024 13:29:39 +0000 Subject: [PATCH] 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 --- Mathlib.lean | 4 +- Mathlib/Algebra/Order/Field/Basic.lean | 47 ++++++++++++ Mathlib/NumberTheory/Harmonic/Bounds.lean | 71 +++++++++++++++++++ Mathlib/NumberTheory/Harmonic/Defs.lean | 40 +++++++++++ .../Harmonic.lean => Harmonic/Int.lean} | 19 +---- 5 files changed, 162 insertions(+), 19 deletions(-) create mode 100644 Mathlib/NumberTheory/Harmonic/Bounds.lean create mode 100644 Mathlib/NumberTheory/Harmonic/Defs.lean rename Mathlib/NumberTheory/{Padics/Harmonic.lean => Harmonic/Int.lean} (79%) diff --git a/Mathlib.lean b/Mathlib.lean index 92abcf5ddba15..5c6580391cea3 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -2908,6 +2908,9 @@ import Mathlib.NumberTheory.FLT.Four import Mathlib.NumberTheory.FermatPsp import Mathlib.NumberTheory.FrobeniusNumber import Mathlib.NumberTheory.FunctionField +import Mathlib.NumberTheory.Harmonic.Bounds +import Mathlib.NumberTheory.Harmonic.Defs +import Mathlib.NumberTheory.Harmonic.Int import Mathlib.NumberTheory.KummerDedekind import Mathlib.NumberTheory.LSeries.Basic import Mathlib.NumberTheory.LSeries.Convergence @@ -2947,7 +2950,6 @@ import Mathlib.NumberTheory.NumberField.Embeddings import Mathlib.NumberTheory.NumberField.FractionalIdeal import Mathlib.NumberTheory.NumberField.Norm import Mathlib.NumberTheory.NumberField.Units -import Mathlib.NumberTheory.Padics.Harmonic import Mathlib.NumberTheory.Padics.Hensel import Mathlib.NumberTheory.Padics.PadicIntegers import Mathlib.NumberTheory.Padics.PadicNorm diff --git a/Mathlib/Algebra/Order/Field/Basic.lean b/Mathlib/Algebra/Order/Field/Basic.lean index 90834becb8a5d..0bff91471eb23 100644 --- a/Mathlib/Algebra/Order/Field/Basic.lean +++ b/Mathlib/Algebra/Order/Field/Basic.lean @@ -791,6 +791,53 @@ theorem lt_inv_of_neg (ha : a < 0) (hb : b < 0) : a < b⁻¹ ↔ b < a⁻¹ := lt_iff_lt_of_le_iff_le (inv_le_of_neg hb ha) #align lt_inv_of_neg lt_inv_of_neg +/-! +### Monotonicity results involving inversion +-/ + + +theorem sub_inv_antitoneOn_Ioi : + AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Ioi c) := + antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦ + inv_le_inv (sub_pos.mpr hb) (sub_pos.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl + +theorem sub_inv_antitoneOn_Iio : + AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Iio c) := + antitoneOn_iff_forall_lt.mpr fun _ ha _ hb hab ↦ + inv_le_inv_of_neg (sub_neg.mpr hb) (sub_neg.mpr ha) |>.mpr <| sub_le_sub (le_of_lt hab) le_rfl + +theorem sub_inv_antitoneOn_Icc_right (ha : c < a) : + AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b) := by + by_cases hab : a ≤ b + · exact sub_inv_antitoneOn_Ioi.mono <| (Set.Icc_subset_Ioi_iff hab).mpr ha + · simp [hab, Set.Subsingleton.antitoneOn] + +theorem sub_inv_antitoneOn_Icc_left (ha : b < c) : + AntitoneOn (fun x ↦ (x-c)⁻¹) (Set.Icc a b) := by + by_cases hab : a ≤ b + · exact sub_inv_antitoneOn_Iio.mono <| (Set.Icc_subset_Iio_iff hab).mpr ha + · simp [hab, Set.Subsingleton.antitoneOn] + +theorem inv_antitoneOn_Ioi : + AntitoneOn (fun x:α ↦ x⁻¹) (Set.Ioi 0) := by + convert sub_inv_antitoneOn_Ioi + exact (sub_zero _).symm + +theorem inv_antitoneOn_Iio : + AntitoneOn (fun x:α ↦ x⁻¹) (Set.Iio 0) := by + convert sub_inv_antitoneOn_Iio + exact (sub_zero _).symm + +theorem inv_antitoneOn_Icc_right (ha : 0 < a) : + AntitoneOn (fun x:α ↦ x⁻¹) (Set.Icc a b) := by + convert sub_inv_antitoneOn_Icc_right ha + exact (sub_zero _).symm + +theorem inv_antitoneOn_Icc_left (hb : b < 0) : + AntitoneOn (fun x:α ↦ x⁻¹) (Set.Icc a b) := by + convert sub_inv_antitoneOn_Icc_left hb + exact (sub_zero _).symm + /-! ### Relating two divisions -/ diff --git a/Mathlib/NumberTheory/Harmonic/Bounds.lean b/Mathlib/NumberTheory/Harmonic/Bounds.lean new file mode 100644 index 0000000000000..dcd77a719e910 --- /dev/null +++ b/Mathlib/NumberTheory/Harmonic/Bounds.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2024 Arend Mellendijk. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Arend Mellendijk +-/ + +import Mathlib.Analysis.SpecialFunctions.Integrals +import Mathlib.Analysis.SumIntegralComparisons +import Mathlib.NumberTheory.Harmonic.Defs + +/-! + +This file proves $\log(n+1) \le H_n \le 1 + \log(n)$ for all natural numbers $n$. + +-/ + +open BigOperators + +theorem log_add_one_le_harmonic (n : ℕ) : + Real.log ↑(n+1) ≤ harmonic n := by + calc _ = ∫ x in (1:ℕ)..↑(n+1), x⁻¹ := ?_ + _ ≤ ∑ d in Finset.Icc 1 n, (d:ℝ)⁻¹ := ?_ + _ = harmonic n := ?_ + · rw [Nat.cast_one, integral_inv (by simp [(show ¬ (1 : ℝ) ≤ 0 by norm_num)]), div_one] + · exact (inv_antitoneOn_Icc_right <| by norm_num).integral_le_sum_Ico (Nat.le_add_left 1 n) + · simp only [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_coe_nat] + +theorem harmonic_le_one_add_log (n : ℕ) : + harmonic n ≤ 1 + Real.log n := by + by_cases hn0 : n = 0 + · simp [hn0] + have hn : 1 ≤ n := Nat.one_le_iff_ne_zero.mpr hn0 + simp_rw [harmonic_eq_sum_Icc, Rat.cast_sum, Rat.cast_inv, Rat.cast_coe_nat] + rw [← Finset.sum_erase_add (Finset.Icc 1 n) _ (Finset.left_mem_Icc.mpr hn), add_comm, + Nat.cast_one, inv_one] + refine add_le_add_left ?_ 1 + simp only [Nat.lt_one_iff, Finset.mem_Icc, Finset.Icc_erase_left] + calc ∑ d : ℕ in .Ico 2 (n + 1), (d : ℝ)⁻¹ + _ = ∑ d in .Ico 2 (n + 1), (↑(d + 1) - 1)⁻¹ := ?_ + _ ≤ ∫ x in (2).. ↑(n + 1), (x - 1)⁻¹ := ?_ + _ = ∫ x in (1)..n, x⁻¹ := ?_ + _ = Real.log ↑n := ?_ + · simp_rw [Nat.cast_add, Nat.cast_one, add_sub_cancel] + · exact @AntitoneOn.sum_le_integral_Ico 2 (n + 1) (fun x : ℝ ↦ (x - 1)⁻¹) (by linarith [hn]) <| + sub_inv_antitoneOn_Icc_right (by norm_num) + · convert intervalIntegral.integral_comp_sub_right _ 1 + · norm_num + · simp only [Nat.cast_add, Nat.cast_one, add_sub_cancel] + · convert integral_inv _ + · rw [div_one] + · simp only [Nat.one_le_cast, hn, Set.uIcc_of_le, Set.mem_Icc, Nat.cast_nonneg, + and_true, not_le, zero_lt_one] + +theorem log_le_harmonic_floor (y : ℝ) (hy : 0 ≤ y) : + Real.log y ≤ harmonic ⌊y⌋₊ := by + by_cases h0 : y = 0 + · simp [h0] + · calc + _ ≤ Real.log ↑(Nat.floor y + 1) := ?_ + _ ≤ _ := log_add_one_le_harmonic _ + gcongr + apply (Nat.le_ceil y).trans + norm_cast + exact Nat.ceil_le_floor_add_one y + +theorem harmonic_floor_le_one_add_log (y : ℝ) (hy : 1 ≤ y) : + harmonic ⌊y⌋₊ ≤ 1 + Real.log y := by + refine (harmonic_le_one_add_log _).trans ?_ + gcongr + · exact_mod_cast Nat.floor_pos.mpr hy + · exact Nat.floor_le <| zero_le_one.trans hy diff --git a/Mathlib/NumberTheory/Harmonic/Defs.lean b/Mathlib/NumberTheory/Harmonic/Defs.lean new file mode 100644 index 0000000000000..2bb005937373a --- /dev/null +++ b/Mathlib/NumberTheory/Harmonic/Defs.lean @@ -0,0 +1,40 @@ +/- +Copyright (c) 2023 Koundinya Vajjha. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Koundinya Vajjha, Thomas Browning +-/ + +import Mathlib.Algebra.BigOperators.Order +import Mathlib.Algebra.BigOperators.Intervals +import Mathlib.Tactic.Linarith +import Mathlib.Data.Nat.Interval + +/-! + +This file defines the harmonic numbers. + +* `Mathilb/NumberTheory/Harmonic/Int.lean` proves that the `n`th harmonic number is not an integer. +* `Mathlib/NumberTheory/Harmonic/Bounds.lean` provides basic log bounds. + +-/ + +open BigOperators + +/-- The nth-harmonic number defined as a finset sum of consecutive reciprocals. -/ +def harmonic : ℕ → ℚ := fun n => ∑ i in Finset.range n, (↑(i + 1))⁻¹ + +@[simp] +lemma harmonic_zero : harmonic 0 = 0 := + rfl + +@[simp] +lemma harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹ := + Finset.sum_range_succ .. + +lemma harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n := + Finset.sum_pos (fun _ _ => inv_pos.mpr (by norm_cast; linarith)) <| + Finset.nonempty_range_iff.mpr Hn + +lemma harmonic_eq_sum_Icc {n : ℕ} : harmonic n = ∑ i in Finset.Icc 1 n, (↑i)⁻¹ := by + rw [harmonic, Finset.range_eq_Ico, Finset.sum_Ico_add' (fun (i : ℕ) ↦ (i : ℚ)⁻¹) 0 n (c := 1), + Nat.Ico_succ_right] diff --git a/Mathlib/NumberTheory/Padics/Harmonic.lean b/Mathlib/NumberTheory/Harmonic/Int.lean similarity index 79% rename from Mathlib/NumberTheory/Padics/Harmonic.lean rename to Mathlib/NumberTheory/Harmonic/Int.lean index 61ad846e0031d..c46fc2774c456 100644 --- a/Mathlib/NumberTheory/Padics/Harmonic.lean +++ b/Mathlib/NumberTheory/Harmonic/Int.lean @@ -5,9 +5,9 @@ Authors: Koundinya Vajjha, Thomas Browning -/ import Mathlib.Algebra.CharP.Basic +import Mathlib.NumberTheory.Harmonic.Defs import Mathlib.NumberTheory.Padics.PadicNumbers - /-! 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 -/ -open BigOperators - -/-- The nth-harmonic number defined as a finset sum of consecutive reciprocals. -/ -def harmonic : ℕ → ℚ := fun n => ∑ i in Finset.range n, (↑(i + 1))⁻¹ - -@[simp] -lemma harmonic_zero : harmonic 0 = 0 := - rfl - -@[simp] -lemma harmonic_succ (n : ℕ) : harmonic (n + 1) = harmonic n + (↑(n + 1))⁻¹ := by - apply Finset.sum_range_succ - -lemma harmonic_pos {n : ℕ} (Hn : n ≠ 0) : 0 < harmonic n := - Finset.sum_pos (fun _ _ => inv_pos.mpr (by norm_cast; linarith)) - (by rwa [Finset.nonempty_range_iff]) - /-- The 2-adic valuation of the n-th harmonic number is the negative of the logarithm of n. -/ theorem padicValRat_two_harmonic (n : ℕ) : padicValRat 2 (harmonic n) = -Nat.log 2 n := by