case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
obtain ⟨H₁, H₂⟩ := inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
have hB : B = (∑' i : ι, g i ^ q) ^ (1 / q) := by
  rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
case intro.refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ (∑' (i : ι), f i * g i) ≤ A * B

case intro.refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ HasSum (fun i => f i * g i) (∑' (i : ι), f i * g i)
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
refine' ⟨∑' i, f i * g i, _, _⟩
no goals
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ A = (∑' (i : ι), f i ^ p) ^ (1 / p)
rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]
no goals
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (∑' (i : ι), g i ^ q) ^ (1 / q)
rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
no goals
case intro.refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ (∑' (i : ι), f i * g i) ≤ A * B
simpa [hA, hB] using H₂
no goals
case intro.refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : (∑' (i : ι), f i * g i) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ HasSum (fun i => f i * g i) (∑' (i : ι), f i * g i)
simpa only [rpow_self_rpow_inv hpq.ne_zero] using H₁.hasSum