-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lq_tsum_of_nonneg (hpq : p.IsConjExponent 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)

Proof state:
ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent 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)

Tactic:
lift f to ι → ℝ≥0 using hf

Result:
case intro
ι : Type u
g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent 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)

Proof state:
case intro
ι : Type u
g : ι → ℝ
p q : ℝ
hpq : p.IsConjExponent 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)

Tactic:
lift g to ι → ℝ≥0 using hg

Result:
case intro.intro
ι : Type u
p q : ℝ
hpq : p.IsConjExponent 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)

Proof state:
case intro.intro
ι : Type u
p q : ℝ
hpq : p.IsConjExponent q
f : ι → ℝ≥0
hf_sum : Summable fun i => ↑(f i) ^ p
g : ι → ℝ≥0
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)

Tactic:
norm_cast at *

Result:
case intro.intro
ι : Type u
p q : ℝ
hpq : p.IsConjExponent 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)

Proof state:
case intro.intro
ι : Type u
p q : ℝ
hpq : p.IsConjExponent 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)

Tactic:
beta_reduce at *

Result:
case intro.intro
ι : Type u
p q : ℝ
hpq : p.IsConjExponent q
f : ι → ℝ≥0
hf_sum : Summable fun i => ↑(f i) ^ p
g : ι → ℝ≥0
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)

Proof state:
case intro.intro
ι : Type u
p q : ℝ
hpq : p.IsConjExponent 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)

Tactic:
exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum

Result:
no goals