Nat.factorization_choose_le_log
theorem Nat.factorization_choose_le_log : ∀ {p n k : ℕ}, (n.choose k).factorization p ≤ p.log n
This theorem provides an upper bound on the multiplicity of a prime number 'p' in a binomial coefficient 'n choose k'. Specifically, it states that the multiplicity of 'p' in 'n choose k' is less than or equal to the logarithm base 'p' of 'n'. This gives a logarithmic upper bound on how many times a prime number divides into a particular binomial coefficient.
More concisely: The multiplicity of a prime number p in the binomial coefficient n choose k is bounded by the logarithm base p of n.
|
Nat.le_two_mul_of_factorization_centralBinom_pos
theorem Nat.le_two_mul_of_factorization_centralBinom_pos :
∀ {p n : ℕ}, 0 < n.centralBinom.factorization p → p ≤ 2 * n
This theorem states that for any natural numbers `p` and `n`, if the factorization of the central binomial coefficient of `n` at `p` is positive, then `p` is less than or equal to twice `n`. In other words, if `p` is a factor that appears in the prime factorization of the central binomial coefficient of `n` (with non-zero multiplicity), then `p` cannot be greater than `2n`. The central binomial coefficient of `n` is the number of ways to choose `n` elements from a set of `2n` elements, denoted as $\binom{2n}{n}$ in combinatorics.
More concisely: If `p` is a factor of the central binomial coefficient of `n` with non-zero multiplicity, then `p` is at most 2 times `n`.
|
Nat.prod_pow_factorization_choose
theorem Nat.prod_pow_factorization_choose :
∀ (n k : ℕ), k ≤ n → ((Finset.range (n + 1)).prod fun p => p ^ (n.choose k).factorization p) = n.choose k := by
sorry
The theorem `Nat.prod_pow_factorization_choose` states that for any natural numbers `n` and `k` with `k` less than or equal to `n`, the product of each element `p` in the set of natural numbers less than `n + 1` raised to the power of the number of times `p` appears in the prime factorization of binomial coefficient `n.choose k`, is equal to the binomial coefficient `n.choose k` itself. In mathematical terms, for a fixed `n` and `k` in natural numbers, it verifies the equation $\prod_{p < n + 1} p^{(n \choose k) \text{.factorization}\, p} = {n \choose k}$. The prime factorization is considered with respect to a unique factorization monoid.
More concisely: For any natural numbers $n$ and $k$ with $k \leq n$, the product of each prime $p$ raised to the power of its exponent in the prime factorization of binomial coefficient $n \choose k$ equals $n \choose k$.
|
Nat.prod_pow_factorization_centralBinom
theorem Nat.prod_pow_factorization_centralBinom :
∀ (n : ℕ), ((Finset.range (2 * n + 1)).prod fun p => p ^ n.centralBinom.factorization p) = n.centralBinom := by
sorry
The theorem `Nat.prod_pow_factorization_centralBinom` states that for every natural number `n`, the `n`th central binomial coefficient is equal to the product of its prime factors raised to their respective powers, where the prime factors are less than or equal to `2n + 1`. In other words, it expresses the central binomial coefficient as the product over its prime factorization.
More concisely: The central binomial coefficient `n choose k` equals the product of `n`'s prime factors, each raised to the power of their multiplicity in `n`, where the prime factors are less than or equal to `2n + 1`.
|
Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul
theorem Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul :
∀ {p n : ℕ}, 2 < n → p ≤ n → 2 * n < 3 * p → n.centralBinom.factorization p = 0
This theorem states that for any natural numbers `p` and `n` where `n` is greater than 2, if `p` is less than or equal to `n` and `2 * n` is less than `3 * p`, then `p` does not appear in the factorization of the central binomial coefficient of `n`. In other words, any prime number that is greater than approximately `2 * n / 3` and less than `n` does not divide the central binomial coefficient of `n`.
More concisely: For natural numbers `p` and `n` with `n` > 2, if `p` <= `n` and `2 * n` < `3 * p`, then `p` does not divide the central binomial coefficient of `n`.
|
Nat.pow_factorization_choose_le
theorem Nat.pow_factorization_choose_le : ∀ {p n k : ℕ}, 0 < n → p ^ (n.choose k).factorization p ≤ n
The theorem `Nat.pow_factorization_choose_le` states that for any natural numbers `p`, `n`, and `k`, where `n` is greater than 0, the value of `p` raised to the power of the factorization of `n.choose k` (the binomial coefficient "n choose k") with respect to `p`, is less than or equal to `n`. In mathematical terms, this could be written as: for any p, n, k ∈ ℕ with n > 0, we have p^(factorization(n choose k)) ≤ n.
More concisely: For any natural numbers p, n, and k with n > 0, the value of p raised to the power of the factorization of the binomial coefficient n choose k is less than or equal to n. (p^(factorization(n choose k)) ≤ n)
|
Nat.factorization_choose_le_one
theorem Nat.factorization_choose_le_one : ∀ {p n k : ℕ}, n < p ^ 2 → (n.choose k).factorization p ≤ 1
This theorem states that for any given natural numbers `p`, `n` and `k`, if `n` is less than the square of `p`, then in the factorization of the binomial coefficient `n choose k`, the multiplicity of `p` is less than or equal to 1. In other words, primes greater than about the square root of `n` appear in the prime factorization of the binomial coefficient `n choose k` with a multiplicity of 0 or 1.
More concisely: For any natural numbers $p$, $n$, and $k$, if $n < p^2$, then the prime $p$ has multiplicity at most $1$ in the prime factorization of the binomial coefficient $\binom{n}{k}$.
|
Nat.factorization_centralBinom_eq_zero_of_two_mul_lt
theorem Nat.factorization_centralBinom_eq_zero_of_two_mul_lt :
∀ {p n : ℕ}, 2 * n < p → n.centralBinom.factorization p = 0
This theorem states that if a prime number `p` has a positive multiplicity in the `n`th central binomial coefficient, then `p` must not exceed `2 * n`. In other words, if the multiplicity of prime `p` is positive in the factorization of the `n`th central binomial coefficient, then the value of `p` should be less than twice `n`.
More concisely: A prime number `p` cannot have positive multiplicity in the `n`th central binomial coefficient if `p > 2 * n`.
|