proposition: Lemma half_mean_0 : forall Un k m, 0 <= k -> (1 <= m)%nat -> (forall n, 0 <= Un n) -> (forall n, Un n <= k / INR (S n)) -> Rseq_cv (fun N => / INR (2 * N + m) * sum_f_R0 Un (pred N)) 0.
proof: Proof. intros Un k m kpos mpos Unpos Unbound. apply Rseq_cv_shift_compat; unfold Rseq_shift; simpl pred. eapply Rseq_cv_0_pos_maj_compat. intro. rewrite Rmult_comm; apply Rle_mult_inv_pos. apply cond_pos_sum; assumption. INR_solve. intro. eapply Rle_trans. apply Rmult_le_compat. apply Rlt_le; apply Rinv_0_lt_compat; INR_solve. apply cond_pos_sum; assumption. apply Rlt_le; apply (Rinv_lt_contravar (INR (S n))); INR_solve. apply (sum_growing _ (fun n => k / INR (S n))); apply Unbound. replace (sum_f_R0 (fun n0 : nat => k / INR (S n0)) n) with (sum_f_R0 (fun n0 : nat => / INR (S n0) * k) n) by (apply Rseq_sum_ext; intro; field; INR_solve). rewrite <- scal_sum. rewrite <- Rmult_assoc; rewrite Rmult_comm with _ k; rewrite Rmult_assoc. 2: replace 0 with (k * 0) by ring. 2: apply Rseq_cv_mult_compat. 2: apply Rseq_constant_cv. 2: apply inverse_mean_cv_0. unfold Rseq_mult, Rseq_constant. apply (Rmult_le_compat_l k _ _ kpos). unfold inverse_mean, Rdiv. rewrite Rmult_comm. intuition. Qed.
imports: Reals Lra Rsequence_facts Rseries Rsequence_subsequence Rtactic Lia ZArith