Rational hitting lists: determinant

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Determinant.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

@[simp]

theorem Complexity.RationalHitting.DeterminantAlgorithm.vector_get_ofFn {α : Type u_1} {n : ℕ} (f : Fin n → α) (i : Fin n) : (Vector.ofFn f).get i = f i

@[reducible, inline]

abbrev Complexity.RationalHitting.DeterminantAlgorithm.Table (n : ℕ) : Type

A dense square integer matrix stored as a vector of row vectors.

Equations

• Complexity.RationalHitting.DeterminantAlgorithm.Table n = Vector (Vector ℤ n) n

def Complexity.RationalHitting.DeterminantAlgorithm.denote {n : ℕ} (A : Table n) : Matrix (Fin n) (Fin n) ℤ

Read a dense integer table as a matrix.

Equations

• Complexity.RationalHitting.DeterminantAlgorithm.denote A i j = (Vector.get A i).get j

def Complexity.RationalHitting.DeterminantAlgorithm.tabulate {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : Table n

Materialize every entry of an integer matrix into a dense table.

Equations

• Complexity.RationalHitting.DeterminantAlgorithm.tabulate A = Vector.ofFn fun (i : Fin n) => Vector.ofFn fun (j : Fin n) => A i j

@[simp]

theorem Complexity.RationalHitting.DeterminantAlgorithm.denote_tabulate {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : denote (tabulate A) = A

def Complexity.RationalHitting.DeterminantAlgorithm.step {n : ℕ} (A F : Table n) : Table n

One division-free Bird determinant stage on stored tables.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.RationalHitting.DeterminantAlgorithm.stages {n : ℕ} (A : Table n) : ℕ → Table n

Iterate the division-free determinant stage.

Equations

• Complexity.RationalHitting.DeterminantAlgorithm.stages A 0 = A
• Complexity.RationalHitting.DeterminantAlgorithm.stages A k.succ = Complexity.RationalHitting.DeterminantAlgorithm.step A (Complexity.RationalHitting.DeterminantAlgorithm.stages A k)

theorem Complexity.RationalHitting.DeterminantAlgorithm.stages_spec {n : ℕ} (A : Table n) (k : ℕ) : denote (stages A k) = (BirdDet.Spec.stepEntry (denote A))^[k] (denote A)

def Complexity.RationalHitting.DeterminantAlgorithm.determinant {n : ℕ} : Table n → ℤ

Compute the determinant from the final Bird stage, including dimension zero.

Equations

• One or more equations did not get rendered due to their size.
• Complexity.RationalHitting.DeterminantAlgorithm.determinant x_2 = 1

theorem Complexity.RationalHitting.DeterminantAlgorithm.sumFrom_eq_sum_Ico {n lo : ℕ} (f : ℕ → ℤ) : BirdDet.sumFrom n lo f = ∑ k ∈ Finset.Ico lo n, f k

theorem Complexity.RationalHitting.DeterminantAlgorithm.sumFrom_fin_tail {n : ℕ} (i : Fin n) (f : ℕ → ℤ) : BirdDet.sumFrom n (↑i + 1) f = ∑ k > i, f ↑k

theorem Complexity.RationalHitting.DeterminantAlgorithm.iterate_array_spec {n : ℕ} (A : Array ℤ) (hA : A.size = n * n) (t : ℕ) (i j : Fin n) : (BirdDet.stepEntry n A)^[t] (BirdDet.get n A) ↑i ↑j = (BirdDet.Spec.stepEntry (Matrix.ofArray A hA))^[t] (Matrix.ofArray A hA) i j

theorem Complexity.RationalHitting.DeterminantAlgorithm.array_spec {n : ℕ} (A : Array ℤ) (hA : A.size = n * n) : BirdDet.birdDet n A = BirdDet.Spec.birdDet (Matrix.ofArray A hA)

theorem Complexity.RationalHitting.DeterminantAlgorithm.spec_eq_det {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) : BirdDet.Spec.birdDet A = A.det

theorem Complexity.RationalHitting.DeterminantAlgorithm.determinant_eq {n : ℕ} (A : Table n) : determinant A = (denote A).det

A genuine executable determinant, not Matrix.det's permutation sum.

theorem Complexity.RationalHitting.DeterminantAlgorithm.step_bound {n : ℕ} (A F : Matrix (Fin n) (Fin n) ℤ) (B C : ℕ) (hA : ∀ (i j : Fin n), |A i j| ≤ ↑B) (hF : ∀ (i j : Fin n), |F i j| ≤ ↑C) (i j : Fin n) : |BirdDet.Spec.stepEntry A F i j| ≤ ↑(2 * n * B * C)

theorem Complexity.RationalHitting.DeterminantAlgorithm.stages_bound {n : ℕ} (A : Table n) (B : ℕ) (hA : ∀ (i j : Fin n), |denote A i j| ≤ ↑B) (k : ℕ) (i j : Fin n) : |denote (stages A k) i j| ≤ ↑(B * (2 * n * B) ^ k)

Every stored table entry has only linearly many multiplicative growth stages.

theorem Complexity.RationalHitting.DeterminantAlgorithm.self_le_two_pow (n : ℕ) : n ≤ 2 ^ n

theorem Complexity.RationalHitting.DeterminantAlgorithm.stages_power_bound {n : ℕ} (A : Table n) (b : ℕ) (hA : ∀ (i j : Fin n), |denote A i j| ≤ 2 ^ b) (k : ℕ) (i j : Fin n) : |denote (stages A k) i j| ≤ 2 ^ (b + k * (1 + n + b))

Binary exponent bound for all stored intermediate tables, including singular inputs.