proposition: Lemma mean_power_of_two_eq a : (forall i, 0 <= a i) -> forall k, sqrtk k (prod (pow2 k) a) = sum (pow2 k) a / INR (pow2 k) -> forall i j, lt i (pow2 k) -> lt j (pow2 k) -> a i = a j.
proof: Proof. intros pa k E. cut (forall i, lt i (pow2 k) -> a i = sum (pow2 k) a / INR (pow2 k)). { intros C i j Hi Hj. rewrite (C i Hi), (C j Hj). auto. } revert a pa E; induction k; intros a pa; simpl. - intros E i Hi. inversion Hi. field. lia. - remember (pow2 k) as n. assert (R : (n + (n + 0) = n + n)%nat) by ring; rewrite R; clear R. rewrite prod_plus, sum_plus. pose proof IHk a pa as HL. pose proof IHk (shift n a) ltac:(intros; apply pa) as HR. clear IHk. intros E. pose proof mean_power_of_two a pa k as L1. pose proof mean_power_of_two (shift n a) ltac:(intro; apply pa) k as R1. rewrite <-Heqn in *. rewrite sqrtk_mult in E; try (apply prod_pos; intro; apply pa). replace (n + n)%nat with (n * 2)%nat in E |- *. 2:lia. rewrite mult_INR in E |- *. assert (dhalf : forall x, (x + x) / 2 = x). { intros x; unfold Rdiv. rewrite Rmult_plus_distr_r, Rdiv_fold, <-double_var. auto. } unfold Rdiv in E |- *. assert (INR n <> 0). { assert (n <> O). subst. clear; induction k; simpl; auto. lia. auto with *. } rewrite Rinv_mult_distr in E |- *; auto with *. rewrite <-Rmult_assoc, Rmult_plus_distr_r in E |- *. repeat rewrite Rdiv_fold in *. remember (sqrtk k (prod n a)) as g1 eqn:Eg1. remember (sqrtk k (prod n (shift n a))) as g2 eqn:Eg2. remember (sum n a / INR n) as a1 eqn:Ea1. remember (sum n (shift n a) / INR n) as a2 eqn:Ea2. pose proof mean_aux g1 g2 a1 a2 as Rec. do 2 assert_specialize Rec by (subst; apply sqrtk_pos, prod_pos; intro; apply pa). repeat assert_specialize Rec by auto. assert_specialize HR by intuition. assert_specialize HL by intuition. replace a2 with a1 in * by intuition congruence. replace (INR 2) with 2 by (compute; ring). rewrite dhalf. clear -HL HR. intros i li. assert (D : (i < n \/ i >= n)%nat) by lia. destruct D as [D|D]. + apply HL, D. + specialize (HR (i - n)%nat ltac:(lia)). exact_eq HR; f_equal. unfold shift; f_equal. lia. Qed.
imports: Lia Reals Psatz