awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (f x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)) ^ p) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, f x ^ p / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p) 1
inr₂ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p = 1
inr₃ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p * p) = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
have inr₄ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (p⁻¹ * p) = 1
Tactic: simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one,
      div_self hf.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (f x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)) ^ p) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, f x ^ p / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p) 1
inr₂ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p = 1
inr₃ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p * p) = 1
inr₄ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (p⁻¹ * p) = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
have inr₅ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (β := ℝ) (∑ i ∈ s, f i ^ p) 1 = 1
Tactic: simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one,
      div_self hf.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (f x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)) ^ p) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, f x ^ p / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p) 1
inr₂ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p = 1
inr₃ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p * p) = 1
inr₄ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (p⁻¹ * p) = 1
inr₅ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (β := ℝ) (∑ i ∈ s, f i ^ p) 1 = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
have inr₆ : HDiv.hDiv (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, f i ^ p) = 1
Tactic: simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one,
      div_self hf.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (g x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ^ q) 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
have inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, g x ^ q / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q) 1
Tactic: simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero,
      rpow_one, div_self hg.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (g x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ^ q) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, g x ^ q / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q) 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
have inr₂ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q = 1
Tactic: simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero,
      rpow_one, div_self hg.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (g x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ^ q) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, g x ^ q / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q) 1
inr₂ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
have inr₃ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q * q) = 1
Tactic: simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero,
      rpow_one, div_self hg.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (g x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ^ q) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, g x ^ q / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q) 1
inr₂ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q = 1
inr₃ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q * q) = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
have inr₄ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (q⁻¹ * q) = 1
Tactic: simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero,
      rpow_one, div_self hg.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (g x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ^ q) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, g x ^ q / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q) 1
inr₂ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q = 1
inr₃ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q * q) = 1
inr₄ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (q⁻¹ * q) = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
have inr₅ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (β := ℝ) (∑ i ∈ s, g i ^ q) 1 = 1
Tactic: simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero,
      rpow_one, div_self hg.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (g x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ^ q) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, g x ^ q / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q) 1
inr₂ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) ^ q = 1
inr₃ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q * q) = 1
inr₄ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (q⁻¹ * q) = 1
inr₅ : (∑ i ∈ s, g i ^ q) / HPow.hPow (α := ℝ≥0) (β := ℝ) (∑ i ∈ s, g i ^ q) 1 = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
have inr₆ : HDiv.hDiv (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, g i ^ q) = 1
Tactic: simp_rw [g', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.symm.ne_zero,
      rpow_one, div_self hg.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (f i * g i) ^ r) (1 / r) ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have h : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) =
  (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q)) ^ (1 / r)
Tactic: convert!
    rpow_le_rpow_iff (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos' : 0 < 1 / r) |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq s f g hpqr using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) =
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q)) ^ (1 / r)
have hr : r ≠ 0
Tactic: have hr := hpqr.pos'.ne'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hr : r ≠ 0
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) =
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q)) ^ (1 / r)
have h : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) =
  HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p * (1 / r)) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q * (1 / r))
Tactic: simp only [← rpow_mul, mul_rpow]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have inl : ∀ (hp : LE.le (α := ℝ) 1 1),
  ∑ i ∈ s, w i * f i ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (HSub.hSub (α := ℝ) 1 1⁻¹) *
      HPow.hPow (α := ℝ≥0) (β := ℝ) (∑ i ∈ s, w i * HPow.hPow (β := ℝ) (f i) 1) 1⁻¹
Tactic: obtain rfl | hp := hp.eq_or_lt
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
inl :
  ∀ (hp : LE.le (α := ℝ) 1 1),
    ∑ i ∈ s, w i * f i ≤
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (HSub.hSub (α := ℝ) 1 1⁻¹) *
        HPow.hPow (α := ℝ≥0) (β := ℝ) (∑ i ∈ s, w i * HPow.hPow (β := ℝ) (f i) 1) 1⁻¹
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have inr : ∀ (hp : 1 < p),
  ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
Tactic: obtain rfl | hp := hp.eq_or_lt
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have inr : Eq (α := ℝ≥0) (∑ i ∈ s, w i * f i) (∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i))
Tactic: calc
    _ = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i) := ?_
    _ ≤ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) *
          (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) :=
        inner_le_Lp_mul_Lq _ _ _ (.symm <| Real.holderConjugate_iff.mpr ⟨hp, by simp⟩)
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
inr : Eq (α := ℝ≥0) (∑ i ∈ s, w i * f i) (∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i))
⊢ ∑ i ∈ s, w i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have inr₁ : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) (1 / (1 - p⁻¹)⁻¹) *
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) (1 / p) =
  HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
Tactic: calc
    _ = ∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i) := ?_
    _ ≤ (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) ^ (1 / (1 - p⁻¹)⁻¹) *
          (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) ^ (1 / p) :=
        inner_le_Lp_mul_Lq _ _ _ (.symm <| Real.holderConjugate_iff.mpr ⟨hp, by simp⟩)
    _ = _ := ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, w i * f i) (∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i))
have inr : ∀ (i : ι), (↑(w i * f i) : ℝ) = (↑(w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)) : ℝ)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
i : ι
⊢ (↑(w i * f i) : ℝ) = (↑(w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)) : ℝ)
have inr : 1 - p⁻¹ + p⁻¹ = 1
Tactic: rw [← mul_assoc, ← rpow_of_add_eq _ one_ne_zero, rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) (1 / (1 - p⁻¹)⁻¹) *
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) (1 / p) =
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have hp₀ : p ≠ 0
Tactic: have hp₀ : p ≠ 0 := by positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
hp₀ : p ≠ 0
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i ^ (1 - p⁻¹)) ^ (1 - p⁻¹)⁻¹) (1 / (1 - p⁻¹)⁻¹) *
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i ^ p⁻¹ * f i) ^ p) (1 / p) =
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have hp₁ : 1 - p⁻¹ ≠ 0
Tactic: have hp₁ : 1 - p⁻¹ ≠ 0 := by simp [sub_eq_zero, hp.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
s : Finset ι
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have hp : 0 < p
Tactic: obtain ⟨hp, hq, hr⟩ := hpqr.all_pos
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
s : Finset ι
hp : 0 < p
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have hq : 0 < q
Tactic: obtain ⟨hp, hq, hr⟩ := hpqr.all_pos
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have hr : 0 < r
Tactic: obtain ⟨hp, hq, hr⟩ := hpqr.all_pos
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have refine_1 : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p)
Tactic: refine le_trans (Lr_rpow_le_Lp_mul_Lq s f g hpqr) (mul_le_mul ?_ ?_ bot_le bot_le)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
refine_1 : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p)
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have refine_2 : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
Tactic: refine le_trans (Lr_rpow_le_Lp_mul_Lq s f g hpqr) (mul_le_mul ?_ ?_ bot_le bot_le)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p)
have refine_1 : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have refine_2 : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (∑' (i : ι), g i ^ q)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ (f i * g i) ^ r) ∧
    ∑' (i : ι), (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have H₁ : ∀ (s : Finset ι),
  ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
Tactic: have H₁ : ∀ s : Finset ι,
      ∑ i ∈ s, (f i * g i) ^ r ≤ (∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q) := by
    intro s
    obtain ⟨hp, hq, hr⟩ := hpqr.all_pos
    refine le_trans (Lr_rpow_le_Lp_mul_Lq s f g hpqr) (mul_le_mul ?_ ?_ bot_le bot_le)
    · gcongr
      exact hf.sum_le_tsum _ (fun _ _ => zero_le)
    · gcongr
      exact hg.sum_le_tsum _ (fun _ _ => zero_le)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
⊢ BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i * g i) ^ r)
have refine : Membership.mem (γ := Set ℝ≥0) (upperBounds (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i * g i) ^ r))
  (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q))
Tactic: refine ⟨(∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q), ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ (f i * g i) ^ r) ∧
    ∑' (i : ι), (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have bdd : BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i * g i) ^ r)
Tactic: have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i * g i) ^ r) := by
    refine ⟨(∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q), ?_⟩
    rintro a ⟨s, rfl⟩
    exact H₁ s
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
H₁ :
  ∀ (s : Finset ι),
    ∑ i ∈ s, (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
bdd : BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i * g i) ^ r)
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ (f i * g i) ^ r) ∧
    ∑' (i : ι), (f i * g i) ^ r ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)
have H₂ : Summable (α := ℝ≥0) fun (i : ι) ↦ (f i * g i) ^ r
Tactic: have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
⊢ HPow.hPow (α := ℝ≥0) (∑' (i : ι), (f i * g i) ^ r) (1 / r) ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
have h : HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q) =
  (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)
Tactic: convert!
    rpow_le_rpow_iff (inv_eq_one_div r ▸ inv_pos.mpr hpqr.pos') |>.mpr <|
      Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
⊢ HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q) =
    (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)
have hr : r ≠ 0
Tactic: have hr := hpqr.pos'.ne'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
hr : r ≠ 0
⊢ HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q) =
    (HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)
have h : HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q) =
  HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p * (1 / r)) *
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q * (1 / r))
Tactic: simp only [← rpow_mul, mul_rpow]