case inl
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
f : ι → α
⊢ ((∑ i in ∅, f i) / ↑(card ∅)) ^ 2 ≤ (∑ i in ∅, f i ^ 2) / ↑(card ∅)

case inr
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
obtain rfl | hs := s.eq_empty_or_nonempty
case inr
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
case inr
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : Finset.Nonempty s
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
rw [← card_pos, ← @Nat.cast_pos α] at hs
case inr
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ (∑ i in s, f i) ^ 2 * ↑(card s) ≤ (↑(card s) * ∑ i in s, f i ^ 2) * ↑(card s)
case inr
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ ((∑ i in s, f i) / ↑(card s)) ^ 2 ≤ (∑ i in s, f i ^ 2) / ↑(card s)
rw [div_pow, div_le_div_iff (sq_pos_of_ne_zero _ hs.ne') hs, sq (s.card : α), mul_left_comm, ←
  mul_assoc]
no goals
case inr
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
s : Finset ι
f : ι → α
hs : 0 < ↑(card s)
⊢ (∑ i in s, f i) ^ 2 * ↑(card s) ≤ (↑(card s) * ∑ i in s, f i ^ 2) * ↑(card s)
exact mul_le_mul_of_nonneg_right sq_sum_le_card_mul_sum_sq hs.le
no goals
case inl
ι : Type u_2
α : Type u_1
β : Type ?u.24207
inst✝ : LinearOrderedField α
f : ι → α
⊢ ((∑ i in ∅, f i) / ↑(card ∅)) ^ 2 ≤ (∑ i in ∅, f i ^ 2) / ↑(card ∅)
simp