## Stream: Coq users

### Topic: How to prove that geom. series (with q < 1) goes to 0

#### Lessness (Apr 11 2021 at 16:34):

More specifically, I am trying to prove this:

``````Require Import Reals.
Open Scope R.

Theorem T (a: R) (eps: R) (H1: eps > 0):
exists n, forall i, (i > n)%nat -> - eps <= a / 2 ^ i < eps.
Proof.
``````

Thanks in advance for any hints.

#### Lessness (Apr 11 2021 at 16:36):

I found the theorem `cv_pow_half` in the Standard Library. If I use it, I can easily prove my theorem.

But it's unsatisfying and I want to prove it "myself".

#### Emilio Jesús Gallego Arias (Apr 11 2021 at 16:36):

You need to construct a function from `eps` to `n` that will give you the correct bound

#### Emilio Jesús Gallego Arias (Apr 11 2021 at 16:37):

call that function `f`, then `exists (f eps)` will give you the desired `n` and if `f` is the right one you should be able to finish the proof by calculus

#### Lessness (Apr 11 2021 at 19:15):

Yess, I did it.

``````Require Import Reals Lra Lia Field.
Open Scope R.

Definition nat_up (a: R) (H: a > 0): { n | INR n > a }.
Proof.
(* Proof by magic *)
exists (Z.to_nat (up a)).
rewrite INR_IZR_INZ.
rewrite Z2Nat.id.
apply archimed.
apply le_IZR.
pose (proj1 (archimed a)).
lra.
Qed.

Definition not_a_log_2 (a eps: R) (H: 0 < eps): { i | Rabs a / (2 ^ i) < eps }.
Proof.
destruct (Rlt_le_dec (Rabs a) eps).
+ exists O. simpl. lra.
+ assert (forall i a eps (H: 0 < eps), Rabs a / 2 ^ i < eps <-> Rabs a / eps < 2 ^ i).
{ intros. split; intros.
- unfold Rdiv. replace (2 ^ i) with (2 ^ i * eps0 * / eps0).
apply Rmult_lt_compat_r.
{ apply Rinv_0_lt_compat; auto. }
replace (2 ^ i * eps0) with (eps0 * 2 ^ i) by lra.
replace (Rabs a0) with (Rabs a0 / 2 ^ i * 2 ^ i).
apply Rmult_lt_compat_r; auto.
{ clear H1. induction i; simpl; lra. }
{ field. clear H1. induction i; simpl; lra. }
{ field. lra. }
- unfold Rdiv. replace eps0 with (eps0 * 2 ^ i * / 2 ^ i).
apply Rmult_lt_compat_r; auto.
{ apply Rinv_0_lt_compat. clear H1. induction i; simpl; lra. }
replace (eps0 * 2 ^ i) with (2 ^ i * eps0) by lra.
replace (Rabs a0) with (Rabs a0 / eps0 * eps0).
apply Rmult_lt_compat_r; auto.
{ field. lra. }
{ field. clear H1. induction i; simpl; lra. } }
assert { i | Rabs a / eps < 2 ^ i }.
{ assert (Rabs a / eps > 0).
{ unfold Rdiv. apply Rmult_gt_0_compat. lra. apply Rinv_0_lt_compat. auto. }
destruct (nat_up _ H1) as [n H2]. exists n.
assert (forall n, INR (S n) = INR n + 1).
{ intros. destruct n0. simpl. field. simpl. auto. }
assert (INR n < 2 ^ n).
{ clear H2. induction n.
+ simpl. lra.
+ rewrite H3. simpl. assert (1 <= 2 ^ n).
{ clear IHn. induction n. simpl. lra. simpl. lra. }
lra. }
lra. }
destruct H1 as [i H1]. exists i. apply H0; auto.
Qed.

Theorem T (a: R) (eps: R) (H1: eps > 0):
exists n, forall i, (i > n)%nat -> Rabs a / 2 ^ i < eps.
Proof.
destruct (not_a_log_2 a eps H1).
exists x. intros. assert (2 ^ i = 2 ^ x * 2 ^ (i - x)).
{ assert (i = x + (i - x))%nat by lia.
rewrite H0 at 1. rewrite pow_add. auto. }
rewrite H0. generalize (i - x)%nat.
clear H0. induction n.
+ simpl. replace (2 ^ x * 1) with (2 ^ x) by field. auto.
+ simpl. replace (Rabs a / (2 ^ x * (2 * 2 ^ n))) with (Rabs a / (2 ^ x * 2 ^ n) / 2).
lra. field. assert (forall n, 2 ^ n <> 0).
{ induction n0. lra. simpl. lra. }
split; eauto.
Qed.
``````

#### Lessness (Apr 12 2021 at 19:29):

Maybe some kind of `nat_up` and corresponding `archimed` theorem could be added to Standard Library?
I remember that this isn't the first time I prove something like it.

Last updated: Jan 27 2023 at 01:03 UTC