Mathlib.Data.Nat.Pairing

Nat.pair definition

(a b : ℕ) : ℕ

Full source

/-- Pairing function for the natural numbers. -/
@[pp_nodot]
def pair (a b : ℕ) : ℕ :=
  if a < b then b * b + a else a * a + a + b

Natural number pairing function

Informal description

The pairing function for natural numbers is defined as follows: for any two natural numbers $ a $ and $ b $, \[ \text{pair}(a, b) = \begin{cases} b^2 + a & \text{if } a < b, \\ a^2 + a + b & \text{otherwise.} \end{cases} \] This function maps pairs of natural numbers to a single natural number in a monotone fashion.

Nat.unpair definition

(n : ℕ) : ℕ × ℕ

Full source

/-- Unpairing function for the natural numbers. -/
@[pp_nodot]
def unpair (n : ℕ) : ℕℕ × ℕ :=
  let s := sqrt n
  if n - s * s < s then (n - s * s, s) else (s, n - s * s - s)

Natural number unpairing function

Informal description

The function takes a natural number $ n $ and returns a pair of natural numbers $(a, b)$ defined as follows: Let $ s = \lfloor \sqrt{n} \rfloor $. If $ n - s^2 < s $, then $(a, b) = (n - s^2, s)$; otherwise, $(a, b) = (s, n - s^2 - s)$. This function is the inverse of the pairing function described in the head statements.

Nat.pair_unpair theorem

(n : ℕ) : pair (unpair n).1 (unpair n).2 = n

Full source

@[simp]
theorem pair_unpair (n : ℕ) : pair (unpair n).1 (unpair n).2 = n := by
  dsimp only [unpair]; let s := sqrt n
  have sm : s * s + (n - s * s) = n := Nat.add_sub_cancel' (sqrt_le _)
  split_ifs with h
  · simp [s, pair, h, sm]
  · have hl : n - s * s - s ≤ s := Nat.sub_le_iff_le_add.2
      (Nat.sub_le_iff_le_add'.2 <| by rw [← Nat.add_assoc]; apply sqrt_le_add)
    simp [s, pair, hl.not_lt, Nat.add_assoc, Nat.add_sub_cancel' (le_of_not_gt h), sm]

Inverse Property of Natural Number Pairing and Unpairing Functions: $\text{pair} \circ \text{unpair} = \text{id}$

Informal description

For any natural number $n$, the pairing function applied to the components of the unpairing function evaluated at $n$ returns $n$ itself. That is, if $(a, b) = \text{unpair}(n)$, then $\text{pair}(a, b) = n$.

Nat.pair_unpair' theorem

{n a b} (H : unpair n = (a, b)) : pair a b = n

Full source

theorem pair_unpair' {n a b} (H : unpair n = (a, b)) : pair a b = n := by
  simpa [H] using pair_unpair n

Inverse Property of Pairing and Unpairing Functions: $\text{pair} \circ \text{unpair} = \text{id}$ (variant)

Informal description

For any natural numbers $n$, $a$, and $b$, if the unpairing function satisfies $\text{unpair}(n) = (a, b)$, then the pairing function applied to $a$ and $b$ returns $n$, i.e., $\text{pair}(a, b) = n$.

Nat.unpair_pair theorem

(a b : ℕ) : unpair (pair a b) = (a, b)

Full source

@[simp]
theorem unpair_pair (a b : ℕ) : unpair (pair a b) = (a, b) := by
  dsimp only [pair]; split_ifs with h
  · show unpair (b * b + a) = (a, b)
    have be : sqrt (b * b + a) = b := sqrt_add_eq _ (le_trans (le_of_lt h) (Nat.le_add_left _ _))
    simp [unpair, be, Nat.add_sub_cancel_left, h]
  · show unpair (a * a + a + b) = (a, b)
    have ae : sqrt (a * a + (a + b)) = a := by
      rw [sqrt_add_eq]
      exact Nat.add_le_add_left (le_of_not_gt h) _
    simp [unpair, ae, Nat.not_lt_zero, Nat.add_assoc, Nat.add_sub_cancel_left]

Inverse Property of Natural Number Pairing and Unpairing Functions

Informal description

For any natural numbers $a$ and $b$, the unpairing function applied to the pairing function evaluated at $(a, b)$ returns $(a, b)$, i.e., $\text{unpair}(\text{pair}(a, b)) = (a, b)$.

Nat.pairEquiv definition

: ℕ × ℕ ≃ ℕ

Full source

/-- An equivalence between `ℕ × ℕ` and `ℕ`. -/
@[simps -fullyApplied]
def pairEquiv : ℕℕ × ℕℕ × ℕ ≃ ℕ :=
  ⟨uncurry pair, unpair, fun ⟨a, b⟩ => unpair_pair a b, pair_unpair⟩

Natural number pairing equivalence

Informal description

The equivalence between pairs of natural numbers and single natural numbers is defined by the pairing function $\text{pair} : \mathbb{N} \times \mathbb{N} \to \mathbb{N}$ and its inverse $\text{unpair} : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$. Specifically, for any $(a, b) \in \mathbb{N} \times \mathbb{N}$, we have $\text{unpair}(\text{pair}(a, b)) = (a, b)$, and for any $n \in \mathbb{N}$, we have $\text{pair}(\text{unpair}(n)) = n$.

Nat.surjective_unpair theorem

: Surjective unpair

Full source

theorem surjective_unpair : Surjective unpair :=
  pairEquiv.symm.surjective

Surjectivity of the Natural Number Unpairing Function

Informal description

The natural number unpairing function $\text{unpair} : \mathbb{N} \to \mathbb{N} \times \mathbb{N}$ is surjective. That is, for every pair of natural numbers $(a, b) \in \mathbb{N} \times \mathbb{N}$, there exists a natural number $n \in \mathbb{N}$ such that $\text{unpair}(n) = (a, b)$.

Nat.pair_eq_pair theorem

{a b c d : ℕ} : pair a b = pair c d ↔ a = c ∧ b = d

Full source

@[simp]
theorem pair_eq_pair {a b c d : ℕ} : pairpair a b = pair c d ↔ a = c ∧ b = d :=
  pairEquiv.injective.eq_iff.trans (@Prod.ext_iff ℕ ℕ (a, b) (c, d))

Pairing Function is Injective: $\text{pair}(a, b) = \text{pair}(c, d) \leftrightarrow a = c \land b = d$

Informal description

For any natural numbers $a, b, c, d$, the pairing function satisfies $\text{pair}(a, b) = \text{pair}(c, d)$ if and only if $a = c$ and $b = d$.

Nat.unpair_lt theorem

{n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n

Full source

theorem unpair_lt {n : ℕ} (n1 : 1 ≤ n) : (unpair n).1 < n := by
  let s := sqrt n
  simp only [unpair, Nat.sub_le_iff_le_add]
  by_cases h : n - s * s < s <;> simp [s, h, ↓reduceIte]
  · exact lt_of_lt_of_le h (sqrt_le_self _)
  · simp only [not_lt] at h
    have s0 : 0 < s := sqrt_pos.2 n1
    exact lt_of_le_of_lt h (Nat.sub_lt n1 (Nat.mul_pos s0 s0))

First Component of Unpairing is Less Than Input for Positive Natural Numbers

Informal description

For any natural number $n \geq 1$, the first component of the unpairing of $n$ is strictly less than $n$, i.e., if $(a, b) = \text{unpair}(n)$, then $a < n$.

Nat.unpair_zero theorem

: unpair 0 = 0

Full source

@[simp]
theorem unpair_zero : unpair 0 = 0 := by
  rw [unpair]
  simp

Unpairing Function at Zero: $\text{unpair}(0) = 0$

Informal description

The unpairing function evaluated at $0$ returns $0$, i.e., $\text{unpair}(0) = 0$.

Nat.unpair_left_le theorem

: ∀ n : ℕ, (unpair n).1 ≤ n

Full source

theorem unpair_left_le : ∀ n : ℕ, (unpair n).1 ≤ n
  | 0 => by simp
  | _ + 1 => le_of_lt (unpair_lt (Nat.succ_pos _))

First Component of Unpairing is Bounded by Input

Informal description

For any natural number $n$, the first component of the unpairing of $n$ is less than or equal to $n$, i.e., if $(a, b) = \text{unpair}(n)$, then $a \leq n$.

Nat.left_le_pair theorem

(a b : ℕ) : a ≤ pair a b

Full source

theorem left_le_pair (a b : ℕ) : a ≤ pair a b := by simpa using unpair_left_le (pair a b)

Left component is bounded by the pairing function on natural numbers

Informal description

For any natural numbers $a$ and $b$, the first component $a$ is less than or equal to the paired value $\mathrm{pair}(a, b)$, where $\mathrm{pair}(a, b)$ is defined as: \[ \mathrm{pair}(a, b) = \begin{cases} b^2 + a & \text{if } a < b, \\ a^2 + a + b & \text{otherwise.} \end{cases} \]

Nat.right_le_pair theorem

(a b : ℕ) : b ≤ pair a b

Full source

theorem right_le_pair (a b : ℕ) : b ≤ pair a b := by
  by_cases h : a < b
  · simpa [pair, h] using le_trans (le_mul_self _) (Nat.le_add_right _ _)
  · simp [pair, h]

Right component is bounded by the pairing function on natural numbers

Informal description

For any natural numbers $a$ and $b$, the second component $b$ is less than or equal to the paired value $\mathrm{pair}(a, b)$, where $\mathrm{pair}(a, b)$ is defined as: \[ \mathrm{pair}(a, b) = \begin{cases} b^2 + a & \text{if } a < b, \\ a^2 + a + b & \text{otherwise.} \end{cases} \]

Nat.unpair_right_le theorem

(n : ℕ) : (unpair n).2 ≤ n

Full source

theorem unpair_right_le (n : ℕ) : (unpair n).2 ≤ n := by
  simpa using right_le_pair n.unpair.1 n.unpair.2

Right Component Bound in Natural Number Unpairing: $b \leq n$

Informal description

For any natural number $n$, the second component of the unpairing function evaluated at $n$ is less than or equal to $n$. That is, if $(a, b) = \text{unpair}(n)$, then $b \leq n$.

Nat.pair_lt_pair_left theorem

{a₁ a₂} (b) (h : a₁ < a₂) : pair a₁ b < pair a₂ b

Full source

theorem pair_lt_pair_left {a₁ a₂} (b) (h : a₁ < a₂) : pair a₁ b < pair a₂ b := by
  by_cases h₁ : a₁ < b <;> simp [pair, h₁, Nat.add_assoc]
  · by_cases h₂ : a₂ < b <;> simp [pair, h₂, h]
    simp? at h₂ says simp only [not_lt] at h₂
    apply Nat.add_lt_add_of_le_of_lt
    · exact Nat.mul_self_le_mul_self h₂
    · exact Nat.lt_add_right _ h
  · simp at h₁
    simp only [not_lt_of_gt (lt_of_le_of_lt h₁ h), ite_false]
    apply add_lt_add
    · exact Nat.mul_self_lt_mul_self h
    · apply Nat.add_lt_add_right; assumption

Monotonicity of Pairing Function in First Argument

Informal description

For any natural numbers $a_1, a_2$ and $b$, if $a_1 < a_2$, then the pairing function satisfies $\text{pair}(a_1, b) < \text{pair}(a_2, b)$.

Nat.pair_lt_pair_right theorem

(a) {b₁ b₂} (h : b₁ < b₂) : pair a b₁ < pair a b₂

Full source

theorem pair_lt_pair_right (a) {b₁ b₂} (h : b₁ < b₂) : pair a b₁ < pair a b₂ := by
  by_cases h₁ : a < b₁
  · simpa [pair, h₁, Nat.add_assoc, lt_trans h₁ h, h] using mul_self_lt_mul_self h
  · simp only [pair, h₁, ↓reduceIte, Nat.add_assoc]
    by_cases h₂ : a < b₂ <;> simp [pair, h₂, h]
    simp? at h₁ says simp only [not_lt] at h₁
    rw [Nat.add_comm, Nat.add_comm _ a, Nat.add_assoc, Nat.add_lt_add_iff_left]
    rwa [Nat.add_comm, ← sqrt_lt, sqrt_add_eq]
    exact le_trans h₁ (Nat.le_add_left _ _)

Monotonicity of Pairing Function in Second Argument: $\text{pair}(a, b_1) < \text{pair}(a, b_2)$ when $b_1 < b_2$

Informal description

For any natural number $a$ and natural numbers $b_1, b_2$ with $b_1 < b_2$, the pairing function satisfies $\text{pair}(a, b_1) < \text{pair}(a, b_2)$.

Nat.pair_lt_max_add_one_sq theorem

(m n : ℕ) : pair m n < (max m n + 1) ^ 2

Full source

theorem pair_lt_max_add_one_sq (m n : ℕ) : pair m n < (max m n + 1) ^ 2 := by
  simp only [pair, Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul, Nat.add_assoc]
  split_ifs <;> simp [Nat.max_eq_left, Nat.max_eq_right, Nat.le_of_lt,  not_lt.1, *] <;> omega

Upper Bound on Natural Pairing Function: $\text{pair}(m, n) < (\max(m, n) + 1)^2$

Informal description

For any natural numbers $m$ and $n$, the value of the pairing function $\text{pair}(m, n)$ is strictly less than the square of $\max(m, n) + 1$, i.e., \[ \text{pair}(m, n) < (\max(m, n) + 1)^2. \]

Nat.max_sq_add_min_le_pair theorem

(m n : ℕ) : max m n ^ 2 + min m n ≤ pair m n

Full source

theorem max_sq_add_min_le_pair (m n : ℕ) : max m n ^ 2 + min m n ≤ pair m n := by
  rw [pair]
  rcases lt_or_le m n with h | h
  · rw [if_pos h, max_eq_right h.le, min_eq_left h.le, Nat.pow_two]
  rw [if_neg h.not_lt, max_eq_left h, min_eq_right h, Nat.pow_two, Nat.add_assoc,
    Nat.add_le_add_iff_left]
  exact Nat.le_add_left _ _

Lower Bound for Natural Pairing Function: $\max(m,n)^2 + \min(m,n) \leq \text{pair}(m,n)$

Informal description

For any natural numbers $m$ and $n$, the sum of the square of the maximum of $m$ and $n$ and the minimum of $m$ and $n$ is less than or equal to the value of the pairing function $\text{pair}(m, n)$. In other words, \[ (\max(m, n))^2 + \min(m, n) \leq \text{pair}(m, n). \]

Nat.add_le_pair theorem

(m n : ℕ) : m + n ≤ pair m n

Full source

theorem add_le_pair (m n : ℕ) : m + n ≤ pair m n := by
  simp only [pair, Nat.add_assoc]
  split_ifs
  · have := le_mul_self n
    omega
  · exact Nat.le_add_left _ _

Sum Bound for Natural Pairing Function: $m + n \leq \text{pair}(m, n)$

Informal description

For any natural numbers $m$ and $n$, the sum $m + n$ is less than or equal to the value of the pairing function $\text{pair}(m, n)$.

Nat.unpair_add_le theorem

(n : ℕ) : (unpair n).1 + (unpair n).2 ≤ n

Full source

theorem unpair_add_le (n : ℕ) : (unpair n).1 + (unpair n).2 ≤ n :=
  (add_le_pair _ _).trans_eq (pair_unpair _)

Sum of Unpaired Components Bound: $a + b \leq n$

Informal description

For any natural number $n$, the sum of the components of its unpairing satisfies $(a, b) = \text{unpair}(n) \implies a + b \leq n$.

iSup_unpair theorem

 {α} [CompleteLattice α] (f : ℕ → ℕ → α) : ⨆ n : ℕ, f n.unpair.1 n.unpair.2 = ⨆ (i : ℕ) (j : ℕ), f i j

Full source

theorem iSup_unpair {α} [CompleteLattice α] (f : ℕ → ℕ → α) :
    ⨆ n : ℕ, f n.unpair.1 n.unpair.2 = ⨆ (i : ℕ) (j : ℕ), f i j := by
  rw [← (iSup_prod : ⨆ i : ℕ × ℕ, f i.1 i.2 = _), ← Nat.surjective_unpair.iSup_comp]

Supremum Equality via Unpairing Function: $\sup_n f(a_n, b_n) = \sup_{i,j} f(i,j)$

Informal description

For any complete lattice $\alpha$ and any function $f : \mathbb{N} \times \mathbb{N} \to \alpha$, the supremum of $f$ over all pairs obtained via the unpairing function equals the supremum of $f$ over all pairs of natural numbers. That is, \[ \sup_{n \in \mathbb{N}} f(a_n, b_n) = \sup_{i \in \mathbb{N}} \sup_{j \in \mathbb{N}} f(i, j), \] where $(a_n, b_n) = \text{unpair}(n)$.

iInf_unpair theorem

 {α} [CompleteLattice α] (f : ℕ → ℕ → α) : ⨅ n : ℕ, f n.unpair.1 n.unpair.2 = ⨅ (i : ℕ) (j : ℕ), f i j

Full source

theorem iInf_unpair {α} [CompleteLattice α] (f : ℕ → ℕ → α) :
    ⨅ n : ℕ, f n.unpair.1 n.unpair.2 = ⨅ (i : ℕ) (j : ℕ), f i j :=
  iSup_unpair (show ℕ → ℕ → αᵒᵈ from f)

Infimum Equality via Unpairing Function: $\inf_n f(a_n, b_n) = \inf_{i,j} f(i,j)$

Informal description

For any complete lattice $\alpha$ and any function $f : \mathbb{N} \times \mathbb{N} \to \alpha$, the infimum of $f$ over all pairs obtained via the unpairing function equals the infimum of $f$ over all pairs of natural numbers. That is, \[ \inf_{n \in \mathbb{N}} f(a_n, b_n) = \inf_{i \in \mathbb{N}} \inf_{j \in \mathbb{N}} f(i, j), \] where $(a_n, b_n) = \text{unpair}(n)$.

Set.iUnion_unpair_prod theorem

 {α β} {s : ℕ → Set α} {t : ℕ → Set β} : ⋃ n : ℕ, s n.unpair.fst ×ˢ t n.unpair.snd = (⋃ n, s n) ×ˢ ⋃ n, t n

Full source

theorem iUnion_unpair_prod {α β} {s : ℕ → Set α} {t : ℕ → Set β} :
    ⋃ n : ℕ, s n.unpair.fst ×ˢ t n.unpair.snd = (⋃ n, s n) ×ˢ ⋃ n, t n := by
  rw [← Set.iUnion_prod]
  exact surjective_unpair.iUnion_comp (fun x => s x.fst ×ˢ t x.snd)

Union of Unpaired Cartesian Products Equals Product of Unions

Informal description

For any sequences of sets $s : \mathbb{N} \to \mathcal{P}(\alpha)$ and $t : \mathbb{N} \to \mathcal{P}(\beta)$, the union over all natural numbers $n$ of the Cartesian products $s(a_n) \times t(b_n)$, where $(a_n, b_n) = \text{unpair}(n)$, is equal to the Cartesian product of the union of all $s(n)$ with the union of all $t(n)$. In symbols: \[ \bigcup_{n \in \mathbb{N}} s(a_n) \times t(b_n) = \left(\bigcup_{n \in \mathbb{N}} s(n)\right) \times \left(\bigcup_{n \in \mathbb{N}} t(n)\right), \] where $\text{unpair}(n) = (a_n, b_n)$ is the natural number unpairing function.

Set.iUnion_unpair theorem

{α} (f : ℕ → ℕ → Set α) : ⋃ n : ℕ, f n.unpair.1 n.unpair.2 = ⋃ (i : ℕ) (j : ℕ), f i j

Full source

theorem iUnion_unpair {α} (f : ℕ → ℕ → Set α) :
    ⋃ n : ℕ, f n.unpair.1 n.unpair.2 = ⋃ (i : ℕ) (j : ℕ), f i j :=
  iSup_unpair f

Union Equality via Unpairing Function: $\bigcup_n f(a_n, b_n) = \bigcup_{i,j} f(i,j)$

Informal description

For any function $f : \mathbb{N} \times \mathbb{N} \to \mathcal{P}(\alpha)$, the union over all natural numbers $n$ of the sets $f(a_n, b_n)$, where $(a_n, b_n) = \text{unpair}(n)$, is equal to the union over all pairs $(i, j) \in \mathbb{N} \times \mathbb{N}$ of the sets $f(i, j)$. In symbols: \[ \bigcup_{n \in \mathbb{N}} f(a_n, b_n) = \bigcup_{i \in \mathbb{N}} \bigcup_{j \in \mathbb{N}} f(i, j). \]

Set.iInter_unpair theorem

{α} (f : ℕ → ℕ → Set α) : ⋂ n : ℕ, f n.unpair.1 n.unpair.2 = ⋂ (i : ℕ) (j : ℕ), f i j

Full source

theorem iInter_unpair {α} (f : ℕ → ℕ → Set α) :
    ⋂ n : ℕ, f n.unpair.1 n.unpair.2 = ⋂ (i : ℕ) (j : ℕ), f i j :=
  iInf_unpair f

Intersection Equality via Unpairing Function: $\bigcap_n f(a_n, b_n) = \bigcap_{i,j} f(i,j)$

Informal description

For any function $f : \mathbb{N} \times \mathbb{N} \to \mathcal{P}(\alpha)$, the intersection over all natural numbers $n$ of the sets $f(a_n, b_n)$, where $(a_n, b_n) = \text{unpair}(n)$, is equal to the intersection over all pairs $(i, j) \in \mathbb{N} \times \mathbb{N}$ of the sets $f(i, j)$. In symbols: \[ \bigcap_{n \in \mathbb{N}} f(a_n, b_n) = \bigcap_{i \in \mathbb{N}} \bigcap_{j \in \mathbb{N}} f(i, j). \]