OAI/NumberTheory/Ostmann/Characters/CharacterPoissonCutoff.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual rounded initial cutoff covers the Poisson window

  1. theorem OAI.Ostmann.eventual_character_poisson_cutoff line 12

    Source documentation

    The original two-sqrt reserve absorbs the fixed Fourier support and the covering error of the selected cells, including the floor in the cutoff.

    theorem eventual_character_poisson_cutoff (C H : ℝ) (hH : 0 ≤ H) :
    ∀ᶠ m : ℝ in atTop, ∀ Δ : ℝ, 0 ≤ Δ →
      H * Real.exp (Δ + C) ≤ naturalTransferCutoff Δ m 0 := by
…

    Mentions: OAI.Ostmann.naturalTransferCutoff

  2. theorem OAI.Ostmann.eventual_character_poisson_window line 32