Lifting arithmetic weights through prime-factor roots

The flooring root divides each prime multiplicity by d. It is multiplicative on coprime arguments and recovers n from n^d. Thus a scalar admissible weight can be lifted to an additional coordinate without assuming that the weight itself is multiplicative.

def NairTenenbaum.positiveFloorRoot (d n : ℕ+) : ℕ+

The prime-factor flooring root on positive integers.

Equations

• NairTenenbaum.positiveFloorRoot d n = ⟨(↑d).floorRoot ↑n, ⋯⟩

@[simp]

theorem NairTenenbaum.positiveFloorRoot_pow (d n : ℕ+) : positiveFloorRoot d (n ^ ↑d) = n

theorem NairTenenbaum.positiveFloorRoot_dvd (d n : ℕ+) : ↑(positiveFloorRoot d n) ∣ ↑n

theorem NairTenenbaum.positiveFloorRoot_coprime (d : ℕ+) {m n : ℕ+} (h : (↑m).Coprime ↑n) : (↑(positiveFloorRoot d m)).Coprime ↑(positiveFloorRoot d n)

theorem NairTenenbaum.positiveFloorRoot_mul (d : ℕ+) {m n : ℕ+} (h : (↑m).Coprime ↑n) : positiveFloorRoot d (m * n) = positiveFloorRoot d m * positiveFloorRoot d n

theorem NairTenenbaum.bigOmega_le_of_dvd {m n : ℕ} (hn : n ≠ 0) (h : m ∣ n) : bigOmega m ≤ bigOmega n

theorem NairTenenbaum.admissible_floorRoot {A B ε : ℝ} {F : ArithmeticMap 1} (hF : Admissible A B ε F) (hA : 1 ≤ A) (hB : 0 ≤ B) (hε : 0 ≤ ε) (d : ℕ+) : Admissible A B ε fun (n : Tuple 1) => F fun (x : Fin 1) => positiveFloorRoot d (n 0)

Lifting a scalar weight along the flooring root preserves its admissibility parameters. The bound deliberately uses the ambient argument rather than its root.