awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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₀ : 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 * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have 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∞)
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)
-- 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₀ : 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 * f i ≤
    HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) * HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * f i ^ p) p⁻¹
have 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∞)
Tactic: rw [coe_mul] at this
Cleared hypotheses: this
-- 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₀ : 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∞)
⊢ ∑ 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 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⁻¹
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
Cleared hypotheses: this
-- 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₀ : 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⁻¹
⊢ ∑ 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 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⁻¹
Tactic: simp only [toNNReal_mul, coe_mul, sub_nonneg, hp₁.le, coe_rpow_of_nonneg, coe_finsetSum] at this
Cleared hypotheses: this
-- 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
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 ∈ 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 h : ∀ (i : ι) (hi : i ∈ s), w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
Tactic: convert! this using 2 with i hi
-- 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
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∞)
⊢ ∑ 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 h₁ : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i) (1 - p⁻¹) = HPow.hPow (α := ℝ≥0∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹)
Tactic: convert! this using 2 with i hi
-- 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
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 * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
have h : ∀ (hw : w i = 0), w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
Tactic: obtain hw | hw := eq_or_ne (w i) 0
-- 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
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∞)
⊢ w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
have h₁ : ∀ (hw : w i ≠ 0), w i * f i = (↑(w i).toNNReal : ℝ≥0∞) * (↑(f i).toNNReal : ℝ≥0∞)
Tactic: obtain hw | hw := eq_or_ne (w i) 0
-- 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
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∞)
have h : f i ≠ ∞
Tactic: rw [coe_toNNReal (H'.1 _ hi), coe_toNNReal]
-- 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
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∞) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞)) (1 - p⁻¹)
have h : ∀ (i : ι) (hi : i ∈ s), (↑(w i).toNNReal : ℝ≥0∞) = w i
Tactic: convert! rfl with i hi
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (p - 1) * ∑ i ∈ s, f i ^ p
have inl : ∀ (hp : 1 = 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (p - 1) * ∑ i ∈ s, f i ^ p
have inr : ∀ (hp : 1 < 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
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (p - 1) * ∑ i ∈ s, f i ^ p
have hpq : p.HolderConjugate q
Tactic: have hpq : p.HolderConjugate q := .conjExponent hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f : ι → ℝ≥0∞
p : ℝ
hp_1 : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : p.HolderConjugate q
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (p - 1) * ∑ i ∈ s, f i ^ p
have hp₁ : 1 / p * p = 1
Tactic: have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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
have rw : 1 / q * p = p / q
Tactic: rw [← hpq.div_conj_eq_sub_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, f i) p ≤ HPow.hPow (α := ℝ≥0∞) (↑(#s) : ℝ≥0∞) (p - 1) * ∑ i ∈ s, f i ^ p
have hq : 1 / q * p = p - 1
Tactic: have hq : 1 / q * p = p - 1 := by
    rw [← hpq.div_conj_eq_sub_one]
    ring
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p : ℝ
hp : 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)
have 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)
Tactic: by_cases H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ 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)
have 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)
Tactic: by_cases H' : (∑ i ∈ s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i ∈ s, g i ^ p) ^ (1 / p) = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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) = ∞
⊢ 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)
have 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)
Tactic: rcases H' with H' | H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
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)
⊢ 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)
have 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)
Tactic: rcases H' with H' | H'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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) = ∞)
⊢ 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)
have pos : 0 < p
Tactic: have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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
⊢ 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)
have H'₁ : (∀ 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'
Cleared hypotheses: H'
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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, (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)
have 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∞)
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)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
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∞) (∑ 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)
have 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)
Tactic: push_cast [ENNReal.coe_rpow_of_nonneg, le_of_lt pos, le_of_lt (one_div_pos.2 pos)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
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
⊢ ∑ i ∈ s, w i * z i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)
have this : 0 < p
Tactic: have : 0 < p := by positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ ∑ i ∈ s, w i * z i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)
have rw : HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
Tactic: rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ ∑ i ∈ s, w i * z i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)
have hx : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i ^ p)
Tactic: rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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)
⊢ ∑ i ∈ s, w i * z i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)
have rw₁ : LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)
Tactic: rw [← rpow_le_rpow_iff _ _ this, ← rpow_mul, one_div_mul_cancel (ne_of_gt this), rpow_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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)
⊢ ∑ i ∈ s, w i * z i ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)
have rw₂ : 0 ≤ 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]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i ^ p)
have hx : ∀ i ∈ s, 0 ≤ w i * z i ^ p
Tactic: apply_rules [sum_nonneg, rpow_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i ^ p
have hx : 0 ≤ w i → 0 ≤ w i * z i ^ p
Tactic: positivity [hw i hi, hz i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
i : ι
hi : i ∈ s
hx hx₁ hx₂ : 0 ≤ w i → 0 ≤ w i * z i ^ p
⊢ 0 ≤ w i * z i ^ p
have hx₃ : 0 ≤ w i → 0 ≤ z i → 0 ≤ w i * z i ^ p
Tactic: positivity [hw i hi, hz i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ LE.le (α := ℝ) 0 (∑ i ∈ s, w i * z i)
have apply_rules : ∀ i ∈ s, 0 ≤ w i * z i
Tactic: apply_rules [sum_nonneg, rpow_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
i : ι
hi : i ∈ s
⊢ 0 ≤ w i * z i
have positivity : 0 ≤ w i → 0 ≤ w i * z i
Tactic: positivity [hw i hi, hz i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
i : ι
hi : i ∈ s
positivity positivity₁ positivity₂ : 0 ≤ w i → 0 ≤ w i * z i
⊢ 0 ≤ w i * z i
have positivity₃ : 0 ≤ w i → 0 ≤ z i → 0 ≤ w i * z i
Tactic: positivity [hw i hi, hz i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
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
⊢ 0 ≤ HPow.hPow (α := ℝ) (∑ i ∈ s, w i * z i ^ p) (1 / p)
have hx : ∀ i ∈ s, 0 ≤ w i * z i ^ p
Tactic: apply_rules [sum_nonneg, rpow_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
have refine_2 : ∀
  (h :
    HPow.hPow (α := ℝ≥0) (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) p ≤
      ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p),
  (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
Tactic: have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
w₁ w₂ z₁ z₂ : ℝ≥0
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
refine_2 :
  ∀
    (h :
      HPow.hPow (α := ℝ≥0) (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) p ≤
        ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p),
    (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p
have refine_1 : Eq (α := ℝ≥0) (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i) 1
Tactic: have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
have inl : ∀ (hp : LE.le (α := ℝ) 1 1),
  HPow.hPow (β := ℝ) (z₁ + z₂) 1 ≤
    HPow.hPow (α := ℝ≥0) 2 (HSub.hSub (α := ℝ) 1 1) * (HPow.hPow (β := ℝ) z₁ 1 + HPow.hPow (β := ℝ) z₂ 1)
Tactic: rcases eq_or_lt_of_le hp with (rfl | h'p)
Cleared hypotheses: p, hp