OAI/LinearAlgebra/MatrixMultiplication/Model.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MatrixMultiplication.Arithmetic.Gate line 11

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:13 (same declaration text).

2. def OAI.MatrixMultiplication.Arithmetic.Gate.eval line 22

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:24 (same declaration text).

3. def OAI.MatrixMultiplication.Arithmetic.Gate.cost line 30

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:32 (same declaration text).

4. inductive OAI.MatrixMultiplication.Arithmetic.Program line 39

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:41 (same declaration text).

5. def OAI.MatrixMultiplication.Arithmetic.Program.eval line 47

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:49 (same declaration text).

6. def OAI.MatrixMultiplication.Arithmetic.Program.cost line 52

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:54 (same declaration text).

7. abbrev OAI.MatrixMultiplication.Arithmetic.MatrixInput line 58

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:60 (same declaration text).

8. def OAI.MatrixMultiplication.Arithmetic.matrixInputs line 60

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:62 (same declaration text).

9. structure OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm line 66

   Also declared: ComparatorChallenges/MatrixMultiplication.lean:68 (same declaration text).

10. def OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm.eval line 75

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:77 (same declaration text).

11. def OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm.Correct line 80

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:82 (same declaration text).

12. def OAI.MatrixMultiplication.Arithmetic.MatrixAlgorithm.cost line 83

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:85 (same declaration text).

13. def OAI.MatrixMultiplication.Arithmetic.AdmissibleExponent line 88

    Source documentation

    Positive slack, one uniform constant, and a correct program at every size.

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:90 (same declaration text).

    def AdmissibleExponent (F : Type*) [Field F] (τ : ℝ) : Prop :=
    …

14. def OAI.MatrixMultiplication.Arithmetic.omega line 93

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:95 (same declaration text).

15. def OAI.MatrixMultiplication.Arithmetic.innerSize line 96

    Source documentation

    The inner dimension of an n × n^k by n^k × n multiplication.

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:98 (same declaration text).

    def innerSize (n : ℕ) (k : ℝ) : ℕ := ⌈(n : ℝ) ^ k⌉₊

16. def OAI.MatrixMultiplication.Arithmetic.RectangularAdmissibleExponent line 98

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:100 (same declaration text).

17. def OAI.MatrixMultiplication.Arithmetic.rectangularOmega line 103

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:105 (same declaration text).

18. def OAI.MatrixMultiplication.Arithmetic.complexAlpha line 107

    Source documentation

    The dual exponent is a supremum of exact exponent-two rectangular shapes.

    Also declared: ComparatorChallenges/MatrixMultiplication.lean:109 (same declaration text).

    def complexAlpha : ℝ :=
    …