case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q

case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : ¬(a = ⊤ ∨ b = ⊤)
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
by_cases h : a = ⊤ ∨ b = ⊤
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : ¬(a = ⊤ ∨ b = ⊤)
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
push_neg  at h
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ ENNReal.toNNReal a * ENNReal.toNNReal b ≤
    ENNReal.toNNReal a ^ p / Real.toNNReal p + ENNReal.toNNReal b ^ q / Real.toNNReal q
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
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]
no goals
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ ENNReal.toNNReal a * ENNReal.toNNReal b ≤
    ENNReal.toNNReal a ^ p / Real.toNNReal p + ENNReal.toNNReal b ^ q / Real.toNNReal q
exact NNReal.young_inequality_real a.toNNReal b.toNNReal hpq
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
refine' le_trans le_top (le_of_eq _)
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
repeat rw [div_eq_mul_inv]
no goals
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
cases' h with h h <;> rw [h] <;> simp [h, hpq.pos, hpq.symm.pos]
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
rw [div_eq_mul_inv]
no goals
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ Real.toNNReal p ≠ 0
simp [hpq.pos]
no goals
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ Real.toNNReal q ≠ 0
simp [hpq.symm.pos]