case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p

case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
cases' eq_or_lt_of_le hp with hp hp
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
let q : ℝ := p / (p - 1)
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
have hpq : p.IsConjugateExponent q := by rw [Real.isConjugateExponent_iff hp]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
hq : 1 / q * p = p - 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
have hq : 1 / q * p = p - 1 := by
  rw [← hpq.div_conj_eq_sub_one]
  ring
no goals
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
hq : 1 / q * p = p - 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
simpa only [NNReal.mul_rpow, ← NNReal.rpow_mul, hp₁, hq, one_mul, one_rpow, rpow_one,
  Pi.one_apply, sum_const, Nat.smul_one_eq_coe] using
  NNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg
no goals
case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
simp [← hp]
no goals
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ Real.IsConjugateExponent p q
rw [Real.isConjugateExponent_iff hp]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p / q
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p - 1
rw [← hpq.div_conj_eq_sub_one]
no goals
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p / q
ring