A division-free determinant algorithm

This file defines birdDet, an implementation of an division-free algorithm for computing determinants. The algorithm runs in O(n^4) for an n-by-n matrix.

This determinant algorithm comes from:

Title: A simple division-free algorithm for computing determinants. Author: Richard S. Bird URL: https://doi.org/10.1016/j.ipl.2011.08.006

Main definitions

• BirdDet.birdDet: The entrypoint for the determinant calculation.
• BirdDet.get: matrix entry lookup.
• BirdDet.sumFrom: The sum f lo + ... + f (n - 1).
• BirdDet.iter: The internal scalar recurrence for Bird's algorithm.

Main lemmas

The lemmas in this file are unfolding equations.

def BirdDet.get {R : Type u_1} [CommRing R] (n : ℕ) (A : Array R) (i j : ℕ) : R

get n A i j returns the (i, j)th entry of the n × n matrix whose entries are stored in A in row-major order.

The function does not check the matrix index bounds.

Equations

• BirdDet.get n A i j = A.getD (i * n + j) 0

@[irreducible]

def BirdDet.sumFrom {R : Type u_1} [CommRing R] (n lo : ℕ) (f : ℕ → R) : R

Sum f lo + ... + f (n - 1). Returns zero when n <= lo.

Equations

• BirdDet.sumFrom n lo f = if lo < n then f lo + BirdDet.sumFrom n (lo + 1) f else 0

def BirdDet.iter {R : Type u_1} [CommRing R] (n : ℕ) (A : Array R) (t : ℕ) (F : ℕ → ℕ → R) : ℕ → ℕ → R

Scalar formula for one recurrence step.

Bird's paper defines a matrix recursion for an n × n matrix A:

F_0 = A
F_{t+1} = μ(F_t) * A

where μ(F_t) is obtained from F_t by replacing each diagonal entry F_t k k with the negative sum of the diagonal entries below it, setting the entries in the lower triangular part to 0, and leaving all other entries unchanged:

μ(F_t) =
  0                                   if i >= j
  - ∑ k from i+1 to n-1, F_t k k      if i = j
  F_t i j                             if i < j

If we write out the entry-wise matrix multiplication F_{t+1} i j = (μ(F_t) * A) i j we obtain:

F_{t+1} i j =
  - (∑ k from i+1 to n-1, F_t k k) * (A i j)
  + ∑ k from i+1 to n-1, (F_t i k) * (A k j)

Equations

• One or more equations did not get rendered due to their size.
• BirdDet.iter n A 0 F = F

def BirdDet.birdDet {R : Type u_1} [CommRing R] (n : ℕ) (A : Array R) : R

birdDet n A computes the determinant of the n × n matrix whose entries are stored in A in row-major order.

Equations

• BirdDet.birdDet 0 A = 1
• BirdDet.birdDet t_1.succ A = (-1) ^ t_1 * BirdDet.iter t_1.succ A t_1 (BirdDet.get t_1.succ A) 0 0

theorem BirdDet.sumFrom_step {R : Type u_1} [CommRing R] (n lo : ℕ) (f : ℕ → R) (h : lo < n) : BirdDet.sumFrom n lo f = f lo + BirdDet.sumFrom n (lo + 1) f

theorem BirdDet.sumFrom_stop {R : Type u_1} [CommRing R] (n lo : ℕ) (f : ℕ → R) (h : ¬lo < n) : BirdDet.sumFrom n lo f = 0

theorem BirdDet.iter_zero {R : Type u_1} [CommRing R] (n : ℕ) (A : Array R) (F : ℕ → ℕ → R) (i j : ℕ) : BirdDet.iter n A 0 F i j = F i j

theorem BirdDet.iter_succ {R : Type u_1} [CommRing R] (n : ℕ) (A : Array R) (t : ℕ) (F : ℕ → ℕ → R) (i j : ℕ) : BirdDet.iter n A (t + 1) F i j = (-BirdDet.sumFrom n (i + 1) fun (k : ℕ) => BirdDet.iter n A t F k k) * BirdDet.get n A i j + BirdDet.sumFrom n (i + 1) fun (k : ℕ) => BirdDet.iter n A t F i k * BirdDet.get n A k j

theorem BirdDet.birdDet_zero {R : Type u_1} [CommRing R] (A : Array R) : birdDet 0 A = 1

theorem BirdDet.birdDet_eq {R : Type u_1} [CommRing R] (n k : ℕ) (A : Array R) (hn : n = k + 1) : birdDet n A = (-1) ^ k * BirdDet.iter n A k (BirdDet.get n A) 0 0