-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lq_tsum {f g : ι → ℝ≥0} {p q : ℝ} (hpq : p.IsConjExponent q)
    (hf : Summable fun i => f i ^ p) (hg : 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)

Proof state:
case refine_2
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≤ (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.symm.pos)]

Result:
case refine_2
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, g i ^ q ≤ ∑' (i : ι), g i ^ q

Proof state:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
refine le_trans (inner_le_Lp_mul_Lq s f g hpq) (mul_le_mul ?_ ?_ bot_le bot_le)

Result:
case refine_1
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p)

case refine_2
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ (∑ i ∈ s, g i ^ q) ^ (1 / q) ≤ (∑' (i : ι), g i ^ q) ^ (1 / q)

Proof state:
case refine_1
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ (∑ i ∈ s, f i ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p)

Tactic:
rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.pos)]

Result:
case refine_1
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, f i ^ p ≤ ∑' (i : ι), f i ^ p

Proof state:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i)

Tactic:
refine ⟨(∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q), ?_⟩

Result:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) ∈
    upperBounds (Set.range fun s => ∑ i ∈ s, f i * g i)

Proof state:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / 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)

Tactic:
have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i) := by
  refine ⟨(∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q), ?_⟩
  rintro a ⟨s, rfl⟩
  exact H₁ s

Result:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i)
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Proof state:
case intro
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
s : Finset ι
⊢ (fun s => ∑ i ∈ s, f i * g i) s ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
exact H₁ s

Result:
no goals

Proof state:
case refine_2
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, g i ^ q ≤ ∑' (i : ι), g i ^ q

Tactic:
exact sum_le_tsum _ (fun _ _ => zero_le _) hg

Result:
no goals

Proof state:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
⊢ ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
intro s

Result:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Proof state:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i)
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable

Result:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i)
H₂ : Summable fun i => f i * g i
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Proof state:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, f i * g i)
H₂ : Summable fun i => f i * g i
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)

Tactic:
exact ⟨H₂, tsum_le_of_sum_le H₂ H₁⟩

Result:
no goals

Proof state:
case refine_1
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, f i ^ p ≤ ∑' (i : ι), f i ^ p

Tactic:
exact sum_le_tsum _ (fun _ _ => zero_le _) hf

Result:
no goals

Proof state:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) ∈
    upperBounds (Set.range fun s => ∑ i ∈ s, f i * g i)

Tactic:
rintro a ⟨s, rfl⟩

Result:
case intro
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i ∈ s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
s : Finset ι
⊢ (fun s => ∑ i ∈ s, f i * g i) s ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)