awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : LE.le (α := ℝ) (∑ x ∈ s, w x / n / z x)⁻¹ (∏ x ∈ s, z x ^ (w x / n))
⊢ Eq (α := ℝ) (∏ i ∈ s, (z i ^ w i) ^ n⁻¹) (∏ x ∈ s, z x ^ (w x / n))
have h : ∀ (i : ι) (hi : i ∈ s), (z i ^ w i) ^ n⁻¹ = z i ^ (w i / n)
Tactic: refine Finset.prod_congr rfl (fun i hi => ?_)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : LE.le (α := ℝ) (∑ x ∈ s, w x / n / z x)⁻¹ (∏ x ∈ s, z x ^ (w x / n))
i : ι
hi : i ∈ s
⊢ (z i ^ w i) ^ n⁻¹ = z i ^ (w i / n)
have h : z i ^ (w i * n⁻¹) = z i ^ (w i / n)
Tactic: rw [← Real.rpow_mul (le_of_lt <| hz i hi) (w _) n⁻¹, div_eq_mul_inv (w _) n]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hz : ∀ i ∈ s, 0 < z i
n : ℝ := ∑ i ∈ s, w i
hw' : 0 < n
this : LE.le (α := ℝ) (∑ x ∈ s, w x / n / z x)⁻¹ (∏ x ∈ s, z x ^ (w x / n))
i : ι
hi : i ∈ s
h : z i ^ (w i * n⁻¹) = z i ^ (w i / n)
⊢ (z i ^ w i) ^ n⁻¹ = z i ^ (w i / n)
have h₁ : z i ^ (w i * n⁻¹) = z i ^ (w i * n⁻¹)
Tactic: rw [← Real.rpow_mul (le_of_lt <| hz i hi) (w _) n⁻¹, div_eq_mul_inv (w _) n]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u_1
s : Finset ι
hs : s.Nonempty
w z : ι → ℝ
hw : ∀ i ∈ s, 0 < w i
hw' : LT.lt (α := ℝ) 0 (∑ i ∈ s, w i)
hz : ∀ i ∈ s, 0 < z i
⊢ Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1
have refine_2 : HMul.hMul (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i)⁻¹ = 1
Tactic: simp_rw [div_eq_mul_inv (w _) (∑ i ∈ s, w i), ← Finset.sum_mul _ _ (∑ i ∈ s, w i)⁻¹]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
have pos : ∀ (h : a = ∞ ∨ b = ∞), a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
Tactic: by_cases! h : a = ⊤ ∨ b = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
pos : ∀ (h : a = ∞ ∨ b = ∞), a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
have neg : ∀ (h : a ≠ ∞ ∧ b ≠ ∞), a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
Tactic: by_cases! h : a = ⊤ ∨ b = ⊤
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
have pos : ∞ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
Tactic: refine le_trans le_top (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
⊢ ∞ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
have pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q / ENNReal.ofReal q
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q / ENNReal.ofReal q
have pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
Tactic: rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
⊢ ∞ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
have pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
Tactic: repeat rw [div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
have pos : ∀ (h : a = ∞), ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
pos : ∀ (h : a = ∞), ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
have pos₁ : ∀ (h : b = ∞), ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
Tactic: rcases h with h | h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
have pos : ∞ = HPow.hPow (α := ℝ≥0∞) ∞ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : b = ∞
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
have pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + HPow.hPow (α := ℝ≥0∞) ∞ q * (ENNReal.ofReal q)⁻¹
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
have neg : a.toNNReal * b.toNNReal ≤ a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal
Tactic: rw [← coe_toNNReal h.left, ← coe_toNNReal h.right, ← coe_mul, ← coe_rpow_of_nonneg _ hpq.nonneg,
    ← coe_rpow_of_nonneg _ hpq.symm.nonneg, ENNReal.ofReal, ENNReal.ofReal, ←
    @coe_div (Real.toNNReal p) _ (by simp [hpq.pos]), ←
    @coe_div (Real.toNNReal q) _ (by simp [hpq.symm.pos]), ← coe_add, coe_le_coe]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i * g i) 1
have hp : 0 < p.toNNReal
Tactic: have hp : 0 < p.toNNReal := zero_lt_one.trans hpq.toNNReal.lt
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i * g i) 1
have hq : 0 < q.toNNReal
Tactic: have hq : 0 < q.toNNReal := zero_lt_one.trans hpq.toNNReal.symm.lt
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
have rw : HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x ^ p / p.toNNReal) (∑ x ∈ s, g x ^ q / q.toNNReal) =
  (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
Tactic: rw [sum_add_distrib, sum_div, sum_div]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
rw :
  HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x ^ p / p.toNNReal) (∑ x ∈ s, g x ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
⊢ ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
have rw₁ : HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x ^ p / p.toNNReal) (∑ x ∈ s, g x ^ q / q.toNNReal) =
  ∑ i ∈ s, f i ^ p / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
Tactic: rw [sum_add_distrib, sum_div, sum_div]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
rw :
  HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x ^ p / p.toNNReal) (∑ x ∈ s, g x ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
rw₁ :
  HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x ^ p / p.toNNReal) (∑ x ∈ s, g x ^ q / q.toNNReal) =
    ∑ i ∈ s, f i ^ p / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
⊢ ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
have rw₂ : HAdd.hAdd (α := ℝ≥0) (∑ x ∈ s, f x ^ p / p.toNNReal) (∑ x ∈ s, g x ^ q / q.toNNReal) =
  HAdd.hAdd (α := ℝ≥0) (∑ i ∈ s, f i ^ p / p.toNNReal) (∑ i ∈ s, g i ^ q / q.toNNReal)
Tactic: rw [sum_add_distrib, sum_div, sum_div]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal ≤ 1 / p.toNNReal + 1 / q.toNNReal
have h₁ : 0 ≤ p.toNNReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
h₁ : 0 ≤ p.toNNReal
⊢ (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal ≤ 1 / p.toNNReal + 1 / q.toNNReal
have h₂ : 0 ≤ q.toNNReal
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 1 / p.toNNReal + 1 / q.toNNReal = 1
have simp_rw : p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1
Tactic: simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i * g i) 1
have i : ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
  (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
Tactic: calc
    ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) :=
      Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq
    _ = (∑ i ∈ s, f i ^ p) / Real.toNNReal p + (∑ i ∈ s, g i ^ q) / Real.toNNReal q := by
      rw [sum_add_distrib, sum_div, sum_div]
    _ ≤ 1 / Real.toNNReal p + 1 / Real.toNNReal q := by gcongr
    _ = 1 := by simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
i :
  ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i * g i) 1
have i₁ : (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal ≤ 1 / p.toNNReal + 1 / q.toNNReal
Tactic: calc
    ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) :=
      Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq
    _ = (∑ i ∈ s, f i ^ p) / Real.toNNReal p + (∑ i ∈ s, g i ^ q) / Real.toNNReal q := by
      rw [sum_add_distrib, sum_div, sum_div]
    _ ≤ 1 / Real.toNNReal p + 1 / Real.toNNReal q := by gcongr
    _ = 1 := by simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LE.le (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 1
hg : LE.le (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
i :
  ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal
i₁ : (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal ≤ 1 / p.toNNReal + 1 / q.toNNReal
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i * g i) 1
have i₂ : 1 / p.toNNReal + 1 / q.toNNReal = 1
Tactic: calc
    ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) :=
      Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq
    _ = (∑ i ∈ s, f i ^ p) / Real.toNNReal p + (∑ i ∈ s, g i ^ q) / Real.toNNReal q := by
      rw [sum_add_distrib, sum_div, sum_div]
    _ ≤ 1 / Real.toNNReal p + 1 / Real.toNNReal q := by gcongr
    _ = 1 := by simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have simp : ∀ i ∈ s, f i = 0 ∨ g i = 0
Tactic: simp only [hf, hpq.ne_zero, one_div, sum_eq_zero_iff, zero_rpow, zero_mul,
    inv_eq_zero, Ne, not_false_iff, le_zero_iff, mul_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0
i : ι
his : i ∈ s
⊢ f i = 0 ∨ g i = 0
have h : f i = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0
i : ι
his : i ∈ s
⊢ f i = 0
have h : ∀ (hf : ∀ i ∈ s, f i ^ p = 0) (i : ι) (his : i ∈ s), f i = 0
Tactic: rw [sum_eq_zero_iff] at hf
Cleared hypotheses: hf, i, his
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have inl : ∀ (hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0),
  ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
inl :
  ∀ (hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0),
    ∑ i ∈ s, f i * g i ≤
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have inr : ∀ (hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)),
  ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: obtain hf | hf := eq_zero_or_pos (∑ i ∈ s, f i ^ p)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have inr : ∀ (hg : Eq (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 0),
  ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: obtain hg | hg := eq_zero_or_pos (∑ i ∈ s, g i ^ q)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
inr :
  ∀ (hg : Eq (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 0),
    ∑ i ∈ s, f i * g i ≤
      HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have inr₁ : ∀ (hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)),
  ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: obtain hg | hg := eq_zero_or_pos (∑ i ∈ s, g i ^ q)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : Eq (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 0
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f i * g i) (∑ i ∈ s, g i * f i)
have e_f : ∀ (i : ι), (↑(f i * g i) : ℝ) = (↑(g i * f i) : ℝ)
Tactic: congr with i
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : Eq (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 0
i : ι
⊢ (↑(f i * g i) : ℝ) = (↑(g i * f i) : ℝ)
have e_f : (↑(g i * f i) : ℝ) = (↑(g i * f i) : ℝ)
Tactic: rw [mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : Eq (α := ℝ≥0) (∑ i ∈ s, g i ^ q) 0
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have i : Eq (α := ℝ≥0) (∑ i ∈ s, f i * g i) (∑ i ∈ s, g i * f i)
Tactic: calc
      ∑ i ∈ s, f i * g i = ∑ i ∈ s, g i * f i := by
        congr with i
        rw [mul_comm]
      _ ≤ (∑ i ∈ s, g i ^ q) ^ (1 / q) * (∑ i ∈ s, f i ^ p) ^ (1 / p) :=
        (inner_le_Lp_mul_Lp_of_norm_eq_zero s g f hpq.symm hg)
      _ = (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q) := mul_comm _ _
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (hypothesis)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
this : LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have this₁ : (∑ i ∈ s, f i * g i) /
    (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ≤
  1
Tactic: simp_rw [f', g', div_mul_div_comm, ← sum_div] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
this :
  (∑ i ∈ s, f i * g i) /
      (HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)) ≤
    1
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have rwa : 0 < HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
Tactic: rwa [div_le_iff₀, one_mul] at this
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
⊢ ∑ i ∈ s, f i * g i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
have inr : LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1
Tactic: suffices (∑ i ∈ s, f' i * g' i) ≤ 1 by
    simp_rw [f', g', div_mul_div_comm, ← sum_div] at this
    rwa [div_le_iff₀, one_mul] at this
    positivity
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1
have inr : Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
Tactic: refine inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq ?_) (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f' i * g' i) 1
have inr₁ : Eq (α := ℝ≥0) (∑ i ∈ s, g' i ^ q) 1
Tactic: refine inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq ?_) (le_of_eq ?_)
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (f x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)) ^ p) 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
have inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, f x ^ p / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p) 1
Tactic: simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one,
      div_self hf.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (f x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)) ^ p) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, f x ^ p / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p) 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
have inr₂ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p = 1
Tactic: simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one,
      div_self hf.ne']
-- Lean 4 proof step from Mathlib.Analysis.MeanInequalities (goal)
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, f i ^ p)
hg : LT.lt (α := ℝ≥0) 0 (∑ i ∈ s, g i ^ q)
f' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ f i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)
g' : (i : ι) → ℝ≥0 := fun (i : ι) ↦ g i / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)
inr : Eq (α := ℝ≥0) (∑ x ∈ s, (f x / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)) ^ p) 1
inr₁ : Eq (α := ℝ≥0) (∑ x ∈ s, f x ^ p / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p) 1
inr₂ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) ^ p = 1
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f' i ^ p) 1
have inr₃ : (∑ i ∈ s, f i ^ p) / HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p * p) = 1
Tactic: simp_rw [f', div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel₀ hpq.ne_zero, rpow_one,
      div_self hf.ne']