Stream: Coq users

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


view this post on Zulip 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.
Admitted.

Thanks in advance for any hints.

view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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