ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on
theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on :
∀ {R : Type u_1} [inst : AddCommGroup R] {f g : ℕ → R} (s : Set ℕ),
(∀ (m n : ℕ), m ∣ n → n ∈ s → m ∈ s) →
((∀ n > 0, n ∈ s → (n.divisors.sum fun i => f i) = g n) ↔
∀ n > 0, n ∈ s → (n.divisorsAntidiagonal.sum fun x => ArithmeticFunction.moebius x.1 • g x.2) = f n)
This theorem, named `ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on`, is about the Möbius inversion principle for functions mapping to an additive commutative group (denoted by `R`), but the principle only holds on a well-behaved set (`s`).
For given functions `f` and `g` from natural numbers to `R`, and a set `s` of natural numbers which is 'closed' under divisors (i.e., if `m` divides `n` and `n` is in `s`, then `m` must also be in `s`), the theorem states the following:
The condition that, for every natural number `n` greater than zero in the set `s`, the sum of `f` over the divisors of `n` equals `g(n)`, is equivalent to the condition that, for every such `n`, the sum over the divisors' antidiagonal of the Möbius function applied to the first element of the antidiagonal pair, scaled by `g` applied to the second element of the pair, equals `f(n)`.
In other words, it provides a way of 'inverting' the operation of summing a function over the divisors of a number, using the Möbius function. The term 'antidiagonal' refers to pairs of numbers (`x`, `y`) such that `x * y = n`.
More concisely: For functions `f` and `g` from natural numbers to an additive commutative group, and a set `s` of natural numbers closed under divisors, the sum of `f` over the divisors of each `n` in `s` equals `g(n)` if and only if the sum of the Möbius function scaled by `g` over the antidiagonals of `s` equals `f`.
|
ArithmeticFunction.zeta_apply_ne
theorem ArithmeticFunction.zeta_apply_ne : ∀ {x : ℕ}, x ≠ 0 → ArithmeticFunction.zeta x = 1
The theorem `ArithmeticFunction.zeta_apply_ne` states that for any natural number `x`, as long as `x` is not equal to zero, the value of the function `ArithmeticFunction.zeta` at `x` is equal to one. This is a characteristic of the Dirichlet Series, also known as the Riemann `ζ` function, where the function value is `1` for any non-zero natural number.
More concisely: For any natural number `x` unequal to zero, `ArithmeticFunction.zeta x = 1`.
|
ArithmeticFunction.ext
theorem ArithmeticFunction.ext :
∀ {R : Type u_1} [inst : Zero R] ⦃f g : ArithmeticFunction R⦄, (∀ (x : ℕ), f x = g x) → f = g
This theorem states that for any type `R` which has a zero element, if `f` and `g` are arithmetic functions from natural numbers to `R` (meaning they map 0 to 0), then `f` and `g` are identical if and only if they assign the same value to each natural number. In other words, two arithmetic functions are considered equal if they produce the same output for every natural number input.
More concisely: For any type `R` with a zero element, two arithmetic functions `f` and `g` from natural numbers to `R` are equal if and only if they agree on all natural numbers, i.e., `∀n, f n = g n`.
|
ArithmeticFunction.IsMultiplicative.iff_ne_zero
theorem ArithmeticFunction.IsMultiplicative.iff_ne_zero :
∀ {R : Type u_1} [inst : MonoidWithZero R] {f : ArithmeticFunction R},
f.IsMultiplicative ↔ f 1 = 1 ∧ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → f (m * n) = f m * f n
The theorem named `ArithmeticFunction.IsMultiplicative.iff_ne_zero` states that for any arithmetic function `f` mapping natural numbers to an algebraic structure of type `R` equipped with a `MonoidWithZero` instance, `f` is multiplicative if and only if `f` maps the number 1 to 1 and for any two non-zero natural numbers `m` and `n` that are coprime (their greatest common divisor is 1), the value of `f` at the product `m * n` equals the product of the values of `f` at `m` and `n`. This theorem essentially provides an equivalent definition for a multiplicative arithmetic function that is more convenient for certain proofs.
More concisely: An arithmetic function is multiplicative if and only if it maps the number 1 to 1 and the product of two coprime natural numbers to the product of the function values at those numbers.
|
ArithmeticFunction.IsMultiplicative.map_mul_of_coprime
theorem ArithmeticFunction.IsMultiplicative.map_mul_of_coprime :
∀ {R : Type u_1} [inst : MonoidWithZero R] {f : ArithmeticFunction R},
f.IsMultiplicative → ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
The theorem `ArithmeticFunction.IsMultiplicative.map_mul_of_coprime` states that for any type `R` equipped with the structure of a `MonoidWithZero` and an arithmetic function `f` on `R` which is multiplicative, if `m` and `n` are two natural numbers that are coprime (i.e., their greatest common divisor is 1), then the value of the function at the product `m * n` equals the product of the function's values at `m` and `n`. This theorem is an important property for multiplicative arithmetic functions in number theory.
More concisely: For any coprime natural numbers m and n and multiplicative arithmetic function f on a MonoidWithZero R, f (m * n) = f(m) * f(n).
|
ArithmeticFunction.ppow_zero
theorem ArithmeticFunction.ppow_zero :
∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R}, f.ppow 0 = ↑ArithmeticFunction.zeta
This theorem states that for any semiring `R` and any arithmetic function `f` from natural numbers to `R`, the pointwise power of `f` with an exponent of 0 is equal to the Dirichlet series (also known as the Riemann zeta function). In other words, when an arithmetic function is raised to the power of 0, the resulting function is a function that maps all non-zero natural numbers to 1 and 0 to 0, which is the behavior of the Riemann zeta function.
More concisely: For any semiring `R` and arithmetic function `f` from natural numbers to `R`, the pointwise power `f^0` is the Dirichlet series of `f` (Riemann zeta function) which maps all non-zero natural numbers to 1 and 0 to 0.
|
ArithmeticFunction.mul_apply
theorem ArithmeticFunction.mul_apply :
∀ {R : Type u_1} [inst : Semiring R] {f g : ArithmeticFunction R} {n : ℕ},
(f * g) n = n.divisorsAntidiagonal.sum fun x => f x.1 * g x.2
The theorem `ArithmeticFunction.mul_apply` states that for any semiring `R` and any two arithmetic functions `f` and `g` from natural numbers into `R`, the value of the product of `f` and `g` at any natural number `n` is equal to the sum over the divisor antidiagonal of `n` of the products of the values of `f` at the first element of the pair and `g` at the second element of the pair. Here, the divisor antidiagonal of `n` is the set of pairs of natural numbers whose product is `n`.
More concisely: For any semiring R and arithmetic functions f and g from natural numbers to R, the product of f and g at a natural number n equals the sum, over the divisor antidiagonal of n, of the products of f at the first element and g at the second element of each pair.
|
ArithmeticFunction.prodPrimeFactors_apply
theorem ArithmeticFunction.prodPrimeFactors_apply :
∀ {R : Type u_1} [inst : CommMonoidWithZero R] {f : ℕ → R} {n : ℕ},
n ≠ 0 → (ArithmeticFunction.prodPrimeFactors fun p => f p) n = n.primeFactors.prod fun p => f p
This theorem states that for any non-zero natural number `n` and any function `f` from natural numbers to an arbitrary type `R` (where `R` is a type equipped with both commutative monoid and zero structure), the value of applying the arithmetic function defined by the product of `f` over the prime factors of `n` is the same as the product of `f` applied to each of the prime factors of `n`. In mathematical terms, this theorem is expressing the equality $\prod_{p \mid n} f(p) = \prod_{p \in \text{primeFactors}(n)} f(p)$, where $\prod$ denotes the product over a set.
More concisely: For any non-zero natural number `n` and function `f` from natural numbers to a commutative monoid `R`, the product of `f` applied to the prime factors of `n` equals the value of `f` applied to the product of `n`'s prime factors.
|
ArithmeticFunction.moebius_apply_of_squarefree
theorem ArithmeticFunction.moebius_apply_of_squarefree :
∀ {n : ℕ}, Squarefree n → ArithmeticFunction.moebius n = (-1) ^ ArithmeticFunction.cardFactors n
This theorem states that for a natural number `n` that is squarefree (meaning that the only squares that divide `n` are the squares of units), the value of the Möbius function `μ` at `n` equals `(-1)` raised to the power of the number of prime factors of `n`. In other words, if `n` is squarefree, the sign of the Möbius function at `n` depends on whether `n` has an even or odd number of distinct prime factors. If the number of prime factors is even, `μ(n) = 1`, and if the number of prime factors is odd, `μ(n) = -1`.
More concisely: For a squarefree natural number `n`, the Möbius function `μ(n)` equals `(-1)^k`, where `k` is the number of prime factors of `n`.
|
ArithmeticFunction.ppow_apply
theorem ArithmeticFunction.ppow_apply :
∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R} {k x : ℕ}, 0 < k → (f.ppow k) x = f x ^ k := by
sorry
This theorem states that for any type `R` that forms a semiring, an arithmetic function `f` from natural numbers to `R`, and any two natural numbers `k` and `x` such that `k` is greater than 0, the application of the pointwise power function on `f` with exponent `k` to `x` is equal to the `k`th power of the application of `f` to `x`. In other words, the pointwise power function raises each output of the arithmetic function to the `k`th power.
More concisely: For any semiring `R`, arithmetic function `f` from natural numbers to `R`, and natural numbers `k` > 0, the pointwise power of `f` with exponent `k` equals the `k`th power of the application of `f`: (ⁱⁱⁱf)(k)(x) = (ⁱⁱⁱf)(x)⁽ⁱk⁾ for all x ∈ ℕ.
|
ArithmeticFunction.coe_mul_zeta_apply
theorem ArithmeticFunction.coe_mul_zeta_apply :
∀ {R : Type u_1} [inst : Semiring R] {f : ArithmeticFunction R} {x : ℕ},
(f * ↑ArithmeticFunction.zeta) x = x.divisors.sum fun i => f i
This theorem states that for any semiring `R`, and for any arithmetic function `f` from natural numbers to `R`, the product of `f` and the Dirichlet zeta function (when the zeta function is viewed as an arithmetic function from natural numbers to `R`), evaluated at a natural number `x`, is equal to the sum of the function `f` evaluated at each divisor of `x`. In other words, it states that `(f * ζ)(x) = Σ (f i)`, where the sum is over all `i` that are divisors of `x`.
More concisely: For any semiring `R` and arithmetic function `f` from natural numbers to `R`, the product of `f` and the Dirichlet zeta function equals the sum of `f` evaluated at each divisor of the natural number `x`. In mathematical notation, `(f * ζ)(x) = Σ (f i)`, where the sum is over all divisors `i` of `x`.
|
ArithmeticFunction.map_zero
theorem ArithmeticFunction.map_zero : ∀ {R : Type u_1} [inst : Zero R] {f : ArithmeticFunction R}, f 0 = 0
The theorem `ArithmeticFunction.map_zero` states that for any type `R` that has a zero element, and any arithmetic function `f` mapping from natural numbers to `R`, the value of `f` at 0 is always the zero element of `R`. In more mathematical terms, if `f` is an arithmetic function, `f(0) = 0`.
More concisely: For any arithmetic function `f` and type `R` with a zero element, `f(0) = 0`.
|
ArithmeticFunction.isMultiplicative_zeta
theorem ArithmeticFunction.isMultiplicative_zeta : ArithmeticFunction.zeta.IsMultiplicative
This theorem states that the ζ-arithmetic function, also known as the Riemann zeta function, is multiplicative. In mathematical terms, an arithmetic function `f` is defined to be multiplicative if `f(1) = 1` and for any two coprime natural numbers `m` and `n`, `f(m * n) = f(m) * f(n)`. Here, the Riemann zeta function is defined such that `ζ(0) = 0` and `ζ(x) = 1` for all other `x`. This theorem asserts that this ζ-function satisfies the properties of a multiplicative arithmetic function.
More concisely: The Riemann zeta function, defined as 0 for 0 and 1 for all other natural numbers, and multiplicatively for coprime numbers, is a multiplicative arithmetic function.
|
ArithmeticFunction.coe_zeta_mul_coe_moebius
theorem ArithmeticFunction.coe_zeta_mul_coe_moebius :
∀ {R : Type u_1} [inst : Ring R], ↑ArithmeticFunction.zeta * ↑ArithmeticFunction.moebius = 1
This theorem states that for any ring R, the product of the Dirichlet series of the Riemann ζ function and the Möbius function equals 1. In more detail, it asserts that multiplying the function ζ, which is defined to be 0 when its argument is 0 and 1 otherwise, with the Möbius function μ, which takes on values of 1, -1 or 0 depending on whether its argument is squarefree with an even number of distinct prime factors, squarefree with an odd number of distinct prime factors or not squarefree, respectively, results in the multiplicative identity in the ring R.
More concisely: For any ring R, the product of the Riemann ζ function and the Möbius function is the multiplicative identity in R.
|
ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq
theorem ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq :
∀ {R : Type u_1} [inst : AddCommGroup R] {f g : ℕ → R},
(∀ n > 0, (n.divisors.sum fun i => f i) = g n) ↔
∀ n > 0, (n.divisorsAntidiagonal.sum fun x => ArithmeticFunction.moebius x.1 • g x.2) = f n
This theorem is known as the Möbius inversion for functions to an additive commutative group. It states that for all natural numbers `n` greater than 0, the sum of the function `f` over the divisors of `n` equals to the function `g` evaluated at `n` if and only if for all `n` greater than 0, the sum over the antidiagonal divisors of `n` of the Möbius function evaluated at the first element of the pair times the function `g` evaluated at the second element equals to the function `f` evaluated at `n`. In mathematical notation, we have $\sum_{i \mid n} f(i) = g(n)$ if and only if $\sum_{i,j :ij=n} \mu(i) . g(j) = f(n)$ for all $n > 0$. Here $\mu(i)$ refers to the Möbius function.
More concisely: The Möbius function evaluations on the divisors of a natural number `n` are inverted by the function values on the pair of divisors `i` and `j` with product equal to `n`, i.e., $\sum_{i \mid n} \mu(i)g(i) = f(n)$ if and only if $\sum_{i,j : ij=n} g(i) = f(n)$.
|
ArithmeticFunction.IsMultiplicative.map_one
theorem ArithmeticFunction.IsMultiplicative.map_one :
∀ {R : Type u_1} [inst : MonoidWithZero R] {f : ArithmeticFunction R}, f.IsMultiplicative → f 1 = 1
The theorem `ArithmeticFunction.IsMultiplicative.map_one` states that for any type `R` which is a monoid with zero, and any arithmetic function `f` from natural numbers to `R`, if `f` is a multiplicative function (meaning that `f` of `1` equals `1` and `f` of the product of any two coprime natural numbers equals the product of `f` applied to each of the numbers), then `f` of `1` must be equal to `1`.
More concisely: If `f` is a multiplicative arithmetic function on a monoid with zero, then `f` maps `1` to `1`.
|
ArithmeticFunction.moebius_mul_coe_zeta
theorem ArithmeticFunction.moebius_mul_coe_zeta : ArithmeticFunction.moebius * ↑ArithmeticFunction.zeta = 1
The theorem `ArithmeticFunction.moebius_mul_coe_zeta` states that the multiplication of the Möbius function (`ArithmeticFunction.moebius`) and the cast of the Riemann zeta function (`ArithmeticFunction.zeta`) to an arithmetic function of integers results in the identity function. This is the mathematical statement of the Möbius inversion formula, which states that if a function `f` is defined on the positive integers and `f(1) = 1`, then the Möbius function `μ` and the Riemann zeta function `ζ` satisfy `f * μ = ζ`.
More concisely: The Möbius function multiplied with the integer-valued Riemann zeta function yields the identity function.
|