Finite truncation collision estimate
ProvedOAI.PiExponent.Collision.finite_tested_series_collision_boundnumber-theoryopenai-pi-exponent-017
For every finite cutoff N, the determinant of the matrix formed from degrees d<N obeys the collision estimate under the target coefficient and parameter bounds.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Choose.Basic import Mathlib.Topology.Algebra.InfiniteSum.Basic import Mathlib.LinearAlgebra.Matrix.Determinant.Basic open scoped BigOperators Topology
Formal statement
theorem OAI.PiExponent.Collision.finite_tested_series_collision_bound
{ι κ : Type*} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
(group : ι → κ) (B : ι → ℕ → ℂ) (C : κ → ℕ → ι → ℂ)
(D s : ℝ) (L : ι → ℝ) (N : ℕ)
(hD : 0 ≤ D) (hs0 : 0 ≤ s) (hs1 : s < 1)
(hL : ∀ r, 0 ≤ L r)
(hC : ∀ A d c, ‖C A d c‖ ≤ D)
(hB : ∀ r d, ‖B r d‖ ≤ L r * (s * s) ^ d) :
‖Matrix.det (fun r c => ∑ d ∈ Finset.range N, B r d * C (group r) d c)‖ ≤
(((Fintype.card ι).factorial : ℝ) * D ^ Fintype.card ι * (∏ r, L r)) *
s ^ (∑ A : κ, (((Finset.univ : Finset ι).filter
(fun r => group r = A)).card.choose 2)) *
((1 - s)⁻¹) ^ Fintype.card ι := by sorrySource