OAI/NumberTheory/Ostmann/Characters/CharacterBandCutoffs.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Integer endpoints for the separated character prime bands

  1. theorem OAI.Ostmann.eventual_double_exp_integer_margin line 12

    Source documentation

    A fixed positive gap in log-log scale supplies the factor two required by the one-sided character estimate, even after rounding upward.

    theorem eventual_double_exp_integer_margin (α β : ℝ) (hβ : 0 < β) (hαβ : α < β) :
    ∀ᶠ L : ℝ in atTop,
      2 * (⌈Real.exp (Real.exp (α * L))⌉₊ : ℝ) ≤ Real.exp (Real.exp (β * L)) := by
…
  2. theorem OAI.Ostmann.eventual_character_band_lower line 33
  3. theorem OAI.Ostmann.character_band_upper line 43