awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ = ∞)
⊢ (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞

Tactic:
replace H' : (∀ i ∈ s, w i ≠ ⊤) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ⊤ := by
    simpa [rpow_eq_top_iff, hp₀, hp₁, hp₀.not_gt, hp₁.not_gt, sum_eq_top, not_or] using H'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
⊢ (↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal) (1 - p⁻¹) *
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) p⁻¹) :
      ℝ≥0∞)

Tactic:
have := coe_le_coe.2 <| NNReal.inner_le_weight_mul_Lp s hp.le (fun i ↦ ENNReal.toNNReal (w i))
    fun i ↦ ENNReal.toNNReal (f i)
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  (↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal) (1 - p⁻¹) *
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) p⁻¹) :
      ℝ≥0∞)
⊢ (↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal) (1 - p⁻¹)) : ℝ≥0∞) *
      (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) p⁻¹) : ℝ≥0∞)

Tactic:
rw [coe_mul] at this

Premises used: ENNReal.coe_mul
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  (↑(∑ i ∈ s, (w i).toNNReal * (f i).toNNReal) : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal) (1 - p⁻¹)) : ℝ≥0∞) *
      (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal * (f i).toNNReal ^ p) p⁻¹) : ℝ≥0∞)
⊢ ∑ x ∈ s, (↑(w x * f x).toNNReal : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal) (1 - p⁻¹)) : ℝ≥0∞) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
simp_rw [coe_rpow_of_nonneg _ <| inv_nonneg.2 hp₀.le, coe_finsetSum, ← ENNReal.toNNReal_rpow,
    ← ENNReal.toNNReal_mul, sum_congr rfl fun i hi ↦ coe_toNNReal (H'.2 i hi)] at this

Premises used: ENNReal.coe_toNNReal, ENNReal.coe_finsetSum, Iff.mpr, ENNReal.coe_rpow_of_nonneg, LT.lt.le, ENNReal.toNNReal_rpow, inv_nonneg, And.right, ENNReal.toNNReal_mul, Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x * f x).toNNReal : ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, (w i).toNNReal) (1 - p⁻¹)) : ℝ≥0∞) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
simp only [toNNReal_mul, coe_mul, sub_nonneg, hp₁.le, coe_rpow_of_nonneg, coe_finsetSum] at this

Premises used: ENNReal.coe_finsetSum, ENNReal.coe_rpow_of_nonneg, LT.lt.le, ENNReal.coe_mul, ENNReal.toNNReal_mul, sub_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹

Tactic:
this
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
h : ∀ (i : ι) (hi : i ∈ s), w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
h₁ :
  HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (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:
convert! this using 2 with i hi
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
i : ι
hi : i ∈ s
h : ∀ (hw : w i = 0), w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
h₁ : ∀ (hw : w i ≠ 0), w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
⊢ w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)

Tactic:
obtain hw | hw := eq_or_ne (w i) 0

Premises used: eq_or_ne, OfNat.ofNat
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
i : ι
hi : i ∈ s
hw : w i = 0
⊢ w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)

Tactic:
simp [hw]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
i : ι
hi : i ∈ s
hw : w i ≠ 0
h : f i ≠ ∞
⊢ w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)

Tactic:
rw [coe_toNNReal (H'.1 _ hi), coe_toNNReal]

Premises used: ENNReal.coe_toNNReal, And.left
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
i : ι
hi : i ∈ s
hw : w i ≠ 0
⊢ f i ≠ ∞

Tactic:
simpa [mul_eq_top, hw, hp₀, hp₀.not_gt, H'.1 _ hi] using H'.2 _ hi

Premises used: ENNReal.mul_eq_top, And.right, And.left, LT.lt.not_gt
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
h : ∀ (i : ι) (hi : i ∈ s), (↑(w i).toNNReal : ℝ≥0∞) = w i
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹)

Tactic:
convert! rfl with i hi

Premises used: rfl
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
i : ι
hi : i ∈ s
⊢ (↑(w i).toNNReal : ℝ≥0∞) = w i

Tactic:
coe_toNNReal (H'.1 _ hi)

Premises used: ENNReal.coe_toNNReal, And.left
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
p : ℝ
hp_1 : 1 ≤ p
w f : ι → ℝ≥0∞
hp : 1 < p
hp₀ : 0 < p
hp₁ : p⁻¹ < 1
H : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) ≠ 0 ∧ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹ ≠ 0
H' : (∀ i ∈ s, w i ≠ ∞) ∧ ∀ i ∈ s, w i * f i ^ p ≠ ∞
this :
  ∑ x ∈ s, (↑(w x).toNNReal : ℝ≥0∞) * (↑(f x).toNNReal : ℝ≥0∞) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹) *
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
i : ι
hi : i ∈ s
⊢ (↑(w i).toNNReal : ℝ≥0∞) = w i

Tactic:
exact coe_toNNReal (H'.1 _ hi)

Premises used: ENNReal.coe_toNNReal, And.left
-- 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 [ENNReal.mul_rpow_of_nonneg _ _ hpq.nonneg, ← ENNReal.rpow_mul, hp₁, hq, coe_one,
    one_mul, one_rpow, rpow_one, Pi.one_apply, sum_const, Nat.smul_one_eq_cast] using
    ENNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg

Premises used: ENNReal.one_rpow, ENNReal.rpow_mul, ENNReal.mul_rpow_of_nonneg, Pi.one_apply, ENNReal.rpow_one, Real.HolderConjugate.symm, ENNReal.coe_one, ENNReal.rpow_le_rpow, Nat.smul_one_eq_cast, OfNat.ofNat, ENNReal.inner_le_Lp_mul_Lq, one_mul, Real.HolderTriple.nonneg, Finset.sum_const
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos :
  ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞),
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)
neg :
  ∀
    (H' :
      ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞)),
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)

Tactic:
by_cases H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ⊤

Premises used: HDiv.hDiv, HPow.hPow, OfNat.ofNat, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞
pos :
  ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞),
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)
pos₁ :
  ∀ (H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞),
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
      HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)

Tactic:
rcases H' with H' | H'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)

Tactic:
simp [H', -one_div]

Premises used: one_div
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)

Tactic:
simp [H', -one_div]

Premises used: one_div
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞)
⊢ 0 < p

Tactic:
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞)
pos : 0 < p
⊢ (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞

Tactic:
simpa [ENNReal.rpow_eq_top_iff, asymm pos, pos, ENNReal.sum_eq_top, not_or] using H'

Premises used: asymm, ENNReal.rpow_eq_top_iff, not_or, ENNReal.sum_eq_top
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
H' : ¬(HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) = ∞ ∨ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p) = ∞)
pos : 0 < p
⊢ (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞

Tactic:
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤ := by
    simpa [ENNReal.rpow_eq_top_iff, asymm pos, pos, ENNReal.sum_eq_top, not_or] using H'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
⊢ (↑(HPow.hPow (α := ℝ≥0)
          (∑ i ∈ s, HAdd.hAdd (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) ((fun (i : ι) ↦ (g i).toNNReal) i) ^ p)
          (1 / p)) :
      ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) p) (1 / p) +
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (g i).toNNReal) i) p) (1 / p)) :
      ℝ≥0∞)

Tactic:
have :=
    ENNReal.coe_le_coe.2
      (@NNReal.Lp_add_le _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _
        hp)
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  (↑(HPow.hPow (α := ℝ≥0)
          (∑ i ∈ s, HAdd.hAdd (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) ((fun (i : ι) ↦ (g i).toNNReal) i) ^ p)
          (1 / p)) :
      ℝ≥0∞) ≤
    (↑(HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (f i).toNNReal) i) p) (1 / p) +
          HPow.hPow (α := ℝ≥0) (∑ i ∈ s, HPow.hPow (α := ℝ≥0) ((fun (i : ι) ↦ (g i).toNNReal) i) p) (1 / p)) :
      ℝ≥0∞)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, ((↑(f x).toNNReal : ℝ≥0∞) + (↑(g x).toNNReal : ℝ≥0∞)) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) (1 / p) +
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ p) (1 / p)

Tactic:
push_cast [ENNReal.coe_rpow_of_nonneg, le_of_lt pos, le_of_lt (one_div_pos.2 pos)] at this

Premises used: Iff.mpr, le_of_lt, ENNReal.coe_rpow_of_nonneg, one_div_pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ i ∈ s, f i ≠ ∞) ∧ ∀ i ∈ s, g i ≠ ∞
this :
  HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, ((↑(f x).toNNReal : ℝ≥0∞) + (↑(g x).toNNReal : ℝ≥0∞)) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(f x).toNNReal : ℝ≥0∞) ^ p) (1 / p) +
      HPow.hPow (α := ℝ≥0∞) (∑ x ∈ s, (↑(g x).toNNReal : ℝ≥0∞) ^ p) (1 / p)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, (f i + g i) ^ p) (1 / p) ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i ^ p) (1 / p) + HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, g i ^ p) (1 / p)

Tactic:
simp_all
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
n : ℕ
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) n ≤ ∑ i ∈ s, w i * z i ^ n

Tactic:
(convexOn_pow n).map_sum_le hw hw' hz

Premises used: ConvexOn.map_sum_le, convexOn_pow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
n : ℕ
hn : Even n
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) n ≤ ∑ i ∈ s, w i * z i ^ n

Tactic:
hn.convexOn_pow.map_sum_le hw hw' fun _ _ => Set.mem_univ _

Premises used: ConvexOn.map_sum_le, Set.mem_univ, Even.convexOn_pow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 < z i
m : ℤ
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) m ≤ ∑ i ∈ s, w i * z i ^ m

Tactic:
(convexOn_zpow m).map_sum_le hw hw' hz

Premises used: ConvexOn.map_sum_le, convexOn_zpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
(convexOn_rpow hp).map_sum_le hw hw' hz

Premises used: ConvexOn.map_sum_le, convexOn_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ 0 < p

Tactic:
positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
⊢ 0 < p

Tactic:
have : 0 < p := by positivity
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
rw : HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
hx : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i ^ p)
rw₁ : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)
rw₂ : 0 ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)
⊢ ∑ i ∈ s, w i * z i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)

Tactic:
rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]

Premises used: ne_of_gt, Real.rpow_one, Real.rpow_le_rpow_iff, one_div_mul_cancel, Real.rpow_mul
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp

Premises used: Real.rpow_arith_mean_le_arith_mean_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
⊢ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p

Tactic:
exact rpow_arith_mean_le_arith_mean_rpow s w z hw hw' hz hp

Premises used: Real.rpow_arith_mean_le_arith_mean_rpow
-- Module: Mathlib.Analysis.MeanInequalitiesPow
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ i ∈ s, 0 ≤ w i
hw' : Eq (α := ℝ) (∑ i ∈ s, w i) 1
hz : ∀ i ∈ s, 0 ≤ z i
p : ℝ
hp : 1 ≤ p
this : 0 < p
hx : ∀ i ∈ s, 0 ≤ w i * z i ^ p
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i ^ p)

Tactic:
apply_rules [sum_nonneg, rpow_nonneg]

Premises used: Finset.sum_nonneg, Real.rpow_nonneg