awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i)

Tactic:
exact sum_nonneg fun i _ ↦ by have := hw i; positivity

Premises used: Finset.sum_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
⊢ ∀ (i : ι), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
lift :
  ∀ (f : (i : ι) → ℝ≥0)
    (hf_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p),
    (Summable (α := ℝ) fun (i : ι) ↦ ((fun (i : ι) ↦ (↑(f i) : ℝ)) i * g i) ^ r) ∧
      ∑' (i : ι), ((fun (i : ι) ↦ (↑(f i) : ℝ)) i * g i) ^ r ≤
        HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
          HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)
⊢ (Summable (α := ℝ) fun (i : ι) ↦ (f i * g i) ^ r) ∧
    ∑' (i : ι), (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ g i ^ q
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p
⊢ ∀ (i : ι), 0 ≤ g i

Tactic:
hg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ g i ^ q
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p
lift :
  ∀ (g : (i : ι) → ℝ≥0)
    (hg_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q),
    (Summable (α := ℝ) fun (i : ι) ↦
        HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r) ∧
      ∑' (i : ι), HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r ≤
        HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
          HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (r / q)
⊢ (Summable (α := ℝ) fun (i : ι) ↦ ((fun (i : ι) ↦ (↑(f i) : ℝ)) i * g i) ^ r) ∧
    ∑' (i : ι), ((fun (i : ι) ↦ (↑(f i) : ℝ)) i * g i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
lift g to ι → ℝ≥0 using hg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p
g : (i : ι) → ℝ≥0
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q
beta_reduce :
  ∀ (hf_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) (g : (i : ι) → ℝ≥0)
    (hg_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(g i) : ℝ) ^ q),
    (Summable (α := ℝ) fun (i : ι) ↦ ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r) ∧
      ∑' (i : ι), ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r ≤
        HPow.hPow (α := ℝ) (∑' (i : ι), (↑(f i) : ℝ) ^ p) (r / p) *
          HPow.hPow (α := ℝ) (∑' (i : ι), (↑(g i) : ℝ) ^ q) (r / q)
⊢ (Summable (α := ℝ) fun (i : ι) ↦
      HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r) ∧
    ∑' (i : ι), HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (r / q)

Tactic:
beta_reduce at *
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(f i) : ℝ) ^ p
g : (i : ι) → ℝ≥0
hg_sum : Summable (α := ℝ) fun (i : ι) ↦ (↑(g i) : ℝ) ^ q
norm_cast :
  ∀ (hf_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ f a ^ p) (hg_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ g a ^ q),
    (Summable (α := ℝ≥0) fun (a : ι) ↦ (f a * g a) ^ r) ∧
      ∑' (a : ι), (f a * g a) ^ r ≤
        HPow.hPow (α := ℝ≥0) (∑' (a : ι), f a ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (a : ι), g a ^ q) (r / q)
⊢ (Summable (α := ℝ) fun (i : ι) ↦ ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r) ∧
    ∑' (i : ι), ((↑(f i) : ℝ) * (↑(g i) : ℝ)) ^ r ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), (↑(f i) : ℝ) ^ p) (r / p) *
        HPow.hPow (α := ℝ) (∑' (i : ι), (↑(g i) : ℝ) ^ q) (r / q)

Tactic:
norm_cast at *
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f g : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ f a ^ p
hg_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ g a ^ q
⊢ (Summable (α := ℝ≥0) fun (a : ι) ↦ (f a * g a) ^ r) ∧
    ∑' (a : ι), (f a * g a) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (a : ι), f a ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (a : ι), g a ^ q) (r / q)

Tactic:
NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf_sum hg_sum

Premises used: NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q r : ℝ
hpqr : p.HolderTriple q r
f g : (i : ι) → ℝ≥0
hf_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ f a ^ p
hg_sum : Summable (α := ℝ≥0) fun (a : ι) ↦ g a ^ q
⊢ (Summable (α := ℝ≥0) fun (a : ι) ↦ (f a * g a) ^ r) ∧
    ∑' (a : ι), (f a * g a) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (a : ι), f a ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (a : ι), g a ^ q) (r / q)

Tactic:
exact NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf_sum hg_sum

Premises used: NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate 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 ≤
      HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
simpa using summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum

Premises used: Real.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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) ^ r

Tactic:
(summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum).1

Premises used: And.left, Real.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate 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

Tactic:
(summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).1

Premises used: Real.summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg, And.left
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
⊢ ∑' (i : ι), (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
(summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum).2

Premises used: And.right, Real.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
⊢ LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)

Tactic:
have hf' : 0 ≤ ∑' i, f i ^ p := tsum_nonneg fun i ↦ rpow_nonneg (hf i) p
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
⊢ LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)

Tactic:
have hg' : 0 ≤ ∑' i, g i ^ q := tsum_nonneg fun i ↦ rpow_nonneg (hg i) q
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
⊢ 0 < r

Tactic:
have hr := hpqr.pos'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
i : ι
positivity positivity₁ positivity₂ : 0 ≤ f i → 0 ≤ (f i * g i) ^ r
positivity₃ positivity₄ : 0 ≤ f i → 0 ≤ g i → 0 ≤ (f i * g i) ^ r
⊢ 0 ≤ (f i * g i) ^ r

Tactic:
positivity [hf i, hg i]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
⊢ 0 ≤ HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
h :
  HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q) =
    (HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), (f i * g i) ^ r) (1 / r) ≤
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
convert!
    rpow_le_rpow_iff (tsum_nonneg fun i ↦ by positivity [hf i, hg i]) (by positivity)
          (inv_eq_one_div r ▸ inv_pos.mpr hr) |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg hpqr hf hg hf_sum hg_sum using 1

Premises used: Iff.mpr, Real.Lr_rpow_le_Lp_mul_Lq_tsum_of_nonneg, Real.rpow_le_rpow_iff, tsum_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
h :
  HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q) =
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p * (1 / r)) *
      HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q * (1 / r))
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q) =
    (HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)

Tactic:
rw [mul_rpow (rpow_nonneg hf' _) (rpow_nonneg hg' _), ← Real.rpow_mul hg', ← Real.rpow_mul hf']

Premises used: Real.mul_rpow, Real.rpow_nonneg, Real.rpow_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q r : ℝ
hpqr : p.HolderTriple q r
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
hf' : LE.le (α := ℝ) 0 (∑' (i : ι), f i ^ p)
hg' : LE.le (α := ℝ) 0 (∑' (i : ι), g i ^ q)
hr : 0 < r
⊢ HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q) =
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (r / p * (1 / r)) *
      HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (r / q * (1 / r))

Tactic:
field_simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate 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
⊢ ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
(summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg hpq hf hg hf_sum hg_sum).2

Premises used: Real.summable_and_inner_le_Lp_mul_Lq_tsum_of_nonneg, And.right
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate 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)
⊢ ∀ (i : ι), 0 ≤ f i

Tactic:
hf
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate 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)
lift :
  ∀ (f : (i : ι) → ℝ≥0) (hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((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
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun (i : ι) ↦ f i * g i) C

Tactic:
lift f to ι → ℝ≥0 using hf
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate 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 : (i : ι) → ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)
⊢ ∀ (i : ι), 0 ≤ g i

Tactic:
hg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
g : ι → ℝ
p q : ℝ
hpq : p.HolderConjugate 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 : (i : ι) → ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)
lift :
  ∀ (g : (i : ι) → ℝ≥0) (hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)),
    ∃ (C : ℝ),
      0 ≤ C ∧
        C ≤ A * B ∧
          HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun (i : ι) ↦ (fun (i : ι) ↦ (↑(f i) : ℝ)) i * g i) C

Tactic:
lift g to ι → ℝ≥0 using hg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : (i : ι) → ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)
g : (i : ι) → ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)
⊢ 0 ≤ A

Tactic:
hA
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : (i : ι) → ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) (A ^ p)
g : (i : ι) → ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)
lift :
  ∀ (A : ℝ≥0) (hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)),
    ∃ (C : ℝ),
      0 ≤ C ∧
        C ≤ (↑A : ℝ) * B ∧
          HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ A * B ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C

Tactic:
lift A to ℝ≥0 using hA
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
B : ℝ
hB : 0 ≤ B
f g : (i : ι) → ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)
⊢ 0 ≤ B

Tactic:
hB
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
B : ℝ
hB : 0 ≤ B
f g : (i : ι) → ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) (B ^ q)
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)
lift :
  ∀ (B : ℝ≥0) (hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) ((↑B : ℝ) ^ q)),
    ∃ (C : ℝ),
      0 ≤ C ∧
        C ≤ (↑A : ℝ) * (↑B : ℝ) ∧
          HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) * B ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C

Tactic:
lift B to ℝ≥0 using hB
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ HPow.hPow (α := ℝ) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i) q) ((↑B : ℝ) ^ q)
beta_reduce :
  ∀ (hf_sum : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)) (B : ℝ≥0)
    (hg_sum : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ q) ((↑B : ℝ) ^ q)),
    ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
⊢ ∃ (C : ℝ),
    0 ≤ C ∧
      C ≤ (↑A : ℝ) * (↑B : ℝ) ∧
        HasSum (fun (i : ι) ↦ HMul.hMul (α := ℝ) ((fun (i : ι) ↦ (↑(f i) : ℝ)) i) ((fun (i : ι) ↦ (↑(g i) : ℝ)) i)) C

Tactic:
beta_reduce at *
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ q) ((↑B : ℝ) ^ q)
⊢ HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)

Tactic:
norm_cast at hf_sum hg_sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) ^ p) ((↑A : ℝ) ^ p)
B : ℝ≥0
hg_sum : HasSum (fun (i : ι) ↦ (↑(g i) : ℝ) ^ q) ((↑B : ℝ) ^ q)
hf_sum₁ : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
⊢ HasSum (fun (a : ι) ↦ g a ^ q) (B ^ q)

Tactic:
norm_cast at hf_sum hg_sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun (a : ι) ↦ f a ^ p) (A ^ p)
hg_sum : HasSum (fun (a : ι) ↦ g a ^ q) (B ^ q)
obtain :
  ∀ (C : ℝ≥0) (hC : C ≤ A * B) (H : HasSum (fun (i : ι) ↦ f i * g i) C),
    ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C

Tactic:
obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum

Premises used: NNReal.inner_le_Lp_mul_Lq_hasSum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥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 : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C

Tactic:
⟨C, C.prop, hC, ?_⟩

Premises used: Subtype.prop, And.intro, Exists.intro, NNReal.toReal
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥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
refine : HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) (↑C : ℝ)
⊢ ∃ (C : ℝ), 0 ≤ C ∧ C ≤ (↑A : ℝ) * (↑B : ℝ) ∧ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) C

Tactic:
refine ⟨C, C.prop, hC, ?_⟩
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
p q : ℝ
hpq : p.HolderConjugate q
f g : (i : ι) → ℝ≥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 norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HasSum (fun (a : ι) ↦ f a * g a) C
⊢ HasSum (fun (i : ι) ↦ (↑(f i) : ℝ) * (↑(g i) : ℝ)) (↑C : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i|) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, |f i| ^ p

Tactic:
rpow_sum_le_const_mul_sum_rpow s f hp

Premises used: Real.rpow_sum_le_const_mul_sum_rpow
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
h : Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, |f i|)
h₁ : Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ) (↑(#s) : ℝ) (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
convert! rpow_sum_le_const_mul_sum_rpow s f hp using 2

Premises used: Real.rpow_sum_le_const_mul_sum_rpow
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
h : ∀ x ∈ s, f x = |f x|
⊢ Eq (α := ℝ) (∑ i ∈ s, f i) (∑ i ∈ s, |f i|)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
h : ∀ x ∈ s, f x ^ p = |f x| ^ p
⊢ Eq (α := ℝ) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, |f i| ^ p)

Tactic:
apply sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i = |f i|

Tactic:
simp only [abs_of_nonneg, hf i hi]

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p

Tactic:
simp only [abs_of_nonneg, hf i hi]

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, |f i + g i| ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ) (∑ i ∈ s, |f i| ^ p) (1 / p) + HPow.hPow (α := ℝ) (∑ i ∈ s, |g i| ^ p) (1 / p)

Tactic:
Lp_add_le s f g hp

Premises used: Real.Lp_add_le