OAI/NumberTheory/Ostmann/ZeroDensity/ActualRealZeroRegion.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual low-height real-character zero-free region

  1. theorem OAI.Ostmann.exists_actual_real_low_height_region line 15

    Source documentation

    A single absolute zero-free constant works for every real primitive character. Shrinking the progression constant will align the two inputs.

    theorem exists_actual_real_low_height_region : ∃ κ : ℝ, 0 < κ ∧
    ∀ P : PublishedProgressionInput, P.kappa ≤ κ → ActualRealLowHeightRegion P := by
…

    Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.ActualRealLowHeightRegion