PrimeCellPriors.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Cell masses of the actual weighted prime samples

The fiber identity specifies a finite log/residue partition. The sampling weight is the original reciprocal-prime weight, not an abstract nearby distribution. Its comparison with the retained Page density is derived from the published progression inputs.

def OAI.Ostmann.primeSamplePrior line 20
theorem OAI.Ostmann.primeSamplePrior_nonneg line 23
theorem OAI.Ostmann.primeSamplePrior_mass line 28
theorem OAI.Ostmann.primeSamplePrior_normalized line 34

theorem OAI.Ostmann.primeSamplePrior_cell line 41

Source documentation

Exact identification of a cell of the original prime sample.

theorem primeSamplePrior_cell {C : Type*}
    (S : Finset ℕ) (w : ℝ → ℝ) (Z : ℝ) (cell : ℕ → C) (c : C)
    (q a : ℕ) (s t : ℝ)
    (hfiber : S.filter (fun p => cell p = c) =
      (Finset.Ioc ⌊Real.exp s⌋₊ ⌊Real.exp t⌋₊).filter
        (fun p => p.Prime ∧ Nat.ModEq q p a)) :
    cellPrior (primeSamplePrior S w Z) (fun p => cell p) c =
      Z * weightedReciprocalPrimeInterval q a s t w := by
…

Mentions: OAI.Ostmann.cellPrior, OAI.Ostmann.primeSamplePrior, OAI.Ostmann.weightedReciprocalPrimeInterval

theorem OAI.Ostmann.PublishedProgressionInput.primeSamplePrior_cell_error line 65

Source documentation

A concrete per-cell comparison, including normalization and the cutoff variation. Only the cited theta/Page input is unproved.

theorem PublishedProgressionInput.primeSamplePrior_cell_error
    (P : PublishedProgressionInput) {C : Type*}
    (S : Finset ℕ) (w : ℝ → ℝ) (Z : ℝ) (hZ : 0 ≤ Z) (cell : ℕ → C) (c : C)
    {q Q a : ℕ} (hQ : 2 ≤ Q) (hq : 1 ≤ q) (hqQ : q ≤ Q) (ha : a.Coprime q)
    {s t : ℝ} (hs : 1 ≤ s) (hst : s ≤ t) (hshort : t ≤ s + 1)
    (hfiber : S.filter (fun p => cell p = c) =
      (Finset.Ioc ⌊Real.exp s⌋₊ ⌊Real.exp t⌋₊).filter
        (fun p => p.Prime ∧ Nat.ModEq q p a))
    (hwc : ContinuousOn w (Set.Icc s t)) (w₀ η : ℝ) (hη : 0 ≤ η)
    (hw : ∀ y ∈ Set.Ioc s t, |w y - w₀| ≤ η) :
    |cellPrior (primeSamplePrior S w Z) (fun p => cell p) c -
      Z * ∫ y in Set.Ioc s t, w y * primeLogDensity (Nat.totient q)
…

Mentions: OAI.Ostmann.PublishedProgressionInput, OAI.Ostmann.cellPrior, OAI.Ostmann.primeSamplePrior, OAI.Ostmann.primeLogDensity