awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.MeanInequalities
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))
⊢ n = n⁻¹⁻¹

Tactic:
simp
-- Module: Mathlib.Analysis.MeanInequalities
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))
refine_3 : (∑ i ∈ s, n⁻¹ * (w i / z i))⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹
⊢ n / ∑ i ∈ s, w i / z i ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹

Tactic:
nth_rw 1 [div_eq_mul_inv, (show n = (n⁻¹)⁻¹ by simp), ← mul_inv, Finset.mul_sum _ _ n⁻¹]

Premises used: Finset.mul_sum, mul_inv, div_eq_mul_inv, Inv.inv
-- Module: Mathlib.Analysis.MeanInequalities
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))
refine_3 : (∑ x ∈ s, w x / n / z x)⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹
⊢ (∑ i ∈ s, n⁻¹ * (w i / z i))⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹

Tactic:
simp_rw [inv_mul_eq_div n ((w _) / (z _)), div_right_comm _ _ n]

Premises used: div_right_comm, inv_mul_eq_div, HDiv.hDiv
-- Module: Mathlib.Analysis.MeanInequalities
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))
⊢ LE.le (α := ℝ) (∑ x ∈ s, w x / n / z x)⁻¹ (∏ x ∈ s, z x ^ (w x / n))

Tactic:
this
-- Module: Mathlib.Analysis.MeanInequalities
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))
h : HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)
⊢ (∑ x ∈ s, w x / n / z x)⁻¹ ≤ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹

Tactic:
convert! this
-- Module: Mathlib.Analysis.MeanInequalities
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
positivity positivity₁ positivity₂ positivity₃ : 0 < z i → 0 ≤ z i ^ w i
⊢ 0 ≤ z i ^ w i

Tactic:
positivity [hz i hi]
-- Module: Mathlib.Analysis.MeanInequalities
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))
h : Eq (α := ℝ) (∏ i ∈ s, (z i ^ w i) ^ n⁻¹) (∏ x ∈ s, z x ^ (w x / n))
⊢ HPow.hPow (α := ℝ) (∏ i ∈ s, z i ^ w i) n⁻¹ = ∏ x ∈ s, z x ^ (w x / n)

Tactic:
rw [← Real.finsetProd_rpow s _ (fun i hi ↦ by positivity [hz i hi])]

Premises used: Real.finsetProd_rpow
-- Module: Mathlib.Analysis.MeanInequalities
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))

Tactic:
Finset.prod_congr rfl (fun i hi => ?_)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
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))
h : ∀ (i : ι) (hi : i ∈ s), (z i ^ w i) ^ n⁻¹ = z i ^ (w i / n)
⊢ Eq (α := ℝ) (∏ i ∈ s, (z i ^ w i) ^ n⁻¹) (∏ x ∈ s, z x ^ (w x / n))

Tactic:
refine Finset.prod_congr rfl (fun i hi => ?_)

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Analysis.MeanInequalities
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)
h₁ h₂ : z i ^ (w i * n⁻¹) = z i ^ (w i * n⁻¹)
⊢ (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]

Premises used: le_of_lt, div_eq_mul_inv, Inv.inv, Real.rpow_mul
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ ∀ i ∈ s, LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)

Tactic:
fun i hi ↦ div_pos (hw i hi) hw'

Premises used: div_pos
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ ∀ i ∈ s, LT.lt (α := ℝ) 0 ((fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i)

Tactic:
exact fun i hi ↦ div_pos (hw i hi) hw'

Premises used: div_pos
-- Module: Mathlib.Analysis.MeanInequalities
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
refine_2 : HMul.hMul (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i)⁻¹ = 1
⊢ Eq (α := ℝ) (∑ i ∈ s, (fun (i : ι) ↦ w i / ∑ i ∈ s, w i) i) 1

Tactic:
simp_rw [div_eq_mul_inv (w _) (∑ i ∈ s, w i), ← Finset.sum_mul _ _ (∑ i ∈ s, w i)⁻¹]

Premises used: div_eq_mul_inv, Inv.inv, Finset.sum, Finset.sum_mul
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ HMul.hMul (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i)⁻¹ = 1

Tactic:
mul_inv_cancel₀ hw'.ne'

Premises used: mul_inv_cancel₀, LT.lt.ne'
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ HMul.hMul (α := ℝ) (∑ i ∈ s, w i) (∑ i ∈ s, w i)⁻¹ = 1

Tactic:
exact mul_inv_cancel₀ hw'.ne'

Premises used: mul_inv_cancel₀, LT.lt.ne'
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b p q : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hpq : p.HolderConjugate q
⊢ a * b ≤ a ^ p / p + b ^ q / q

Tactic:
simpa [← rpow_mul, ha, hb, hpq.ne_zero, hpq.symm.ne_zero, _root_.div_eq_inv_mul] using
    geom_mean_le_arith_mean2_weighted hpq.inv_nonneg hpq.symm.inv_nonneg
      (rpow_nonneg ha p) (rpow_nonneg hb q) hpq.inv_add_inv_eq_one

Premises used: Real.HolderTriple.inv_nonneg, Real.HolderTriple.ne_zero, Real.HolderConjugate.symm, Real.HolderConjugate.inv_add_inv_eq_one, Real.rpow_nonneg, div_eq_inv_mul, Real.rpow_mul, Real.geom_mean_le_arith_mean2_weighted
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b p q : ℝ
hpq : p.HolderConjugate q
⊢ a * b ≤ |a| ^ p / p + |b| ^ q / q

Tactic:
calc
    a * b ≤ |a * b| := le_abs_self (a * b)
    _ = |a| * |b| := abs_mul a b
    _ ≤ |a| ^ p / p + |b| ^ q / q :=
      Real.young_inequality_of_nonneg (abs_nonneg a) (abs_nonneg b) hpq

Premises used: Trans.trans, le_abs_self, HMul.hMul, abs_mul, Real.young_inequality_of_nonneg, abs_nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b p q : ℝ≥0
hpq : p.HolderConjugate q
⊢ a * b ≤ a ^ (↑p : ℝ) / p + b ^ (↑q : ℝ) / q

Tactic:
Real.young_inequality_of_nonneg a.coe_nonneg b.coe_nonneg hpq.coe

Premises used: NNReal.HolderConjugate.coe, NNReal.coe_nonneg, Real.young_inequality_of_nonneg, NNReal.toReal
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
⊢ a * b ≤ a ^ p / p.toNNReal + b ^ q / q.toNNReal

Tactic:
simpa [Real.coe_toNNReal, hpq.nonneg, hpq.symm.nonneg] using young_inequality a b hpq.toNNReal

Premises used: Real.HolderConjugate.toNNReal, NNReal.young_inequality, Real.HolderConjugate.symm, Real.coe_toNNReal, Real.HolderTriple.nonneg
-- Module: Mathlib.Analysis.MeanInequalities
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
neg : ∀ (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

Tactic:
by_cases! h : a = ⊤ ∨ b = ⊤
-- Module: Mathlib.Analysis.MeanInequalities
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

Tactic:
le_trans le_top (le_of_eq ?_)

Premises used: le_top, le_of_eq, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
pos : ∞ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
refine le_trans le_top (le_of_eq ?_)

Premises used: le_top, le_of_eq, le_trans
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q / ENNReal.ofReal q
⊢ ∞ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q / ENNReal.ofReal q

Tactic:
rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞ ∨ b = ∞
pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
⊢ ∞ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

Tactic:
repeat rw [div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.Analysis.MeanInequalities
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)⁻¹
pos₁ : ∀ (h : b = ∞), ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Tactic:
rcases h with h | h
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞
pos : ∞ = HPow.hPow (α := ℝ≥0∞) ∞ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Tactic:
rw [h]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : b = ∞
pos : ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + HPow.hPow (α := ℝ≥0∞) ∞ q * (ENNReal.ofReal q)⁻¹
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Tactic:
rw [h]
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a = ∞
⊢ ∞ = HPow.hPow (α := ℝ≥0∞) ∞ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹

Tactic:
simp [hpq.pos, hpq.symm.pos]

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : b = ∞
⊢ ∞ = a ^ p * (ENNReal.ofReal p)⁻¹ + HPow.hPow (α := ℝ≥0∞) ∞ q * (ENNReal.ofReal q)⁻¹

Tactic:
simp [hpq.pos, hpq.symm.pos]

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ p.toNNReal ≠ 0

Tactic:
simp [hpq.pos]

Premises used: Real.HolderTriple.pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ q.toNNReal ≠ 0

Tactic:
simp [hpq.symm.pos]

Premises used: Real.HolderConjugate.symm, Real.HolderTriple.pos
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
neg : a.toNNReal * b.toNNReal ≤ a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

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]

Premises used: ENNReal.coe_toNNReal, ENNReal.ofReal, Real.HolderConjugate.symm, ENNReal.coe_rpow_of_nonneg, ENNReal.coe_le_coe, ENNReal.coe_add, ENNReal.coe_mul, And.right, And.left, ENNReal.coe_div, Real.HolderTriple.nonneg
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a.toNNReal * b.toNNReal ≤ a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal

Tactic:
NNReal.young_inequality_real a.toNNReal b.toNNReal hpq

Premises used: ENNReal.toNNReal, NNReal.young_inequality_real
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
a b : ℝ≥0∞
p q : ℝ
hpq : p.HolderConjugate q
h : a ≠ ∞ ∧ b ≠ ∞
⊢ a.toNNReal * b.toNNReal ≤ a.toNNReal ^ p / p.toNNReal + b.toNNReal ^ q / q.toNNReal

Tactic:
exact NNReal.young_inequality_real a.toNNReal b.toNNReal hpq

Premises used: ENNReal.toNNReal, NNReal.young_inequality_real
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ 0 < p.toNNReal

Tactic:
have hp : 0 < p.toNNReal := zero_lt_one.trans hpq.toNNReal.lt
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ 0 < q.toNNReal

Tactic:
have hq : 0 < q.toNNReal := zero_lt_one.trans hpq.toNNReal.symm.lt
-- Module: Mathlib.Analysis.MeanInequalities
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) (∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal))

Tactic:
Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq

Premises used: Finset.sum_le_sum, NNReal.young_inequality_real
-- Module: Mathlib.Analysis.MeanInequalities
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
rw₂ 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)
⊢ ∑ 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:
rw [sum_add_distrib, sum_div, sum_div]

Premises used: Finset.sum_add_distrib, Finset.sum_div
-- Module: Mathlib.Analysis.MeanInequalities
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
h₂ : 0 ≤ q.toNNReal
⊢ (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal ≤ 1 / p.toNNReal + 1 / q.toNNReal

Tactic:
gcongr
-- Module: Mathlib.Analysis.MeanInequalities
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
simp_rw : p.toNNReal⁻¹ + q.toNNReal⁻¹ = 1
⊢ 1 / p.toNNReal + 1 / q.toNNReal = 1

Tactic:
simp_rw [one_div, hpq.toNNReal.inv_add_inv_eq_one]

Premises used: Real.HolderConjugate.toNNReal, NNReal.HolderConjugate.inv_add_inv_eq_one, one_div
-- Module: Mathlib.Analysis.MeanInequalities
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
i₂ : 1 / p.toNNReal + 1 / q.toNNReal = 1
⊢ LE.le (α := ℝ≥0) (∑ i ∈ s, f i * g i) 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]

Premises used: HPow.hPow, Finset.sum_le_sum, Finset.sum, NNReal.young_inequality_real, Real.toNNReal
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : Eq (α := ℝ≥0) (∑ i ∈ s, f i ^ p) 0
simp : ∀ i ∈ s, f i = 0 ∨ g i = 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:
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]

Premises used: inv_eq_zero, NNReal.zero_rpow, le_zero_iff, MulZeroClass.zero_mul, Real.HolderTriple.ne_zero, Ne, mul_eq_zero, one_div, not_false_iff, Finset.sum_eq_zero_iff
-- Module: Mathlib.Analysis.MeanInequalities
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
h : f i = 0
⊢ f i = 0 ∨ g i = 0

Tactic:
left
-- Module: Mathlib.Analysis.MeanInequalities
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
h : ∀ (hf : ∀ i ∈ s, f i ^ p = 0) (i : ι) (his : i ∈ s), f i = 0
⊢ f i = 0

Tactic:
rw [sum_eq_zero_iff] at hf

Premises used: Finset.sum_eq_zero_iff
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0

Tactic:
(rpow_eq_zero_iff.mp (hf i his)).left

Premises used: And.left, Iff.mp, NNReal.rpow_eq_zero_iff
-- Module: Mathlib.Analysis.MeanInequalities
Goal:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.HolderConjugate q
hf : ∀ i ∈ s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0

Tactic:
exact (rpow_eq_zero_iff.mp (hf i his)).left

Premises used: And.left, Iff.mp, NNReal.rpow_eq_zero_iff
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∑ 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)

Premises used: eq_zero_or_pos, HPow.hPow, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
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)

Tactic:
inner_le_Lp_mul_Lp_of_norm_eq_zero s f g hpq hf

Premises used: _private.0.NNReal.inner_le_Lp_mul_Lp_of_norm_eq_zero
-- Module: Mathlib.Analysis.MeanInequalities
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)

Tactic:
exact inner_le_Lp_mul_Lp_of_norm_eq_zero s f g hpq hf

Premises used: _private.0.NNReal.inner_le_Lp_mul_Lp_of_norm_eq_zero
-- Module: Mathlib.Analysis.MeanInequalities
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)
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)
⊢ ∑ 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)

Premises used: eq_zero_or_pos, HPow.hPow, Finset.sum
-- Module: Mathlib.Analysis.MeanInequalities
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
e_f : ∀ (i : ι), (↑(f i * g i) : ℝ) = (↑(g i * f i) : ℝ)
⊢ Eq (α := ℝ≥0) (∑ i ∈ s, f i * g i) (∑ i ∈ s, g i * f i)

Tactic:
congr with i
-- Module: Mathlib.Analysis.MeanInequalities
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 : ι
e_f e_f₁ : (↑(g i * f i) : ℝ) = (↑(g i * f i) : ℝ)
⊢ (↑(f i * g i) : ℝ) = (↑(g i * f i) : ℝ)

Tactic:
rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.Analysis.MeanInequalities
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, g i * f i ≤ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p)

Tactic:
(inner_le_Lp_mul_Lp_of_norm_eq_zero s g f hpq.symm hg)

Premises used: _private.0.NNReal.inner_le_Lp_mul_Lp_of_norm_eq_zero, Real.HolderConjugate.symm
-- Module: Mathlib.Analysis.MeanInequalities
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
⊢ HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) =
    HPow.hPow (α := ℝ≥0) (∑ i ∈ s, f i ^ p) (1 / p) * HPow.hPow (α := ℝ≥0) (∑ i ∈ s, g i ^ q) (1 / q)

Tactic:
mul_comm _ _

Premises used: mul_comm
-- Module: Mathlib.Analysis.MeanInequalities
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 : Eq (α := ℝ≥0) (∑ i ∈ s, f i * g i) (∑ i ∈ s, g i * f i)
⊢ ∑ 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:
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 _ _

Premises used: _private.0.NNReal.inner_le_Lp_mul_Lp_of_norm_eq_zero, Real.HolderConjugate.symm, HDiv.hDiv, HPow.hPow, mul_comm, OfNat.ofNat, Finset.sum