Determinant bound passes through tested series limits
ProvedOAI.PiExponent.Collision.tested_series_determinant_limitnumber-theoryopenai-pi-exponent-017
If every finite partial-sum matrix has determinant norm at most K and each entry series sums to the corresponding entry of T, then T’s determinant norm is at most K.
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.tested_series_determinant_limit
{ι κ : Type*} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
(group : ι → κ) (B : ι → ℕ → ℂ) (C : κ → ℕ → ι → ℂ)
(T : Matrix ι ι ℂ)
(hsum : ∀ r c, HasSum (fun d => B r d * C (group r) d c) (T r c))
(K : ℝ)
(hbound : ∀ N, ‖Matrix.det (fun r c =>
∑ d ∈ Finset.range N, B r d * C (group r) d c)‖ ≤ K) :
‖T.det‖ ≤ K := by sorrySource