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.
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".
You need to construct a function from eps
to n
that will give you the correct bound
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
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.
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: Oct 13 2024 at 01:02 UTC