ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this :
  ↑(∑ i in s,
        (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i *
          (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i) ≤
    ↑((∑ i in s, (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i ^ p) ^ (1 / p) *
        (∑ i in s, (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i ^ q) ^ (1 / q))
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) * (∑ i in s, abs (g i) ^ q) ^ (1 / q)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) * (∑ i in s, abs (g i) ^ q) ^ (1 / q)
have :=
  NNReal.coe_le_coe.2
    (NNReal.inner_le_Lp_mul_Lq s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩)
      hpq)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this : ∑ x in s, abs (f x) * abs (g x) ≤ (∑ x in s, abs (f x) ^ p) ^ (1 / p) * (∑ x in s, abs (g x) ^ q) ^ (1 / q)
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) * (∑ i in s, abs (g i) ^ q) ^ (1 / q)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this :
  ↑(∑ i in s,
        (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i *
          (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i) ≤
    ↑((∑ i in s, (fun i => { val := abs (f i), property := (_ : 0 ≤ abs (f i)) }) i ^ p) ^ (1 / p) *
        (∑ i in s, (fun i => { val := abs (g i), property := (_ : 0 ≤ abs (g i)) }) i ^ q) ^ (1 / q))
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) * (∑ i in s, abs (g i) ^ q) ^ (1 / q)
push_cast at this
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this : ∑ x in s, abs (f x) * abs (g x) ≤ (∑ x in s, abs (f x) ^ p) ^ (1 / p) * (∑ x in s, abs (g x) ^ q) ^ (1 / q)
i : ι
x✝ : i ∈ s
⊢ f i * g i ≤ abs (f i) * abs (g i)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this : ∑ x in s, abs (f x) * abs (g x) ≤ (∑ x in s, abs (f x) ^ p) ^ (1 / p) * (∑ x in s, abs (g x) ^ q) ^ (1 / q)
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, abs (f i) ^ p) ^ (1 / p) * (∑ i in s, abs (g i) ^ q) ^ (1 / q)
refine' le_trans (sum_le_sum fun i _ => _) this
no goals
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this : ∑ x in s, abs (f x) * abs (g x) ≤ (∑ x in s, abs (f x) ^ p) ^ (1 / p) * (∑ x in s, abs (g x) ^ q) ^ (1 / q)
i : ι
x✝ : i ∈ s
⊢ f i * g i ≤ abs (f i) * abs (g i)
simp only [← abs_mul, le_abs_self]