BoundedPrimeTuples.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniformly bounded tuple lengths in the manuscript's actual prime detector. The bound depends on xi, not on the envelope scale.

lemma OAI.CubicFirstMoment.eventually_prime_tuple_norm_bound line 13
lemma OAI.CubicFirstMoment.distinguished_subset_card_lt line 22

theorem OAI.CubicFirstMoment.bounded_distinguished_primary_tuples line 38

Source documentation

The actual ordered distinguished expansion can be cut off at one fixed tuple length throughout a whole norm envelope.

theorem bounded_distinguished_primary_tuples {ξ C : ℝ}
    (hξ : 0 < ξ) (hξz : ξ ≤ 2/5) (hC : 0 < C)
    {ψ : ℝ → ℝ}
    (hψone : ∀ x : ℝ, 0 < x → x ≤ 1 → ψ x = 1)
    (hψzero : ∀ x : ℝ, 2 ≤ x → ψ x = 0) :
    ∃ k : ℕ, ∀ᶠ X : ℝ in atTop, ∀ n : Eisenstein,
      primary n → Squarefree n → norm n ≤ C*X →
      (roughProduct ψ (X^(2/5:ℝ)) n:ℂ) =
        ∑ s ∈ (primaryPrimeFactors n).powerset with s.card < k,
          ((s.card.factorial:ℂ)⁻¹)*
            (∑ e : Fin s.card ≃ s,
              ∏ i : Fin s.card, distinguishedPrimeWeight ψ (X^ξ) (X^(2/5:ℝ)) (e i))*
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.roughProduct, OAI.CubicFirstMoment.primaryPrimeFactors, OAI.CubicFirstMoment.distinguishedPrimeWeight