Lean-verified proofs for [44]
Lean-verified proofs for [44]
Sergeev I. S. Lower bounds for additive
complexity of linear operators and bilinear algorithms for matrix and polynomial multiplication over GF(2).
Mathematical Notes. 2025. 118(4), 848-862.
- Basic concepts, bounds on the reduced complexity (Lemma 1, Theorem 1). LEAN
- Reduced complexity and additive complexity of matrix multiplication (Lemma 2). LEAN
(requires Lemma 1 and Theorem 1)
- A lower bound for the complexity of independent matrices (Theorem 2). LEAN
(requires basic concepts)
- Tightness of the bound of Theorem 2 (Theorem 3). LEAN
- Corollaries from Section 6 (Corollaries 1, 2, 3(ineq. 1), 4(ineq. 1)). LEAN
(requires Lemma 1, Lemma 2, Theorem 2)
- A lower bound for the complexity of the Sierpiński (disjointness) matrix (Corollary 6). LEAN
(requires basic concepts and Theorem 2)
Lean-verified proofs were derived by an AI-assistant from text proofs in Reaslab environment.
return to the main page