Totient corrections on products and restricted prime support

theorem NairTenenbaum.totientTwist_mul_le (g : ℕ) {a b : ℕ} (ha : a ≠ 0) (hb : b ≠ 0) : totientTwist g (a * b) ≤ totientTwist g a * totientTwist g b

theorem NairTenenbaum.totientTwist_prod_le {ι : Type u_1} (g : ℕ) (S : Finset ι) (f : ι → ℕ) (hf : ∀ i ∈ S, f i ≠ 0) : totientTwist g (∏ i ∈ S, f i) ≤ ∏ i ∈ S, totientTwist g (f i)

theorem NairTenenbaum.totientTwist_mass_le {r : ℕ} (g : ℕ) (m : Tuple r) : totientTwist g (mass m) ≤ ∏ i : Fin r, totientTwist g ↑(m i)

theorem NairTenenbaum.totientTwist_le_of_primeFactors_subset (g : ℕ) {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) (hsub : m.primeFactors ⊆ n.primeFactors) : totientTwist g m ≤ totientTwist g n