case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ (∑ x in ∅, f x) ^ (n + 1) / ↑(card ∅) ^ n ≤ ∑ x in ∅, f x ^ (n + 1)

case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
rcases s.eq_empty_or_nonempty with (rfl | hs)
case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ 0 ≤ 0
case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ (∑ x in ∅, f x) ^ (n + 1) / ↑(card ∅) ^ n ≤ ∑ x in ∅, f x ^ (n + 1)
simp_rw [Finset.sum_empty, zero_pow' _ (Nat.succ_ne_zero n), zero_div]
no goals
case inl
ι : Type u
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ ∅ → 0 ≤ f a
⊢ 0 ≤ 0
rfl
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
have hs0 : 0 < (s.card : ℝ) := Nat.cast_pos.2 hs.card_pos
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
suffices (∑ x in s, f x / s.card) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / s.card by
  rwa [← Finset.sum_div, ← Finset.sum_div, div_pow, pow_succ' (s.card : ℝ), ← div_div,
    div_le_iff hs0, div_mul, div_self hs0.ne', div_one] at this
case inr.refine_3
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
this :
  (fun x => x ^ (n + 1)) (∑ i in s, (fun x => 1 / ↑(card s)) i • ((fun x => x) ∘ f) i) ≤
    ∑ i in s, (fun x => 1 / ↑(card s)) i • (fun x => x ^ (n + 1)) (((fun x => x) ∘ f) i)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)

case inr.refine_1
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∀ (i : ι), i ∈ s → 0 ≤ (fun x => 1 / ↑(card s)) i

case inr.refine_2
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∑ i in s, (fun x => 1 / ↑(card s)) i = 1
case inr
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
have :=
  @ConvexOn.map_sum_le ℝ ℝ ℝ ι _ _ _ _ _ _ (Set.Ici 0) (fun x => x ^ (n + 1)) s
    (fun _ => 1 / s.card) ((↑) ∘ f) (convexOn_pow (n + 1)) ?_ ?_ fun i hi =>
    Set.mem_Ici.2 (hf i hi)
no goals
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
this : (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
⊢ (∑ x in s, f x) ^ (n + 1) / ↑(card s) ^ n ≤ ∑ x in s, f x ^ (n + 1)
rwa [← Finset.sum_div, ← Finset.sum_div, div_pow, pow_succ' (s.card : ℝ), ← div_div,
  div_le_iff hs0, div_mul, div_self hs0.ne', div_one] at this
no goals
case inr.refine_3
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
this :
  (fun x => x ^ (n + 1)) (∑ i in s, (fun x => 1 / ↑(card s)) i • ((fun x => x) ∘ f) i) ≤
    ∑ i in s, (fun x => 1 / ↑(card s)) i • (fun x => x ^ (n + 1)) (((fun x => x) ∘ f) i)
⊢ (∑ x in s, f x / ↑(card s)) ^ (n + 1) ≤ ∑ x in s, f x ^ (n + 1) / ↑(card s)
simpa only [inv_mul_eq_div, one_div, Algebra.id.smul_eq_mul] using this
no goals
case inr.refine_1
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∀ (i : ι), i ∈ s → 0 ≤ (fun x => 1 / ↑(card s)) i
simp only [one_div, inv_nonneg, Nat.cast_nonneg, imp_true_iff]
no goals
case inr.refine_2
ι : Type u
s : Finset ι
f : ι → ℝ
n : ℕ
hf : ∀ (a : ι), a ∈ s → 0 ≤ f a
hs : Finset.Nonempty s
hs0 : 0 < ↑(card s)
⊢ ∑ i in s, (fun x => 1 / ↑(card s)) i = 1
simpa only [one_div, Finset.sum_const, nsmul_eq_mul] using mul_inv_cancel hs0.ne'