feat(convex/specific_functions): specific case of Jensen's inequality…

… for powers (#16186)

Proves a specific case of Jensen's inequality: a powers of a sum divided by the cardinality of the `finset` is less than or equal to the sum of the powers.

src/analysis/convex/specific_functions.lean

@@ -31,7 +31,7 @@ For `p : ℝ`, prove that `λ x, x ^ p` is concave when `0 ≤ p ≤ 1` and stri
 -/
 
 open real set
-open_locale big_operators
+open_locale big_operators nnreal
 
 /-- `exp` is strictly convex on the whole real line. -/
 lemma strict_convex_on_exp : strict_convex_on ℝ univ exp :=
@@ -82,6 +82,30 @@ begin
     nat.sub_pos_of_lt hn) (nat.cast_pos.2 $ zero_lt_two.trans_le hn),
 end
 
+/-- Specific case of Jensen's inequality for sums of powers -/
+lemma real.pow_sum_div_card_le_sum_pow {α : Type*} {s : finset α} {f : α → ℝ} (n : ℕ)
+  (hf : ∀ a ∈ s, 0 ≤ f a) : (∑ x in s, f x) ^ (n + 1) / s.card ^ n ≤ ∑ x in s, (f x) ^ (n + 1) :=
+begin
+  by_cases hs0 : s = ∅,
+  { simp_rw [hs0, finset.sum_empty, zero_pow' _ (nat.succ_ne_zero n), zero_div] },
+  { have hs : s.card ≠ 0 := hs0 ∘ finset.card_eq_zero.1,
+    have hs' : (s.card : ℝ) ≠ 0 := (nat.cast_ne_zero.2 hs),
+    have hs'' : 0 < (s.card : ℝ) := nat.cast_pos.2 (nat.pos_of_ne_zero hs),
+    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 hs'', div_mul, div_self hs', div_one] at this,
+    have := @convex_on.map_sum_le ℝ ℝ ℝ α _ _ _ _ _ _ (set.Ici 0) (λ x, x ^ (n + 1)) s
+      (λ _, 1 / s.card) (coe ∘ f) (convex_on_pow (n + 1)) _ _ (λ i hi, set.mem_Ici.2 (hf i hi)),
+    { simpa only [inv_mul_eq_div, one_div, algebra.id.smul_eq_mul] using this },
+    { simp only [one_div, inv_nonneg, nat.cast_nonneg, implies_true_iff] },
+    { simpa only [one_div, finset.sum_const, nsmul_eq_mul] using mul_inv_cancel hs' }}
+end
+
+lemma nnreal.pow_sum_div_card_le_sum_pow {α : Type*} (s : finset α) (f : α → ℝ≥0) (n : ℕ) :
+  (∑ x in s, f x) ^ (n + 1) / s.card ^ n ≤ ∑ x in s, (f x) ^ (n + 1) :=
+by simpa only [← nnreal.coe_le_coe, nnreal.coe_sum, nonneg.coe_div, nnreal.coe_pow] using
+  @real.pow_sum_div_card_le_sum_pow α s (coe ∘ f) n (λ _ _, nnreal.coe_nonneg _)
+
 lemma finset.prod_nonneg_of_card_nonpos_even
   {α β : Type*} [linear_ordered_comm_ring β]
   {f : α → β} [decidable_pred (λ x, f x ≤ 0)]