awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
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)
this : LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1
⊢ (∑ i ∈ s, f i * g i) /
      (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ≤
    1

Tactic:
simp_rw [f', g', div_mul_div_comm, ← sum_div] at this

Premises used: div_mul_div_comm, Finset.sum_div
-- Module: Mathlib.Analysis.MeanInequalities
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)
this :
  (∑ i ∈ s, f i * g i) /
      (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ≤
    1
rwa : 0 < HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
rwa [div_le_iff₀, one_mul] at this

Premises used: div_le_iff₀, one_mul
-- Module: Mathlib.Analysis.MeanInequalities
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)
this :
  (∑ i ∈ s, f i * g i) /
      (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ≤
    1
⊢ 0 < HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalities
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 : LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
suffices (∑ i ∈ s, f' i * g' i) ≤ 1 by
    simp_rw [f', g', div_mul_div_comm, ← sum_div] at this
    rwa [div_le_iff₀, one_mul] at this
    positivity
-- Module: Mathlib.Analysis.MeanInequalities
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)
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1

Tactic:
inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq ?_) (le_of_eq ?_)

Premises used: _private.0.NNReal.inner_le_Lp_mul_Lp_of_norm_le_one, le_of_eq
-- Module: Mathlib.Analysis.MeanInequalities
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) (∑ i ∈ s, f' i ^ p) 1
inr₁ : Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1

Tactic:
refine inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq ?_) (le_of_eq ?_)

Premises used: _private.0.NNReal.inner_le_Lp_mul_Lp_of_norm_le_one, le_of_eq
-- Module: Mathlib.Analysis.MeanInequalities
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
inr₆ : HDiv.hDiv (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑ i ∈ s, f i ^ p) = 1
⊢ Eq (α := ℝ≥0) (∑ 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']

Premises used: Real.HolderTriple.ne_zero, NNReal.rpow_mul, LT.lt.ne', Finset.sum_div, one_div, NNReal.div_rpow, NNReal.rpow_one, inv_mul_cancel₀, div_self
-- Module: Mathlib.Analysis.MeanInequalities
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
inr₆ : HDiv.hDiv (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (∑ i ∈ s, g i ^ q) = 1
⊢ Eq (α := ℝ≥0) (∑ 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']

Premises used: Real.HolderTriple.ne_zero, Real.HolderConjugate.symm, NNReal.rpow_mul, LT.lt.ne', Finset.sum_div, one_div, NNReal.div_rpow, NNReal.rpow_one, inv_mul_cancel₀, div_self
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ ∑ i ∈ s, (f i * g i) ^ r ≤
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q)

Tactic:
simpa [mul_rpow, ← NNReal.rpow_mul, ← mul_div_assoc, hpqr.pos'.ne', fieldEq] using
    inner_le_Lp_mul_Lq s (fun i ↦ f i ^ r) (fun i ↦ g i ^ r) hpqr.holderConjugate_div_div

Premises used: Real.HolderTriple.holderConjugate_div_div, mul_div_assoc, NNReal.rpow_mul, LT.lt.ne', HPow.hPow, Real.HolderTriple.pos', fieldEq, NNReal.mul_rpow, NNReal.inner_le_Lp_mul_Lq
-- Module: Mathlib.Analysis.MeanInequalities
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) (r / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q)) ^ (1 / r)

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

Premises used: Iff.mpr, Eq.rec, inv_pos, inv_eq_one_div, Real.HolderTriple.pos', NNReal.Lr_rpow_le_Lp_mul_Lq, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
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)
⊢ 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)

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

Premises used: Iff.mpr, Eq.rec, inv_pos, inv_eq_one_div, Real.HolderTriple.pos', NNReal.Lr_rpow_le_Lp_mul_Lq, NNReal.rpow_le_rpow_iff
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
⊢ r ≠ 0

Tactic:
have hr := hpqr.pos'.ne'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q r : ℝ
hpqr : p.HolderTriple q r
hr : r ≠ 0
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))
⊢ 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:
simp only [← rpow_mul, mul_rpow]

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

Tactic:
field_simp
-- Module: Mathlib.Analysis.MeanInequalities
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⁻¹
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⁻¹
⊢ ∑ 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

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
w f : ι → ℝ≥0
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:
simp
-- Module: Mathlib.Analysis.MeanInequalities
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))

Tactic:
?_
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ p⁻¹ + (1 - p⁻¹)⁻¹⁻¹ = 1

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
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⁻¹

Tactic:
?_
-- Module: Mathlib.Analysis.MeanInequalities
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))
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⁻¹
⊢ ∑ 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:
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⟩)
    _ = _ := ?_

Premises used: Iff.mpr, HMul.hMul, HSub.hSub, Real.HolderConjugate.symm, HDiv.hDiv, Inv.inv, HPow.hPow, Real.holderConjugate_iff, And.intro, OfNat.ofNat, Finset.sum, NNReal.inner_le_Lp_mul_Lq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
inr : ∀ (i : ι), (↑(w i * f i) : ℝ) = (↑(w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)) : ℝ)
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, w i * f i) (∑ i ∈ s, w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i))

Tactic:
congr with i
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
i : ι
inr : 1 - p⁻¹ + p⁻¹ = 1
⊢ (↑(w i * f i) : ℝ) = (↑(w i ^ (1 - p⁻¹) * (w i ^ p⁻¹ * f i)) : ℝ)

Tactic:
rw [← mul_assoc, ← rpow_of_add_eq _ one_ne_zero, rpow_one]

Premises used: mul_assoc, one_ne_zero, NNReal.rpow_one, NNReal.rpow_of_add_eq
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
i : ι
⊢ 1 - p⁻¹ + p⁻¹ = 1

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ p ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
⊢ p ≠ 0

Tactic:
have hp₀ : p ≠ 0 := by positivity
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
hp₀ : p ≠ 0
⊢ 1 - p⁻¹ ≠ 0

Tactic:
simp [sub_eq_zero, hp.ne']

Premises used: sub_eq_zero, LT.lt.ne'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
hp₀ : p ≠ 0
⊢ 1 - p⁻¹ ≠ 0

Tactic:
have hp₁ : 1 - p⁻¹ ≠ 0 := by simp [sub_eq_zero, hp.ne']
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0
hp : 1 < p
hp₀ : p ≠ 0
hp₁ : 1 - 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⁻¹

Tactic:
simp [mul_rpow, div_inv_eq_mul, one_mul, one_div, hp₀, hp₁]

Premises used: one_div, div_inv_eq_mul, NNReal.mul_rpow, one_mul
-- 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
s : Finset ι
⊢ 0 < p

Tactic:
obtain ⟨hp, hq, hr⟩ := hpqr.all_pos

Premises used: Real.HolderTriple.all_pos
-- 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
s : Finset ι
hp : 0 < p
⊢ 0 < q

Tactic:
obtain ⟨hp, hq, hr⟩ := hpqr.all_pos

Premises used: Real.HolderTriple.all_pos
-- 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
s : Finset ι
hp : 0 < p
hq : 0 < q
⊢ 0 < r

Tactic:
obtain ⟨hp, hq, hr⟩ := hpqr.all_pos

Premises used: Real.HolderTriple.all_pos
-- 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
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)

Tactic:
le_trans (Lr_rpow_le_Lp_mul_Lq s f g hpqr) (mul_le_mul ?_ ?_ bot_le bot_le)

Premises used: mul_le_mul, NNReal.Lr_rpow_le_Lp_mul_Lq, bot_le, le_trans
-- 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
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)
refine_2 : HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / 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)

Tactic:
refine le_trans (Lr_rpow_le_Lp_mul_Lq s f g hpqr) (mul_le_mul ?_ ?_ bot_le bot_le)

Premises used: mul_le_mul, NNReal.Lr_rpow_le_Lp_mul_Lq, bot_le, le_trans
-- 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
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
refine_1 : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (r / p) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p)

Tactic:
gcongr
-- 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
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)

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

Premises used: zero_le, Summable.sum_le_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
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (∑' (i : ι), f i ^ p)

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

Premises used: zero_le, Summable.sum_le_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
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
refine_2 : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (∑' (i : ι), g i ^ q)
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (r / q) ≤ HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
gcongr
-- 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
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (∑' (i : ι), g i ^ q)

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

Premises used: zero_le, Summable.sum_le_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
s : Finset ι
hp : 0 < p
hq : 0 < q
hr : 0 < r
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (∑' (i : ι), g i ^ q)

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

Premises used: zero_le, Summable.sum_le_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
⊢ ∀ (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)
-- 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)
⊢ BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i * g i) ^ r)

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

Premises used: HMul.hMul, HDiv.hDiv, BddAbove, Set.Nonempty, HPow.hPow, tsum, Exists.intro, SummationFilter.unconditional
-- 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)
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))
⊢ BddAbove (α := ℝ≥0) (Set.range fun (s : Finset ι) ↦ ∑ i ∈ s, (f i * g i) ^ r)

Tactic:
refine ⟨(∑' i, f i ^ p) ^ (r / p) * (∑' i, g i ^ q) ^ (r / q), ?_⟩
-- 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)
s : Finset ι
⊢ (fun (s : Finset ι) ↦ (∑ i ∈ s, (f i * g i) ^ r : ℝ≥0)) s ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
H₁ s
-- 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)
s : Finset ι
⊢ (fun (s : Finset ι) ↦ (∑ i ∈ s, (f i * g i) ^ r : ℝ≥0)) s ≤
    HPow.hPow (α := ℝ≥0) (∑' (i : ι), f i ^ p) (r / p) * HPow.hPow (α := ℝ≥0) (∑' (i : ι), g i ^ q) (r / q)

Tactic:
exact H₁ s
-- 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)
⊢ 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
-- 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)
⊢ Summable (α := ℝ≥0) fun (i : ι) ↦ (f i * g i) ^ r

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