[Merged by Bors] - feat: the n-th harmonic number is not an integer for n > 1.

Mathlib.lean

@@ -2609,6 +2609,7 @@ import Mathlib.NumberTheory.NumberField.Discriminant
 import Mathlib.NumberTheory.NumberField.Embeddings
 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/Data/Finset/Basic.lean

@@ -2325,6 +2325,12 @@ theorem sdiff_singleton_eq_self (ha : a ∉ s) : s \ {a} = s :=
   sdiff_eq_self_iff_disjoint.2 <| by simp [ha]
 #align finset.sdiff_singleton_eq_self Finset.sdiff_singleton_eq_self
 
+theorem Nontrivial.sdiff_singleton_nonempty {c : α} {s : Finset α} (hS : s.Nontrivial) :
+    (s \ {c}).Nonempty := by
+  rw [Finset.sdiff_nonempty, Finset.subset_singleton_iff]
+  push_neg
+  exact ⟨by rintro rfl; exact Finset.not_nontrivial_empty hS, hS.ne_singleton⟩
+
 theorem sdiff_sdiff_left' (s t u : Finset α) : (s \ t) \ u = s \ t ∩ (s \ u) :=
   _root_.sdiff_sdiff_left'
 #align finset.sdiff_sdiff_left' Finset.sdiff_sdiff_left'
@@ -3103,6 +3109,10 @@ theorem range_filter_eq {n m : ℕ} : (range n).filter (· = m) = if m < n then
   · simp
 #align finset.range_filter_eq Finset.range_filter_eq
 
+lemma range_nontrivial {n : ℕ} (hn : 1 < n) : (Finset.range n).Nontrivial := by
+  rw [Finset.Nontrivial, Finset.coe_range]
+  exact ⟨0, zero_lt_one.trans hn, 1, hn, zero_ne_one⟩
+
 end Range
 
 -- useful rules for calculations with quantifiers

Mathlib/Data/Rat/Defs.lean

@@ -511,6 +511,10 @@ theorem coe_int_num_of_den_eq_one {q : ℚ} (hq : q.den = 1) : (q.num : ℚ) = q
   rfl
 #align rat.coe_int_num_of_denom_eq_one Rat.coe_int_num_of_den_eq_one
 
+lemma eq_num_of_isInt {q : ℚ} (h : q.isInt) : q = q.num := by
+  rw [Rat.isInt, Nat.beq_eq_true_eq] at h
+  exact (Rat.coe_int_num_of_den_eq_one h).symm
+
 theorem den_eq_one_iff (r : ℚ) : r.den = 1 ↔ ↑r.num = r :=
   ⟨Rat.coe_int_num_of_den_eq_one, fun h => h ▸ Rat.coe_int_den r.num⟩
 #align rat.denom_eq_one_iff Rat.den_eq_one_iff

Mathlib/NumberTheory/Padics/Harmonic.lean

@@ -0,0 +1,57 @@
+/-
+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.NumberTheory.Padics.PadicIntegers
+import Mathlib.Data.Int.Log
+/-!
+
+The nth Harmonic number is not an integer. We formalize the proof using
+2-adic valuations. This proof is due to Kürschák.
+
+Reference:
+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
+  induction' n with n ih
+  · simp
+  · rcases eq_or_ne n 0 with rfl | hn
+    · simp
+    rw [harmonic_succ]
+    have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹
+    · rw [ih, padicValRat.inv, padicValRat.of_nat, Ne, neg_inj, Nat.cast_inj]
+      exact Nat.log_ne_padicValNat_succ hn
+    rw [padicValRat.add_eq_min (harmonic_succ n ▸ (harmonic_pos n.succ_ne_zero).ne')
+        (harmonic_pos hn).ne' (inv_ne_zero (Nat.cast_ne_zero.mpr n.succ_ne_zero)) key, ih,
+        padicValRat.inv, padicValRat.of_nat, min_neg_neg, neg_inj, ← Nat.cast_max, Nat.cast_inj]
+    exact Nat.max_log_padicValNat_succ_eq_log_succ n
+
+/-- The n-th harmonic number is not an integer for n ≥ 2. -/
+theorem harmonic_not_int {n : ℕ} (h : 2 ≤ n) : ¬ (harmonic n).isInt := by
+  apply padicNorm.not_int_of_not_padic_int 2
+  rw [padicNorm.eq_zpow_of_nonzero (harmonic_pos (ne_zero_of_lt h)).ne',
+      padicValRat_two_harmonic, neg_neg, zpow_coe_nat]
+  exact one_lt_pow one_lt_two (Nat.log_pos one_lt_two h).ne'

Mathlib/NumberTheory/Padics/PadicNorm.lean

@@ -305,6 +305,13 @@ theorem nat_lt_one_iff (m : ℕ) : padicNorm p m < 1 ↔ p ∣ m := by
   rw [← Int.coe_nat_dvd, ← int_lt_one_iff, Int.cast_ofNat]
 #align padic_norm.nat_lt_one_iff padicNorm.nat_lt_one_iff
 
+/-- If a rational is not a p-adic integer, it is not an integer. -/
+theorem not_int_of_not_padic_int (p : ℕ) {a : ℚ} [hp : Fact (Nat.Prime p)]
+    (H : 1 < padicNorm p a) : ¬ a.isInt := by
+  contrapose! H
+  rw [Rat.eq_num_of_isInt H]
+  apply padicNorm.of_int
+
 open BigOperators
 
 theorem sum_lt {α : Type*} {F : α → ℚ} {t : ℚ} {s : Finset α} :

Mathlib/NumberTheory/Padics/PadicVal.lean

@@ -202,6 +202,10 @@ def padicValRat (p : ℕ) (q : ℚ) : ℤ :=
   padicValInt p q.num - padicValNat p q.den
 #align padic_val_rat padicValRat
 
+lemma padicValRat_def (p : ℕ) (q : ℚ) :
+    padicValRat p q = padicValInt p q.num - padicValNat p q.den :=
+  rfl
+
 namespace padicValRat
 
 open multiplicity
@@ -431,6 +435,38 @@ theorem min_le_padicValRat_add {q r : ℚ} (hqr : q + r ≠ 0) :
   (fun h => by rw [min_eq_right h, add_comm]; exact le_padicValRat_add_of_le (by rwa [add_comm]) h)
 #align padic_val_rat.min_le_padic_val_rat_add padicValRat.min_le_padicValRat_add
 
+/-- Ultrametric property of a p-adic valuation. -/
+lemma add_eq_min {q r : ℚ} (hqr : q + r ≠ 0) (hq : q ≠ 0) (hr : r ≠ 0)
+    (hval : padicValRat p q ≠ padicValRat p r) :
+    padicValRat p (q + r) = min (padicValRat p q) (padicValRat p r) := by
+  have h1 := min_le_padicValRat_add (p := p) hqr
+  have h2 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right q r) hq)
+  have h3 := min_le_padicValRat_add (p := p) (ne_of_eq_of_ne (add_neg_cancel_right r q) hr)
+  rw [add_neg_cancel_right, padicValRat.neg] at h2 h3
+  rw [add_comm] at h3
+  refine' le_antisymm (le_min _ _) h1
+  · contrapose! h2
+    rw [min_eq_right h2.le] at h3
+    exact lt_min h2 (lt_of_le_of_ne h3 hval)
+  · contrapose! h3
+    rw [min_eq_right h3.le] at h2
+    exact lt_min h3 (lt_of_le_of_ne h2 hval.symm)
+
+lemma add_eq_of_lt {q r : ℚ} (hqr : q + r ≠ 0)
+    (hq : q ≠ 0) (hr : r ≠ 0) (hval : padicValRat p q < padicValRat p r) :
+    padicValRat p (q + r) = padicValRat p q := by
+  rw [add_eq_min hqr hq hr (ne_of_lt hval), min_eq_left (le_of_lt hval)]
+
+lemma lt_add_of_lt {q r₁ r₂ : ℚ} (hqr : r₁ + r₂ ≠ 0)
+    (hval₁ : padicValRat p q < padicValRat p r₁) (hval₂ : padicValRat p q < padicValRat p r₂) :
+    padicValRat p q < padicValRat p (r₁ + r₂) :=
+  lt_of_lt_of_le (lt_min hval₁ hval₂) (padicValRat.min_le_padicValRat_add hqr)
+
+@[simp]
+lemma self_pow_inv (r : ℕ) : padicValRat p ((p : ℚ) ^ r)⁻¹ = -r := by
+  rw [padicValRat.inv, neg_inj, padicValRat.pow (Nat.cast_ne_zero.mpr hp.elim.ne_zero),
+      padicValRat.self hp.elim.one_lt, mul_one]
+
 open BigOperators
 
 /-- A finite sum of rationals with positive `p`-adic valuation has positive `p`-adic valuation
@@ -448,6 +484,20 @@ theorem sum_pos_of_pos {n : ℕ} {F : ℕ → ℚ} (hF : ∀ i, i < n → 0 < pa
         exact hF _ (lt_trans hi (lt_add_one _))
 #align padic_val_rat.sum_pos_of_pos padicValRat.sum_pos_of_pos
 
+/-- If the p-adic valuation of a finite set of positive rationals is greater than a given rational
+number, then the p-adic valuation of their sum is also greater than the same rational number. -/
+theorem lt_sum_of_lt {p j : ℕ} [hp : Fact (Nat.Prime p)] {F : ℕ → ℚ} {S : Finset ℕ}
+    (hS : S.Nonempty) (hF : ∀ i, i ∈ S → padicValRat p (F j) < padicValRat p (F i))
+    (hn1 : ∀ i : ℕ, 0 < F i) : padicValRat p (F j) < padicValRat p (∑ i in S, F i) := by
+  induction' hS using Finset.Nonempty.cons_induction with k s S' Hnot Hne Hind
+  · rw [Finset.sum_singleton]
+    exact hF k (by simp)
+  · rw [Finset.cons_eq_insert, Finset.sum_insert Hnot]
+    exact padicValRat.lt_add_of_lt
+      (ne_of_gt (add_pos (hn1 s) (Finset.sum_pos (fun i _ => hn1 i) Hne)))
+      (hF _ (by simp [Finset.mem_insert, true_or]))
+      (Hind (fun i hi => hF _ (by rw [Finset.cons_eq_insert,Finset.mem_insert]; exact Or.inr hi)))
+
 end padicValRat
 
 namespace padicValNat
@@ -535,6 +585,40 @@ theorem padicValNat_primes {q : ℕ} [hp : Fact p.Prime] [hq : Fact q.Prime] (ne
     (not_congr (Iff.symm (prime_dvd_prime_iff_eq hp.1 hq.1))).mp neq
 #align padic_val_nat_primes padicValNat_primes
 
+/-- The p-adic valuation of `n` is less than or equal to its logarithm w.r.t `p`.-/
+lemma padicValNat_le_nat_log (n : ℕ) : padicValNat p n ≤ Nat.log p n := by
+  rcases n with _ | n
+  · simp
+  rcases p with _ | _ | p
+  · simp
+  · simp
+  exact Nat.le_log_of_pow_le p.one_lt_succ_succ (le_of_dvd n.succ_pos pow_padicValNat_dvd)
+
+/-- The p-adic valuation of `n` is equal to the logarithm w.r.t `p` iff
+    `n` is less than `p` raised to one plus the p-adic valuation of `n`. -/
+lemma nat_log_eq_padicValNat_iff {n : ℕ} [hp : Fact (Nat.Prime p)] (hn : 0 < n) :
+    Nat.log p n = padicValNat p n ↔ n < p ^ (padicValNat p n + 1) := by
+  rw [Nat.log_eq_iff (Or.inr ⟨(Nat.Prime.one_lt' p).out, by linarith⟩), and_iff_right_iff_imp]
+  exact (fun _ => Nat.le_of_dvd hn pow_padicValNat_dvd)
+
+lemma Nat.log_ne_padicValNat_succ {n : ℕ} (hn : n ≠ 0) : log 2 n ≠ padicValNat 2 (n + 1) := by
+  rw [Ne, log_eq_iff (by simp [hn])]
+  rintro ⟨h1, h2⟩
+  rw [← lt_add_one_iff, ← mul_one (2 ^ _)] at h1
+  rw [← add_one_le_iff, pow_succ] at h2
+  refine' not_dvd_of_between_consec_multiples h1 (lt_of_le_of_ne' h2 _) pow_padicValNat_dvd
+  exact pow_succ_padicValNat_not_dvd n.succ_ne_zero ∘ dvd_of_eq
+
+lemma Nat.max_log_padicValNat_succ_eq_log_succ (n : ℕ) :
+    max (log 2 n) (padicValNat 2 (n + 1)) = log 2 (n + 1) := by
+  apply le_antisymm (max_le (le_log_of_pow_le one_lt_two (pow_log_le_add_one 2 n))
+    (padicValNat_le_nat_log (n + 1)))
+  rw [le_max_iff, or_iff_not_imp_left, not_le]
+  intro h
+  replace h := le_antisymm (add_one_le_iff.mpr (lt_pow_of_log_lt one_lt_two h))
+    (pow_log_le_self 2 n.succ_ne_zero)
+  rw [h, padicValNat.prime_pow, ← h]
+
 open BigOperators
 
 theorem range_pow_padicValNat_subset_divisors {n : ℕ} (hn : n ≠ 0) :