ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ ↑(Real.toNNReal p) / Real.toNNReal p + b ^ q / Real.toNNReal q
ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ p / Real.toNNReal p + b ^ q / Real.toNNReal q
nth_rw 1 [← Real.coe_toNNReal p hpq.nonneg]
ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ ↑(Real.toNNReal p) / Real.toNNReal p + b ^ ↑(Real.toNNReal q) / Real.toNNReal q
ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ ↑(Real.toNNReal p) / Real.toNNReal p + b ^ q / Real.toNNReal q
nth_rw 1 [← Real.coe_toNNReal q hpq.symm.nonneg]
no goals
ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ ↑(Real.toNNReal p) / Real.toNNReal p + b ^ ↑(Real.toNNReal q) / Real.toNNReal q
exact young_inequality a b hpq.one_lt_nnreal hpq.inv_add_inv_conj_nnreal