PrefixOmissions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Few omissions above the addition prefix

This is the deterministic first step in the weighted multiplicity estimate of moments.tex: total and prefix regularity leave at most 4τℓ omissions above a prefix containing every added prime.

theorem OAI.JointDickman.omitted_above_count line 15
theorem OAI.JointDickman.primePrefix_mono line 37

theorem OAI.JointDickman.regular_omissions_above_prefix line 46

Source documentation

All additions below one grid point force almost all higher prime factors to be shared by the two regular coefficients.

theorem regular_omissions_above_prefix {B L : ℕ} {τ C : ℝ} {A R : Finset ℕ}
    (hL : 1 ≤ L) (hA : RegularPrimeSet B L τ C A) (hR : RegularPrimeSet B L τ C R)
    {k : ℕ} (hk : k ∈ Icc 1 L)
    (hadd : R \ A ⊆ primePrefix B ((k : ℝ)/L) (R \ A)) :
    (((A \ R) \ primePrefix B ((k : ℝ)/L) (A ∪ R)).card : ℝ) ≤
      4*τ*auxiliaryLogLength B := by
…

Mentions: OAI.JointDickman.RegularPrimeSet, OAI.JointDickman.primePrefix, OAI.JointDickman.auxiliaryLogLength