Divisor equivalences, factor pairs, and shifted-index sums

For N ≠ 0, the divisors d of N with a = N + d (respectively a = N - d) are at most one, and such a divisor exists exactly when a - N divides N (respectively N - a divides a). These lemmas evaluate the corresponding indicator sums over N.divisors.

Nat.sum_divisorsAntidiagonal_ite_dvd regroups a sum over the factor pairs (a, b) of n, restricted to a ∣ m, as a sum over the divisors of gcd(m, n).

Int.pos_pos_mul_eq_of_mem_divisorsAntidiagonal_toNat and Int.prodMk_toNat_mem_divisorsAntidiagonal_toNat identify the pairs of n.toNat.divisorsAntidiagonal, for an integer n, with the factorisations of n into two positive integers.

Nat.sum_divisorsAntidiagonal_filter_sub evaluates differences over the factor pairs with strictly increasing factors. Nat.injOn_add_divisorsAntidiagonal_filter_lt and Int.isSquare_sq_sub_four_mul_iff_exists_mem_divisorsAntidiagonal identify those factor pairs by their sum and by a positive square discriminant.

TauCeti.nontrivialDivisorEquiv identifies divisors greater than one with the subtype of N.divisors omitting the unit divisor.

theorem Nat.sum_divisors_ite_eq_add {M : Type u_1} [AddCommMonoid M] {N : ℕ} (hN : N ≠ 0) (a : ℕ) (f : ℕ → M) : (∑ d ∈ N.divisors, if a = N + d then f d else 0) = if N < a ∧ a - N ∣ N then f (a - N) else 0

The sum over the divisors d of N of f d restricted to a = N + d.

theorem Nat.sum_divisors_ite_eq_sub {M : Type u_1} [AddCommMonoid M] {N : ℕ} (a : ℕ) (f : ℕ → M) : (∑ d ∈ N.divisors, if a = N - d then f d else 0) = if a < N ∧ N - a ∣ a then f (N - a) else 0

The sum over the divisors d of N of f d restricted to a = N - d.

theorem Nat.sum_divisorsAntidiagonal_ite_dvd {M : Type u_1} [AddCommMonoid M] {n : ℕ} (hn : n ≠ 0) (m : ℕ) (f : ℕ → ℕ → M) : (∑ p ∈ n.divisorsAntidiagonal, if p.1 ∣ m then f p.1 (p.2 * (m / p.1)) else 0) = ∑ d ∈ (m.gcd n).divisors, f d (m * n / d ^ 2)

Regrouping a sum over the factor pairs (a, b) of n ≠ 0, restricted to a ∣ m, by the divisors d of gcd(m, n): the pair (d, n / d) contributes f d (m * n / d ^ 2), since (n / d) * (m / d) = m * n / d ^ 2.

theorem Nat.sum_divisorsAntidiagonal_filter_sub {A : Type u_2} [AddCommGroup A] (n : ℕ) (f : ℕ → A) : ∑ p ∈ n.divisorsAntidiagonal with p.1 < p.2, (f p.2 - f p.1) = ∑ d ∈ n.divisors, f d - ∑ p ∈ n.divisorsAntidiagonal, f (min p.1 p.2)

On the factor pairs with increasing factors, subtracting the value at the smaller factor from that at the larger factor is the full divisor sum minus the sum at the minimum factor.

theorem Nat.injOn_add_divisorsAntidiagonal_filter_lt (n : ℕ) : Set.InjOn (fun (p : ℕ × ℕ) => p.1 + p.2) ↑({p ∈ n.divisorsAntidiagonal | p.1 < p.2})

A factor pair with strictly increasing factors is determined by its sum.

theorem Int.pos_pos_mul_eq_of_mem_divisorsAntidiagonal_toNat {n : ℤ} {p : ℕ × ℕ} (hp : p ∈ n.toNat.divisorsAntidiagonal) : 0 < ↑p.1 ∧ 0 < ↑p.2 ∧ ↑p.1 * ↑p.2 = n

The factors of a pair in n.toNat.divisorsAntidiagonal are positive integers with product n.

theorem Int.prodMk_toNat_mem_divisorsAntidiagonal_toNat {n u v : ℤ} (hu : 0 < u) (hv : 0 < v) (h : u * v = n) : (u.toNat, v.toNat) ∈ n.toNat.divisorsAntidiagonal

A factorisation n = u v into positive integers is the pair (u.toNat, v.toNat) of n.toNat.divisorsAntidiagonal.

theorem Int.isSquare_sq_sub_four_mul_iff_exists_mem_divisorsAntidiagonal (n : ℕ) (hn : 0 < n) (t : ℤ) (hD : 4 * ↑n < t ^ 2) : IsSquare (t ^ 2 - 4 * ↑n) ↔ ∃ p ∈ n.divisorsAntidiagonal, p.1 < p.2 ∧ |t| = ↑p.1 + ↑p.2

At positive discriminant and determinant, a square discriminant is equivalent to a positive factorisation with increasing factors and sum equal to the absolute trace.

def TauCeti.nontrivialDivisorEquiv {N : ℕ} [NeZero N] : { d : ℕ // 1 < d ∧ d ∣ N } ≃ { d : ↥N.divisors // d ≠ ⟨1, ⋯⟩ }

Divisors greater than one correspond to positive divisors other than the unit divisor.

@[simp]

theorem TauCeti.nontrivialDivisorEquiv_apply_val {N : ℕ} [NeZero N] (d : { d : ℕ // 1 < d ∧ d ∣ N }) : ↑↑(nontrivialDivisorEquiv d) = ↑d

The divisor equivalence preserves the underlying natural number.

@[simp]

theorem TauCeti.nontrivialDivisorEquiv_symm_apply_val {N : ℕ} [NeZero N] (d : { d : ↥N.divisors // d ≠ ⟨1, ⋯⟩ }) : ↑(nontrivialDivisorEquiv.symm d) = ↑↑d

The inverse divisor equivalence preserves the underlying natural number.