Comparison with prime-power dependent increments

The exponential moment requires an increment depending on the valuation, not just the prime. Selecting whole prime powers preserves that valuation and therefore gives an exact expansion over the existing unitary splittings.

noncomputable def NairTenenbaum.primePowerProduct (l : ℕ → ℕ → ℝ) (n : ℕ) : ℝ

The product of the local prime-power weights over the prime factors.

Equations

• NairTenenbaum.primePowerProduct l n = ∏ p ∈ n.primeFactors, l p (n.factorization p)

@[simp]

theorem NairTenenbaum.primePowerProduct_one (l : ℕ → ℕ → ℝ) : primePowerProduct l 1 = 1

theorem NairTenenbaum.primePowerProduct_nonneg {l : ℕ → ℕ → ℝ} (hl : ∀ (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), 0 ≤ l p ν) (n : ℕ) : 0 ≤ primePowerProduct l n

theorem NairTenenbaum.primePowerProduct_mul (l : ℕ → ℕ → ℝ) {m n : ℕ} (hmn : m.Coprime n) : primePowerProduct l (m * n) = primePowerProduct l m * primePowerProduct l n

theorem NairTenenbaum.primePowerProduct_prime_pow_succ (l : ℕ → ℕ → ℝ) {p : ℕ} (hp : Nat.Prime p) (ν : ℕ) : primePowerProduct l (p ^ (ν + 1)) = l p (ν + 1)

theorem NairTenenbaum.primePowerProduct_unitaryPart (l : ℕ → ℕ → ℝ) (n : ℕ+) {s : Finset ℕ} (hs : s ⊆ (↑n).primeFactors) : primePowerProduct l ↑(unitaryPart n s) = ∏ p ∈ s, l p ((↑n).factorization p)

theorem NairTenenbaum.primePowerProduct_one_add (l : ℕ → ℕ → ℝ) (n : ℕ+) : primePowerProduct (fun (p ν : ℕ) => 1 + l p ν) ↑n = ∑ s ∈ (↑n).primeFactors.powerset, primePowerProduct l ↑(unitaryPart n s)

theorem NairTenenbaum.primePowerProduct_rpow (β : ℝ) {n : ℕ} (hn : n ≠ 0) : primePowerProduct (fun (p ν : ℕ) => (↑p ^ ν) ^ β) n = ↑n ^ β

Reconstruct a real power from its complete prime-power factors.

theorem NairTenenbaum.prod_primePowerProduct_one_add {r : ℕ} (l : Fin r → ℕ → ℕ → ℝ) (n : Tuple r) : ∏ i : Fin r, primePowerProduct (fun (p ν : ℕ) => 1 + l i p ν) ↑(n i) = ∑ t ∈ unitaryChoices n, ∏ i : Fin r, primePowerProduct (l i) ↑(tupleUnitaryPart n t i)

theorem NairTenenbaum.tuple_primePower_comparison_pointwise {r : ℕ} {w : Tuple r → ℝ} {U : Fin r → ℕ+ → ℝ} {l : Fin r → ℕ → ℕ → ℝ} (hl : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), 0 ≤ l i p ν) (n : Tuple r) (hw : ∀ t ∈ unitaryChoices n, w n ≤ (∏ i : Fin r, U i (tupleUnitaryPart n t i)) * w (tupleUnitaryRest n t)) : w n * ∏ i : Fin r, primePowerProduct (fun (p ν : ℕ) => 1 + l i p ν) ↑(n i) ≤ ∑ t ∈ unitaryChoices n, (∏ i : Fin r, U i (tupleUnitaryPart n t i) * primePowerProduct (l i) ↑(tupleUnitaryPart n t i)) * w (tupleUnitaryRest n t)

Pointwise coprime comparison with increments at arbitrary prime powers.

theorem NairTenenbaum.tuple_unitary_convolution_sum {r : ℕ} {w v : Tuple r → ℝ} {K : Fin r → ℕ+ → ℝ} (hw : ∀ (n : Tuple r), 0 ≤ w n) (hK : ∀ (i : Fin r) (n : ℕ+), 0 ≤ K i n) (S : Finset (Tuple r)) (T : Fin r → Finset ℕ+) (hpart : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, ∀ (i : Fin r), tupleUnitaryPart n t i ∈ T i) (hrest : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, tupleUnitaryRest n t ∈ S) (hv : ∀ n ∈ S, v n ≤ ∑ t ∈ unitaryChoices n, (∏ i : Fin r, K i (tupleUnitaryPart n t i)) * w (tupleUnitaryRest n t)) : ∑ n ∈ S, v n ≤ (∏ i : Fin r, ∑ a ∈ T i, K i a) * ∑ b ∈ S, w b

The finite convolution estimate with separate coordinate domains. In particular those domains may retain a prescribed finite prime support.