harmonic_not_int
theorem harmonic_not_int : ∀ {n : ℕ}, 2 ≤ n → ¬(harmonic n).isInt = true
The theorem states that the n-th harmonic number is not an integer for any n that is greater than or equal to 2. In other words, when we calculate the n-th harmonic number - defined as the sum of the reciprocals of all the natural numbers up to n - the resulting value will never be an integer if n is 2 or more.
More concisely: The n-th harmonic number, being the sum of the reciprocal of the first n natural numbers, is not an integer for any n ≥ 2.
|
padicValRat_two_harmonic
theorem padicValRat_two_harmonic : ∀ (n : ℕ), padicValRat 2 (harmonic n) = -↑(Nat.log 2 n)
This theorem states that for every natural number `n`, the 2-adic valuation of the nth harmonic number is equal to the negative of the logarithm base 2 of `n`. The nth harmonic number is defined as the sum of the reciprocals of the natural numbers up to `n`, and the 2-adic valuation of a rational number is defined as the difference between the 2-adic valuations of its numerator and denominator. The logarithm base 2 of `n` is the maximum power of 2 that does not exceed `n`.
More concisely: For every natural number `n`, the 2-adic valuation of the nth harmonic number is equal to the negative of the maximum logarithm base 2 of `n`.
|
padicNorm_two_harmonic
theorem padicNorm_two_harmonic : ∀ {n : ℕ}, n ≠ 0 → ‖↑(harmonic n)‖ = 2 ^ Nat.log 2 n
This theorem states that for any natural number `n` that is not equal to zero, the 2-adic norm of the `n`-th harmonic number is equal to 2 raised to the power of the logarithm of `n` in base 2. In mathematical terms, if `n` is a non-zero natural number and `H_n` denotes the `n`-th harmonic number (defined as the sum of reciprocal of the first `n` natural numbers), then the 2-adic norm of `H_n` is `2^log_2(n)`. The 2-adic norm of a number refers to the highest power of 2 that divides the number, and `log_2(n)` refers to the highest power of 2 that is less than or equal to `n`.
More concisely: For any non-zero natural number `n`, the 2-adic norm of the `n`-th harmonic number `H_n` equals 2 raised to the power of the logarithm of `n` in base 2. That is, `norm_2(H_n) = 2^log_2(n)`.
|