Thin matrix preprocessing and query trade-offs

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

proven

Loading review…

Natural Language Statement

Theorem

Theorem 24 and Corollary 31 give preprocessing time/space and per-entry query bounds. For every $\varepsilon<\varepsilon^*$ and $q>0$ , some $\gamma>0$ permits $O(N^2\log^2 D/D^\gamma)$ preprocessing and $O(D^q\log D)$ queries when $2\leq D\leq N^\varepsilon$ . Corollary 31 supplies explicit parameter choices.

Concept map

6 concepts; 2 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

Evidence

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

1 `corollary31` proven

no assumptions

thm✓Lax350013.MatrixTradeoffs (1st statement)

⊢Lax350013Proofs.ThreeSumApsp.lax_wordRam_corollary_31

2 `theorem24` proven

- thm✓Lax350013.MatrixTradeoffs
→
thm✓Lax350013.MatrixTradeoffs (2nd statement)
⊢Lax350013Proofs.ThreeSumApsp.lax_wordRam_theorem_24

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.ThinMatrices
26	import Lax350013.MatrixParameters
27
28	/-!
29	---
30	title: Thin matrix preprocessing and query trade-offs
31	type: theorem
32	---
33	Theorem 24 and Corollary 31 give preprocessing time/space and per-entry query bounds. For every $\varepsilon<\varepsilon^*$ and $q>0$ , some $\gamma>0$ permits $O(N^2\log^2 D/D^\gamma)$ preprocessing and $O(D^q\log D)$ queries when $2\leq D\leq N^\varepsilon$ . Corollary 31 supplies explicit parameter choices.
34	-/
35
36	namespace Lax350013.MatrixTradeoffs
37
38	open Finset
39	open Lax350013.WordRAM
40	open Lax350013.RAMResources
41	open Lax350013.ThinMatrices
42	open Lax350013.MatrixParameters
43
44	/-- The hypotheses on the input in Corollaries 31 and 32 and Theorems 24 and 25: "where 2 ≤ D ≤
45	N^ε", with entries "of absolute value at most N^{O(1)}". `lo` is the lower bound on `D`, which is 2
46	there. (`N ≥ 1` follows if `lo = 2`; for `lo = 1` it excludes `N = 0`, `D = 1`, `ε = 0`, where the
47	bounds with the factor `N²` would be 0.) -/
48	def thinDom (lo : ℕ) (ε : ℝ) (c₀ : ℕ) (x : ThinPair) : Prop :=
49	1 ≤ x.N ∧ lo ≤ x.D ∧ (x.D : ℝ) ≤ (x.N : ℝ) ^ ε ∧ x.U = x.N ^ c₀
50
51	/-- The conclusion of Theorem 24 and Corollary 31: there is a data structure for the inputs with
52	`2 ≤ D ≤ N^ε` with preprocessing in `O(N² log² D/D^γ)` time and space and queries in
53	`O(D^q log D)` time. -/
54	def HasDataStructure (ε γ q : ℝ) : Prop :=
55	∀ c₀ : ℕ, ∃ (P Q : List Instr) (qI qJ qOut : ℤ) (b : ℕ) (C : ℝ),
56	IsDataStructure P Q qI qJ qOut b [] (thinDom 2 ε c₀)
57	(fun x => C * ((x.N : ℝ) ^ 2 * Real.log x.D ^ 2 / (x.D : ℝ) ^ γ))
58	(fun x => C * ((x.N : ℝ) ^ 2 * Real.log x.D ^ 2 / (x.D : ℝ) ^ γ))
59	(fun x => C * ((x.D : ℝ) ^ q * Real.log x.D))
60
61	/-- Theorem 24: "For every ε < ε*, and every q > 0, there is a γ > 0 such that the
62	following holds. Given as input matrices X ∈ ℤ^{N×D} and Y ∈ ℤ^{D×N}, where 2 ≤ D ≤ N^ε, whose
63	entries are integers of absolute value at most N^{O(1)}, we can preprocess them deterministically in
64	O(N² log² D/D^γ) time and space, after which any single entry (XY)[I,J] can be computed
65	deterministically in O(D^q log D) time." -/
66	def Theorem_24 : Prop :=
67	∀ ε q : ℝ, ε < epsStar → 0 < q → ∃ γ : ℝ, 0 < γ ∧ HasDataStructure ε γ q
68
69	/-- Corollary 31: "Let c > 10 and 0 < θ < 0.9, let ρ_c := 9/(c−1), and let γ := θ
70	ln(1/ρ_c)/ln 4 > 0 and q := (H(θ) + θ ln 9)/ln 4. Given as input matrices X ∈ ℤ^{N×D} and Y ∈
71	ℤ^{D×N} whose entries are integers of absolute value at most N^{O(1)}, where 2 ≤ D ≤ N^ε and ε <
72	R_c(γ), with R_c as in (11), we can preprocess them deterministically in O(N² log² D/D^γ) time and
73	space, after which any single entry (XY)[I,J] can be computed deterministically in O(D^q log D)
74	time. The constants hidden in the O(·) depend on c, θ, and ε." -/
75	def Corollary_31 : Prop :=
76	∀ c θ ε : ℝ, 10 < c → 0 < θ → θ < 0.9 → ε < Rc c (gammaOf c θ) →
77	HasDataStructure ε (gammaOf c θ) (qOf θ)
78
79	/-- For every `ε < ε₀` and every `q > 0` there is a `γ > 0` such that, whenever `D ≤ N^ε`, the pair
80	can be preprocessed in `O(N²/D^γ)` time (and space), after which any single entry can be computed in
81	`O(D^q)` time. The paper has this sentence with `ε₀ = 0.1204` (Theorem 3).
82
83	NOTE. The paper states no lower bound on `D` and `N` here, and speaks of time only; `D ≥ 1` and
84	`N ≥ 1` are assumed, and the space is bounded like the time. Theorem 24 has logarithmic factors and
85	assumes `D ≥ 2`; on the step from there Section 4.1 says: "The logarithmic factors in both theorems
86	can be removed by halving γ and applying Theorem 24 with q/2 in place of q; for D = 1 the bounds are
87	trivial." -/
88	def DataStructureBelow (ε₀ : ℝ) : Prop :=
89	∀ ε q : ℝ, ε < ε₀ → 0 < q → ∃ γ : ℝ, 0 < γ ∧
90	∀ c₀ : ℕ, ∃ (P Q : List Instr) (qI qJ qOut : ℤ) (b : ℕ) (C : ℝ),
91	IsDataStructure P Q qI qJ qOut b [] (thinDom 1 ε c₀)
92	(fun x => C * ((x.N : ℝ) ^ 2 / (x.D : ℝ) ^ γ))
93	(fun x => C * ((x.N : ℝ) ^ 2 / (x.D : ℝ) ^ γ))
94	(fun x => C * (x.D : ℝ) ^ q)
95
96	/-- Thin matrix preprocessing and query trade-offs: Theorem 24. -/
97	axiom theorem24 : Theorem_24
98
99
100	/-- Thin matrix preprocessing and query trade-offs: Corollary 31. -/
101	axiom corollary31 : Corollary_31
102
103	end Lax350013.MatrixTradeoffs
104

Show ProofShow Proof

Builds on

Used by

Lax350013.MatrixPreprocessing

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

Thin matrix preprocessing and query trade-offs

Flags

Flag this concept

Natural Language Statement

Theorem

1 `corollary31` proven

2 `theorem24` proven

Lean source view on GitHub

Discussion

Settings

Your comments

Thin matrix preprocessing and query trade-offs

Natural Language Statement

Theorem

1 corollary31 proven

2 theorem24 proven

Lean source view on GitHub

Discussion

1 `corollary31` proven

2 `theorem24` proven