feat(NumberTheory/Divisors): add divisorAntidiagonal equivalence. (leanprover-community#27837)

Author: CBirkbeck

Mathlib.lean

@@ -4825,6 +4825,7 @@ import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
 import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
 import Mathlib.NumberTheory.Transcendental.Liouville.Measure
 import Mathlib.NumberTheory.Transcendental.Liouville.Residual
+import Mathlib.NumberTheory.TsumDivsorsAntidiagonal
 import Mathlib.NumberTheory.VonMangoldt
 import Mathlib.NumberTheory.WellApproximable
 import Mathlib.NumberTheory.Wilson

Mathlib/NumberTheory/TsumDivsorsAntidiagonal.lean

@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import Mathlib.NumberTheory.Divisors
+import Mathlib.Data.PNat.Defs
+
+/-!
+# Lemmas on infinite sums over the antidiagonal of the divisors function
+
+This file contains lemmas about the antidiagonal of the divisors function. It defines the map from
+`Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b` to `(a, b)`.
+
+-/
+
+/-- The map from `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b`
+to `(a , b)`. -/
+def divisorsAntidiagonalFactors (n : ℕ+) : Nat.divisorsAntidiagonal n → ℕ+ × ℕ+ :=
+    fun x ↦
+   ⟨⟨x.1.1, Nat.pos_of_mem_divisors (Nat.fst_mem_divisors_of_mem_antidiagonal x.2)⟩,
+    (⟨x.1.2, Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal x.2)⟩ : ℕ+),
+    Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal x.2)⟩
+
+lemma divisorsAntidiagonalFactors_eq {n : ℕ+} (x : Nat.divisorsAntidiagonal n) :
+    (divisorsAntidiagonalFactors n x).1.1 * (divisorsAntidiagonalFactors n x).2.1 = n := by
+  simp [divisorsAntidiagonalFactors, (Nat.mem_divisorsAntidiagonal.mp x.2).1]
+
+lemma divisorsAntidiagonalFactors_one (x : Nat.divisorsAntidiagonal 1) :
+    (divisorsAntidiagonalFactors 1 x) = (1, 1) := by
+  have h := Nat.mem_divisorsAntidiagonal.mp x.2
+  simp only [mul_eq_one, ne_eq, one_ne_zero, not_false_eq_true, and_true] at h
+  simp [divisorsAntidiagonalFactors, h.1, h.2]
+
+/-- The equivalence from the union over `n` of `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+`
+given by sending `n = a * b` to `(a , b)`. -/
+def sigmaAntidiagonalEquivProd : (Σ n : ℕ+, Nat.divisorsAntidiagonal n) ≃ ℕ+ × ℕ+ where
+  toFun x := divisorsAntidiagonalFactors x.1 x.2
+  invFun x :=
+    ⟨⟨x.1.val * x.2.val, mul_pos x.1.2 x.2.2⟩, ⟨x.1, x.2⟩, by simp [Nat.mem_divisorsAntidiagonal]⟩
+  left_inv := by
+    rintro ⟨n, ⟨k, l⟩, h⟩
+    rw [Nat.mem_divisorsAntidiagonal] at h
+    ext <;> simp [divisorsAntidiagonalFactors, ← PNat.coe_injective.eq_iff, h.1]
+  right_inv _ := rfl
+
+lemma sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ+ × ℕ+) :
+    (sigmaAntidiagonalEquivProd.symm x).1 = x.1.1 * x.2.1 := rfl
+
+lemma sigmaAntidiagonalEquivProd_symm_apply_snd (x : ℕ+ × ℕ+) :
+    (sigmaAntidiagonalEquivProd.symm x).2 = (x.1.1, x.2.1) := rfl