Exponents for thin matrix preprocessing

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

definition

Loading review…

Natural Language Statement

Definition

The entropy expression and parameter functions governing the preprocessing/query trade-off in Section 4. The threshold is $\varepsilon^*=\log 4/(5\log 10)>0.1204$ . The cost expressions retain the paper’s integer recursion parameters and logarithmic factors.

Concept map

1 concept; 4 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/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
26	/-!
27	---
28	title: Exponents for thin matrix preprocessing
29	type: definition
30	---
31	The entropy expression and parameter functions governing the preprocessing/query trade-off in Section 4. The threshold is $\varepsilon^*=\log 4/(5\log 10)>0.1204$ . The cost expressions retain the paper’s integer recursion parameters and logarithmic factors.
32	-/
33
34	namespace Lax350013.MatrixParameters
35
36	open Finset
37
38	/-- Section 2.3.3: "N₀ := 3^{L-m}". Meant for `m ≤ L`; for `m > L` the subtraction of natural
39	numbers is cut off at 0 and the value is 1. -/
40	def N0 (L m : ℕ) : ℕ := 3 ^ (L - m)
41
42	/-- Section 2.3.3: "K := binom(L, m)", the number of subsets of `{1, …, L}` of size `m`. -/
43	def K (L m : ℕ) : ℕ := L.choose m
44
45	/-- Section 2.4.3: "α_d := binom(m, d) 9^d". -/
46	def alpha (m d : ℕ) : ℕ := m.choose d * 9 ^ d
47
48	/-- The decay rate of the `β_d` (Table 1, and Section 4.3): "ρ := 9m / (L - m + 1)". -/
49	noncomputable def rho (L m : ℕ) : ℝ := 9 * (m : ℝ) / ((L : ℝ) - (m : ℝ) + 1)
50
51	/-- The expression inside the `O(·)` of (8) (preprocessing time and space of Theorem 30):
52	"L m ρ^t/(1 - ρ) N² + N · 10^L / (√K N₀)". -/
53	noncomputable def cost8 (L m t N : ℕ) : ℝ :=
54	(L : ℝ) * (m : ℝ) * (rho L m ^ t / (1 - rho L m)) * (N : ℝ) ^ 2
55	+ (N : ℝ) * (10 : ℝ) ^ L / (Real.sqrt (K L m : ℝ) * (N0 L m : ℝ))
56
57	/-- The expression inside the `O(·)` of the query time of Theorem 30:
58	"L ∑_{d=0}^{t} α_d". -/
59	noncomputable def costQuery (L m t : ℕ) : ℝ := (L : ℝ) * ∑ d ∈ range (t + 1), (alpha m d : ℝ)
60
61	/-- The expression inside the `O(·)` of (9), Theorem 30, for a set of `W` positions:
62	"L \|W\| ∑_{d=0}^{t} α_d + L m ρ^t/(1 - ρ) N² + N · 10^L / (√K N₀)". The paper labels the three terms
63	"queries", "boxes" and "encodings". -/
64	noncomputable def cost9 (L m t N W : ℕ) : ℝ :=
65	(L : ℝ) * (W : ℝ) * ∑ d ∈ range (t + 1), (alpha m d : ℝ) + cost8 L m t N
66
67	/-- Section 4.4: "let H(x) := -x ln x - (1 - x) ln(1 - x) be the entropy function (with natural
68	logarithms)". (Lean's `Real.log 0 = 0` gives `H(0) = H(1) = 0`, the usual convention.) -/
69	noncomputable def entropy (θ : ℝ) : ℝ := -θ * Real.log θ - (1 - θ) * Real.log (1 - θ)
70
71	/-- The denominator of equation (11), which the paper calls `ln Λ`:
72	`c ln 10 - (1/2) c H(1/c) - (c - 1) ln 3 + γ ln 4`, where "Λ := 10^c e^{-(1/2) c H(1/c)} 3^{-(c-1)}
73	4^γ" (Section 4.4). -/
74	noncomputable def lnΛ (c γ : ℝ) : ℝ :=
75	c * Real.log 10 - (1 / 2) * c * entropy (1 / c) - (c - 1) * Real.log 3 + γ * Real.log 4
76
77	/-- Equation (11): "R_c(γ) := ln 4 / ln Λ". -/
78	noncomputable def Rc (c γ : ℝ) : ℝ := Real.log 4 / lnΛ c γ
79
80	/-- Section 4.1: "Let ε* := ln 4 / (5 ln 10)". -/
81	noncomputable def epsStar : ℝ := Real.log 4 / (5 * Real.log 10)
82
83	/-- Corollary 31: "ρ_c := 9/(c - 1)". -/
84	noncomputable def rhoC (c : ℝ) : ℝ := 9 / (c - 1)
85
86	/-- Corollary 31: "γ := θ ln(1/ρ_c) / ln 4". -/
87	noncomputable def gammaOf (c θ : ℝ) : ℝ := θ * Real.log (1 / rhoC c) / Real.log 4
88
89	/-- Corollary 31: "q := (H(θ) + θ ln 9) / ln 4". -/
90	noncomputable def qOf (θ : ℝ) : ℝ := (entropy θ + θ * Real.log 9) / Real.log 4
91
92	end Lax350013.MatrixParameters
93

Builds on

none

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

Exponents for thin matrix preprocessing

Flags

Flag this concept

Natural Language Statement

Definition

Lean source view on GitHub

Discussion

Settings

Your comments