Encoding arbitrary scalar weights in doubled exponent substitutions

An additional coordinate for each factor carries the lifted scalar weight. The weighted mass is squared, so dividing the smooth-tail parameter by two preserves both the decay exponent and the cutoff in Lemma 2.

def NairTenenbaum.liftedExponents {k r : ℕ} (γ : Fin k → Fin r → ℕ) : Fin (k + r) → Fin r → ℕ

Append a diagonal block containing the column sums of the original matrix.

Equations

• NairTenenbaum.liftedExponents γ = Fin.append γ fun (i j : Fin r) => if i = j then NairTenenbaum.totalExponent γ i else 0

@[simp]

theorem NairTenenbaum.totalExponent_lifted {k r : ℕ} (γ : Fin k → Fin r → ℕ) (i : Fin r) : totalExponent (liftedExponents γ) i = 2 * totalExponent γ i

@[simp]

theorem NairTenenbaum.weightedMass_lifted {k r : ℕ} (γ : Fin k → Fin r → ℕ) (n : Tuple r) : weightedMass (liftedExponents γ) n = weightedMass γ n ^ 2

theorem NairTenenbaum.liftedExponents_pos {k r : ℕ} {γ : Fin k → Fin r → ℕ} (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (i : Fin r) : 0 < totalExponent (liftedExponents γ) i

noncomputable def NairTenenbaum.liftedArithmeticMap {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (F : ArithmeticMap k) (θ : Fin r → ℕ → ℝ) : ArithmeticMap (k + r)

The scalar factors are evaluated on prime-factor roots of the new coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem NairTenenbaum.admissible_liftedArithmeticMap {k r : ℕ} {A B T ε : ℝ} {F : ArithmeticMap k} {θ : Fin r → ℕ → ℝ} (hF : Admissible A B ε F) (hθ : ∀ (i : Fin r), Admissible A T ε fun (n : Tuple 1) => θ i ↑(n 0)) (hA : 1 ≤ A) (hB : 0 ≤ B) (hT : 0 ≤ T) (hε : 0 ≤ ε) (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) : Admissible A (B * T ^ r) ε (liftedArithmeticMap γ hγ F θ)

@[simp]

theorem NairTenenbaum.pullback_lifted {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (F : ArithmeticMap k) (θ : Fin r → ℕ → ℝ) (n : Tuple r) : pullback (liftedExponents γ) (liftedArithmeticMap γ hγ F θ) n = pullback γ F n * ∏ i : Fin r, θ i ↑(n i)

theorem NairTenenbaum.rootTupleWeight_lifted {k r : ℕ} (γ : Fin k → Fin r → ℕ) (hγ : ∀ (i : Fin r), 0 < totalExponent γ i) (F : ArithmeticMap k) (θ : Fin r → ℕ → ℝ) (n : Tuple r) : rootTupleWeight (liftedExponents γ) (liftedArithmeticMap γ hγ F θ) (fun (x : Fin r) => Polynomial.X) n = pullback γ F n * ∏ i : Fin r, θ i ↑(n i) / ↑↑(n i)