Faster computation of selected matrix-product entries

Lax350013.SparseMatrixProduct · concepts/Lax350013/SparseMatrixProduct.lean · lax-350013

proven

Loading review…

Natural Language Statement

Theorem

Theorem 1 computes up to $N^2/\sqrt D$ selected entries in $O(N^2/D^{0.063})$ time when $1\leq D$ and $D^{18}\leq N$ . More generally, for $D\leq N^\varepsilon$ , $\varepsilon<0.1204$ , any $N^2/D^\kappa$ selected entries admit a polynomial saving for every $\kappa>0$ . The individual statements also record Theorems 5, 25 and 30 and Corollaries 26 and 32.

Concept map

8 concepts

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 6 statements. Each proof establishes one of them relative to its assumptions.

Lean source view on GitHub

Show types on hover

1	/-
2	Copyright (c) 2026 Anthropic, PBC. All rights reserved.
3	Released under Apache 2.0 license as described in the file LICENSE.
4	SPDX-License-Identifier: Apache-2.0
5	-/
6	/-
7	Modified for the independent Lax packaging by Édouard Bonnet, 2026.
8	Derived from 3sum-apsp/EndStatement.lean / PaperStatements.lean at upstream commit e1a4e6508154ea59f030480661590a9fe3018011.
9	Changes: Lax module/namespace layout, separated concepts and proofs, archive
10	annotations, and compatibility with the archive Lean/mathlib environment.
11	See NOTICE and README.md in the submission root for provenance and scope.
12	-/
13
14	import Mathlib.Algebra.MvPolynomial.Basic
15	import Mathlib.Analysis.SpecialFunctions.Log.Base
16	import Mathlib.Analysis.SpecialFunctions.Log.Basic
17	import Mathlib.Analysis.SpecialFunctions.Pow.Real
18	import Mathlib.Combinatorics.SimpleGraph.Basic
19	import Mathlib.Data.Finset.Sort
20	import Mathlib.LinearAlgebra.Matrix.Notation
21	import Mathlib.MeasureTheory.Integral.Bochner.Basic
22	import Mathlib.NumberTheory.PrimeCounting
23	import Mathlib.Probability.Independence.Basic
24	import Mathlib.Tactic.DeriveFintype
25	import Lax350013.MatrixPreprocessing
26
27	/-!
28	---
29	title: Faster computation of selected matrix-product entries
30	type: theorem
31	---
32	Theorem 1 computes up to $N^2/\sqrt D$ selected entries in $O(N^2/D^{0.063})$ time when $1\leq D$ and $D^{18}\leq N$ . More generally, for $D\leq N^\varepsilon$ , $\varepsilon<0.1204$ , any $N^2/D^\kappa$ selected entries admit a polynomial saving for every $\kappa>0$ . The individual statements also record Theorems 5, 25 and 30 and Corollaries 26 and 32.
33	-/
34
35	namespace Lax350013.SparseMatrixProduct
36
37	open Finset
38	open Lax350013.WordRAM
39	open Lax350013.RAMResources
40	open Lax350013.ThinMatrices
41	open Lax350013.MatrixParameters
42	open Lax350013.MatrixTradeoffs
43	open Lax350013.MatrixPreprocessing
44
45	/-- Theorem 5: "Let D ≥ 4 be a power of four and N ≥ D^18. Given as input matrices X ∈
46	ℤ^{N×D} and Y ∈ ℤ^{D×N}, whose entries are integers of absolute value at most N^{O(1)}, as well as a
47	set W of at most N²/√D positions of an N × N matrix, the entries (XY)[I,J], (I,J) ∈ W, can be
48	computed deterministically in time O(N² log² D/D^{1/18})." `c` is the exponent hidden in
49	`N^{O(1)}`. (As a statement about the existence of programs, this follows from
50	`Corollary_26_wanted`, whose bound is smaller on these inputs: a statement of this kind cannot say
51	by which algorithm a bound is reached.) -/
52	def Theorem_5 : Prop :=
53	∀ c : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ),
54	Solves (thinProduct []) P b
55	(fun x => (∃ k : ℕ, x.D = 4 ^ k) ∧ 4 ≤ x.D ∧ x.D ^ 18 ≤ x.N ∧
56	(x.W.length : ℝ) ≤ (x.N : ℝ) ^ 2 / Real.sqrt x.D ∧ x.U = x.N ^ c)
57	(fun x => C * ((x.N : ℝ) ^ 2 * Real.log x.D ^ 2 / (x.D : ℝ) ^ (1 / 18 : ℝ)))
58
59	/-- Theorem 25: "For every ε < ε* and every κ > 0 there is a γ > 0 such that the
60	following holds. Given as input matrices [...], where 2 ≤ D ≤ N^ε, [...] as well as a set W of at
61	most N²/D^κ positions of an N × N matrix, the entries (XY)[I,J], (I,J) ∈ W, can be computed
62	deterministically in time O(N² log² D/D^γ)." -/
63	def Theorem_25 : Prop :=
64	∀ ε κ : ℝ, ε < epsStar → 0 < κ → ∃ γ : ℝ, 0 < γ ∧
65	∀ c₀ : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ),
66	Solves (thinProduct []) P b
67	(fun x => thinDom 2 ε c₀ x.toThinPair ∧ (x.W.length : ℝ) ≤ (x.N : ℝ) ^ 2 / (x.D : ℝ) ^ κ)
68	(fun x => C * ((x.N : ℝ) ^ 2 * Real.log x.D ^ 2 / (x.D : ℝ) ^ γ))
69
70	/-- Corollary 26, last sentence: "Hence, for every set W of positions of an N × N
71	matrix, the entries (XY)[I,J], (I,J) ∈ W, can be computed deterministically in O(\|W\| D^{0.437} +
72	N²/D^{0.063}) time". (With `D ≥ 1`, as in `Corollary_26`.) -/
73	def Corollary_26_wanted : Prop :=
74	∀ c : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ),
75	Solves (thinProduct []) P b (fun x => 1 ≤ x.D ∧ x.D ^ 18 ≤ x.N ∧ x.U = x.N ^ c)
76	(fun x => C * ((x.W.length : ℝ) * (x.D : ℝ) ^ (0.437 : ℝ) +
77	(x.N : ℝ) ^ 2 / (x.D : ℝ) ^ (0.063 : ℝ)))
78
79	/-- Theorem 30, the offline form (9): "In particular, for every set W of positions of
80	an N × N matrix, the entries (XY)[I,J], (I,J) ∈ W, can be computed deterministically in time O(L \|W\|
81	∑_{d=0}^{t} α_d + L m ρ^t/(1 − ρ) N² + N·10^L/(√K N₀))." -/
82	def Theorem_30_wanted : Prop :=
83	∀ c : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ), ∀ m L t : ℕ,
84	Solves (thinProduct [(m : ℤ), (L : ℤ), (t : ℤ)]) P b
85	(fun x => theorem30Dom c m L t x.toThinPair)
86	(fun x => C * cost9 L m t x.N x.W.length)
87
88	/-- Corollary 32: "Let c, θ, γ, q, X, Y, D, and ε be as in Corollary 31, and let κ > 0.
89	For every set W of at most N²/D^κ positions of an N × N matrix, the entries (XY)[I,J], (I,J) ∈ W,
90	can be computed deterministically in time O(N² log² D (D^{−γ} + D^{q−κ}))". -/
91	def Corollary_32 : Prop :=
92	∀ c θ ε κ : ℝ, 10 < c → 0 < θ → θ < 0.9 → ε < Rc c (gammaOf c θ) → 0 < κ →
93	∀ c₀ : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ),
94	Solves (thinProduct []) P b
95	(fun x => thinDom 2 ε c₀ x.toThinPair ∧ (x.W.length : ℝ) ≤ (x.N : ℝ) ^ 2 / (x.D : ℝ) ^ κ)
96	(fun x => C * ((x.N : ℝ) ^ 2 * Real.log x.D ^ 2 *
97	((x.D : ℝ) ^ (-gammaOf c θ) + (x.D : ℝ) ^ (qOf θ - κ))))
98
99	/-- For every `ε < ε₀` and every `κ > 0` there is a `γ > 0` such that, whenever `D ≤ N^ε`, the
100	entries at any set of at most `N²/D^κ` positions can be computed in `O(N²/D^γ)` time. The paper has
101	this sentence with `ε₀ = 0.1204` (Theorem 1).
102
103	NOTE. The paper states no lower bound on `D` and `N` here; `D ≥ 1` and `N ≥ 1` are assumed. On the
104	case `D = 1`, which Theorem 25 and Corollary 32 exclude, see the NOTE at `DataStructureBelow`. -/
105	def WantedBelow (ε₀ : ℝ) : Prop :=
106	∀ ε κ : ℝ, ε < ε₀ → 0 < κ → ∃ γ : ℝ, 0 < γ ∧
107	∀ c₀ : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ),
108	Solves (thinProduct []) P b
109	(fun x => thinDom 1 ε c₀ x.toThinPair ∧ (x.W.length : ℝ) ≤ (x.N : ℝ) ^ 2 / (x.D : ℝ) ^ κ)
110	(fun x => C * ((x.N : ℝ) ^ 2 / (x.D : ℝ) ^ γ))
111
112	/-- Theorem 1: "Let N ≥ D^18, let X ∈ ℤ^{N×D} and Y ∈ ℤ^{D×N} have entries of absolute
113	value N^{O(1)}, and let W be any set of \|W\| ≤ N²/√D positions. The entries (XY)[I,J], (I,J) ∈ W,
114	can be computed deterministically in O(N²/D^{0.063}) operations on O(log N)-bit integers. More
115	generally, for every ε < 0.1204 and every κ > 0 there is a γ > 0 such that, whenever D ≤ N^ε
116	and \|W\| ≤ N²/D^κ, the task takes O(N²/D^γ) operations."
117
118	NOTE. The paper states no lower bound on `D`; `D ≥ 1` is assumed, and in the last sentence also
119	`N ≥ 1` (see `WantedBelow`). -/
120	def Theorem_1 : Prop :=
121	(∀ c₀ : ℕ, ∃ (P : List Instr) (b : ℕ) (C : ℝ),
122	Solves (thinProduct []) P b
123	(fun x => 1 ≤ x.D ∧ x.D ^ 18 ≤ x.N ∧ (x.W.length : ℝ) ≤ (x.N : ℝ) ^ 2 / Real.sqrt x.D ∧
124	x.U = x.N ^ c₀)
125	(fun x => C * ((x.N : ℝ) ^ 2 / (x.D : ℝ) ^ (0.063 : ℝ)))) ∧
126	WantedBelow 0.1204
127
128	/-- Faster computation of selected matrix-product entries: Theorem 5. -/
129	axiom theorem5 : Theorem_5
130
131
132	/-- Faster computation of selected matrix-product entries: Theorem 25. -/
133	axiom theorem25 : Theorem_25
134
135
136	/-- Faster computation of selected matrix-product entries: Corollary 26 wanted. -/
137	axiom corollary26_wanted : Corollary_26_wanted
138
139
140	/-- Faster computation of selected matrix-product entries: Theorem 30 wanted. -/
141	axiom theorem30_wanted : Theorem_30_wanted
142
143
144	/-- Faster computation of selected matrix-product entries: Corollary 32. -/
145	axiom corollary32 : Corollary_32
146
147
148	/-- Faster computation of selected matrix-product entries: Theorem 1. -/
149	axiom theorem1 : Theorem_1
150
151	end Lax350013.SparseMatrixProduct
152

Show ProofShow ProofShow ProofShow ProofShow ProofShow Proof

Builds on

Lax350013.MatrixPreprocessing

Used by

none

From Mathlib

Discussion

Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

Loading discussion…

Lax Lean Archive

Faster computation of selected matrix-product entries

Flags

Flag this concept

Natural Language Statement

Theorem

1 `corollary26_wanted` proven

2 `corollary32` proven

3 `theorem1` proven

4 `theorem25` proven

5 `theorem30_wanted` proven

6 `theorem5` proven

Lean source view on GitHub

Discussion

Settings