awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
have rw : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
Tactic: rw [h_rpow a, h_rpow b, one_div p, NNReal.le_rpow_inv_iff hp_pos, ← NNReal.rpow_mul, mul_comm,
    mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q : ℝ
a b : ℝ≥0
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0), a ^ q = (a ^ p) ^ (q / p)
h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
have rwa : ∀ (h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p),
  ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (p / q) ≤ a ^ p + b ^ p
Tactic: rwa [one_div_div] at h_rpow_add_rpow_le_add
Cleared hypotheses: h_rpow_add_rpow_le_add
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have inl : ∀ (hp : LE.le (α := ℝ) 0 0) (hp1 : LE.le (α := ℝ) 0 1),
  HPow.hPow (β := ℝ) (a + b) 0 ≤ HPow.hPow (β := ℝ) a 0 + HPow.hPow (β := ℝ) b 0
Tactic: rcases hp.eq_or_lt with (rfl | hp_pos)
Cleared hypotheses: p, hp, hp1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
inl :
  ∀ (hp : LE.le (α := ℝ) 0 0) (hp1 : LE.le (α := ℝ) 0 1),
    HPow.hPow (β := ℝ) (a + b) 0 ≤ HPow.hPow (β := ℝ) a 0 + HPow.hPow (β := ℝ) b 0
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have inr : ∀ (hp_pos : 0 < p), (a + b) ^ p ≤ a ^ p + b ^ p
Tactic: rcases hp.eq_or_lt with (rfl | hp_pos)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have h : (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
Tactic: have h := rpow_add_rpow_le a b hp_pos hp1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) ^ (1 / 1) ≤ (a ^ p + b ^ p) ^ (1 / p)
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have h₁ : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
Tactic: rw [one_div_one, one_div] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have h₁ : HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
Tactic: rw [NNReal.rpow_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have h₁ : a + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
Tactic: rw [NNReal.rpow_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : a + HPow.hPow (β := ℝ) b 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have h₁ : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
Tactic: rw [NNReal.rpow_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0
hp : 0 ≤ p
hp1 : p ≤ 1
hp_pos : 0 < p
h : HPow.hPow (β := ℝ) (HPow.hPow (β := ℝ) a 1 + HPow.hPow (β := ℝ) b 1) 1 ≤ (a ^ p + b ^ p) ^ p⁻¹
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have h₁ : a + b ≤ (a ^ p + b ^ p) ^ p⁻¹
Tactic: repeat' rw [NNReal.rpow_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have lift : ∀ (a : ℝ≥0), (↑a : ℝ) ^ p + b ^ p ≤ ((↑a : ℝ) + b) ^ p
Tactic: lift a to NNReal using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ (↑a : ℝ) ^ p + b ^ p ≤ ((↑a : ℝ) + b) ^ p
have lift : ∀ (b : ℝ≥0), (↑a : ℝ) ^ p + (↑b : ℝ) ^ p ≤ ((↑a : ℝ) + (↑b : ℝ)) ^ p
Tactic: lift b to NNReal using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
have lift : ∀ (a : ℝ≥0), ((↑a : ℝ) ^ p + b ^ p) ^ (1 / p) ≤ (↑a : ℝ) + b
Tactic: lift a to NNReal using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p b : ℝ
hb : 0 ≤ b
hp1 : 1 ≤ p
a : ℝ≥0
⊢ ((↑a : ℝ) ^ p + b ^ p) ^ (1 / p) ≤ (↑a : ℝ) + b
have lift : ∀ (b : ℝ≥0), ((↑a : ℝ) ^ p + (↑b : ℝ) ^ p) ^ (1 / p) ≤ (↑a : ℝ) + (↑b : ℝ)
Tactic: lift b to NNReal using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
have lift : ∀ (a : ℝ≥0), ((↑a : ℝ) ^ q + b ^ q) ^ (1 / q) ≤ ((↑a : ℝ) ^ p + b ^ p) ^ (1 / p)
Tactic: lift a to NNReal using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q b : ℝ
hb : 0 ≤ b
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0
⊢ ((↑a : ℝ) ^ q + b ^ q) ^ (1 / q) ≤ ((↑a : ℝ) ^ p + b ^ p) ^ (1 / p)
have lift : ∀ (b : ℝ≥0), ((↑a : ℝ) ^ q + (↑b : ℝ) ^ q) ^ (1 / q) ≤ ((↑a : ℝ) ^ p + (↑b : ℝ) ^ p) ^ (1 / p)
Tactic: lift b to NNReal using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
⊢ (a + b) ^ p ≤ a ^ p + b ^ p
have lift : ∀ (a : ℝ≥0), ((↑a : ℝ) + b) ^ p ≤ (↑a : ℝ) ^ p + b ^ p
Tactic: lift a to NNReal using ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p b : ℝ
hb : 0 ≤ b
hp : 0 ≤ p
hp1 : p ≤ 1
a : ℝ≥0
⊢ ((↑a : ℝ) + b) ^ p ≤ (↑a : ℝ) ^ p + b ^ p
have lift : ∀ (b : ℝ≥0), ((↑a : ℝ) + (↑b : ℝ)) ^ p ≤ (↑a : ℝ) ^ p + (↑b : ℝ) ^ p
Tactic: lift b to NNReal using hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := by positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
have hp_nonneg : 0 ≤ p
Tactic: have hp_nonneg : 0 ≤ p := by positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
have hp_not_neg : ¬p < 0
Tactic: have hp_not_neg : ¬p < 0 := by simp [hp_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
have h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
Tactic: have h_top_iff_rpow_top : ∀ (i : ι), i ∈ s → (w i * z i = ⊤ ↔ w i * z i ^ p = ⊤) := by
    simp [ENNReal.mul_eq_top, hp_pos, hp_not_neg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
have refine_1 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p = ∞ → Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
Tactic: refine le_of_top_imp_top_of_toNNReal_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
refine_1 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p = ∞ → Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≤ ∑ i ∈ s, w i * z i ^ p
have refine_2 : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞ →
  Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞ →
    (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)
Tactic: refine le_of_top_imp_top_of_toNNReal_le ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
⊢ HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p = ∞ → Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
have refine_1 : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) 0 ∧ p < 0 ∨ (∃ a ∈ s, w a * z a = ∞) ∧ 0 < p → ∃ a ∈ s, w a * z a ^ p = ∞
Tactic: rw [rpow_eq_top_iff, sum_eq_top, sum_eq_top]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h_1 : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) ∞
⊢ False
have h_top_rpow_sum₁ : Ne (α := ℝ≥0∞) ∞ ∞
Tactic: rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
Cleared hypotheses: h_top_rpow_sum, h_1, h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
⊢ (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)
have h_top : ∀ a ∈ s, w a * z a ≠ ∞
Tactic: have h_top : ∀ a : ι, a ∈ s → w a * z a ≠ ⊤ :=
      haveI h_top_sum : ∑ i ∈ s, w i * z i ≠ ⊤ := by
        intro h
        rw [h, top_rpow_of_pos hp_pos] at h_top_rpow_sum
        exact h_top_rpow_sum rfl
      fun a ha => (lt_top_of_sum_ne_top h_top_sum ha).ne
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
i : ι
hi : i ∈ s
⊢ w i * z i ^ p ≠ ∞
have h_top₁ : w i * z i ≠ ∞
Tactic: specialize h_top i hi
Cleared hypotheses: h_top
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ∞
⊢ w i * z i ^ p ≠ ∞
have rwa : ¬w i * z i ^ p = ∞
Tactic: rwa [Ne, ← h_top_iff_rpow_top i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
i : ι
hi : i ∈ s
h_top : w i * z i ≠ ∞
rwa : ¬w i * z i ^ p = ∞
⊢ w i * z i ^ p ≠ ∞
have rwa₁ : ¬w i * z i = ∞
Tactic: rwa [Ne, ← h_top_iff_rpow_top i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
⊢ (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)
have h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
Tactic: have h_top_rpow : ∀ a : ι, a ∈ s → w a * z a ^ p ≠ ⊤ := by
      intro i hi
      specialize h_top i hi
      rwa [Ne, ← h_top_iff_rpow_top i hi]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ (HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p).toNNReal ≤ ENNReal.toNNReal (∑ i ∈ s, w i * z i ^ p)
have refine_2 : HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (w x).toNNReal * (z x).toNNReal) p ≤ ∑ x ∈ s, (w x).toNNReal * (z x).toNNReal ^ p
Tactic: simp_rw [toNNReal_sum h_top_rpow, toNNReal_rpow, toNNReal_sum h_top, toNNReal_mul,
      toNNReal_rpow]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ HPow.hPow (α := ℝ≥0) (∑ x ∈ s, (w x).toNNReal * (z x).toNNReal) p ≤ ∑ x ∈ s, (w x).toNNReal * (z x).toNNReal ^ p
have refine_2 : Eq (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) 1
Tactic: refine
      NNReal.rpow_arith_mean_le_arith_mean_rpow s (fun i => (w i).toNNReal)
        (fun i => (z i).toNNReal) ?_ hp
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ ∑ i ∈ s, w i = (↑(∑ i ∈ s, (w i).toNNReal) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞))
Tactic: rw [coe_finsetSum]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) (∑ a ∈ s, (↑(w a).toNNReal : ℝ≥0∞))
have refine : ∀ (i : ι) (hi : i ∈ s), w i ≠ ∞
Tactic: refine sum_congr rfl fun i hi => (coe_toNNReal ?_).symm
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
i : ι
hi : i ∈ s
⊢ w i ≠ ∞
have refine : Ne (α := ℝ≥0∞) (∑ x ∈ s, w x) ∞
Tactic: refine (lt_top_of_sum_ne_top ?_ hi).ne
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) 1
have h_sum_nnreal : ∑ i ∈ s, w i = (↑(∑ i ∈ s, (w i).toNNReal) : ℝ≥0∞)
Tactic: have h_sum_nnreal : ∑ i ∈ s, w i = ↑(∑ i ∈ s, (w i).toNNReal) := by
      rw [coe_finsetSum]
      refine sum_congr rfl fun i hi => (coe_toNNReal ?_).symm
      refine (lt_top_of_sum_ne_top ?_ hi).ne
      exact hw'.symm ▸ ENNReal.one_ne_top
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
h_sum_nnreal : ∑ i ∈ s, w i = (↑(∑ i ∈ s, (w i).toNNReal) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) 1
have refine_2 : (↑(∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) : ℝ≥0∞) = (↑1 : ℝ≥0∞)
Tactic: rwa [← coe_inj, ← h_sum_nnreal]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
ι : Type u
s : Finset ι
w z : ι → ℝ≥0∞
hw' : Eq (α := ℝ≥0∞) (∑ i ∈ s, w i) 1
p : ℝ
hp : 1 ≤ p
hp_pos : 0 < p
hp_nonneg : 0 ≤ p
hp_not_neg : ¬p < 0
h_top_iff_rpow_top : ∀ i ∈ s, w i * z i = ∞ ↔ w i * z i ^ p = ∞
h_top_rpow_sum : HPow.hPow (α := ℝ≥0∞) (∑ i ∈ s, w i * z i) p ≠ ∞
h : Ne (α := ℝ≥0∞) (∑ i ∈ s, w i * z i ^ p) ∞
h_top : ∀ a ∈ s, w a * z a ≠ ∞
h_top_rpow : ∀ a ∈ s, w a * z a ^ p ≠ ∞
h_sum_nnreal : ∑ i ∈ s, w i = (↑(∑ i ∈ s, (w i).toNNReal) : ℝ≥0∞)
refine_2 : (↑(∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) : ℝ≥0∞) = (↑1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, (fun (i : ι) ↦ (w i).toNNReal) i) 1
have refine_2₁ : ∑ i ∈ s, w i = (↑1 : ℝ≥0∞)
Tactic: rwa [← coe_inj, ← h_sum_nnreal]
-- 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 h : (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
Tactic: convert!
    rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (ENNReal.add_halves 1) hp
      using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
h : (z₁ + z₂) ^ p = (1 / 2 * (2 * z₁) + 1 / 2 * (2 * z₂)) ^ p
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
have h₁ : HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
Tactic: convert!
    rpow_arith_mean_le_arith_mean2_rpow (1 / 2) (1 / 2) (2 * z₁) (2 * z₂) (ENNReal.add_halves 1) hp
      using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 1 ≤ p
⊢ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p) = 1 / 2 * (2 * z₁) ^ p + 1 / 2 * (2 * z₂) ^ p
have h : 2⁻¹ * HPow.hPow (α := ℝ≥0∞) 2 p * (z₁ ^ p + z₂ ^ p) =
  2⁻¹ * (HPow.hPow (α := ℝ≥0∞) 2 p * z₁ ^ p) + 2⁻¹ * (HPow.hPow (α := ℝ≥0∞) 2 p * z₂ ^ p)
Tactic: simp only [mul_rpow_of_nonneg _ _ (zero_le_one.trans hp), rpow_sub _ _ two_ne_zero ofNat_ne_top,
      ENNReal.div_eq_inv_mul, rpow_one, mul_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have hp_pos : 0 < p
Tactic: have hp_pos : 0 < p := by positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have pos : ∀ (h_top : a + b = ∞), a ^ p + b ^ p ≤ (a + b) ^ p
Tactic: by_cases h_top : a + b = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
pos : ∀ (h_top : a + b = ∞), a ^ p + b ^ p ≤ (a + b) ^ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have neg : ∀ (h_top : ¬a + b = ∞), a ^ p + b ^ p ≤ (a + b) ^ p
Tactic: by_cases h_top : a + b = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : a + b = ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have h_top₁ : (a + b) ^ p = ∞
Tactic: rw [← @ENNReal.rpow_eq_top_iff_of_pos (a + b) p hp_pos] at h_top
Cleared hypotheses: h_top
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : (a + b) ^ p = ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have pos : a ^ p + b ^ p ≤ ∞
Tactic: rw [h_top]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have ha_top : a ≠ ∞
Tactic: obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
ha_top : a ≠ ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have hb_top : b ≠ ∞
Tactic: obtain ⟨ha_top, hb_top⟩ := add_ne_top.mp h_top
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
h_top : ¬a + b = ∞
ha_top : a ≠ ∞
hb_top : b ≠ ∞
⊢ a ^ p + b ^ p ≤ (a + b) ^ p
have neg : ∀ (a : ℝ≥0) (h_top : ¬(↑a : ℝ≥0∞) + b = ∞), (↑a : ℝ≥0∞) ^ p + b ^ p ≤ ((↑a : ℝ≥0∞) + b) ^ p
Tactic: lift a to ℝ≥0 using ha_top
Cleared hypotheses: a, h_top, ha_top