OAI/Computability/RationalHitting/Determinant.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.RationalHitting.DeterminantAlgorithm.Table line 9
2. def OAI.RationalHitting.DeterminantAlgorithm.denote line 11
3. def OAI.RationalHitting.DeterminantAlgorithm.tabulate line 14
4. lemma OAI.RationalHitting.DeterminantAlgorithm.denote_tabulate line 17
5. def OAI.RationalHitting.DeterminantAlgorithm.step line 20
6. def OAI.RationalHitting.DeterminantAlgorithm.stages line 23
7. lemma OAI.RationalHitting.DeterminantAlgorithm.stages_spec line 27
8. def OAI.RationalHitting.DeterminantAlgorithm.determinant line 33
9. lemma OAI.RationalHitting.DeterminantAlgorithm.sumFrom_eq_sum_Ico line 39
10. lemma OAI.RationalHitting.DeterminantAlgorithm.sumFrom_fin_tail line 45
11. lemma OAI.RationalHitting.DeterminantAlgorithm.iterate_array_spec line 53
12. lemma OAI.RationalHitting.DeterminantAlgorithm.array_spec line 63
13. lemma OAI.RationalHitting.DeterminantAlgorithm.spec_eq_det line 69
14. theorem OAI.RationalHitting.DeterminantAlgorithm.determinant_eq line 77

    Source documentation

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

    theorem determinant_eq {n : ℕ} (A : Table n) : determinant A = (denote A).det := by
    …

    Mentions: OAI.RationalHitting.DeterminantAlgorithm.Table, OAI.RationalHitting.DeterminantAlgorithm.determinant, OAI.RationalHitting.DeterminantAlgorithm.denote

15. lemma OAI.RationalHitting.DeterminantAlgorithm.step_bound line 83
16. theorem OAI.RationalHitting.DeterminantAlgorithm.stages_bound line 113

    Source documentation

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

    theorem stages_bound {n : ℕ} (A : Table n) (B : ℕ)
        (hA : ∀ i j, |denote A i j| ≤ B) (k : ℕ) (i j : Fin n) :
        |denote (stages A k) i j| ≤ (B*(2*n*B)^k : ℕ) := by
    …

    Mentions: OAI.RationalHitting.DeterminantAlgorithm.Table, OAI.RationalHitting.DeterminantAlgorithm.denote, OAI.RationalHitting.DeterminantAlgorithm.stages

17. lemma OAI.RationalHitting.DeterminantAlgorithm.self_le_two_pow line 123
18. theorem OAI.RationalHitting.DeterminantAlgorithm.stages_power_bound line 132

    Source documentation

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

    theorem stages_power_bound {n : ℕ} (A : Table n) (b : ℕ)
        (hA : ∀ i j, |denote A i j| ≤ (2 : ℤ)^b) (k : ℕ) (i j : Fin n) :
        |denote (stages A k) i j| ≤ (2 : ℤ)^(b+k*(1+n+b)) := by
    …

    Mentions: OAI.RationalHitting.DeterminantAlgorithm.Table, OAI.RationalHitting.DeterminantAlgorithm.denote, OAI.RationalHitting.DeterminantAlgorithm.stages