Smooth tails with the full bad-prime mass retained

noncomputable def NairTenenbaum.splitSmoothTailBound (A B κ : ℝ) (g D : ℕ) : ℝ

The product of the bad-prime and good-part smooth-moment constants.

Equations

• NairTenenbaum.splitSmoothTailBound A B κ g D = NairTenenbaum.badPrimeMomentBound B g D * NairTenenbaum.smoothTailUniformBound A B κ g D

theorem NairTenenbaum.splitSmoothTailBound_pos {A B κ : ℝ} (hB : 0 < B) {g D : ℕ} (hg : 0 < g) (hD : 0 < D) : 0 < splitSmoothTailBound A B κ g D

theorem NairTenenbaum.PolynomialSystem.split_smooth_moment_le {k r : ℕ} (P : PolynomialSystem k r) {A B ε κ z : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hg : 0 < P.total.natDegree) (hgε : ↑P.total.natDegree * ε ≤ 1 / 8) (hsmall : ↑P.total.natDegree ^ 2 * (ε + κ / Real.log z) ≤ 1 / 4) (hzκ : 4 ^ (↑P.total.natDegree * κ) ≤ z) (N : ℕ+) (U : Tuple r → Finset (Tuple r)) (hbox : ∀ v ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, ∀ u ∈ U v, ∀ (i : Fin r), u i ≤ N) (hs : ∀ v ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, ∀ u ∈ U v, ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) : ∑ v ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, ∑ u ∈ U v, badPrimeTupleKernel A B ε (totalExponent P.exponent) P.radical u * (rootTupleWeight P.exponent F P.R v * ∏ i : Fin r, totientTwist P.total.natDegree ↑(v i)) * ↑(weightedMass P.exponent (u * v)) ^ (κ / Real.log z) ≤ splitSmoothTailBound A B κ P.total.natDegree P.badDiscriminant * ∑ m ∈ positiveUpTo z, P.weight F m

The moments of the bad and good parts multiply. The cutoff on the bad part may depend on the good tuple.

theorem NairTenenbaum.PolynomialSystem.split_smooth_tail_le {k r : ℕ} (P : PolynomialSystem k r) {A B ε κ z X : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hX : 0 < X) (hg : 0 < P.total.natDegree) (hgε : ↑P.total.natDegree * ε ≤ 1 / 8) (hsmall : ↑P.total.natDegree ^ 2 * (ε + κ / Real.log z) ≤ 1 / 4) (hzκ : 4 ^ (↑P.total.natDegree * κ) ≤ z) (N : ℕ+) (U : Tuple r → Finset (Tuple r)) (hbox : ∀ v ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, ∀ u ∈ U v, ∀ (i : Fin r), u i ≤ N) (hs : ∀ v ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, ∀ u ∈ U v, ∀ (i : Fin r), ↑(u i) ∈ Nat.factoredNumbers P.badDiscriminant.primeFactors) : ∑ v ∈ smoothWeightUpTo P.exponent P.discriminant (Finset.Icc 0 ⌊z⌋₊) N, ∑ u ∈ U v with X < ↑(weightedMass P.exponent (u * v)), badPrimeTupleKernel A B ε (totalExponent P.exponent) P.radical u * (rootTupleWeight P.exponent F P.R v * ∏ i : Fin r, totientTwist P.total.natDegree ↑(v i)) ≤ splitSmoothTailBound A B κ P.total.natDegree P.badDiscriminant * Real.exp (-κ * Real.log X / Real.log z) * ∑ m ∈ positiveUpTo z, P.weight F m

The smooth-tail saving is imposed on the original combined prefix mass. Arbitrarily large bad-prime powers are allowed and accounted for in the constant.

theorem NairTenenbaum.split_moment_conditions {g : ℕ} (hg : 0 < g) {ε κ z : ℝ} (hε : 0 ≤ ε) (hκ : 0 ≤ κ) (hz : 2 ≤ z) (hsmall : ↑g ^ 2 * ε ≤ 1 / 8) (hlog : 8 * ↑g ^ 2 * κ ≤ Real.log z) : ↑g * ε ≤ 1 / 8 ∧ ↑g ^ 2 * (ε + κ / Real.log z) ≤ 1 / 4 ∧ 4 ^ (↑g * κ) ≤ z

One logarithmic lower bound supplies both moment gaps.