PrimeCellPartitionConstruction.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Constructing the actual prime log/residue partition

The fiber identities used by the joint comparison follow from separated log intervals and residue classes. They are not additional distribution hypotheses.

def OAI.Ostmann.primeLogCellSet line 16
theorem OAI.Ostmann.primeLogCellSet_disjoint line 20
def OAI.Ostmann.primeCellSupport line 34
def OAI.Ostmann.primeCellLabel line 38
theorem OAI.Ostmann.primeCellLabel_mem line 42
theorem OAI.Ostmann.primeCellLabel_fiber line 54

def OAI.Ostmann.buildPrimeCellPartition line 79

Source documentation

A fully constructed partition of the actual primes in the selected log cells. Separation is a numerical/residue property, not an assertion about the distribution of primes.

noncomputable def buildPrimeCellPartition {C : Type*} [Fintype C]
    (q : ℕ) (hq : 1 ≤ q) (a : C → ℕ) (s t : C → ℝ) (c₀ : C)
    (hs : ∀ c, 1 ≤ s c) (hst : ∀ c, s c ≤ t c) (hshort : ∀ c, t c ≤ s c + 1)
    (ha : ∀ c, (a c).Coprime q)
    (hsep : ∀ c d, c ≠ d → ¬Nat.ModEq q (a c) (a d) ∨ t c ≤ s d ∨ t d ≤ s c) :
    PrimeCellPartition (primeCellSupport q a s t) C where
…

Mentions: OAI.Ostmann.PrimeCellPartition, OAI.Ostmann.primeCellSupport