A uniform bound for the actual normalized signed tags

The finite set here is the existing signedTags, with one member for each accepted multiplicity profile, including the empty profile. No factorial copies are introduced. The estimates do not require any condition on the supplied prime labelling: numerical acceptance itself bounds every label.

def MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.words (J : ℕ) : ℕ → Finset (List ℕ)

All words of length at most R over the labels less than J.

Equations

• MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.words J 0 = {[]}
• MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.words J R.succ = insert [] (Finset.image (fun (p : ℕ × List ℕ) => p.1 :: p.2) (Finset.range J ×ˢ MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.words J R))

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.mem_words {J R : ℕ} {t : List ℕ} (hlen : t.length ≤ R) (hlabel : ∀ j ∈ t, j < J) : t ∈ words J R

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.card_words_le (J R : ℕ) : (words J R).card ≤ (J + 1) ^ R

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.accepted_prod_lt {upper : Bool} {D ε : ℝ} {t : List ℕ} (hD : 1 ≤ D) (hε : 0 ≤ ε) (h : SignedTagAccepted upper (geometricLower D ε (ε ^ 9)) (fun (j : ℕ) => geometricLower D ε (ε ^ 9) (j + 1)) D t) : (List.map (geometricLower D ε (ε ^ 9)) t).prod < D

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.accepted_length_le {upper : Bool} {D ε : ℝ} {t : List ℕ} (hD : 1 < D) (hε : 0 < ε) (h : SignedTagAccepted upper (geometricLower D ε (ε ^ 9)) (fun (j : ℕ) => geometricLower D ε (ε ^ 9) (j + 1)) D t) : t.length ≤ ⌊ε⁻¹ ^ 2⌋₊

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.TagCardinality.accepted_label_lt {upper : Bool} {D ε : ℝ} {t : List ℕ} (hD : 1 < D) (hε : 0 < ε) (h : SignedTagAccepted upper (geometricLower D ε (ε ^ 9)) (fun (j : ℕ) => geometricLower D ε (ε ^ 9) (j + 1)) D t) {j : ℕ} (hj : j ∈ t) : j < ⌊ε⁻¹ ^ 11⌋₊ + 1

theorem MathlibNt.SieveTheory.LiLiuPrereqWF.signedTags_card_le_uniform (upper : Bool) (P : Finset ℕ) {D ε : ℝ} (label : ℕ → ℕ) (hD : 1 < D) (hε : 0 < ε) : (signedTags upper P D ε label).card ≤ (⌊ε⁻¹ ^ 11⌋₊ + 2) ^ ⌊ε⁻¹ ^ 2⌋₊

An explicit bound independent of the level, prime set, and labelling.