Section ExpSeries.
Variable a:Q.
Definition expSequence := mult_Streams recip_factorials (powers a).
Lemma Str_nth_expSequence : forall n, (Str_nth n expSequence == (1#P_of_succ_nat (pred (fac n)))*a^n)%Q.
The exponential is first defined on [-1,0].
Hypothesis Ha: 0 <= a <= 1.
Lemma expSequence_dnn : DecreasingNonNegative expSequence.
Lemma expSequence_zl : Limit expSequence 0.
End ExpSeries.
Lemma exp_ps_correct : forall a (n:nat) H,
inj_Q IR ((((-(1))^n)*Str_nth n (expSequence (-a)))%Q)[=]Exp_ps n (inj_Q IR a) H.
Lemma Qle_ZO_flip : forall a, -(1) <= a <= 0 -> 0 <= (-a) <= 1.
Definition rational_exp_small_neg (a:Q) (p:-(1) <= a <= 0) : CR
:= let p':= (Qle_ZO_flip p) in InfiniteAlternatingSum (expSequence_dnn p') (expSequence_zl p').
Lemma rational_exp_small_neg_correct : forall (a:Q) Ha,
(@rational_exp_small_neg a Ha == IRasCR (Exp (inj_Q IR a)))%CR.
Lemma expSequence_dnn : DecreasingNonNegative expSequence.
Lemma expSequence_zl : Limit expSequence 0.
End ExpSeries.
Lemma exp_ps_correct : forall a (n:nat) H,
inj_Q IR ((((-(1))^n)*Str_nth n (expSequence (-a)))%Q)[=]Exp_ps n (inj_Q IR a) H.
Lemma Qle_ZO_flip : forall a, -(1) <= a <= 0 -> 0 <= (-a) <= 1.
Definition rational_exp_small_neg (a:Q) (p:-(1) <= a <= 0) : CR
:= let p':= (Qle_ZO_flip p) in InfiniteAlternatingSum (expSequence_dnn p') (expSequence_zl p').
Lemma rational_exp_small_neg_correct : forall (a:Q) Ha,
(@rational_exp_small_neg a Ha == IRasCR (Exp (inj_Q IR a)))%CR.
exp is extended to work on [-2^n, 0] for all n.
Lemma shrink_by_two : forall n a, (-(2^(S n)))%Z <= a <= 0 -> (-(2^n))%Z <= (a/2) <= 0.
Fixpoint rational_exp_neg_bounded (n:nat) (a:Q) : (-(2^n))%Z <= a <= 0 -> CR :=
match n return (-(2^n))%Z <= a <= 0 -> CR with
| O => @rational_exp_small_neg a
| S n' =>
match (Qlt_le_dec_fast a (-(1))) with
| left _ => fun H => CRpower_positive_bounded 2 (1#1) (compress (rational_exp_neg_bounded n' (shrink_by_two n' H)))
| right H' => fun H => rational_exp_small_neg (conj H' (proj2 H))
end
end.
Fixpoint rational_exp_neg_bounded (n:nat) (a:Q) : (-(2^n))%Z <= a <= 0 -> CR :=
match n return (-(2^n))%Z <= a <= 0 -> CR with
| O => @rational_exp_small_neg a
| S n' =>
match (Qlt_le_dec_fast a (-(1))) with
| left _ => fun H => CRpower_positive_bounded 2 (1#1) (compress (rational_exp_neg_bounded n' (shrink_by_two n' H)))
| right H' => fun H => rational_exp_small_neg (conj H' (proj2 H))
end
end.
exp works on all nonpositive numbers.
Lemma rational_exp_neg_bounded_correct : forall n (a:Q) Ha,
(@rational_exp_neg_bounded n a Ha == IRasCR (Exp (inj_Q IR a)))%CR.
Lemma rational_exp_bound_power_2 : forall (a:Q), a <= 0 -> (-2^(Z_of_nat match (Qnum a) with |Z0 => O | Zpos x => Psize x | Zneg x => Psize x end))%Z <= a.
Definition rational_exp_neg (a:Q) : a <= 0 -> CR.
Defined.
Lemma rational_exp_neg_correct : forall (a:Q) Ha,
(@rational_exp_neg a Ha == IRasCR (Exp (inj_Q IR a)))%CR.
(@rational_exp_neg_bounded n a Ha == IRasCR (Exp (inj_Q IR a)))%CR.
Lemma rational_exp_bound_power_2 : forall (a:Q), a <= 0 -> (-2^(Z_of_nat match (Qnum a) with |Z0 => O | Zpos x => Psize x | Zneg x => Psize x end))%Z <= a.
Definition rational_exp_neg (a:Q) : a <= 0 -> CR.
Defined.
Lemma rational_exp_neg_correct : forall (a:Q) Ha,
(@rational_exp_neg a Ha == IRasCR (Exp (inj_Q IR a)))%CR.
exp(x) is bounded below by (3^x) for x nonpositive, and hence
exp(x) is positive.
Lemma minus_one_works_for_rational_exp_small_neg : -(1) <= -(1) <= 0.
Lemma rational_exp_small_neg_posH : forall (a:Q) (p:-(1) <= a <= 0),
('(1#3) <= rational_exp_small_neg p)%CR.
Lemma rational_exp_neg_posH : forall (n:nat) (a:Q) Ha, (-n <= a) ->
('((1#3)^n) <= @rational_exp_neg a Ha)%CR.
Lemma rational_exp_neg_posH' : forall (a:Q) Ha,
('((3#1)^(Zdiv (Qnum a) (Qden a)))%Qpos <= @rational_exp_neg a Ha)%CR.
Lemma rational_exp_neg_pos : forall (a:Q) Ha,
CRpos (@rational_exp_neg a Ha).
Lemma rational_exp_small_neg_posH : forall (a:Q) (p:-(1) <= a <= 0),
('(1#3) <= rational_exp_small_neg p)%CR.
Lemma rational_exp_neg_posH : forall (n:nat) (a:Q) Ha, (-n <= a) ->
('((1#3)^n) <= @rational_exp_neg a Ha)%CR.
Lemma rational_exp_neg_posH' : forall (a:Q) Ha,
('((3#1)^(Zdiv (Qnum a) (Qden a)))%Qpos <= @rational_exp_neg a Ha)%CR.
Lemma rational_exp_neg_pos : forall (a:Q) Ha,
CRpos (@rational_exp_neg a Ha).
exp is extended to all numbers by saying exp(x) = 1/exp(-x) when x
is positive.
Definition rational_exp (a:Q) : CR.
Defined.
Lemma rational_exp_correct : forall (a:Q),
(rational_exp a == IRasCR (Exp (inj_Q IR a)))%CR.
Defined.
Lemma rational_exp_correct : forall (a:Q),
(rational_exp a == IRasCR (Exp (inj_Q IR a)))%CR.
exp is uniformly continuous below any given integer.
Definition exp_bound (z:Z) : Q+ :=
(match z with
|Z0 => 1#1
|Zpos p => (3#1)^p
|Zneg p => (1#2)^p
end)%Qpos.
Lemma exp_bound_bound : forall (z:Z) x, (-∞,⋅] (inj_Q IR (z:Q)) x -> AbsIR (Exp x)[<=]inj_Q IR (exp_bound z:Q).
Lemma exp_bound_uc_prf : forall z:Z, is_UniformlyContinuousFunction (fun a => rational_exp (Qmin z a)) (Qscale_modulus (exp_bound z)).
Included.
Qed.
Definition exp_bound_uc (z:Z) : Q_as_MetricSpace --> CR :=
Build_UniformlyContinuousFunction (@exp_bound_uc_prf z).
(match z with
|Z0 => 1#1
|Zpos p => (3#1)^p
|Zneg p => (1#2)^p
end)%Qpos.
Lemma exp_bound_bound : forall (z:Z) x, (-∞,⋅] (inj_Q IR (z:Q)) x -> AbsIR (Exp x)[<=]inj_Q IR (exp_bound z:Q).
Lemma exp_bound_uc_prf : forall z:Z, is_UniformlyContinuousFunction (fun a => rational_exp (Qmin z a)) (Qscale_modulus (exp_bound z)).
Included.
Qed.
Definition exp_bound_uc (z:Z) : Q_as_MetricSpace --> CR :=
Build_UniformlyContinuousFunction (@exp_bound_uc_prf z).
exp for any real number upto a given integer.
Definition exp_bounded (z:Z) : CR --> CR := (Cbind QPrelengthSpace (exp_bound_uc z)).
Lemma exp_bounded_correct : forall (z:Z) x, (-∞,⋅] (inj_Q _ (z:Q)) x -> (IRasCR (Exp x)==exp_bounded z (IRasCR x))%CR.
Included.
Qed.
Lemma exp_bounded_correct : forall (z:Z) x, (-∞,⋅] (inj_Q _ (z:Q)) x -> (IRasCR (Exp x)==exp_bounded z (IRasCR x))%CR.
Included.
Qed.
exp on all real numbers. exp_bounded should be used instead when x
is known to be bounded by some intenger.
Definition exp (x:CR) : CR := exp_bounded (Qceiling (approximate x ((1#1)%Qpos) + (1#1))) x.
Lemma exp_bound_lemma : forall x : CR, (x <= ' (approximate x (1 # 1)%Qpos + 1))%CR.
Lemma exp_correct : forall x, (IRasCR (Exp x)==exp (IRasCR x))%CR.
Lemma exp_bound_exp : forall (z:Z) (x:CR),
(x <= 'z ->
exp_bounded z x == exp x)%CR.
Lemma exp_Qexp : forall x : Q, (exp (' x) == rational_exp x)%CR.
Lemma exp_bound_lemma : forall x : CR, (x <= ' (approximate x (1 # 1)%Qpos + 1))%CR.
Lemma exp_correct : forall x, (IRasCR (Exp x)==exp (IRasCR x))%CR.
Lemma exp_bound_exp : forall (z:Z) (x:CR),
(x <= 'z ->
exp_bounded z x == exp x)%CR.
Lemma exp_Qexp : forall x : Q, (exp (' x) == rational_exp x)%CR.