PrimeCellIdealization.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Joint idealization of actual cutoff-weighted prime samples

The only analytic input is PublishedProgressionInput. Partition fibers, cutoff variation, and the final numerical error budget are explicit. The ideal masses are the integrals with the retained Page correction.

structure OAI.Ostmann.PrimeCellPartition line 17
def OAI.Ostmann.idealPrimeCellPrior line 32
theorem OAI.Ostmann.idealPrimeCellPrior_nonneg line 40

theorem OAI.Ostmann.PublishedProgressionInput.prime_cell_idealization line 56

Source documentation

A signed complex joint statistic of independent original prime samples is compared with the product of their explicit Page-corrected cell priors. No conditional equidistribution or ideal-mass assumption is needed.

theorem PublishedProgressionInput.prime_cell_idealization
    (P : PublishedProgressionInput) (Q : ℕ) (hQ : 2 ≤ Q)
    (S : Finset ℕ) {C : Type*} [Fintype C] {n : ℕ}
    (D : Fin n → PrimeCellPartition S C) (hmod : ∀ i, (D i).modulus ≤ Q)
    (w : Fin n → ℝ → ℝ) (Z : Fin n → ℝ) (hZ : ∀ i, 0 ≤ Z i)
    (hw : ∀ i p, p ∈ S → 0 ≤ w i (Real.log p))
    (hwi : ∀ i c y, y ∈ Set.Ioc ((D i).lower c) ((D i).upper c) → 0 ≤ w i y)
    (hmass : ∀ i, Z i * (∑ p ∈ S, w i (Real.log p) * (p : ℝ)⁻¹) ≤ 1)
    (hwc : ∀ i c, ContinuousOn (w i) (Set.Icc ((D i).lower c) ((D i).upper c)))
    (w₀ : Fin n → C → ℝ) (ηw δ B η : ℝ)
    (hηw : 0 ≤ ηw) (hδ : 0 ≤ δ) (hB : 0 ≤ B) (hη : 0 ≤ η)
    (hvariation : ∀ i c y, y ∈ Set.Ioc ((D i).lower c) ((D i).upper c) →
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.PrimeCellPartition