Factor-preserving collision bound for logarithmically translated entire columns
ProvedOAI.PiExponent.FinitePeriodCollision.analytic_collision_factor_boundirrationality-measurenumber-theoryopenai-pi-exponent-017
Entire column functions bounded by D on a positive-radius circle satisfy the explicit factorial, row-order, and within-group collision determinant estimate when their translated logarithmic tests lie inside the half-radius region.
Preamble
import Definitions.Def_OAI_PiExponent_FinitePeriodAnalytic open scoped BigOperators open OAI.PiExponent open OAI.PiExponent.DeterminantContradiction.FiniteTranslation open OAI.PiExponent.FinitePeriodCollision
Formal statement
theorem OAI.PiExponent.FinitePeriodCollision.analytic_collision_factor_bound
{ι κ : Type*}
[Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ]
(group : ι → κ) (f : κ → ι → ℂ → ℂ)
(center : ι → ℂ) (ell : ι → ℕ)
(R : NNReal) (hR : 0 < R) (D s : ℝ)
(hD : 0 ≤ D) (hs0 : 0 ≤ s) (hs1 : s < 1)
(hss : s * s = 1 / 2)
(hf : ∀ b c, Differentiable ℂ (f b c))
(hfD : ∀ b c z, z ∈ Metric.sphere (0 : ℂ) (R : ℝ) → ‖f b c z‖ ≤ D)
(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 : ℝ) * D ^ Fintype.card ι *
(2 : ℝ) ^ (∑ r, ell r)) *
s ^ (∑ b : κ,
(((Finset.univ : Finset ι).filter (fun r => group r = b)).card).choose 2) *
((1 - s)⁻¹) ^ Fintype.card ι := by sorrySource