case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : HasSum (fun i => g i ^ q) (B ^ q)
f : ι → ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => (fun i => ↑(f i)) i * g i) C
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : HasSum (fun i => f i ^ p) (A ^ p)
hg_sum : HasSum (fun i => g i ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => f i * g i) C
lift f to ι → ℝ≥0 using hf
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : HasSum (fun i => g i ^ q) (B ^ q)
f : ι → ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => (fun i => ↑(f i)) i * g i) C
lift g to ι → ℝ≥0 using hg
case intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (B ^ q)
A : ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
lift A to ℝ≥0 using hA
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (↑B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
case intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (B ^ q)
A : ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
lift B to ℝ≥0 using hB
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (↑B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
norm_cast at hf_sum hg_sum
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i => f i * g i) C
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i => f i * g i) C
⊢ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ↑C
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i => f i * g i) C
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
refine' ⟨C, C.prop, hC, _⟩
no goals
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i => f i * g i) C
⊢ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ↑C
norm_cast