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>

Mathlib.lean

@@ -2909,6 +2909,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
@@ -2948,7 +2951,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

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 -/
 
 

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

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]

Mathlib/NumberTheory/Padics/Harmonic.lean → 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