ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
⊢ ∑ i in s, f i * g i ≤ 1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
⊢ ∑ i in s, f i * g i ≤ 1
have hp_ne_zero : Real.toNNReal p ≠ 0 := (zero_lt_one.trans hpq.one_lt_nnreal).ne.symm
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ ∑ i in s, f i * g i ≤ 1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
⊢ ∑ i in s, f i * g i ≤ 1
have hq_ne_zero : Real.toNNReal q ≠ 0 := (zero_lt_one.trans hpq.symm.one_lt_nnreal).ne.symm
no goals
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ ∑ i in s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) =
    (∑ i in s, f i ^ p) / Real.toNNReal p + (∑ i in s, g i ^ q) / Real.toNNReal q
rw [sum_add_distrib, sum_div, sum_div]
case refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, f i ^ p) / Real.toNNReal p ≤ 1 / Real.toNNReal p

case refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, g i ^ q) / Real.toNNReal q ≤ 1 / Real.toNNReal q
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, f i ^ p) / Real.toNNReal p + (∑ i in s, g i ^ q) / Real.toNNReal q ≤
    1 / Real.toNNReal p + 1 / Real.toNNReal q
refine' add_le_add _ _
no goals
case refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, f i ^ p) / Real.toNNReal p ≤ 1 / Real.toNNReal p
rwa [div_le_iff hp_ne_zero, div_mul_cancel _ hp_ne_zero]
no goals
case refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, g i ^ q) / Real.toNNReal q ≤ 1 / Real.toNNReal q
rwa [div_le_iff hq_ne_zero, div_mul_cancel _ hq_ne_zero]