CrudeTraceCatalog.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The complete numerical trace catalog has the required crude exponential cost.

theorem OAI.TwoPointCorrelations.crude_trace_catalog_exp_bound line 14

Source documentation

This includes signs, all equality patterns, numerical tuple/padding primes, the step weights, singleton multiplicities, and external dimensions.

theorem crude_trace_catalog_exp_bound (R T S : ℕ) (P Q : Finset ℕ)
    (F : Finset (Fin R → SignedStep)) (L C Cexternal Csingle external : ℝ)
    (hR : 1 ≤ R) (hL : 1 ≤ L) (hlog : 1 ≤ Real.log L) (hRscale : (R : ℝ) ≤ 2 * L)
    (hC : 0 ≤ C) (hCe : 0 ≤ Cexternal)
    (hS : (S : ℝ) ≤ Csingle * L * Real.log L)
    (hext : external ≤ Real.exp (Cexternal * L))
    (hslots : (T : ℝ) ≤ C * R * Real.log L)
    (hT : (T : ℝ) + 1 ≤ L ^ (2 : ℕ)) (hRpoly : (R : ℝ) + 1 ≤ L ^ (2 : ℕ))
    (hP : primeHarmonicMass P ≤ L ^ (2 : ℕ)) (hQ : primeHarmonicMass Q ≤ L ^ (2 : ℕ))
    (hactual : ∀ w ∈ F, Fintype.card (ActualPrimeSlot w) ≤ T)
    (ht : ∀ w ∈ F, ∀ i, Squarefree (w i).tuple)
    (hq : ∀ w ∈ F, ∀ i, Squarefree (w i).padding)
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.ActualPrimeSlot