OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticDiagonalPatternNormRate.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The diagonal budget after both giant and bulk comparisons

  1. theorem OAI.Ostmann.arithmetic_diagonal_pattern_norm_rate line 15

    Source documentation

    The actual pattern sum and paired frequency sum have an absolute bulk constant. The cutoff includes the constructed bottom reserve 2 sqrt(m). The five comparison errors retain their saving after the full history count.

    theorem arithmetic_diagonal_pattern_norm_rate (ψ : SchwartzMap ℝ ℂ) (n k : ℕ)
    (hk : 0 < k) (hn : n ≤ k) (B Cfreq Cprior ε : ℝ)
    (hCfreq : 0 ≤ Cfreq) (hCprior : 1 ≤ Cprior) (hε : 0 < ε)
    (hdepth : 8 * Cprior ≤ (k : ℝ) ^ 3) :
    ∀ᶠ L : ℝ in atTop, let m := spectatorBulkCount k L
…

    Mentions: OAI.Ostmann.spectatorBulkCount