awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
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)
H₂ : Summable (α := ℝ≥0) fun (i : ι) ↦ (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)

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

Premises used: Summable.tsum_le_of_sum_le, And.intro
-- Module: Mathlib.Analysis.MeanInequalities
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)
H₂ : Summable (α := ℝ≥0) fun (i : ι) ↦ (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)

Tactic:
exact ⟨H₂, H₂.tsum_le_of_sum_le H₁⟩
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
⊢ (Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i) ∧
    ∑' (i : ι), f i * g i ≤
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
simpa using summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpq hf hg

Premises used: NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum
-- Module: Mathlib.Analysis.MeanInequalities
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

Tactic:
(summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg).1

Premises used: NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum, And.left
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i

Tactic:
(summable_and_inner_le_Lp_mul_Lq_tsum hpq hf hg).1

Premises used: NNReal.summable_and_inner_le_Lp_mul_Lq_tsum, And.left
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ ∑' (i : ι), (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
(summable_and_Lr_rpow_le_Lp_mul_Lq_tsum hpqr hf hg).2

Premises used: NNReal.summable_and_Lr_rpow_le_Lp_mul_Lq_tsum, And.right
-- Module: Mathlib.Analysis.MeanInequalities
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) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)) ^ (1 / r)

Tactic:
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

Premises used: Iff.mpr, NNReal.Lr_rpow_le_Lp_mul_Lq_tsum, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.MeanInequalities
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 :
  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)
⊢ 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)

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

Premises used: Iff.mpr, NNReal.Lr_rpow_le_Lp_mul_Lq_tsum, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ r ≠ 0

Tactic:
have hr := hpqr.pos'.ne'
-- Module: Mathlib.Analysis.MeanInequalities
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
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))
⊢ 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:
simp only [← rpow_mul, mul_rpow]

Premises used: NNReal.rpow_mul, NNReal.mul_rpow
-- Module: Mathlib.Analysis.MeanInequalities
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 * (1 / r)) *
      HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q * (1 / r))

Tactic:
field_simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Summable (α := ℝ≥0) fun (i : ι) ↦ f i ^ p
hg : Summable (α := ℝ≥0) fun (i : ι) ↦ g i ^ q
⊢ ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
(summable_and_inner_le_Lp_mul_Lq_tsum hpq hf hg).2

Premises used: NNReal.summable_and_inner_le_Lp_mul_Lq_tsum, And.right
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i

Tactic:
obtain ⟨H₁, H₂⟩ := summable_and_inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable

Premises used: NNReal.summable_and_inner_le_Lp_mul_Lq_tsum, HasSum.summable
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
⊢ ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
obtain ⟨H₁, H₂⟩ := summable_and_inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable

Premises used: NNReal.summable_and_inner_le_Lp_mul_Lq_tsum, HasSum.summable
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
rw : A = (A ^ p) ^ (1 / p)
rw₁ rw₂ : A = A
⊢ A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)

Tactic:
rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]

Premises used: Real.HolderTriple.ne_zero, NNReal.rpow_inv_rpow_self, HasSum.tsum_eq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
⊢ A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)

Tactic:
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
rw : B = (B ^ q) ^ (1 / q)
rw₁ rw₂ : B = B
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]

Premises used: Real.HolderTriple.ne_zero, Real.HolderConjugate.symm, NNReal.rpow_inv_rpow_self, HasSum.tsum_eq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
⊢ B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)

Tactic:
have hB : B = (∑' i : ι, g i ^ q) ^ (1 / q) := by
    rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C

Tactic:
⟨∑' i, f i * g i, ?_, ?_⟩

Premises used: HMul.hMul, tsum, And.intro, Exists.intro, SummationFilter.unconditional
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
refine_1 : ∑' (i : ι), f i * g i ≤ A * B
refine_2 : HasSum (α := ℝ≥0) (fun (i : ι) ↦ f i * g i) (∑' (i : ι), f i * g i)
⊢ ∃ C ≤ A * B, HasSum (fun (i : ι) ↦ f i * g i) C

Tactic:
refine ⟨∑' i, f i * g i, ?_, ?_⟩
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
⊢ ∑' (i : ι), f i * g i ≤ A * B

Tactic:
simpa [hA, hB] using H₂
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : HasSum (fun (i : ι) ↦ f i ^ p) (A ^ p)
hg : HasSum (fun (i : ι) ↦ g i ^ q) (B ^ q)
H₁ : Summable (α := ℝ≥0) fun (i : ι) ↦ f i * g i
H₂ :
  ∑' (i : ι), f i * g i ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
hA : A = HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (1 / p)
hB : B = HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (1 / q)
⊢ HasSum (α := ℝ≥0) (fun (i : ι) ↦ f i * g i) (∑' (i : ι), f i * g i)

Tactic:
simpa only [rpow_self_rpow_inv hpq.ne_zero] using H₁.hasSum

Premises used: Real.HolderTriple.ne_zero, Summable.hasSum, NNReal.rpow_self_rpow_inv
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
inl :
  ∀ (hp : 1 = p), HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
inr :
  ∀ (hp : 1 < p), HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
rcases eq_or_lt_of_le hp with hp | hp

Premises used: eq_or_lt_of_le
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 = p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
simp [← hp]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ p.HolderConjugate q

Tactic:
have hpq : p.HolderConjugate q := .conjExponent hp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
⊢ 1 / p * p = 1

Tactic:
have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
hp₁ : 1 / p * p = 1
rw : 1 / q * p = p / q
⊢ 1 / q * p = p - 1

Tactic:
rw [← hpq.div_conj_eq_sub_one]

Premises used: Real.HolderConjugate.div_conj_eq_sub_one
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p / q

Tactic:
ring
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p - 1

Tactic:
have hq : 1 / q * p = p - 1 := by
    rw [← hpq.div_conj_eq_sub_one]
    ring
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
hp₁ : 1 / p * p = 1
hq : 1 / q * p = p - 1
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0) (↑(#s) : ℝ≥0) (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
simpa only [NNReal.mul_rpow, ← NNReal.rpow_mul, hp₁, hq, one_mul, one_rpow, rpow_one,
    Pi.one_apply, sum_const, Nat.smul_one_eq_cast] using
    NNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg

Premises used: Pi.one_apply, NNReal.rpow_le_rpow, Real.HolderConjugate.symm, NNReal.rpow_mul, Nat.smul_one_eq_cast, NNReal.one_rpow, OfNat.ofNat, NNReal.rpow_one, NNReal.mul_rpow, one_mul, Real.HolderTriple.nonneg, NNReal.inner_le_Lp_mul_Lq, Finset.sum_const
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
left :
  Membership.mem (γ := Set ℝ≥0)
    ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
right :
  Membership.mem (γ := Set ℝ≥0)
    (upperBounds ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1}))
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))
⊢ IsGreatest ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))

Tactic:
constructor
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
h :
  (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
⊢ Membership.mem (γ := Set ℝ≥0)
    ((fun (g : ι → ℝ≥0) ↦ ∑ i ∈ s, f i * g i) '' {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1})
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p))

Tactic:
use fun i => f i ^ p / f i / (∑ i ∈ s, f i ^ p) ^ (1 / q)

Premises used: HDiv.hDiv, HPow.hPow, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
h :
  ∀ (hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0),
    (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
      ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
          f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
        HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
h₁ :
  ∀ (hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)),
    (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
      ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
          f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
        HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)

Tactic:
obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)

Premises used: eq_zero_or_pos, HPow.hPow, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)

Tactic:
simp [hf, hpq.ne_zero, hpq.symm.ne_zero]

Premises used: Real.HolderTriple.ne_zero, Real.HolderConjugate.symm
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
⊢ p + q - q ≠ 0

Tactic:
simp [hpq.ne_zero]

Premises used: Real.HolderTriple.ne_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
⊢ p + q - q ≠ 0

Tactic:
have A : p + q - q ≠ 0 := by simp [hpq.ne_zero]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
⊢ ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p

Tactic:
fun y => mul_div_cancel_left_of_imp fun h => ?_

Premises used: mul_div_cancel_left_of_imp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
refine : ∀ (y : ℝ≥0) (h : y = 0), y ^ p = 0
⊢ ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p

Tactic:
refine fun y => mul_div_cancel_left_of_imp fun h => ?_

Premises used: mul_div_cancel_left_of_imp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
y : ℝ≥0
h : y = 0
⊢ y ^ p = 0

Tactic:
simp [h, hpq.ne_zero]

Premises used: Real.HolderTriple.ne_zero
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
⊢ ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p

Tactic:
have B : ∀ y : ℝ≥0, y * y ^ p / y = y ^ p := by
        refine fun y => mul_div_cancel_left_of_imp fun h => ?_
        simp [h, hpq.ne_zero]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
h :
  (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q) = HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
⊢ (Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} fun (i : ι) ↦
      f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) ∧
    ((fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) fun (i : ι) ↦
        f i ^ p / f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q)) =
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)

Tactic:
simp only [Set.mem_setOf_eq, div_rpow, ← sum_div, ← rpow_mul,
        div_mul_cancel₀ _ hpq.symm.ne_zero, rpow_one, div_le_iff₀ hf, one_mul, hpq.mul_eq_add, ←
        rpow_sub' A, add_sub_cancel_right, le_refl, true_and, ← mul_div_assoc, B]

Premises used: div_le_iff₀, le_refl, div_mul_cancel₀, mul_div_assoc, NNReal.rpow_sub', Real.HolderTriple.ne_zero, Real.HolderConjugate.symm, NNReal.rpow_mul, Set.mem_setOf_eq, Real.HolderConjugate.mul_eq_add, Finset.sum_div, add_sub_cancel_right, NNReal.div_rpow, NNReal.rpow_one, one_mul, true_and
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
h : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q) ≠ 0
⊢ (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q) = HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)

Tactic:
rw [div_eq_iff, ← rpow_add hf.ne', one_div, one_div, hpq.inv_add_inv_eq_one, rpow_one]

Premises used: NNReal.rpow_add, LT.lt.ne', Real.HolderConjugate.inv_add_inv_eq_one, div_eq_iff, one_div, NNReal.rpow_one
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / q) ≠ 0

Tactic:
simpa [hpq.symm.ne_zero] using hf.ne'

Premises used: Real.HolderTriple.ne_zero, Real.HolderConjugate.symm, LT.lt.ne'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
g : ι → ℝ≥0
hg : Membership.mem (γ := Set (ι → ℝ≥0)) {g : ι → ℝ≥0 | LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1} g
right :
  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) (1 / p)
⊢ (fun (g : ι → ℝ≥0) ↦ (∑ i ∈ s, f i * g i : ℝ≥0)) g ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)

Tactic:
apply le_trans (inner_le_Lp_mul_Lq s f g hpq)

Premises used: NNReal.inner_le_Lp_mul_Lq, le_trans