proposition: Lemma mean_power_of_two a : (forall i, 0 <= a i) -> forall k, sqrtk k (prod (pow2 k) a) <= sum (pow2 k) a / INR (pow2 k).
proof: Proof. intros pa k; revert a pa; induction k; intros a pa; simpl. lra. remember (pow2 k) as n. assert (R : (n + (n + 0) = n + n)%nat) by ring; rewrite R; clear R. rewrite prod_plus. rewrite sum_plus. pose proof IHk a pa as L. pose proof IHk (shift n a) ltac:(intros; apply pa) as R. clear IHk. eapply Rle_trans. - rewrite sqrtk_mult. all:try (apply prod_pos; intros; apply pa). apply mean2. all: apply sqrtk_pos, prod_pos; intros; apply pa. - unfold Rdiv. do 2 rewrite Rmult_plus_distr_r. replace (INR (n + n)) with (INR (n * 2)) by (f_equal; ring). rewrite mult_INR, (Rinv_mult_distr (INR n)). do 2 rewrite <-Rmult_assoc with (r3 := / INR 2). replace (INR 2) with 2. apply Rplus_le_compat; apply Rmult_le_compat; auto. all: simpl; try lra. all: try (apply sqrtk_pos, prod_pos; intros; apply pa). pose proof INR_pow2 k. subst. lra. Qed.
imports: Lia Reals Psatz