padicNorm_two_harmonic — Mathlib

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]

Похожие утверждения