OAI/NumberTheory/Ostmann/Arithmetic/BulkPageProjection.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The deleted conductor prime removes every spectator Page factor

  1. theorem OAI.Ostmann.bulk_page_projection line 14

    Source documentation

    The prescribed single prime exclusion makes the Page correction depend only on the frequency block. Multiplicities in that block are retained.

    theorem bulk_page_projection {I : Type*} [Fintype I]
    (z : Option PrimitiveRealZero) (r cutoff : ℕ) (p : I → ℕ)
    (hr : 0 < r) (hrcutoff : r < cutoff)
    (hp : ∀ i, (p i).Prime) (hlarge : ∀ i, cutoff ≤ p i)
    (hexcluded : ∀ e, z = some e → ∀ q,
      deletedConductorPrime e.modulus cutoff = some q → ∀ i, q ≠ p i) :
    pageAtModulus (∏ i, bulkResidueModuli r p i) z = pageAtModulus r z := by
…

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