Positive Integer Powers
Positive integer powers is faster than repeated multiplication.It is uniformly continuous on an interval [-c,c].
Section CRpower_positive.
Variable p: positive.
Definition Qpower_positive_modulus (c:Qpos) (e:Qpos) : Q+∞ :=
Qpos2QposInf (e/((p#1)*c^(Zpred p))).
Lemma Qpower_positive_correct : forall p q, (inj_Q IR (Qpower_positive q p)[=]((FId{^}(nat_of_P p)) (inj_Q IR q) CI)).
Let IRpower_p : PartFunct IR := FId{^}(nat_of_P p).
Lemma Qpower_positive_uc_prf (c:Qpos) : is_UniformlyContinuousFunction (fun x => Qpower_positive (QboundAbs c x) p) (Qpower_positive_modulus c).
Definition Qpower_positive_uc (c:Qpos) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (Qpower_positive_uc_prf c).
Variable p: positive.
Definition Qpower_positive_modulus (c:Qpos) (e:Qpos) : Q+∞ :=
Qpos2QposInf (e/((p#1)*c^(Zpred p))).
Lemma Qpower_positive_correct : forall p q, (inj_Q IR (Qpower_positive q p)[=]((FId{^}(nat_of_P p)) (inj_Q IR q) CI)).
Let IRpower_p : PartFunct IR := FId{^}(nat_of_P p).
Lemma Qpower_positive_uc_prf (c:Qpos) : is_UniformlyContinuousFunction (fun x => Qpower_positive (QboundAbs c x) p) (Qpower_positive_modulus c).
Definition Qpower_positive_uc (c:Qpos) : Q_as_MetricSpace --> Q_as_MetricSpace :=
Build_UniformlyContinuousFunction (Qpower_positive_uc_prf c).
CRpower_positive_bounded works on [-c,c].
Definition CRpower_positive_bounded (c:Qpos) : CR --> CR :=
Cmap QPrelengthSpace (Qpower_positive_uc c).
Lemma CRpower_positive_bounded_correct : forall (c:Qpos) x, AbsSmall (inj_Q _ (c:Q)) x -> (IRasCR (x[^](nat_of_P p))==CRpower_positive_bounded c (IRasCR x))%CR.
Lemma CRpower_positive_bounded_weaken : forall (c1 c2:Qpos) x,
((AbsSmall ('c1) x) -> (c1 <= c2)%Q ->
CRpower_positive_bounded c1 x == CRpower_positive_bounded c2 x)%CR.
Cmap QPrelengthSpace (Qpower_positive_uc c).
Lemma CRpower_positive_bounded_correct : forall (c:Qpos) x, AbsSmall (inj_Q _ (c:Q)) x -> (IRasCR (x[^](nat_of_P p))==CRpower_positive_bounded c (IRasCR x))%CR.
Lemma CRpower_positive_bounded_weaken : forall (c1 c2:Qpos) x,
((AbsSmall ('c1) x) -> (c1 <= c2)%Q ->
CRpower_positive_bounded c1 x == CRpower_positive_bounded c2 x)%CR.
CRpower_positive_bounded is should be used when a known bound
on the absolute value of x is available.
Definition CRpower_positive (x:CR) : CR := ucFun (CRpower_positive_bounded (CR_b (1#1) x)) x.
Lemma CRpositive_power_bounded_positive_power : forall (c:Qpos) (x:CR),
((AbsSmall ('c) x) ->
CRpower_positive_bounded c x == CRpower_positive x)%CR.
Lemma CRpower_positive_correct : forall x, (IRasCR (x[^](nat_of_P p))==CRpower_positive (IRasCR x))%CR.
End CRpower_positive.
Lemma CRpower_positive_correct' : forall n x,
(IRasCR (x[^]S n)==CRpower_positive (P_of_succ_nat n) (IRasCR x))%CR.
Lemma CRpositive_power_bounded_positive_power : forall (c:Qpos) (x:CR),
((AbsSmall ('c) x) ->
CRpower_positive_bounded c x == CRpower_positive x)%CR.
Lemma CRpower_positive_correct : forall x, (IRasCR (x[^](nat_of_P p))==CRpower_positive (IRasCR x))%CR.
End CRpower_positive.
Lemma CRpower_positive_correct' : forall n x,
(IRasCR (x[^]S n)==CRpower_positive (P_of_succ_nat n) (IRasCR x))%CR.