no goals
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
convert inner_le_Lp_mul_Lq s f g hpq using 3 <;> apply sum_congr rfl <;> intro i hi <;>
  simp only [abs_of_nonneg, hf i hi, hg i hi]