-- Mathlib/Algebra/Order/Chebyshev.lean
/-- Special case of **Jensen's inequality** for sums of powers. -/
lemma pow_sum_le_card_mul_sum_pow (hf : ∀ i ∈ s, 0 ≤ f i) :
    ∀ n, (∑ i ∈ s, f i) ^ (n + 1) ≤ (#s : α) ^ n * ∑ i ∈ s, f i ^ (n + 1)
  | 0 => by simp
  | n + 1 =>
    calc
      _ = (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ ↑(#s) ^ n * ((∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i) ≤ ↑(#s) ^ n * (↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i)

Tactic:
gcongr _ * ?_

Result:
case h
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i ≤ ↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i ≤ ↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i

Tactic:
exact ((monovaryOn_self ..).pow_left₀ hf _).sum_mul_sum_le_card_mul_sum

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1 + 1) = (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i

Tactic:
rw [pow_succ]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1) * ∑ i ∈ s, f i ≤ (↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i

Tactic:
gcongr

Result:
case a0
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ 0 ≤ ∑ i ∈ s, f i

case h
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ ↑(#s) ^ n * (↑(#s) * ∑ i ∈ s, f i ^ (n + 1) * f i) = ↑(#s) ^ (n + 1) * ∑ i ∈ s, f i ^ (n + 1 + 1)

Tactic:
simp_rw [← mul_assoc, ← pow_succ]

Result:
no goals

Proof state:
case a0
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ 0 ≤ ∑ i ∈ s, f i

case h
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (∑ i ∈ s, f i) ^ (n + 1) ≤ ↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)

Tactic:
exacts [sum_nonneg hf, pow_sum_le_card_mul_sum_pow hf _]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
n : ℕ
⊢ (↑(#s) ^ n * ∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i = ↑(#s) ^ n * ((∑ i ∈ s, f i ^ (n + 1)) * ∑ i ∈ s, f i)

Tactic:
rw [mul_assoc]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
inst✝¹ : LinearOrderedSemiring α
inst✝ : ExistsAddOfLE α
s : Finset ι
f : ι → α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ i ∈ s, f i) ^ (0 + 1) ≤ ↑(#s) ^ 0 * ∑ i ∈ s, f i ^ (0 + 1)

Tactic:
simp

Result:
no goals