Pointwise arithmetic-weight bounds under the height hypothesis

theorem NairTenenbaum.Admissible.extend_le_mass_rpow {k : ℕ} {A B σ : ℝ} {F : ArithmeticMap k} (hF : Admissible A B σ F) (hB : 0 ≤ B) (n : Fin k → ℕ) : extendArithmeticMap F n ≤ B * ↑(∏ j : Fin k, n j) ^ σ * F 1