Require Export realbasis. Require Export proof_utils. Require Export real_facts. Definition si_un (s:stream idigit) (n:nat) : Rdefinitions.R := let (p,k) := bounds n s in let (a,b) := p in (IZR a/IZR(2^k))%R. Theorem bounds_exp_non_0 : forall n s k p, bounds n s = (p,k) -> 0 <= k. induction n. simpl. intros s k p Heq; injection Heq; intros; omega. simpl. intros s k p. destruct s as [d tl]. generalize (IHn tl). destruct (bounds n tl) as [[a b] e]. intros IHn'; generalize (IHn' e (a,b) (refl_equal (a,b,e))). intros IHn''; destruct d; intros Heq; injection Heq; intros; omega. Qed. Theorem si_un_hd_lift : forall d s n, si_un (Cons d s) (S n) = lift d (si_un s n). intros d s n; simpl. case d. unfold si_un; simpl. generalize (bounds_exp_non_0 n s). destruct (bounds n s) as [[a b] k]. intros Hen0; generalize (Hen0 k (a,b) (refl_equal (a,b,k))). intros Hen0'. rewrite Zpower_exp. repeat (rewrite plus_IZR || rewrite mult_IZR). replace (IZR (2^1)) with 2%R. unfold lift, alpha; field; auto with real1. assert (2^k <> 0). apply Zpower_not_0; [assumption | omega]. assert (2 <> 0)%R. apply (not_O_IZR 2); omega. repeat (apply prod_neq_R0 || apply not_O_IZR); auto; fail. auto; fail. omega. omega. unfold si_un; simpl. generalize (bounds_exp_non_0 n s). destruct (bounds n s) as [[a b] k]. intros Hen0; generalize (Hen0 k (a,b) (refl_equal (a,b,k))). intros Hen0'. rewrite Zpower_exp. repeat (rewrite plus_IZR || rewrite mult_IZR). replace (IZR (2^1)) with 2%R. unfold lift, alpha; field; auto with real1. assert (2^k <> 0). apply Zpower_not_0; [assumption | omega]. assert (2 <> 0)%R. apply (not_O_IZR 2); omega. repeat (apply prod_neq_R0 || apply not_O_IZR); auto;fail. auto;fail. omega. omega. unfold si_un. lazy beta iota zeta delta [bounds]; fold bounds. generalize (bounds_exp_non_0 n s). destruct (bounds n s) as [[a b] k]. intros Hen0; generalize (Hen0 k (a,b) (refl_equal (a,b,k))). intros Hen0'. rewrite Zpower_exp. repeat (rewrite plus_IZR || rewrite mult_IZR). replace (IZR 2) with 2%R. replace (IZR (2^2)) with 4%R. replace (IZR (2^1)) with 2%R. unfold lift, alpha. field. assert (2^k <> 0). apply Zpower_not_0; [assumption | omega]. assert (2 <> 0)%R. apply (not_O_IZR 2); omega. repeat (apply prod_neq_R0 || apply not_O_IZR); auto;fail. auto;fail. simpl; field. simpl; field. omega. omega. Qed. Theorem lift_monotonic : forall d x y, (x <= y)%R -> (lift d x <= lift d y)%R. intros [ | | ] x y Hle; unfold lift, alpha; autorewrite with real1; fourier. Qed. Theorem si_un_increase : forall n s, (si_un s n <= si_un s (n+1))%R. induction n. intros [[ | | ] s]; unfold si_un; simpl; fourier. intros [ d s]; rewrite si_un_hd_lift. simpl (S n + 1)%nat. rewrite si_un_hd_lift. apply lift_monotonic; auto. Qed. Theorem si_un_growing : forall s, Un_growing (si_un s). unfold Un_growing. intros s n. replace (S n) with (n+1)%nat. exact (si_un_increase n s). ring. Qed. Theorem si_un_lower_bound_0 : forall n s, (0 <= si_un s n)%R. induction n. intros s; unfold si_un, bounds; simpl; fourier. intros s; apply Rle_trans with (1:= (IHn s)). exact (si_un_growing s n). Qed. Theorem si_un_bounded_1 : forall n s, (si_un s n <= 1)%R. induction n. intros s. unfold si_un. unfold bounds; simpl; fourier. destruct s as [d s]. rewrite si_un_hd_lift. case d; unfold lift, alpha; generalize (IHn s);intros; autorewrite with real1; fourier. Qed. Theorem si_un_bounded : forall s, has_ub (si_un s). intros s. unfold has_ub, EUn, bound. exists 1%R; unfold is_upper_bound. intros x [n Heq]; rewrite Heq; clear Heq. apply si_un_bounded_1. Qed. Definition real_value (s:stream idigit) := let (v,_) := growing_cv (si_un s) (si_un_growing s) (si_un_bounded s) in v. Theorem represent_diff_2pow_n : forall n, forall x r1 r2, represents x r1 -> represents x r2 -> (-1/(2^n) <= r1 - r2 <= 1/(2^n))%R. induction n. simpl. intros x r1 r2 Hr1 Hr2. generalize (represents_interval _ _ Hr1) (represents_interval _ _ Hr2). intros [H1 H2] [H3 H4]. split; fourier. assert (H0lt2 : (0 < 2)%R). fourier. assert (H2n0: (2<> 0)%R). apply (not_O_IZR 2); omega. assert (Hpow_nz : (2^n <> 0)%R). apply pow_nonzero;auto. assert (Hrepl : forall a, (a<> 0)%R -> (2*(1/(2*a))= 1/a)%R). intros a Hna; field. apply prod_neq_R0;auto. apply prod_neq_R0;auto. assert (Hrepl' : forall a, (a<> 0)%R -> (2*(-1/(2*a))= -1/a)%R). intros a Hna; field. apply prod_neq_R0;auto. apply prod_neq_R0;auto. intros x r1 r2 Hr1; case Hr1. intros dx tl r' Hr' _ Hr2; inversion Hr2. unfold lift. replace ((r'+alpha dx)/2 -(r+alpha dx)/2)%R with (r'/2 - r/2)%R. generalize (IHn tl r' r Hr' H1). intros [IHn1 IHn2]. split. apply Rmult_le_reg_l with 2%R; try assumption. simpl; rewrite Hrepl'. replace (2*(r'/2 - r/2))%R with ((r'-r))%R. assumption. field; auto. assumption. apply Rmult_le_reg_l with 2%R; try assumption. simpl; rewrite (Hrepl (2^n)%R). replace (2*(r'/2 - r/2))%R with ((r'-r))%R. assumption. field; auto. assumption. field;auto. Qed. Theorem cv_shift : forall f : nat -> Rdefinitions.R, forall l, Un_cv (fun n => f (S n)) l -> Un_cv f l. intros f l Hcv eps Hpos; destruct (Hcv eps Hpos) as [n H]; exists (S n). intros n'; case n'. intro; assert (Habs :False). omega. elim Habs. intros; apply H; omega. Qed. Theorem real_value_lift : forall d s, real_value (Cons d s) = lift d (real_value s). intros d; unfold lift; unfold real_value. intros s; destruct (growing_cv (si_un (Cons d s)) (si_un_growing (Cons d s)) (si_un_bounded (Cons d s))) as [x Hcv]. destruct (growing_cv (si_un s) (si_un_growing s) (si_un_bounded s)) as [y Hcvy]. apply UL_sequence with (si_un (Cons d s)). auto;fail. assert (Hcv_half : Un_cv (fun _ => (1/2)%R) (1/2)). intros eps Hpos; exists 0%nat; intros n _; rewrite R_dist_eq. fourier. apply cv_shift. apply cv_ext with (fun n => (si_un s n *(1/2) +alpha(d)*(1/2))%R). intros n; rewrite si_un_hd_lift; unfold lift; field. apply (not_O_IZR 2);omega. unfold lift; replace ((y+alpha d)/2)%R with (y*(1/2)+alpha d*(1/2))%R; [idtac|unfold Rdiv;ring]. apply (CV_plus (fun n => si_un s n *(1/2))%R (fun n => alpha d*(1/2))%R). apply (CV_mult (si_un s) (fun n => 1/2)%R); auto;fail. intros eps Hpos; exists 0%nat; intros n _; rewrite R_dist_eq. fourier. Qed. Theorem alpha_bounds : forall d, (0 <= alpha d <= 1)%R. intros [ | | ]; unfold alpha; split; fourier. Qed. Theorem real_value_in01 : forall s, (0 <= real_value s <= 1)%R. intros s; unfold real_value; destruct (growing_cv (si_un s)) as [v Hcv]. split. apply Rle_cv_lim with (fun _:nat => 0%R) (si_un s). intros n; apply si_un_lower_bound_0. intros eps Hpos; exists 0%nat; intros n _. rewrite R_dist_eq; fourier. auto. apply Rle_cv_lim with (si_un s) (fun _:nat => 1%R). intros n; apply si_un_bounded_1. assumption. intros eps Hpos; exists 0%nat; intros n _. rewrite R_dist_eq; fourier. Qed. Theorem represents_real_value : forall s, represents s (real_value s). cofix. intros [d s]. rewrite real_value_lift. constructor. apply represents_real_value. apply real_value_in01. Qed. Theorem smaller_half_is_zero : forall a, (0 < a -> a <= a /2 -> a = 0)%R. intros; fourier. Qed. Theorem represents_equal : forall s r, represents s r -> real_value s = r. intros s r Hrep. assert (Happrox : (forall v, 0 < v -> exists n, 1/(2^n) <= v/2)%R). intros v Hvpos;exists (Zabs_nat (up (1/v))+1)%nat. destruct (archimed (1/v)) as [Hb1 _]. rewrite pow_add. replace (1 / (2 ^ Zabs_nat (up (1 / v))*2^1))%R with ((1 / (2 ^ Zabs_nat (up (1 / v))))*/2)%R. replace (v/2)%R with (v*/2)%R. apply Rmult_le_compat_r. assert (0 < /2)%R. apply Rinv_0_lt_compat;auto. fourier. fourier. apply pow_half_smaller. fourier. field. apply (not_O_IZR 2); omega. replace (2^1)%R with 2%R. field. assert (2<>0)%R. apply (not_O_IZR 2); omega. assert (2^Zabs_nat(up(1*/v)) <> 0)%R. apply pow_nonzero;auto. repeat apply prod_neq_R0;auto. simpl; field. destruct (total_order_T (real_value s) r) as [[Hlt1 | Heq] | Hlt2]. assert (r - real_value s <= (r - real_value s)/2)%R. destruct (Happrox (r - real_value s)%R) as [n Hle]. fourier. assert (-1/(2^n) <= r - real_value s <= 1/(2^n))%R. apply represent_diff_2pow_n with s. apply Hrep. apply represents_real_value. decompose [and] H. apply Rle_trans with (1/(2^n))%R;auto. replace r with ((r - real_value s)+real_value s)%R. rewrite (smaller_half_is_zero (r - real_value s)); auto. field. fourier. field. assumption. assert (real_value s -r <= (real_value s - r)/2)%R. destruct (Happrox (real_value s - r)%R) as [n Hle]. fourier. assert (-1/(2^n) <= real_value s - r<= 1/(2^n))%R. apply represent_diff_2pow_n with s. apply represents_real_value. apply Hrep. decompose [and] H. apply Rle_trans with (1/(2^n))%R;auto. replace (real_value s) with ((real_value s - r) + r)%R. rewrite (smaller_half_is_zero (real_value s - r)); auto. field. fourier. field. Qed.