Logarithm

Logarithm is defined in terms of artanh. ln (n/d) = 2*artan((n-d)/(n+d))

Lemma lnDomainAdaptor : forall a, (0 < a) ->
(let (n,d) := a in (n - d)/(n + d))^2 < 1.

Although rational_ln_slow works on the entire to domain, it is only efficent for values close 1.
Definition rational_ln_slow (a:Q) (p: 0 < a) : CR :=
 scale 2 (rational_artanh_slow (lnDomainAdaptor p)).

Lemma Qpos_adaptor : forall q, 0 < q -> 0[<]inj_Q IR q.

Lemma rational_ln_slow_correct : forall (a:Q) Ha Ha0,
 (@rational_ln_slow a Ha == IRasCR (Log (inj_Q IR a) Ha0))%CR.

Lemma rational_ln_slow_correct' : forall (a:Q) Ha,
 (@rational_ln_slow a Ha == IRasCR (Log (inj_Q IR a) (Qpos_adaptor Ha)))%CR.

Efficeny of ln is imporved by scaling the input by a power of two and adding or subtracting a multiple of ln 2.
Definition ln2 : CR := rational_ln_slow (pos_two Q_as_COrdField).

Lemma ln2_correct : (ln2 == IRasCR (Log 2 (pos_two IR)))%CR.

Lemma ln_scale_by_two_power_adapt : forall (n:Z) q, 0 < q -> 0 < (2^n*q).

Lemma ln_scale_by_two_power : forall (n:Z) q (Hq:0 < q), (rational_ln_slow Hq + scale n ln2 == rational_ln_slow (ln_scale_by_two_power_adapt n Hq))%CR.

Definition ln_scale_power_factor q (Hq:0 < q) : Z.
Defined.

Definition rational_ln (a:Q) (p: 0 < a) : CR :=
 let n := ln_scale_power_factor p in
 (rational_ln_slow (ln_scale_by_two_power_adapt n p) + scale (-n)%Z ln2)%CR.

Lemma rational_ln_correct : forall (a:Q) Ha Ha0,
 (@rational_ln a Ha == IRasCR (Log (inj_Q IR a) Ha0))%CR.

Lemma rational_ln_correct' : forall (a:Q) Ha,
 (@rational_ln a Ha == IRasCR (Log (inj_Q IR a) (Qpos_adaptor Ha)))%CR.

ln is uniformly continuous on any close strictly positive interval.
Lemma ln_uc_prf_pos : forall (c:Qpos) (x:Q), (0 < Qmax c x).

Definition rational_ln_modulus (c:Qpos) (e:Qpos) : Q+∞ :=
Qpos2QposInf (c*e).

Lemma ln_pos_uc_prf (c:Qpos) : is_UniformlyContinuousFunction (fun x => rational_ln (ln_uc_prf_pos c x)) (rational_ln_modulus c).

Definition ln_pos_uc (c:Qpos) : Q_as_MetricSpace --> CR :=
Build_UniformlyContinuousFunction (@ln_pos_uc_prf c).

Definition CRln_pos (c:Qpos) : CR --> CR := (Cbind QPrelengthSpace (ln_pos_uc c)).

Lemma CRln_pos_correct : forall (c:Qpos) x Hx, [⋅,+∞) (inj_Q _ (c:Q)) x -> (IRasCR (Log x Hx)==CRln_pos c (IRasCR x))%CR.

Definition CRln (x:CR) (Hx:('0 < x)%CR) : CR :=
let (c,_) := Hx in CRln_pos c x.
Lemma CRln_correct : forall x Hx Hx0, (IRasCR (Log x Hx)==CRln (IRasCR x) Hx0)%CR.

Lemma CRln_pos_ln : forall (c:Qpos) (x:CR) Hx,
 ('c <= x ->
  CRln_pos c x == CRln x Hx)%CR.

Lemma CRln_wd : forall (x y:CR) Hx Hy, (x == y -> CRln x Hx == CRln y Hy)%CR.

Lemma CRln_irrelvent : forall x Hx Hx0, (CRln x Hx == CRln x Hx0)%CR.