OrdinaryPrimeIntervals.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The ordinary prime interval and its normalization

The conductor-one character is trivial, so the ordinary prime prior has no Page correction. Its logarithmic interval mass and inverse bound are derived from the same published theta input.

theorem OAI.Ostmann.PrimitiveRealZero.modulus_ne_one line 18
theorem OAI.Ostmann.PublishedProgressionInput.localZero_one line 24
theorem OAI.Ostmann.PublishedProgressionInput.ordinary_log_interval line 30
theorem OAI.Ostmann.log_unit_ratio_lower line 42
theorem OAI.Ostmann.theta_log_error_small line 51
theorem OAI.Ostmann.PublishedProgressionInput.ordinary_interval_lower line 75
theorem OAI.Ostmann.PublishedProgressionInput.ordinary_normalization_bound line 88
Source documentation
The normalizing reciprocal costs only a factor linear in the log coordinate, exactly as required by the arithmetic idealization.
```
theorem PublishedProgressionInput.ordinary_normalization_bound (P : PublishedProgressionInput) :
    ∀ᶠ s : ℝ in atTop,
      0 < reciprocalPrimeInterval 1 0 (Real.exp s) (Real.exp (s + 1)) ∧
      (reciprocalPrimeInterval 1 0 (Real.exp s) (Real.exp (s + 1)))⁻¹ ≤ 2 * (s + 1) := by
…
```
Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.reciprocalPrimeInterval