RetainedCharacterPrimeBound.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Signed prime mass for a retained primitive real character

def OAI.Ostmann.samePrimitiveRealCharacter line 14
Source documentation
Equality on natural arguments compares characters even when their moduli occur with different dependent types.
```
def samePrimitiveRealCharacter (e : PrimitiveRealZero) (χ : PrimitiveRealCharacter) : Prop :=
…
```
Mentions: OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.PrimitiveRealCharacter
def OAI.Ostmann.zeroComparisonConstant line 17

theorem OAI.Ostmann.retained_character_prime_lower line 22

Source documentation

The only possible loss beyond the zero-free bound is a Siegel term for the one retained Page character. The Euler and prime-power steps are proved.

theorem retained_character_prime_lower (P : PublishedProgressionInput)
    (H : PublishedRealZeroInput P) (hSiegel : PublishedSiegelBound)
    (ε : ℝ) (hε : 0 < ε) :
    ∃ A K : ℝ, 0 < A ∧ 0 < K ∧
      ∀ (χ : PrimitiveRealCharacter) (Q : ℕ) (R s : ℝ),
        2 ≤ Q → χ.modulus ≤ Q → 0 ≤ R →
        2 * (A + H.errorConstant) ≤ Real.log (4 * (Q : ℝ)) →
        1 < s → s ≤ 1 + 1 / Real.log (4 * (Q : ℝ)) →
        (∀ e : PrimitiveRealZero, selectedPageZero P Q = some e →
          samePrimitiveRealCharacter e χ → (e.modulus : ℝ) ≤ R) →
        -2 * zeroComparisonConstant P * Real.log (4 * (Q : ℝ)) -
            K * R ^ ε - H.errorConstant - A ≤ ∑' n, realPrimeTerm χ.character s n := by
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PublishedRealZeroInput, OAI.Ostmann.PublishedSiegelBound, OAI.Ostmann.PrimitiveRealCharacter, OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.selectedPageZero, OAI.Ostmann.samePrimitiveRealCharacter, OAI.Ostmann.zeroComparisonConstant, OAI.Ostmann.realPrimeTerm