Finite collision estimate for translated row determinants
ProvedOAI.PiExponent.LiteralAnalytic.TranslatedExpansion.translated_row_determinant_finite_collision_boundnumber-theoryopenai-pi-exponent-017
Under the holomorphicity, disk bound, and center hypotheses, the translated row-test determinant is bounded by a finite product of a factorial factor, the uniform analytic bound, row-order costs, a group collision penalty, and a geometric-tail factor.
Preamble
import Definitions.Def_OAI_NumberTheory_PiExponent_Analysis_TranslatedExpansion_CollisionAnalyticHelpers open scoped BigOperators Topology open OAI.PiExponent.Collision open OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.CollisionAnalytic
Formal statement
theorem OAI.PiExponent.LiteralAnalytic.TranslatedExpansion.translated_row_determinant_finite_collision_bound
{ι κ : Type*} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
(group : ι → κ) (f : κ → ι → ℂ → ℂ)
(center : ι → ℂ) (ell : ι → ℕ)
(R : NNReal) (hR : 0 < R) {H budgetCoeff : ℝ}
(hf : ∀ A c, Differentiable ℂ (f A c))
(hfD : ∀ A c z, z ∈ Metric.sphere (0 : ℂ) (R : ℝ) →
‖f A c z‖ ≤ Real.exp (H * budgetCoeff))
(hc : ∀ r, ‖center r‖ + 3 / 4 ≤ (R : ℝ) / 2) :
‖Matrix.det (fun r c => rowTest (ell r)
(fun t => f (group r) c (center r + Complex.log (1 + t))))‖ ≤
(((Fintype.card ι).factorial : ℝ) *
Real.exp (H * budgetCoeff) ^ Fintype.card ι *
(2 : ℝ) ^ (∑ r, ell r)) *
Collision.collisionRatio ^
(∑ A : κ, (((Finset.univ : Finset ι).filter
(fun r => group r = A)).card.choose 2)) *
((1 - Collision.collisionRatio)⁻¹) ^ Fintype.card ι := by sorrySource