English
The 2-adic valuation of the nth harmonic number equals the negative base-2 logarithm of n: v2(Hn) = - log2 n.
Русский
2-адичная оценка гармонического числа Hn равна минус логарифм по основанию 2 от n: v2(Hn) = - log2 n.
LaTeX
$$$v_2(H_n) = -\\\\log_2 n$$$
Lean4
/-- 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
| zero => simp
| succ n ih =>
rcases eq_or_ne n 0 with rfl | hn
· simp
rw [harmonic_succ]
have key : padicValRat 2 (harmonic n) ≠ padicValRat 2 (↑(n + 1))⁻¹ :=
by
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
