Totient comparison after exponential tilting

The corrected comparison remains uniform when the arithmetic weight is tilted by a logarithmic moment. A fixed gap below the local convergence exponent bounds the comparison kernel by a summable power of the prime.

theorem NairTenenbaum.tiltedRootAuxiliary_tail_uniform {A B ε β σ : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1) (γ : ℕ) (hγ : ↑γ * (ε + β) ≤ σ) (Q : Polynomial ℤ) {p : ℕ} (hp : Nat.Prime p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : ∑' (ν : ℕ), tiltedRootAuxiliary A B ε β γ Q (p ^ (ν + 1)) ≤ ↑C * B * ↑p ^ (σ - 1) / (1 - 2 ^ (σ - 1))

Uniform geometric bound for the positive prime-power tail of a tilted auxiliary. Its exponent may vary as long as it stays below σ < 1.

theorem NairTenenbaum.tilted_kernelLocalError_le {A B ε β σ L : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1) (hL : 0 ≤ L) (γ : ℕ) (hγ : ↑γ * (ε + β) ≤ σ) (Q : Polynomial ℤ) {l : ℕ → ℝ} {p : ℕ} (hp : Nat.Prime p) (hl : l p ≤ L / ↑p) (C : ℕ) (hρ : ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : kernelLocalError (tiltedRootAuxiliary A B ε β γ Q) l p ≤ L * ↑C * B / (1 - 2 ^ (σ - 1)) * ↑p ^ (σ - 2)

The weighted prime error has one additional reciprocal prime from the twist.

theorem NairTenenbaum.tilted_kernelLocalError_summable_bound {A B ε β σ L : ℝ} (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1) (hL : 0 ≤ L) (γ : ℕ) (hγ : ↑γ * (ε + β) ≤ σ) (Q : Polynomial ℤ) {l : ℕ → ℝ} (hl₀ : ∀ (p : ℕ), 0 ≤ l p) (hl : ∀ (p : ℕ), Nat.Prime p → l p ≤ L / ↑p) (C : ℕ) (hρ : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount Q (p ^ ν) ≤ C) : (Summable fun (p : Nat.Primes) => kernelLocalError (tiltedRootAuxiliary A B ε β γ Q) l ↑p) ∧ ∑' (p : Nat.Primes), kernelLocalError (tiltedRootAuxiliary A B ε β γ Q) l ↑p ≤ L * ↑C * B / (1 - 2 ^ (σ - 1)) * ∑' (n : ℕ), ↑n ^ (σ - 2)

Uniform summability and total bound for the tilted comparison kernel.

noncomputable def NairTenenbaum.tiltedTotientBound (B σ : ℝ) (g C : ℕ) : ℝ

The comparison constant for totient weights after exponential tilting.

Equations

• NairTenenbaum.tiltedTotientBound B σ g C = Real.exp (2 * (2 ^ g - 1) * ↑C * B / (1 - 2 ^ (σ - 1)) * ∑' (n : ℕ), ↑n ^ (σ - 2))

theorem NairTenenbaum.Admissible.rootTupleWeight_moment_mul_le {k r : ℕ} {A B ε β : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (γ : Fin k → Fin r → ℕ) (Q : Fin r → Polynomial ℤ) (a b : Tuple r) (hab : ∀ (i j : Fin r), (↑(a i)).Coprime ↑(b j)) : rootTupleWeight γ F Q (a * b) * ↑(weightedMass γ (a * b)) ^ β ≤ (∏ i : Fin r, tiltedRootAuxiliary A B ε β (totalExponent γ i) (Q i) ↑(a i)) * (rootTupleWeight γ F Q b * ↑(weightedMass γ b) ^ β)

Multiplying the tuple weight by a moment tilts its coprime majorant by the same amount.

theorem NairTenenbaum.tilted_totient_comparison {k r : ℕ} {A B ε β σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hσ : σ < 1) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), ↑(totalExponent γ i) * (ε + β) ≤ σ) (Q : Fin r → Polynomial ℤ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (g D : ℕ) (S : Finset (Tuple r)) (N : ℕ+) (hbox : ∀ n ∈ S, ∀ (i : Fin r), n i ≤ N) (hdagger : ∀ n ∈ S, Dagger D n) (hrest : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, tupleUnitaryRest n t ∈ S) : ∑ n ∈ S, rootTupleWeight γ F Q n * ↑(weightedMass γ n) ^ β * ∏ i : Fin r, totientTwist g ↑(n i) ≤ (∏ i : Fin r, tiltedTotientBound B σ g (C i)) * ∑ n ∈ S, rootTupleWeight γ F Q n * ↑(weightedMass γ n) ^ β

Corrected totient comparison for the tilted weight on any closed finite domain of dagger tuples. The constant is uniform in the moment exponent.