Multivariable whole prime-power comparison

The prime subsets may be chosen independently in each coordinate. The dagger condition will supply the cross-coordinate coprimality needed by exponent substitution. The finite comparison retains any domain closed under removing whole prime-power factors, including the weighted-mass truncation.

noncomputable def NairTenenbaum.unitaryChoices {r : ℕ} (n : Tuple r) : Finset (Fin r → Finset ℕ)

The possible whole-prime-power selections in each tuple coordinate.

Equations

• NairTenenbaum.unitaryChoices n = Fintype.piFinset fun (i : Fin r) => (↑(n i)).primeFactors.powerset

@[simp]

theorem NairTenenbaum.mem_unitaryChoices {r : ℕ} (n : Tuple r) (t : Fin r → Finset ℕ) : t ∈ unitaryChoices n ↔ ∀ (i : Fin r), t i ⊆ (↑(n i)).primeFactors

def NairTenenbaum.tupleUnitaryPart {r : ℕ} (n : Tuple r) (t : Fin r → Finset ℕ) : Tuple r

The coordinatewise unitary part selected by the chosen prime sets.

Equations

• NairTenenbaum.tupleUnitaryPart n t i = NairTenenbaum.unitaryPart (n i) (t i)

def NairTenenbaum.tupleUnitaryRest {r : ℕ} (n : Tuple r) (t : Fin r → Finset ℕ) : Tuple r

The coordinatewise remainder after removing the selected unitary parts.

Equations

• NairTenenbaum.tupleUnitaryRest n t i = NairTenenbaum.unitaryRest (n i) (t i)

theorem NairTenenbaum.tupleUnitaryPart_mul_rest {r : ℕ} (n : Tuple r) (t : Fin r → Finset ℕ) : tupleUnitaryPart n t * tupleUnitaryRest n t = n

theorem NairTenenbaum.tupleUnitarySplit_injective {r : ℕ} {n m : Tuple r} {s t : Fin r → Finset ℕ} (hs : s ∈ unitaryChoices n) (ht : t ∈ unitaryChoices m) (h : (tupleUnitaryPart n s, tupleUnitaryRest n s) = (tupleUnitaryPart m t, tupleUnitaryRest m t)) : n = m ∧ s = t

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

Coordinatewise prime-product expansion as a sum over all choices.

theorem NairTenenbaum.tuple_comparison_pointwise {r : ℕ} {w : Tuple r → ℝ} {U : Fin r → ℕ+ → ℝ} {l : Fin r → ℕ → ℝ} (hl : ∀ (i : Fin r) (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, radicalProduct (fun (p : ℕ) => 1 + l i p) ↑(n i) ≤ ∑ t ∈ unitaryChoices n, (∏ i : Fin r, U i (tupleUnitaryPart n t i) * radicalProduct (l i) ↑(tupleUnitaryPart n t i)) * w (tupleUnitaryRest n t)

Pointwise comparison for a prescribed tuple and its coprime splittings.

theorem NairTenenbaum.tuple_comparison_sum {r : ℕ} {w : Tuple r → ℝ} {U : Fin r → ℕ+ → ℝ} {l : Fin r → ℕ → ℝ} (hw₀ : ∀ (n : Tuple r), 0 ≤ w n) (hU : ∀ (i : Fin r) (n : ℕ+), 0 ≤ U i n) (hl : ∀ (i : Fin r) (p : ℕ), 0 ≤ l i p) (S : Finset (Tuple r)) (N : ℕ+) (hbox : ∀ n ∈ S, ∀ (i : Fin r), n i ≤ N) (hrest : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, tupleUnitaryRest n t ∈ S) (hw : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, w n ≤ (∏ i : Fin r, U i (tupleUnitaryPart n t i)) * w (tupleUnitaryRest n t)) : ∑ n ∈ S, w n * ∏ i : Fin r, radicalProduct (fun (p : ℕ) => 1 + l i p) ↑(n i) ≤ (∏ i : Fin r, ∑ a ∈ Finset.Icc 1 N, U i a * radicalProduct (l i) ↑a) * ∑ b ∈ S, w b

The tuple version of the finite convolution comparison. The original truncated domain is preserved in the second factor.

theorem NairTenenbaum.tuple_comparison_uniform {r : ℕ} {w : Tuple r → ℝ} {U l : Fin r → ℕ → ℝ} (hw₀ : ∀ (n : Tuple r), 0 ≤ w n) (hU₀ : ∀ (i : Fin r), U i 0 = 0) (hU₁ : ∀ (i : Fin r), U i 1 = 1) (hU : ∀ (i : Fin r) (n : ℕ), 0 ≤ U i n) (hl : ∀ (i : Fin r) (p : ℕ), 0 ≤ l i p) (hmul : ∀ (i : Fin r) (m n : ℕ), m.Coprime n → U i (m * n) = U i m * U i n) (hs : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → Summable fun (ν : ℕ) => U i (p ^ ν)) (hE : ∀ (i : Fin r), Summable fun (p : Nat.Primes) => kernelLocalError (U i) (l i) ↑p) (S : Finset (Tuple r)) (N : ℕ+) (hbox : ∀ n ∈ S, ∀ (i : Fin r), n i ≤ N) (hrest : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, tupleUnitaryRest n t ∈ S) (hw : ∀ n ∈ S, ∀ t ∈ unitaryChoices n, w n ≤ (∏ i : Fin r, U i ↑(tupleUnitaryPart n t i)) * w (tupleUnitaryRest n t)) : ∑ n ∈ S, w n * ∏ i : Fin r, radicalProduct (fun (p : ℕ) => 1 + l i p) ↑(n i) ≤ (∏ i : Fin r, Real.exp (∑' (p : Nat.Primes), kernelLocalError (U i) (l i) ↑p)) * ∑ b ∈ S, w b

Summable coordinate kernels supply a uniform multivariable comparison.