OAI/NumberTheory/Ostmann/ZeroDensity/PageRegularAverage.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The retained Page term in the actual regular-prime average

  1. theorem OAI.Ostmann.pageAtModulus_regular_factor line 12

    Source documentation

    The deletion prescribed before the nongiant priors prevents an exceptional conductor from using any prime in the regular block, including its powers.

    theorem pageAtModulus_regular_factor (z : Option PrimitiveRealZero) (C R T : ℕ)
    (hC : ∀ p, p.Prime → p ∣ C → T ≤ p)
    (hexcluded : ∀ e, z = some e → ∀ p,
      deletedConductorPrime e.modulus T = some p → ¬p ∣ C * R) :
    pageAtModulus (C * R) z = pageAtModulus R z := by
…

    Mentions: OAI.Ostmann.PrimitiveRealZero, OAI.Ostmann.deletedConductorPrime, OAI.Ostmann.pageAtModulus

  2. theorem OAI.Ostmann.pageGiantWeight_modEq line 33
  3. theorem OAI.Ostmann.periodic_coefficient_regular_page_average line 38