awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
b : ℝ≥0∞
hp1 : 1 ≤ p
hp_pos : 0 < p
hb_top : b ≠ ∞
a : ℝ≥0
h_top : ¬(↑a : ℝ≥0∞) + b = ∞
⊢ (↑a : ℝ≥0∞) ^ p + b ^ p ≤ ((↑a : ℝ≥0∞) + b) ^ p
have neg : ∀ (b : ℝ≥0) (h_top : ¬(↑a : ℝ≥0∞) + (↑b : ℝ≥0∞) = ∞),
  (↑a : ℝ≥0∞) ^ p + (↑b : ℝ≥0∞) ^ p ≤ ((↑a : ℝ≥0∞) + (↑b : ℝ≥0∞)) ^ p
Tactic: lift b to ℝ≥0 using hb_top
Cleared hypotheses: b, hb_top, h_top
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
have rw : a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹
Tactic: rw [one_div, ← @ENNReal.le_rpow_inv_iff _ _ p⁻¹ (by simp [lt_of_lt_of_le zero_lt_one hp1])]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ
a b : ℝ≥0∞
hp1 : 1 ≤ p
⊢ a ^ p + b ^ p ≤ (a + b) ^ p⁻¹⁻¹
have rw : a ^ p + b ^ p ≤ (a + b) ^ p
Tactic: rw [inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q : ℝ
a_1 b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
⊢ a ^ q = (a ^ p) ^ (q / p)
have rw : a ^ q = a ^ (p * (q / p))
Tactic: rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p q : ℝ
a_1 b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
a : ℝ≥0∞
rw : a ^ q = a ^ (p * (q / p))
⊢ a ^ q = (a ^ p) ^ (q / p)
have rw₁ : a ^ q = a ^ q
Tactic: rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
have h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
Tactic: have h_rpow : ∀ a : ℝ≥0∞, a ^ q = (a ^ p) ^ (q / p) := fun a => by
    rw [← ENNReal.rpow_mul, mul_div_cancel₀ _ hp_pos.ne']
-- 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)
⊢ ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
have refine : 1 ≤ q / p
Tactic: refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
p q : ℝ
a b : ℝ≥0∞
hp_pos : 0 < p
hpq : p ≤ q
h_rpow : ∀ (a : ℝ≥0∞), a ^ q = (a ^ p) ^ (q / p)
⊢ (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
have h_rpow_add_rpow_le_add : ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p
Tactic: have h_rpow_add_rpow_le_add :
    ((a ^ p) ^ (q / p) + (b ^ p) ^ (q / p)) ^ (1 / (q / p)) ≤ a ^ p + b ^ p := by
    refine rpow_add_rpow_le_add (a ^ p) (b ^ p) ?_
    rwa [one_le_div hp_pos]
-- 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, ENNReal.le_rpow_inv_iff hp_pos, ← ENNReal.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 [ENNReal.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 [ENNReal.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 [ENNReal.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 [ENNReal.rpow_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ≥0∞
hp : 1 ≤ p
⊢ p.LpAddConst = 1
have hnc : p ∉ Set.Ioo 0 1
Tactic: rw [LpAddConst, if_neg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
⊢ LpAddConst 0 = 1
have hnc : 0 ∉ Set.Ioo 0 1
Tactic: rw [LpAddConst, if_neg]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ≥0∞
⊢ (if Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p then HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) else 1) < ∞
have pos : ∀ (h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p), HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) < ∞
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ≥0∞
pos : ∀ (h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p), HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) < ∞
⊢ (if Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p then HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) else 1) < ∞
have neg : ∀ (h : p ∉ Set.Ioo 0 1), LT.lt (α := ℝ≥0∞) 1 ∞
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
⊢ HPow.hPow (α := ℝ≥0∞) 2 (1 / p.toReal - 1) < ∞
have apply : 0 ≤ 1 / p.toReal - 1
Tactic: apply ENNReal.rpow_lt_top_of_nonneg _ ENNReal.ofNat_ne_top
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
p : ℝ≥0∞
h : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) p
⊢ 0 ≤ 1 / p.toReal - 1
have rw : ENNReal.toReal 1 ≤ p⁻¹.toReal
Tactic: rw [one_div, sub_nonneg, ← ENNReal.toReal_inv, ← ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
have pos : ∀ (h : 1 < p), (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
Tactic: by_cases h : 1 < p
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
pos : ∀ (h : 1 < p), (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
have neg : ∀ (h : ¬1 < p), (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
Tactic: by_cases h : 1 < p
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
have left : 0 < (ENNReal.ofReal p)⁻¹
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
left : 0 < (ENNReal.ofReal p)⁻¹
⊢ Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
have right : (ENNReal.ofReal p)⁻¹ < 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (ENNReal.ofReal p)⁻¹ < 1
have right : 1 < ENNReal.ofReal p
Tactic: rwa [ENNReal.inv_lt_one, one_lt_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
have hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
Tactic: have hmem : (ENNReal.ofReal p)⁻¹ ∈ Set.Ioo (0 : ℝ≥0∞) 1 := by
      constructor
      · simp
      · rwa [ENNReal.inv_lt_one, one_lt_ofReal]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
⊢ (ENNReal.ofReal p)⁻¹.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
have rw : (if Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹ then
    HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
  else 1) =
  HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
Tactic: rw [LpAddConst, if_pos hmem]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
rw :
  (if Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹ then
      HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
    else 1) =
    HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
⊢ (ENNReal.ofReal p)⁻¹.LpAddConst = HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
have rw₁ : HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) =
  HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1)
Tactic: rw [LpAddConst, if_pos hmem]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
have pos : (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) * (z₁ ^ p + z₂ ^ p)
Tactic: rw [show LpAddConst (ENNReal.ofReal p)⁻¹ =
        (2 : ℝ≥0∞) ^ (1 / ((ENNReal.ofReal p)⁻¹).toReal - 1) from by
      rw [LpAddConst, if_pos hmem]]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (1 / (ENNReal.ofReal p)⁻¹.toReal - 1) * (z₁ ^ p + z₂ ^ p)
have pos : (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 ((ENNReal.ofReal p).toReal - 1) * (z₁ ^ p + z₂ ^ p)
Tactic: simp only [ENNReal.toReal_inv, div_inv_eq_mul, one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : 1 < p
hmem : Membership.mem (γ := Set ℝ≥0∞) (Set.Ioo 0 1) (ENNReal.ofReal p)⁻¹
⊢ (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 ((ENNReal.ofReal p).toReal - 1) * (z₁ ^ p + z₂ ^ p)
have pos : (z₁ + z₂) ^ p ≤ HPow.hPow (α := ℝ≥0∞) 2 (p - 1) * (z₁ ^ p + z₂ ^ p)
Tactic: rw [ENNReal.toReal_ofReal hp]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (hypothesis)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
have hp1 : p ≤ 1
Tactic: have hp1 : p ≤ 1 := not_lt.mp h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ : ℝ≥0∞
p : ℝ
hp : 0 ≤ p
h : ¬1 < p
hp1 : p ≤ 1
⊢ (z₁ + z₂) ^ p ≤ (ENNReal.ofReal p)⁻¹.LpAddConst * (z₁ ^ p + z₂ ^ p)
have neg : (z₁ + z₂) ^ p ≤ z₁ ^ p + z₂ ^ p
Tactic: rw [LpAddConst_of_one_le (ENNReal.one_le_inv.mpr (ENNReal.ofReal_le_one.mpr hp1)), one_mul]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ p : ℝ≥0∞
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
have pos : ∀ (p_zero : p = 0), (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ p : ℝ≥0∞
pos : ∀ (p_zero : p = 0), (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
have neg : ∀ (p_zero : ¬p = 0), (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
Tactic: by_cases p_zero : p = 0
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
⊢ (z₁ + z₂) ^ p.toReal⁻¹ ≤ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
have h : p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹) =
  (ENNReal.ofReal p.toReal⁻¹)⁻¹.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
Tactic: convert! rpow_add_le_mul_rpow_add_rpow' z₁ z₂ (p := p.toReal⁻¹) (by positivity) using 1
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
⊢ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹) =
    (ENNReal.ofReal p.toReal⁻¹)⁻¹.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
have h : p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) =
  (ENNReal.ofReal p⁻¹.toReal)⁻¹.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
Tactic: rw [← ENNReal.toReal_inv, ENNReal.ofReal_toReal (by simpa), inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
h :
  p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) =
    (ENNReal.ofReal p⁻¹.toReal)⁻¹.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
⊢ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹) =
    (ENNReal.ofReal p.toReal⁻¹)⁻¹.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
have h₁ : p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) = p⁻¹⁻¹.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
Tactic: rw [← ENNReal.toReal_inv, ENNReal.ofReal_toReal (by simpa), inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalitiesPow (goal)
Goal:
z₁ z₂ p : ℝ≥0∞
p_zero : ¬p = 0
h :
  p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) =
    (ENNReal.ofReal p⁻¹.toReal)⁻¹.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
h₁ : p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) = p⁻¹⁻¹.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
⊢ p.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹) =
    (ENNReal.ofReal p.toReal⁻¹)⁻¹.LpAddConst * (z₁ ^ p.toReal⁻¹ + z₂ ^ p.toReal⁻¹)
have h₂ : p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal) = p.LpAddConst * (z₁ ^ p⁻¹.toReal + z₂ ^ p⁻¹.toReal)
Tactic: rw [← ENNReal.toReal_inv, ENNReal.ofReal_toReal (by simpa), inv_inv]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
⊢ rexp ∘ Neg.neg '' univ = Ioi 0
have rw : rexp '' Neg.neg '' univ = Ioi 0
Tactic: rw [Set.image_comp, Set.image_univ_of_surjective neg_surjective, Set.image_univ, Real.range_exp]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
rw : rexp '' Neg.neg '' univ = Ioi 0
⊢ rexp ∘ Neg.neg '' univ = Ioi 0
have rw₁ : rexp '' univ = Ioi 0
Tactic: rw [Set.image_comp, Set.image_univ_of_surjective neg_surjective, Set.image_univ, Real.range_exp]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
rw : rexp '' Neg.neg '' univ = Ioi 0
rw₁ : rexp '' univ = Ioi 0
⊢ rexp ∘ Neg.neg '' univ = Ioi 0
have rw₂ : range rexp = Ioi 0
Tactic: rw [Set.image_comp, Set.image_univ_of_surjective neg_surjective, Set.image_univ, Real.range_exp]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
rw : rexp '' Neg.neg '' univ = Ioi 0
rw₁ : rexp '' univ = Ioi 0
rw₂ : range rexp = Ioi 0
⊢ rexp ∘ Neg.neg '' univ = Ioi 0
have rw₃ : Eq (α := Set ℝ) (Ioi 0) (Ioi 0)
Tactic: rw [Set.image_comp, Set.image_univ_of_surjective neg_surjective, Set.image_univ, Real.range_exp]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ rexp (-x) • cexp (-(↑x : ℂ)) ^ (s - 1) • f = cexp (-s * (↑x : ℂ)) • f
have change : (↑(rexp (-x)) : ℂ) • cexp (-(↑x : ℂ)) ^ (s - 1) • f = cexp (-s * (↑x : ℂ)) • f
Tactic: change (rexp (-x) : ℂ) • _ = _ • f
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (↑(rexp (-x)) : ℂ) • cexp (-(↑x : ℂ)) ^ (s - 1) • f = cexp (-s * (↑x : ℂ)) • f
have rw : ((↑(rexp (-x)) : ℂ) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
Tactic: rw [← smul_assoc, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ ((↑(rexp (-x)) : ℂ) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
have push_cast : (cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
| cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)
have lhs : cexp (-(↑x : ℂ))
Tactic: lhs
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
| cexp (-(↑x : ℂ))
have rw : HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1
Tactic: rw [← cpow_one (cexp _)]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
| cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)
have rw : HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1
Tactic: lhs; rw [← cpow_one (cexp _)]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (cexp (-(↑x : ℂ)) * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
have conv : (HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1 * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
Tactic: conv in cexp _ * _ => lhs; rw [← cpow_one (cexp _)]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
x : ℝ
s : ℂ
f : E
⊢ (HPow.hPow (β := ℂ) (cexp (-(↑x : ℂ))) 1 * cexp (-(↑x : ℂ)) ^ (s - 1)) • f = cexp (-s * (↑x : ℂ)) • f
have rw : cexp (-(↑x : ℂ) * (1 + (s - 1))) • f = cexp (-s * (↑x : ℂ)) • f
Tactic: rw [← cpow_add _ _ (Complex.exp_ne_zero _), cpow_def_of_ne_zero (Complex.exp_ne_zero _),
    Complex.log_exp (by simp [pi_pos]) (by simpa using pi_nonneg)]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ mellin f s =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u))
have rw : Eq.{u_1 + 1} (α := E)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume univ) fun (x : ℝ) ↦
    |(-rexp (-x))| • (↑((rexp ∘ Neg.neg) x) : ℂ) ^ (s - 1) • f ((rexp ∘ Neg.neg) x))
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u)))
Tactic: rw [mellin, ← rexp_neg_image_aux, integral_image_eq_integral_abs_deriv_smul
        MeasurableSet.univ rexp_neg_deriv_aux rexp_neg_injOn_aux]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ Eq.{u_1 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u)))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (u : ℝ) ↦
      cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u)))
have e_f : Eq.{u_1 + 1} (α := ℝ → E) (fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u))) fun (u : ℝ) ↦
  cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
⊢ Eq.{u_1 + 1} (α := ℝ → E) (fun (u : ℝ) ↦ cexp (-s * (↑u : ℂ)) • f (rexp (-u))) fun (u : ℝ) ↦
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have e_f : ∀ (u : ℝ),
  cexp (-s * (↑u : ℂ)) • f (rexp (-u)) =
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: ext u
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
⊢ cexp (-s * (↑u : ℂ)) • f (rexp (-u)) =
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have trans : cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: trans Complex.exp (-s.im * u * I) • (Real.exp (-s.re * u) • f (Real.exp (-u)))
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
trans : cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
⊢ cexp (-s * (↑u : ℂ)) • f (rexp (-u)) =
    cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have trans₁ : cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u)) =
  cexp ((↑(-2 * π * (u * (s.im / (2 * π)))) : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
Tactic: trans Complex.exp (-s.im * u * I) • (Real.exp (-s.re * u) • f (Real.exp (-u)))
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
| cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have lhs : cexp (-s * (↑u : ℂ)) • f (rexp (-u))
Tactic: lhs
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
| cexp (-s * (↑u : ℂ)) • f (rexp (-u))
have rw : cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑u : ℂ)) • f (rexp (-u))
Tactic: rw [← re_add_im s]
-- Lean 4 proof step from Mathlib.Analysis.MellinInversion (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℝ → E
s : ℂ
u : ℝ
| cexp (-s * (↑u : ℂ)) • f (rexp (-u)) = cexp (-(↑s.im : ℂ) * (↑u : ℂ) * I) • rexp (-s.re * u) • f (rexp (-u))
have rw : cexp (-((↑s.re : ℂ) + (↑s.im : ℂ) * I) * (↑u : ℂ)) • f (rexp (-u))
Tactic: lhs; rw [← re_add_im s]