Time bounds for callable algorithms and reductions

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

definition

Loading review…

Natural Language Statement

Definition

Running-time statements interpreted by actual procedures with the preceding memory and resource contracts. A reduction converts any solver satisfying its input contract into a solver for its output problem, charging all calls and overhead. The model is a definition, not an assumed machine oracle.

Concept map

7 concepts; 5 descendants hidden

100%

Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

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/ThreeSumApsp/TimeClaims/Sec3/Definitions.lean / Programs/LightModel.lean / Sec3/Parameters.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.CallableProblems
26
27	/-!
28	---
29	title: Time bounds for callable algorithms and reductions
30	type: definition
31	---
32	Running-time statements interpreted by actual procedures with the preceding memory and resource contracts. A reduction converts any solver satisfying its input contract into a solver for its output problem, charging all calls and overhead. The model is a definition, not an assumed machine oracle.
33	-/
34
35	namespace Lax350013.CallableAlgorithms
36
37	open Finset
38	open Lax350013.StructuredPrograms
39	open Lax350013.ProcedureContracts
40	open Lax350013.CallableProblems
41
42	open Filter Asymptotics
43
44	/-- The largest number of query pairs that is "at most n²/√D" (Corollary 15 and Theorem 17;
45	Theorem 5 has "at most N²/√D"): `⌊n²/√D⌋`. -/
46	noncomputable def queryCap (n D : ℕ) : ℕ := ⌊(n : ℝ) ^ 2 / Real.sqrt D⌋₊
47
48	/-- `f(n) = n^{a+o(1)}`.
49
50	NOTE. We read it as an upper bound, as the paper uses it for times and for numbers and sizes of
51	instances: there is a sequence `ε(n) → 0` with `\|f(n)\| ≤ n^{a+ε(n)}` for all large `n`. -/
52	def IsPowLittleO (f : ℕ → ℝ) (a : ℝ) : Prop :=
53	∃ ε : ℕ → ℝ, Filter.Tendsto ε Filter.atTop (nhds 0) ∧
54	∀ᶠ n : ℕ in Filter.atTop, \|f n\| ≤ (n : ℝ) ^ (a + ε n)
55
56	/-- `f(n) = O(n^a (log n)^{O(1)})`. -/
57	def IsPowPolylog (f : ℕ → ℝ) (a : ℝ) : Prop :=
58	∃ e : ℕ, Asymptotics.IsBigO Filter.atTop f fun n : ℕ => (n : ℝ) ^ a * Real.log n ^ e
59
60	/-- `f(n) = O(n^a)`. -/
61	def IsBigOPow (f : ℕ → ℝ) (a : ℝ) : Prop :=
62	Asymptotics.IsBigO Filter.atTop f fun n : ℕ => (n : ℝ) ^ a
63
64	/-- `log U`, read as `log 2` for `U < 2`, so that a bound with `log U` is positive at `U = 1` as
65	well. It occurs in the bounds of Theorem 21(b) and in the overhead for copying in
66	`ConditionalTimes.Claim.RectMinPlusFromSquare`. -/
67	noncomputable def logU (u : ℝ) : ℝ := Real.log (max u 2)
68
69	/-- The cube root of `n`, rounded up: `⌈n^{1/3}⌉`. -/
70	noncomputable def cbrtCeil (n : ℕ) : ℕ := ⌈(n : ℝ) ^ (1 / 3 : ℝ)⌉₊
71
72	/-- Theorem 21(b): "with T(s)/s nondecreasing". -/
73	def DivNondecreasing (T : ℕ → ℝ) : Prop :=
74	∀ s₁ s₂ : ℕ, 1 ≤ s₁ → s₁ ≤ s₂ → T s₁ / s₁ ≤ T s₂ / s₂
75
76	/-- Theorem 21(b): a running time "T(s) with T(s)/s nondecreasing", for every fixed bound
77	`u` on the numbers.
78
79	NOTE. We also ask that `T(s) ≥ s² (1 + log u)`, which is an upper bound for the time to write down
80	the `3s²` weights of an instance. The paper does not say this, but its bound
81	`O(n² T(n^{1/3}) log² U)` leaves no room for writing down the instances otherwise. The condition is
82	a hypothesis on the running times that are fed into Theorem 21(b), so it makes the claims that use
83	it weaker, not stronger. -/
84	def GoodTime (T : ℕ → ℝ → ℝ) : Prop :=
85	(∀ (s : ℕ) (u : ℝ), 1 ≤ s → (s : ℝ) ^ 2 * (1 + logU u) ≤ T s u) ∧
86	∀ u : ℝ, DivNondecreasing fun s => T s u
87
88	/-- The running time `K s^{3−δ} (log s + 1)^e (1 + log u)²` for Exact Triangle on `s` vertices per
89	part with weights of absolute value at most `u`, as a function of both arguments. -/
90	noncomputable def uniformTime (K δ : ℝ) (e : ℕ) (s : ℕ) (u : ℝ) : ℝ :=
91	K * ((s : ℝ) ^ (3 - δ) * (Real.log s + 1) ^ e * (1 + logU u) ^ 2)
92
93	/-- Theorem 17, the first term of the additional time, "ν n³ log n/g". It pays for the scans.
94	`κ` is the paper's ν. -/
95	noncomputable def termScans (n g : ℕ) (κ : ℝ) : ℝ := κ * (n : ℝ) ^ 3 * Real.log n / (g : ℝ)
96
97	/-- Theorem 17, the second term of the additional time, "n^{ω+o(1)} D^{3/2}". It pays for the
98	choice of the prime. `MM n` stands for the number of ring operations of the matrix multiplication,
99	the paper's `n^{ω+o(1)}`. -/
100	noncomputable def termPrime (MM : ℕ → ℝ) (n D : ℕ) : ℝ := MM n * (D : ℝ) ^ (3 / 2 : ℝ)
101
102	/-- Theorem 17, the third term of the additional time, "n² D g". It pays for building the
103	instances. -/
104	noncomputable def termBuild (n D g : ℕ) : ℝ := (n : ℝ) ^ 2 * (D : ℝ) * (g : ℝ)
105
106	/-- Strassen's number of ring operations, up to a constant: `n^{log₂ 7}`. -/
107	noncomputable def strassen (n : ℕ) : ℝ := (n : ℝ) ^ Real.logb 2 7
108
109	/-- Proof of Theorem 19, by Theorem 5: "Let D be the largest power of four with D ≤
110	n^{1/18}". -/
111	noncomputable def paramD₅ (n : ℕ) : ℕ := 4 ^ Nat.log 4 ⌊(n : ℝ) ^ (1 / 18 : ℝ)⌋₊
112
113	/-- Proof of Theorem 19, by Theorem 5: "and let g := ⌈D^{1/36}⌉". -/
114	noncomputable def paramG₅ (n : ℕ) : ℕ := ⌈(paramD₅ n : ℝ) ^ (1 / 36 : ℝ)⌉₊
115
116	/-- Proof of Theorem 19, by Corollary 26: "Let D := ⌊n^{1/18}⌋". -/
117	noncomputable def paramD₂₆ (n : ℕ) : ℕ := ⌊(n : ℝ) ^ (1 / 18 : ℝ)⌋₊
118
119	/-- Proof of Theorem 19, by Corollary 26: "and g := ⌈D^{0.0315}⌉". -/
120	noncomputable def paramG₂₆ (n : ℕ) : ℕ := ⌈(paramD₂₆ n : ℝ) ^ (0.0315 : ℝ)⌉₊
121
122	/-- Corollary 15: the size `⌊n²/√D⌋` of the sets into which `W` is split (at least 1, so
123	that the split makes sense for all values of the parameters). -/
124	noncomputable def splitCap (n D : ℕ) : ℕ := max 1 (queryCap n D)
125
126	/-- `f(n) = O(n^a)`, as an upper bound. -/
127	def UpperBigOPow (f : ℕ → ℝ) (a : ℝ) : Prop :=
128	∃ C : ℝ, ∀ᶠ n : ℕ in Filter.atTop, f n ≤ C * (n : ℝ) ^ a
129
130	/-- `f(n) = O(n^a (log n)^{O(1)})`, as an upper bound. -/
131	def UpperPowPolylog (f : ℕ → ℝ) (a : ℝ) : Prop :=
132	∃ (C : ℝ) (e : ℕ), ∀ᶠ n : ℕ in Filter.atTop, f n ≤ C * ((n : ℝ) ^ a * Real.log n ^ e)
133
134	/-- There is a sequence `ε(n) → 0` with `f(n) ≤ n^{a+ε(n)}` for all large `n`: a bound on `f` and
135	not on `\|f\|` (that is `IsPowLittleO`). -/
136	def UpperPowLittleO (f : ℕ → ℝ) (a : ℝ) : Prop :=
137	∃ ε : ℕ → ℝ, Filter.Tendsto ε Filter.atTop (nhds 0) ∧
138	∀ᶠ n : ℕ in Filter.atTop, f n ≤ (n : ℝ) ^ (a + ε n)
139
140
141	/-- An interpretation of "a deterministic algorithm solves the problem in time T", for each problem
142	of Sections 2 to 4. Each field is a predicate on running times. The intended meaning of
143	`M.problem T`: there is a deterministic algorithm that gives a correct answer on every input, and
144	that takes time at most `T(parameters)` on every input with these parameters (sizes and `D` as
145	given, at most `w` pairs, numbers at most `u`; sizes and `u` at least 1). -/
146	structure DetTimeModel where
147	/-- Theorem 5: given `X ∈ ℤ^{N×D}`, `Y ∈ ℤ^{D×N}` with entries of absolute value at most
148	`u` and a set of at most `w` positions, compute the wanted entries of `XY` (`IsWantedEntries`).
149	The arguments of the time are `N D w u`. -/
150	thinProduct : (ℕ → ℕ → ℕ → ℝ → ℝ) → Prop
151	/-- #Lop-AE-SparseTri(n, D), Definition 14, with at most `w` query pairs
152	(`LopInstance.IsCountingAnswer`). The arguments of the time are `n D w`. -/
153	lopCount : (ℕ → ℕ → ℕ → ℝ) → Prop
154	/-- Lop-AE-SparseTri(n, D), Definition 13, with at most `w` query pairs
155	(`LopInstance.IsDetectionAnswer`). The arguments of the time are `n D w`. -/
156	lopDetect : (ℕ → ℕ → ℕ → ℝ) → Prop
157	/-- Exact Triangle on `n` vertices per part with integer weights of absolute value at most `u`
158	(`TriangleInstance.HasZeroTriangle`). The arguments of the time are `n u`. -/
159	exactTriangle : (ℕ → ℝ → ℝ) → Prop
160	/-- Negative Triangle, decision (`TriangleInstance.HasNegativeTriangle`). Arguments `n u`. -/
161	negativeTriangle : (ℕ → ℝ → ℝ) → Prop
162	/-- Convolution-3SUM on `N` integers of absolute value at most `u` (`Convolution3SUM`). Arguments
163	`N u`. -/
164	convolution3SUM : (ℕ → ℝ → ℝ) → Prop
165	/-- 3SUM on `n` integers of absolute value at most `u` (`ThreeSum`). Arguments `n u`. -/
166	threeSum : (ℕ → ℝ → ℝ) → Prop
167	/-- The (min,+)-product of two `n × n` integer matrices with entries of absolute value at most `u`
168	(`IsMinPlusProduct`). Arguments `n u`. -/
169	minPlusProduct : (ℕ → ℝ → ℝ) → Prop
170	/-- APSP on directed `n`-vertex graphs with integer weights of absolute value at most `u` and no
171	negative cycles (`IsDistanceMatrix`, `NoNegativeCycle`). Arguments `n u`. -/
172	apsp : (ℕ → ℝ → ℝ) → Prop
173
174	/- ## The bounds in `n`, `D` and the number `w` of positions or query pairs -/
175
176	/-- The bound of Theorem 5 and of the first case of Corollary 15: `n² log² D / D^{1/18}`. -/
177	noncomputable abbrev thinBound (n D : ℕ) : ℝ :=
178	(n : ℝ) ^ 2 * Real.log D ^ 2 / (D : ℝ) ^ (1 / 18 : ℝ)
179
180	/-- The bound of the general case of Corollary 15: `(n² + w √D) log² D / D^{1/18}`. -/
181	noncomputable abbrev splitBound (n D w : ℕ) : ℝ :=
182	((n : ℝ) ^ 2 + (w : ℝ) * Real.sqrt D) * Real.log D ^ 2 / (D : ℝ) ^ (1 / 18 : ℝ)
183
184	/-- The bound of Corollaries 16 and 26: `w D^{0.437} + n² / D^{0.063}`. -/
185	noncomputable abbrev wantedBound (n D w : ℕ) : ℝ :=
186	(w : ℝ) * (D : ℝ) ^ (0.437 : ℝ) + (n : ℝ) ^ 2 / (D : ℝ) ^ (0.063 : ℝ)
187
188	namespace Closure
189
190	/-- A larger bound on the running time is still a bound on the running time (for Exact Triangle). -/
191	def MonoExactTriangle (M : DetTimeModel) : Prop :=
192	∀ T T' : ℕ → ℝ → ℝ, (∀ (s : ℕ) (u : ℝ), 1 ≤ s → 1 ≤ u → T s u ≤ T' s u) →
193	M.exactTriangle T → M.exactTriangle T'
194
195	/-- Two algorithms for Exact Triangle can be combined into one that looks at the number of vertices
196	and runs the first one below a fixed threshold `n₀` and the second one from the threshold on, at a
197	constant extra cost. -/
198	def ChooseBySize (M : DetTimeModel) : Prop :=
199	∀ n₀ : ℕ, ∃ C₀ : ℝ, ∀ T₁ T₂ : ℕ → ℝ → ℝ, M.exactTriangle T₁ → M.exactTriangle T₂ →
200	M.exactTriangle fun n u => (if n < n₀ then T₁ n u else T₂ n u) + C₀
201
202	end Closure
203
204	namespace Claim
205
206	/- ## Time sentences -/
207
208	/-- Theorem 5, the time sentence: "Let D ≥ 4 be a power of four and N ≥ D^18. Given as
209	input matrices X ∈ ℤ^{N×D} and Y ∈ ℤ^{D×N}, whose entries are integers of absolute value at most
210	N^{O(1)}, as well as a set W of at most N²/√D positions of an N × N matrix, the entries (XY)[I,J],
211	(I,J) ∈ W, can be computed deterministically in time O(N² log² D/D^{1/18})." `c` is the exponent
212	hidden in `N^{O(1)}`; the constant may depend on it. -/
213	def Theorem_5 (M : DetTimeModel) : Prop :=
214	∀ c : ℝ, ∃ (C : ℝ) (T : ℕ → ℕ → ℕ → ℝ → ℝ), M.thinProduct T ∧
215	∀ (N D w : ℕ) (u : ℝ), (∃ k : ℕ, D = 4 ^ k) → 4 ≤ D → D ^ 18 ≤ N →
216	(w : ℝ) ≤ (N : ℝ) ^ 2 / Real.sqrt D →
217	u ≤ (N : ℝ) ^ c → T N D w u ≤ C * thinBound N D
218
219	/-- Proof of Theorem 19: "smaller instances are solved by brute force". Trying all `n³`
220	triples; the factor `1 + log u` allows for weights that do not fit into one machine word. -/
221	def BruteForce (M : DetTimeModel) : Prop :=
222	∃ C : ℝ, M.exactTriangle fun n u => C * ((n : ℝ) ^ 3 * (1 + logU u))
223
224	/- ## Transfer claims that the paper proves or calls straightforward -/
225
226	/-- Proof of Corollary 15: "Apply Theorem 5 with N = n to the two biadjacency matrices".
227	Writing down the two matrices and copying the answers costs `O(nD + w + 1)`; their entries are 0
228	and 1. -/
229	def LopCountFromThinProduct (M : DetTimeModel) : Prop :=
230	∃ C₀ : ℝ, ∀ T : ℕ → ℕ → ℕ → ℝ → ℝ, M.thinProduct T →
231	M.lopCount fun n D w => T n D w 1 + C₀ * ((n : ℝ) * (D : ℝ) + (w : ℝ) + 1)
232
233	/-- Proof of Corollary 15: the counts "are nonzero exactly for the query pairs that lie in
234	a triangle". -/
235	def LopDetectFromCount (M : DetTimeModel) : Prop :=
236	∃ C₀ : ℝ, ∀ T : ℕ → ℕ → ℕ → ℝ, M.lopCount T →
237	M.lopDetect fun n D w => T n D w + C₀ * ((w : ℝ) + 1)
238
239	/-- Corollary 15: "splitting W into sets of at most n²/√D query pairs":
240	`⌈w / splitCap n D⌉` sets of at most `splitCap n D` query pairs. The overhead allows for handing
241	the graph to every call. -/
242	def LopSplit (M : DetTimeModel) : Prop :=
243	∃ C₀ : ℝ, ∀ T : ℕ → ℕ → ℕ → ℝ, M.lopCount T →
244	M.lopCount fun n D w =>
245	(⌈(w : ℝ) / (splitCap n D : ℝ)⌉₊ : ℝ) *
246	(T n D (splitCap n D) + C₀ * ((n : ℝ) * (D : ℝ) + 1)) +
247	C₀ * ((w : ℝ) + 1)
248
249	/-- Theorem 17, as a transfer claim: "Let 16 ≤ D ≤ n, and let 1 ≤ g ≤ √D be an integer.
250	Exact Triangle on n vertices per part with weights of absolute value at most n^ν reduces
251	deterministically to at most 4ng instances of Lop-AE-SparseTri(n, D), each with at most n²/√D query
252	pairs, plus O(ν n³ log n/g + n^{ω+o(1)} D^{3/2} + n² D g) additional time", and the sentence after
253	the theorem: "The oracle returns at most n²/√D answers per instance, and the time to read them is
254	counted as part of the oracle calls, rather than as additional time."
255
256	`D` and `g` are given functions of `n`, as in Section 3.3; they are parameters of the claim, not
257	quantified inside it, because the algorithm has to compute them. `MM n` stands for the number of
258	ring operations of the matrix multiplication algorithm used, the paper's `n^{ω+o(1)}`, "or O(n^{log₂
259	7}) with Strassen's algorithm". The term `C n²/√D` next to `T` is the reading of the answers.
260	Where the hypotheses on `D n` and `g n` fail, nothing is claimed about the time.
261
262	`κ` is the paper's ν. The constant `C` does not depend on it. -/
263	def Theorem_17 (M : DetTimeModel) (MM : ℕ → ℝ) (D g : ℕ → ℕ) : Prop :=
264	∃ C : ℝ, 0 ≤ C ∧ ∀ T : ℕ → ℕ → ℕ → ℝ, M.lopDetect T →
265	∃ T' : ℕ → ℝ → ℝ, M.exactTriangle T' ∧
266	∀ (n : ℕ) (κ u : ℝ), 16 ≤ D n → D n ≤ n → 1 ≤ g n → (g n : ℝ) ≤ Real.sqrt (D n) → 1 ≤ κ →
267	u ≤ (n : ℝ) ^ κ →
268	T' n u ≤ 4 * (n : ℝ) * (g n : ℝ) *
269	(T n (D n) (queryCap n (D n)) + C * ((n : ℝ) ^ 2 / Real.sqrt (D n))) +
270	C * (termScans n (g n) κ + termPrime MM n (D n) + termBuild n (D n) (g n))
271
272	/-- For Theorem 21(b): if no closed walk has negative weight, then squaring the weight matrix
273	`⌈log₂ n⌉` times in the (min,+)-product yields the distance matrix, and all finite entries that
274	occur have absolute value at most `nU`, where `U` bounds the edge weights. The constant `c` allows
275	for a finite stand-in for the entries `+∞` of the matrices, the term with `C₀` for writing a matrix,
276	and the `+ 1` for the work that remains when `n = 1`. -/
277	def ApspFromMinPlus (M : DetTimeModel) : Prop :=
278	∃ c C₀ : ℝ, 1 ≤ c ∧ ∀ T : ℕ → ℝ → ℝ, M.minPlusProduct T →
279	M.apsp fun n u =>
280	((Nat.clog 2 n : ℝ) + 1) *
281	(T n (c * ((n : ℝ) * u)) + C₀ * ((n : ℝ) ^ 2 * (1 + logU (c * ((n : ℝ) * u)))))
282
283	/- ## Results cited from the literature, in the form needed for Theorem 21 -/
284
285	/-- CITED. After the proof of [CH20, Theorem 5.1]: from n integers bounded by a power of n, a
286	deterministic reduction computes polylogarithmically many arrays of length Õ(n), whose entries are
287	again bounded by a power of n, in Õ(n^{3/2}) time; three of the integers sum to 0 exactly if one of
288	the arrays is a yes-instance of Convolution-3SUM. `E` is the extra time, `Num` the number of
289	instances, `N` their size, `mag` the bound on their numbers. -/
290	def CH20_Theorem_5_1 (M : DetTimeModel) : Prop :=
291	∀ κ : ℝ, 0 ≤ κ → ∃ (E Num mag : ℕ → ℝ) (N : ℕ → ℕ) (c' κ' : ℝ),
292	IsPowPolylog E (3 / 2) ∧ IsPowPolylog Num 0 ∧ IsPowPolylog (fun n => (N n : ℝ)) 1 ∧
293	(∀ n : ℕ, 1 ≤ n → 1 ≤ N n ∧ 1 ≤ mag n ∧ mag n ≤ c' * (n : ℝ) ^ κ') ∧
294	∀ T : ℕ → ℝ → ℝ, M.convolution3SUM T →
295	∃ T' : ℕ → ℝ → ℝ, M.threeSum T' ∧
296	∀ n : ℕ, 1 ≤ n → T' n ((n : ℝ) ^ κ) ≤ E n + Num n * T (N n) (mag n)
297
298	/-- CITED. After the proof of [VW13, Theorem 4.3]: whether an array of `N` integers is a
299	yes-instance of Convolution-3SUM is decided by asking `O(√N)` times whether there is a zero
300	triangle, each time in an instance with `O(√N)` vertices in each part whose weights are entries of
301	the array, up to sign, or a filler, so that all weights are at most a constant times the bound on
302	the entries.
303
304	NOTE. The time `E` of this reduction is part of the claim, because the time of Theorem 21(a) needs
305	`E(N) = N^{3/2+o(1)}`. -/
306	def VW13_Theorem_4_3 (M : DetTimeModel) : Prop :=
307	∃ (c : ℝ) (E Num : ℕ → ℝ) (size : ℕ → ℕ), 1 ≤ c ∧
308	IsPowLittleO E (3 / 2) ∧ IsBigOPow Num (1 / 2) ∧ IsBigOPow (fun N => (size N : ℝ)) (1 / 2) ∧
309	(∀ N : ℕ, 1 ≤ N → 1 ≤ size N) ∧
310	∀ T : ℕ → ℝ → ℝ, M.exactTriangle T →
311	M.convolution3SUM fun N u => E N * (1 + logU u) + Num N * T (size N) (c * u)
312
313	/-- CITED. [VW13, Theorem 3.3]: whether an instance with weights in `[−U, U]` has a negative
314	triangle is decided by asking `O(log U)` times whether there is a zero triangle, each time after
315	changing the weights, edge by edge, to numbers of absolute value `O(U)`; so a time `T(s)` for Exact
316	Triangle gives the time `O(T(s) log U)`. (The constant is taken at least 2 so that the new running
317	time again satisfies `GoodTime`.) -/
318	def VW13_Theorem_3_3 (M : DetTimeModel) : Prop :=
319	∃ c C : ℝ, 1 ≤ c ∧ 2 ≤ C ∧ ∀ T : ℕ → ℝ → ℝ, GoodTime T → M.exactTriangle T →
320	M.negativeTriangle fun s U => C * (T s (c * U) * logU U)
321
322	/-- CITED. [VW18, Theorem 4.2]: from a running time for Negative Triangle that, divided by the
323	number of vertices, is nondecreasing (`GoodTime`), one gets a running time for the (min,+)-product
324	of two n × n matrices with entries in [−U, U], namely O(n² log U) times the time of Negative
325	Triangle on n^{1/3} vertices per part with weights O(U). -/
326	def VW18_Theorem_4_2 (M : DetTimeModel) : Prop :=
327	∃ c C : ℝ, 1 ≤ c ∧ 0 ≤ C ∧ ∀ T' : ℕ → ℝ → ℝ, GoodTime T' → M.negativeTriangle T' →
328	∃ T'' : ℕ → ℝ → ℝ, M.minPlusProduct T'' ∧
329	∀ (n : ℕ) (U : ℝ), 1 ≤ n → 1 ≤ U →
330	T'' n U ≤ C * ((n : ℝ) ^ 2 * T' (cbrtCeil n) (c * U) * logU U)
331
332	/- ## Claims that are derived from the ones above -/
333
334	/-- Corollary 26, last sentence: "Hence, for every set W of positions of an N × N
335	matrix, the entries (XY)[I,J], (I,J) ∈ W, can be computed deterministically in O(\|W\| D^{0.437} +
336	N²/D^{0.063}) time".
337
338	NOTE. The paper states no lower bound on `D`; `D ≥ 1` is assumed. -/
339	def Corollary_26_wanted (M : DetTimeModel) : Prop :=
340	∀ c : ℝ, ∃ (C : ℝ) (T : ℕ → ℕ → ℕ → ℝ → ℝ), M.thinProduct T ∧
341	∀ (N D w : ℕ) (u : ℝ), 1 ≤ D → D ^ 18 ≤ N → u ≤ (N : ℝ) ^ c →
342	T N D w u ≤ C * wantedBound N D w
343
344	/-- Corollary 15, the first case: "Let D ≥ 4 be a power of four with n ≥ D^18, and
345	consider an instance of #Lop-AE-SparseTri(n,D) or of Lop-AE-SparseTri(n,D) with \|W\| query pairs.
346	If \|W\| ≤ n²/√D, then the instance can be solved deterministically in O(n² log² D/D^{1/18}) time."
347	`Tc` is the time for the counting problem, `Td` for the detection problem. -/
348	def Corollary_15_first (M : DetTimeModel) : Prop :=
349	∃ (C : ℝ) (Tc Td : ℕ → ℕ → ℕ → ℝ), 0 ≤ C ∧ M.lopCount Tc ∧ M.lopDetect Td ∧
350	∀ n D w : ℕ, (∃ k : ℕ, D = 4 ^ k) → 4 ≤ D → D ^ 18 ≤ n → (w : ℝ) ≤ (n : ℝ) ^ 2 / Real.sqrt D →
351	Tc n D w ≤ C * thinBound n D ∧ Td n D w ≤ C * thinBound n D
352
353	/-- Corollary 15, the general case: "In general, splitting W into sets of at most n²/√D
354	query pairs solves it deterministically in time O((n² + \|W\|√D) log² D/D^{1/18})." -/
355	def Corollary_15_general (M : DetTimeModel) : Prop :=
356	∃ (C : ℝ) (Tc Td : ℕ → ℕ → ℕ → ℝ), 0 ≤ C ∧ M.lopCount Tc ∧ M.lopDetect Td ∧
357	∀ n D w : ℕ, (∃ k : ℕ, D = 4 ^ k) → 4 ≤ D → D ^ 18 ≤ n →
358	Tc n D w ≤ C * splitBound n D w ∧ Td n D w ≤ C * splitBound n D w
359
360	/-- Corollary 16: "Let n ≥ D^18, and consider an instance of #Lop-AE-SparseTri(n,D) or
361	of Lop-AE-SparseTri(n,D) with \|W\| query pairs. It can be solved deterministically in O(\|W\|
362	D^{0.437} + n²/D^{0.063}) time."
363
364	NOTE. The paper states no lower bound on `D`; `D ≥ 1` is assumed, as in
365	`Claim.Corollary_26_wanted`. -/
366	def Corollary_16 (M : DetTimeModel) : Prop :=
367	∃ (C : ℝ) (Tc Td : ℕ → ℕ → ℕ → ℝ), 0 ≤ C ∧ M.lopCount Tc ∧ M.lopDetect Td ∧
368	∀ n D w : ℕ, 1 ≤ D → D ^ 18 ≤ n →
369	Tc n D w ≤ C * wantedBound n D w ∧ Td n D w ≤ C * wantedBound n D w
370
371	/-- The bound that the deduction in the proof of Theorem 19 yields from
372	`Claim.Theorem_17` and Corollary 15 or 16 when the dependence on `κ` is kept: one algorithm for
373	Exact Triangle that, for every `n ≥ 16^18` and every `κ ≥ 1`, takes time at most
374	`K κ n^{3−δ} (log n)^e` on weights of absolute value at most `n^κ`. The paper has
375	`(δ, e) = (1/648, 2)` using Theorem 5 and `(δ, e) = (0.00175, 1)` using Corollary 26. -/
376	def Theorem_19_explicit (M : DetTimeModel) (δ : ℝ) (e : ℕ) : Prop :=
377	∃ (K : ℝ) (T : ℕ → ℝ → ℝ), M.exactTriangle T ∧
378	∀ (n : ℕ) (κ u : ℝ), 16 ^ 18 ≤ n → 1 ≤ κ → u ≤ (n : ℝ) ^ κ →
379	T n u ≤ K * (κ * ((n : ℝ) ^ (3 - δ) * Real.log n ^ e))
380
381	/-- Theorem 19: "For every constant ν ≥ 1, Exact Triangle on n vertices per part with
382	integer weights of absolute value at most n^ν can be solved by a deterministic algorithm in
383	O(n^{3−1/648} log² n) time using Theorem 5 (via Corollary 15), and in O(n^{3−ε'} log n) ≤
384	O(n^{3−ε_T}) time using Corollary 26 (via Corollary 16)." This is the first bound. -/
385	def Theorem_19_first (M : DetTimeModel) : Prop :=
386	∀ κ : ℝ, 1 ≤ κ → ∃ (C : ℝ) (T : ℕ → ℝ → ℝ), M.exactTriangle T ∧
387	∀ᶠ n : ℕ in Filter.atTop, T n ((n : ℝ) ^ κ) ≤ C * ((n : ℝ) ^ (3 - 1 / 648 : ℝ) * Real.log n ^ 2)
388
389	/-- Theorem 19, the second bound, with `ε' = 0.00175` and `ε_T = 0.0017`. -/
390	def Theorem_19_second (M : DetTimeModel) : Prop :=
391	∀ κ : ℝ, 1 ≤ κ → ∃ (C : ℝ) (T : ℕ → ℝ → ℝ), M.exactTriangle T ∧
392	(∀ᶠ n : ℕ in Filter.atTop, T n ((n : ℝ) ^ κ) ≤ C * ((n : ℝ) ^ (3 - 0.00175 : ℝ) * Real.log n)) ∧
393	UpperBigOPow (fun n => T n ((n : ℝ) ^ κ)) (3 - 0.0017)
394
395	/-- Exact Triangle is solved in time `K s^{3−δ} (log s + 1)^e (1 + log u)²` for ALL numbers `s ≥ 1`
396	of vertices per part and ALL bounds `u ≥ 1` on the weights.
397
398	NOTE. This claim is not in the paper. It is what our rendering of "Plug Theorem 19 into
399	Theorem 21" needs: Theorem 21(b) asks for a running time `T(s)`, with `T(s)/s` nondecreasing, at a
400	fixed bound on the weights and for all `s`, and Theorem 21(a) produces instances whose weights are
401	bounded in terms of `n`, not of their own size; Theorem 19 bounds the time only for weights at most
402	`s^κ` and for large `s`. `exactTriangleUniform_of_explicit` derives it from
403	`Claim.Theorem_19_explicit`, brute force and the two closure properties; this works because the
404	bound in `Claim.Theorem_17` is polynomial in `κ` with a constant that does not depend on `κ`. -/
405	def ExactTriangleUniform (M : DetTimeModel) (δ : ℝ) (e : ℕ) : Prop :=
406	∃ K : ℝ, 1 ≤ K ∧ M.exactTriangle (uniformTime K δ e)
407
408	/-- Theorem 21(a): "3SUM on n integers of absolute value at most n^ν reduces
409	deterministically, in n^{3/2+o(1)} time, to n^{1/2+o(1)} instances of Exact Triangle on n^{1/2+o(1)}
410	vertices per part with weights of absolute value n^{O(1)} [CH20, VW13]." `E` is the time of the
411	reduction, `Num` the number of instances, `size` their number of vertices per part, `mag` the bound
412	on their weights. -/
413	def Theorem_21a (M : DetTimeModel) : Prop :=
414	∀ κ : ℝ, 0 ≤ κ → ∃ (E Num mag : ℕ → ℝ) (size : ℕ → ℕ) (c' κ' : ℝ),
415	IsPowLittleO E (3 / 2) ∧ IsPowLittleO Num (1 / 2) ∧
416	IsPowLittleO (fun n => (size n : ℝ)) (1 / 2) ∧
417	(∀ n : ℕ, 1 ≤ n → 1 ≤ size n ∧ 1 ≤ mag n ∧ mag n ≤ c' * (n : ℝ) ^ κ') ∧
418	∀ T : ℕ → ℝ → ℝ, M.exactTriangle T →
419	∃ T' : ℕ → ℝ → ℝ, M.threeSum T' ∧
420	∀ n : ℕ, 1 ≤ n → T' n ((n : ℝ) ^ κ) ≤ E n + Num n * T (size n) (mag n)
421
422	/-- Theorem 21(b), first half: "If a deterministic algorithm solves Exact
423	Triangle on s vertices per part with weights of absolute value at most cU, for a suitable constant
424	c, in time T(s) with T(s)/s nondecreasing, then the (min,+)-product of two n × n integer matrices
425	with entries of absolute value at most U can be computed deterministically in O(n² T(n^{1/3}) log²
426	U) time". The paper's `T(s)` is `T s (c * U)`. -/
427	def Theorem_21b_minPlus (M : DetTimeModel) : Prop :=
428	∃ c C : ℝ, 1 ≤ c ∧ ∀ T : ℕ → ℝ → ℝ, GoodTime T → M.exactTriangle T →
429	∃ T' : ℕ → ℝ → ℝ, M.minPlusProduct T' ∧
430	∀ (n : ℕ) (U : ℝ), 1 ≤ n → 1 ≤ U →
431	T' n U ≤ C * ((n : ℝ) ^ 2 * T (cbrtCeil n) (c * U) * logU U ^ 2)
432
433	/-- Theorem 21(b), second half: "and APSP on directed n-vertex graphs with integer
434	weights of absolute value at most n^ν and no negative cycles in O(n² T(n^{1/3}) log³ n) time".
435
436	NOTE. The printed hypothesis speaks of weights "at most cU" without saying what `U` is for APSP;
437	here it is `U = n^{κ+1}`, with `κ` for ν, which bounds the entries during the repeated squaring. -/
438	def Theorem_21b_apsp (M : DetTimeModel) : Prop :=
439	∀ κ : ℝ, 0 ≤ κ → ∃ c C : ℝ, 1 ≤ c ∧ ∀ T : ℕ → ℝ → ℝ, GoodTime T → M.exactTriangle T →
440	∃ T' : ℕ → ℝ → ℝ, M.apsp T' ∧
441	∀ n : ℕ, 2 ≤ n →
442	T' n ((n : ℝ) ^ κ)
443	≤ C * ((n : ℝ) ^ 2 * T (cbrtCeil n) (c * (n : ℝ) ^ (κ + 1)) * Real.log n ^ 3)
444
445	/- ## Bounds in `n` alone, along `u = n^κ` -/
446
447	/-- On numbers of absolute value at most `n^κ` the problem is solved deterministically in a time of
448	the class `Cls a`, for every constant `κ ≥ 0`. Here `S` is the field of a `DetTimeModel` that
449	belongs to the problem, and `Cls` is `UpperBigOPow` for `O(n^a)`, `UpperPowPolylog` for
450	`O(n^a (log n)^{O(1)})` or `UpperPowLittleO` for `n^{a+o(1)}`. -/
451	def SolvedAlongPow (S : (ℕ → ℝ → ℝ) → Prop) (Cls : (ℕ → ℝ) → ℝ → Prop) (a : ℝ) : Prop :=
452	∀ κ : ℝ, 0 ≤ κ → ∃ T : ℕ → ℝ → ℝ, S T ∧ Cls (fun n => T n ((n : ℝ) ^ κ)) a
453
454	/-- Exact Triangle on `n` vertices per part with integer weights of absolute value at most `n^κ` is
455	solved deterministically in `O(n^a)` time, for every constant `κ ≥ 0`. -/
456	abbrev ExactTriangleIn (M : DetTimeModel) (a : ℝ) : Prop :=
457	SolvedAlongPow M.exactTriangle UpperBigOPow a
458
459	/-- 3SUM on `n` integers of absolute value at most `n^κ` is solved deterministically in
460	`n^{a+o(1)}` time, for every constant `κ ≥ 0`. -/
461	abbrev ThreeSumInLittleO (M : DetTimeModel) (a : ℝ) : Prop :=
462	SolvedAlongPow M.threeSum UpperPowLittleO a
463
464	/-- The (min,+)-product of two `n × n` integer matrices with entries of absolute value at most `n^κ`
465	is computed deterministically in `O(n^a (log n)^{O(1)})` time, for every constant `κ ≥ 0`. -/
466	abbrev MinPlusInPolylog (M : DetTimeModel) (a : ℝ) : Prop :=
467	SolvedAlongPow M.minPlusProduct UpperPowPolylog a
468
469	/-- APSP on directed `n`-vertex graphs with integer weights of absolute value at most `n^κ` and no
470	negative cycles is solved deterministically in `O(n^a (log n)^{O(1)})` time, for every constant
471	`κ ≥ 0`. -/
472	abbrev ApspInPolylog (M : DetTimeModel) (a : ℝ) : Prop :=
473	SolvedAlongPow M.apsp UpperPowPolylog a
474
475	end Claim
476
477
478
479	/-- The reading of "is solved in time T" by programs of the light language. -/
480	noncomputable def lightModel : DetTimeModel where
481	thinProduct := ThinSolvedIn
482	lopCount := LopSolvedIn lopCountTask
483	lopDetect := LopSolvedIn lopDetectTask
484	exactTriangle := SolvedIn etTask
485	negativeTriangle := SolvedIn ntTask
486	convolution3SUM := SolvedIn c3Task
487	threeSum := SolvedIn s3Task
488	minPlusProduct := SolvedIn mpTask
489	apsp := SolvedIn apTask
490
491	end Lax350013.CallableAlgorithms
492

Builds on

Lax350013.CallableProblems

Used by

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

Time bounds for callable algorithms and reductions

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments