case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i => g i ^ q
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
⊢ (Summable fun i => (fun i => ↑(f i)) i * g i) ∧
    (∑' (i : ι), (fun i => ↑(f i)) i * g i) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i => f i ^ p
hg_sum : Summable fun i => g i ^ q
⊢ (Summable fun i => f i * g i) ∧
    (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
lift f to ι → ℝ≥0 using hf
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i => (fun i => ↑(g i)) i ^ q
⊢ (Summable fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ∧
    (∑' (i : ι), (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) * (∑' (i : ι), (fun i => ↑(g i)) i ^ q) ^ (1 / q)
case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i => g i ^ q
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
⊢ (Summable fun i => (fun i => ↑(f i)) i * g i) ∧
    (∑' (i : ι), (fun i => ↑(f i)) i * g i) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
lift g to ι → ℝ≥0 using hg
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
hf_sum : Summable fun a => f a ^ p
hg_sum : Summable fun a => g a ^ q
⊢ (Summable fun a => f a * g a) ∧
    (∑' (a : ι), f a * g a) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) * (∑' (a : ι), g a ^ q) ^ (1 / q)
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i => (fun i => ↑(g i)) i ^ q
⊢ (Summable fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ∧
    (∑' (i : ι), (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) * (∑' (i : ι), (fun i => ↑(g i)) i ^ q) ^ (1 / q)
norm_cast  at *
no goals
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
hf_sum : Summable fun a => f a ^ p
hg_sum : Summable fun a => g a ^ q
⊢ (Summable fun a => f a * g a) ∧
    (∑' (a : ι), f a * g a) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) * (∑' (a : ι), g a ^ q) ^ (1 / q)
exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum