Interpolation of nonnegative convergent series

theorem NairTenenbaum.summable_and_tsum_mul_rpow_le {ι : Type u_1} (f g : ι → ℝ) (hf : ∀ (i : ι), 0 ≤ f i) (hg : ∀ (i : ι), 0 ≤ g i) (hsf : Summable f) (hsg : Summable g) {a : ℝ} (ha : 0 < a) (ha₁ : a < 1) : (Summable fun (i : ι) => f i ^ a * g i ^ (1 - a)) ∧ ∑' (i : ι), f i ^ a * g i ^ (1 - a) ≤ (∑' (i : ι), f i) ^ a * (∑' (i : ι), g i) ^ (1 - a)