English
The 2-adic norm of the nth harmonic number satisfies ||Hn||₂ = 2^{log₂ n} (for n ≠ 0).
Русский
2-адичная норма числа гармоники Hn равна 2^{log₂ n} (при n ≠ 0).
LaTeX
$$$\\\\|H_n\\\\|_2 = 2^{\\\\log_2 n}$$$
Lean4
/-- The 2-adic norm of the n-th harmonic number is 2 raised to the logarithm of n in base 2. -/
theorem padicNorm_two_harmonic {n : ℕ} (hn : n ≠ 0) : ‖(harmonic n : ℚ_[2])‖ = 2 ^ (Nat.log 2 n) := by
rw [Padic.eq_padicNorm, padicNorm.eq_zpow_of_nonzero (harmonic_pos hn).ne', padicValRat_two_harmonic, neg_neg,
zpow_natCast, Rat.cast_pow, Rat.cast_natCast, Nat.cast_ofNat]