Corrected multivariable totient comparison

The comparison is proved for the full weight (16), including exponent substitution, the weighted-mass cutoff, and all dagger restrictions.

noncomputable def NairTenenbaum.rootTupleWeight {k r : ℕ} (γ : Fin k → Fin r → ℕ) (F : ArithmeticMap k) (Q : Fin r → Polynomial ℤ) (n : Tuple r) : ℝ

The pullback arithmetic weight multiplied by the coordinate root densities.

Equations

• NairTenenbaum.rootTupleWeight γ F Q n = NairTenenbaum.pullback γ F n * ∏ i : Fin r, ↑(NairTenenbaum.rootCount (Q i) ↑(n i)) / ↑↑(n i)

theorem NairTenenbaum.rootTupleWeight_nonneg {k r : ℕ} (γ : Fin k → Fin r → ℕ) {F : ArithmeticMap k} (hF : ∀ (n : Tuple k), 0 ≤ F n) (Q : Fin r → Polynomial ℤ) (n : Tuple r) : 0 ≤ rootTupleWeight γ F Q n

theorem NairTenenbaum.Admissible.pullback_mul_le_auxiliary {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (γ : Fin k → Fin r → ℕ) (a b : Tuple r) (hab : ∀ (i j : Fin r), (↑(a i)).Coprime ↑(b j)) : pullback γ F (a * b) ≤ (∏ i : Fin r, auxiliary A B ε (totalExponent γ i) ↑(a i)) * pullback γ F b

Cross-coprimality lets the arithmetic majorant survive exponent substitution.

theorem NairTenenbaum.Admissible.rootTupleWeight_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) ≤ (∏ i : Fin r, rootAuxiliary A B ε (totalExponent γ i) (Q i) ↑(a i)) * rootTupleWeight γ F Q b

The root-weighted tuple summand has the product of the proved local auxiliaries as a majorant under cross-coprime multiplication.

theorem NairTenenbaum.sum_weight_twist_eq_sum_weightUpTo {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (D : ℕ) (F : ArithmeticMap k) (Q : Fin r → Polynomial ℤ) (θ : Fin r → ℕ → ℝ) (N : ℕ+) : ∑ m ∈ Finset.Icc 1 N, weight γ D F (fun (i : Fin r) (n : ℕ) => ↑(rootCount (Q i) n) * θ i n) m = ∑ n ∈ weightUpTo γ D N, rootTupleWeight γ F Q n * ∏ i : Fin r, θ i ↑(n i)

A tuple-dependent twist factors out of the root-weighted summand.

theorem NairTenenbaum.multivariable_totient_comparison {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε < 1) (D : ℕ) (Q : Fin r → Polynomial ℤ) (g : ℕ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (N : ℕ+) : ∑ n ∈ Finset.Icc 1 N, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m) * totientTwist g m) n ≤ (∏ i : Fin r, Real.exp (∑' (p : Nat.Primes), localComparisonError A B ε (totalExponent γ i) (Q i) (totientTwist g) ↑p)) * ∑ n ∈ Finset.Icc 1 N, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) n

The corrected global comparison with the full multivariable weight.

theorem NairTenenbaum.multivariable_totient_comparison_real {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε < 1) (D : ℕ) (Q : Fin r → Polynomial ℤ) (g : ℕ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (x : ℝ) : ∑ n ∈ positiveUpTo x, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m) * totientTwist g m) n ≤ (∏ i : Fin r, Real.exp (∑' (p : Nat.Primes), localComparisonError A B ε (totalExponent γ i) (Q i) (totientTwist g) ↑p)) * ∑ n ∈ positiveUpTo x, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) n

The same multivariable comparison at an arbitrary real cutoff, including cutoffs below one.

theorem NairTenenbaum.multivariable_totient_comparison_explicit {k r : ℕ} {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (hγε : ∀ (i : Fin r), ↑(totalExponent γ i) * ε < 1) (D : ℕ) (Q : Fin r → Polynomial ℤ) (g : ℕ) (C : Fin r → ℕ) (hρ : ∀ (i : Fin r) (p : ℕ), Nat.Prime p → ∀ (ν : ℕ), rootCount (Q i) (p ^ ν) ≤ C i) (x : ℝ) : ∑ n ∈ positiveUpTo x, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m) * totientTwist g m) n ≤ (∏ i : Fin r, scalarComparisonBound B (↑(totalExponent γ i) * ε) g (C i)) * ∑ n ∈ positiveUpTo x, weight γ D F (fun (i : Fin r) (m : ℕ) => ↑(rootCount (Q i) m)) n

A coefficient-independent product of explicit comparison constants.

theorem NairTenenbaum.PolynomialSystem.totient_comparison {k r : ℕ} (P : PolynomialSystem k r) {A B ε : ℝ} {F : ArithmeticMap k} (hF : Admissible A B ε F) (hA : 0 ≤ A) (hB : 1 ≤ B) (hε : 0 < ε) (hγε : ∀ (i : Fin r), ↑(totalExponent P.exponent i) * ε < 1) (g : ℕ) (x : ℝ) : ∑ n ∈ positiveUpTo x, NairTenenbaum.weight P.exponent P.discriminant F (fun (i : Fin r) (m : ℕ) => P.rootVector i m * totientTwist g m) n ≤ (∏ i : Fin r, scalarComparisonBound B (↑(totalExponent P.exponent i) * ε) g (max (P.R i).natDegree (P.badDiscriminant ^ 3))) * ∑ n ∈ positiveUpTo x, P.weight F n

The full comparison for an actual polynomial system, with its root bounds discharged and its exponent substitution and dagger restrictions unchanged.