proposition: Theorem geometric_arithmetic_mean (a : nat -> R) (n : nat) : n <> O -> (forall i, (i < n)%nat -> 0 <= a i) -> prod n a <= (sum n a / INR n) ^ n /\ (prod n a = (sum n a / INR n) ^ n -> forall i, (i < n)%nat -> a i = a O).
proof: Proof. assert (H : exists k, lt n (pow2 k)). { exists n. induction n; simpl; lia. } intros p pa. destruct H as (k, Hk). set (alpha := sum n a / INR n). assert (na0 : alpha = 0 -> forall i, lt i n -> a i = 0). { intros a0. remember alpha as al eqn:E. unfold alpha in E. clear alpha. assert (s : sum n a = 0). - replace (sum n a) with (al * INR n). rewrite a0. ring. rewrite E. field. auto with *. - clear -s pa; revert a s pa. induction n; intros a s pa. + intros i Hi; inversion Hi. + cut (a O = 0 /\ sum n (shift 1 a) = 0). * intros (a0, s0) i Hi. specialize (IHn _ s0). assert_specialize IHn. { intros; apply pa; lia. } destruct i. apply a0. specialize (IHn i). assert_specialize IHn. lia. rewrite <-IHn. unfold shift. f_equal. lia. * simpl in s. apply Rplus_eq_R0; auto with *. apply sum_pos_lt. intros i Hi; specialize (pa (S i)). assert_specialize pa. lia. exact_eq pa. f_equal. unfold shift. f_equal. lia. } assert (0 <= alpha). { unfold alpha. clear alpha na0. apply Rmult_le_pos; auto with *. apply sum_pos_lt; auto. } set (b := fun i => if le_lt_dec n i then alpha else a i). assert (pb : forall i, 0 <= b i). { intros i; unfold b. destruct (le_lt_dec n i); auto. } assert (R : prod (pow2 k) b = prod n a * alpha ^ (pow2 k - n)). { replace (pow2 k) with (n + (pow2 k - n))%nat at 1 by lia. rewrite prod_plus. f_equal. - apply prod_ext_lt. intros j Hj. unfold b. destruct (le_lt_dec n j). lia. auto. - generalize (pow2 k - n)%nat as v; intros v. assert (L : le n n) by auto; revert L. generalize n at 2 3. induction v; intros n0 ln0. auto. simpl. f_equal. + unfold shift, b. simpl. destruct (le_lt_dec n n0). auto. lia. + rewrite <-(IHv (plus 1 n0)); auto with *. apply prod_ext. intros x. unfold shift. f_equal. lia. } assert (IH : sum (pow2 k) b / INR (pow2 k) = alpha). { cut (sum (pow2 k) b = alpha * INR (pow2 k)). { intros ->. field. auto with *. } replace (pow2 k) with (n + (pow2 k - n))%nat. 2:lia. rewrite sum_plus. rewrite plus_INR. rewrite Rmult_plus_distr_l. f_equal. - unfold alpha. transitivity (sum n a). + apply sum_ext_lt. intros i Hi; unfold b. destruct (le_lt_dec n i). lia. auto. + field. auto with *. - generalize (pow2 k - n)%nat as v; intros v. assert (L : le n n) by auto; revert L. generalize n at 2 3. induction v; intros n0 ln0. simpl; ring. simpl sum. change (S v) with (plus 1 v). rewrite plus_INR. rewrite Rmult_plus_distr_l. f_equal. + unfold shift, b. simpl. destruct (le_lt_dec n n0). ring. lia. + rewrite <-(IHv (plus 1 n0)); auto with *. apply sum_ext. intros x. unfold shift. f_equal. lia. } split. - Ltac wlog P := match goal with |- ?Q => cut (P -> Q) end. wlog (0 < alpha). { intros wlog. destruct H; auto. assert_specialize na0; auto. apply Req_le. transitivity 0. - destruct n. tauto. simpl. rewrite na0; auto with *. - destruct n. tauto. simpl. rewrite <-H. auto with *. } intros apos. assert (forall i, 0 < alpha ^ i). intros i. apply pow_lt. auto. cut (prod (pow2 k) b <= alpha ^ pow2 k). { rewrite R. replace (pow2 k) with (n + (pow2 k - n))%nat at 2 by lia. rewrite pow_add. intros L. apply Rmult_le_reg_r in L; auto. } rewrite <-IH. pose proof mean_power_of_two b pb k as M. match type of M with ?a <= ?b => assert (0 <= a <= b) as M' end. { split; auto. apply sqrtk_pos, prod_pos, pb. } apply pow_incr with (n := pow2 k) in M'. rewrite pow2_sqrtk in M'. 2: apply prod_pos, pb. apply M'. - intros E. pose proof mean_power_of_two_eq b pb k as HE. assert_specialize HE. { rewrite R, E, <-pow_add. replace (n + (pow2 k - n))%nat with (pow2 k) by lia. rewrite sqrtk_pow2; auto. } intros i li. specialize (HE i O). repeat assert_specialize HE by lia. exact_eq HE; f_equal; unfold b. + destruct (le_lt_dec n i). lia. auto. + destruct (le_lt_dec n 0). lia. auto. Qed.
imports: Lia Reals Psatz