Comparing smooth and truncated sums under the squared-mass lift #
theorem
NairTenenbaum.weight_nonneg_of_positive
{k r : ℕ}
(γ : Fin k → Fin r → ℕ)
(D : ℕ)
{F : ArithmeticMap k}
(hF : ∀ (n : Tuple k), 0 ≤ F n)
{θ : Fin r → ℕ → ℝ}
(hθ : ∀ (i : Fin r) (n : ℕ+), 0 ≤ θ i ↑n)
(N : ℕ+)
:
Only positive arguments occur in the weight, so no sign assumption at zero is needed for the scalar factors.
theorem
NairTenenbaum.truncated_tupleWeight_sum_le
{k r : ℕ}
{F : ArithmeticMap k}
(hF : ∀ (n : Tuple k), 0 ≤ F n)
{θ : Fin r → ℕ → ℝ}
(hθ : ∀ (i : Fin r) (n : ℕ+), 0 ≤ θ i ↑n)
(γ : Fin k → Fin r → ℕ)
(hγ : ∀ (i : Fin r), 0 < totalExponent γ i)
(D : ℕ)
(N : ℕ+)
(z : ℝ)
:
∑ n ∈ weightUpTo γ D N with ↑(weightedMass γ n) ≤ z, pullback γ F n * ∏ i : Fin r, θ i ↑(n i) / ↑↑(n i) ≤ ∑ m ∈ positiveUpTo z, weight γ D F θ m
An additional finite mass bound can be discarded from a truncated tuple sum.
theorem
NairTenenbaum.truncated_liftedTupleWeight_sum_le
{k r : ℕ}
{F : ArithmeticMap k}
(hF : ∀ (n : Tuple k), 0 ≤ F n)
{θ : Fin r → ℕ → ℝ}
(hθ : ∀ (i : Fin r) (n : ℕ+), 0 ≤ θ i ↑n)
(γ : Fin k → Fin r → ℕ)
(hγ : ∀ (i : Fin r), 0 < totalExponent γ i)
(D : ℕ)
(N : ℕ+)
(z : ℝ)
:
∑ n ∈ weightUpTo (liftedExponents γ) D N with ↑(weightedMass (liftedExponents γ) n) ≤ z,
rootTupleWeight (liftedExponents γ) (liftedArithmeticMap γ hγ F θ) (fun (x : Fin r) => Polynomial.X) n ≤ ∑ m ∈ positiveUpTo z, weight γ D F θ m
Squaring the mass only reduces the truncated sum.
theorem
NairTenenbaum.smooth_weight_tail_le_lifted
{k r : ℕ}
{F : ArithmeticMap k}
(hF : ∀ (n : Tuple k), 0 ≤ F n)
{θ : Fin r → ℕ → ℝ}
(hθ : ∀ (i : Fin r) (n : ℕ+), 0 ≤ θ i ↑n)
(γ : Fin k → Fin r → ℕ)
(hγ : ∀ (i : Fin r), 0 < totalExponent γ i)
(D : ℕ)
(N : ℕ+)
(s : Finset ℕ)
{x : ℝ}
(hx : 0 ≤ x)
:
∑ m ∈ Finset.Icc 1 N with ↑m ∈ Nat.factoredNumbers s ∧ x < ↑↑m, weight γ D F θ m ≤ ∑ n ∈ smoothWeightUpTo (liftedExponents γ) D s (N ^ 2) with x ^ 2 < ↑(weightedMass (liftedExponents γ) n),
rootTupleWeight (liftedExponents γ) (liftedArithmeticMap γ hγ F θ) (fun (x : Fin r) => Polynomial.X) n
The original tail embeds into the lifted tail with squared lower and upper mass bounds. Smoothness and both dagger restrictions are retained.