Explicit thin matrix preprocessing bounds

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

proven

Loading review…

Natural Language Statement

Theorem

Corollary 26 gives $O(N^2/D^{0.063})$ preprocessing time and space and $O(D^{0.437})$ time per query for $1\leq D$ and $D^{18}\leq N$ . Theorem 30 gives the underlying bounds at integer recursion parameters. Theorem 3 extends the trade-off to every $\varepsilon<0.1204$ and every positive query exponent.

Concept map

7 concepts; 1 descendant hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

This concept declares 3 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.MatrixTradeoffs
26
27	/-!
28	---
29	title: Explicit thin matrix preprocessing bounds
30	type: theorem
31	---
32	Corollary 26 gives $O(N^2/D^{0.063})$ preprocessing time and space and $O(D^{0.437})$ time per query for $1\leq D$ and $D^{18}\leq N$ . Theorem 30 gives the underlying bounds at integer recursion parameters. Theorem 3 extends the trade-off to every $\varepsilon<0.1204$ and every positive query exponent.
33	-/
34
35	namespace Lax350013.MatrixPreprocessing
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
44	/-- Corollary 26, first two sentences: "Let N ≥ D^18, and let X ∈ ℤ^{N×D} and Y ∈ ℤ^{D×N}
45	have entries of absolute value at most N^{O(1)}. We can preprocess them deterministically in
46	O(N²/D^{0.063}) time and space, after which any single entry (XY)[I,J] can be computed
47	deterministically in O(D^{0.437}) time."
48
49	NOTE. The paper states no lower bound on `D`; `D ≥ 1` is assumed (for `D = 0` the bound
50	`O(D^{0.437})` would be 0 steps). -/
51	def Corollary_26 : Prop :=
52	∀ c : ℕ, ∃ (P Q : List Instr) (qI qJ qOut : ℤ) (b : ℕ) (C : ℝ),
53	IsDataStructure P Q qI qJ qOut b [] (fun x => 1 ≤ x.D ∧ x.D ^ 18 ≤ x.N ∧ x.U = x.N ^ c)
54	(fun x => C * ((x.N : ℝ) ^ 2 / (x.D : ℝ) ^ (0.063 : ℝ)))
55	(fun x => C * ((x.N : ℝ) ^ 2 / (x.D : ℝ) ^ (0.063 : ℝ)))
56	(fun x => C * (x.D : ℝ) ^ (0.437 : ℝ))
57
58	/-- The hypotheses of Theorem 30: "Let m ≥ 1, D = 4^m, L ≥ 10m, 0 ≤ t ≤ m, and N ≥ √K
59	N₀", with entries "of absolute value at most N^{O(1)}". -/
60	def theorem30Dom (c m L t : ℕ) (x : ThinPair) : Prop :=
61	1 ≤ m ∧ x.D = 4 ^ m ∧ 10 * m ≤ L ∧ t ≤ m ∧ Real.sqrt (K L m) * (N0 L m : ℝ) ≤ (x.N : ℝ) ∧
62	x.U = x.N ^ c
63
64	/-- Theorem 30: "we can preprocess them deterministically in time and space" (8). "After
65	this, any single entry (XY)[I,J] can be computed deterministically in O(L ∑_{d=0}^{t}
66	α_d) time." "The constants hidden in the O(·) depend only on the exponent in N^{O(1)}": the
67	constant `C` is chosen after the exponent `c` and before `m`, `L`, `t`. These parameters are given
68	to the preprocessing after `N` and `D`; the two programs do not depend on them. -/
69	def Theorem_30 : Prop :=
70	∀ c : ℕ, ∃ (P Q : List Instr) (qI qJ qOut : ℤ) (b : ℕ) (C : ℝ), ∀ m L t : ℕ,
71	IsDataStructure P Q qI qJ qOut b [(m : ℤ), (L : ℤ), (t : ℤ)] (theorem30Dom c m L t)
72	(fun x => C * cost8 L m t x.N) (fun x => C * cost8 L m t x.N) (fun _ => C * costQuery L m t)
73
74	/-- Theorem 3: "Let N ≥ D^18, and let X ∈ ℤ^{N×D}, Y ∈ ℤ^{D×N} have entries of absolute
75	value N^{O(1)}. The pair (X,Y) can be preprocessed deterministically in O(N²/D^{0.063}) time [...].
76	After this, any single entry (XY)[I,J] can be computed deterministically in O(D^{0.437}) time [...].
77	More generally, for every ε < 0.1204 and every q > 0 there is a γ > 0 such that, whenever D ≤ N^ε,
78	the pair can be preprocessed in O(N²/D^γ) time, after which any single entry can be computed in
79	O(D^q) time." The first part is `Corollary_26`.
80
81	NOTE. The departures are those of the two definitions: `D ≥ 1` in the first part; `D ≥ 1` and
82	`N ≥ 1` in the second; and in both the space is bounded like the time, while the theorem speaks of
83	time only. -/
84	def Theorem_3 : Prop :=
85	Corollary_26 ∧ DataStructureBelow 0.1204
86
87	/-- Explicit thin matrix preprocessing bounds: Corollary 26. -/
88	axiom corollary26 : Corollary_26
89
90
91	/-- Explicit thin matrix preprocessing bounds: Theorem 30. -/
92	axiom theorem30 : Theorem_30
93
94
95	/-- Explicit thin matrix preprocessing bounds: Theorem 3. -/
96	axiom theorem3 : Theorem_3
97
98	end Lax350013.MatrixPreprocessing
99

Show ProofShow ProofShow Proof

Builds on

Lax350013.MatrixTradeoffs

Used by

Lax350013.SparseMatrixProduct

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

Explicit thin matrix preprocessing bounds

Flags

Flag this concept

Natural Language Statement

Theorem

1 `corollary26` proven

2 `theorem3` proven

3 `theorem30` proven

Lean source view on GitHub

Discussion

Settings

Your comments

Explicit thin matrix preprocessing bounds

Natural Language Statement

Theorem

1 corollary26 proven

2 theorem3 proven

3 theorem30 proven

Lean source view on GitHub

Discussion

1 `corollary26` proven

2 `theorem3` proven

3 `theorem30` proven