Compression
Compress improves the compuation by reducing the size of the numerator and denominator of rational numbers. It works by increasing the requested precession, but then rounding the result to a value with a small numerator and denominator.The full euclidean algortihm would find the optimial rational approximation. But for speed we simply do division to quickly find a good rational approximation.
Definition approximateQ (x:Q) (p:positive) :=
let (n,d) := x in (Zdiv (n*p) d#p).
Lemma approximateQ_correct : forall x p, ball (1#p) x (approximateQ x p).
Lemma approximateQ_big : forall (z:Z) a p, (z <= a) -> z <= approximateQ a p.
let (n,d) := x in (Zdiv (n*p) d#p).
Lemma approximateQ_correct : forall x p, ball (1#p) x (approximateQ x p).
Lemma approximateQ_big : forall (z:Z) a p, (z <= a) -> z <= approximateQ a p.
Compress doubles the requried precision and uses the extra leway to
round the rational number.
Definition compress_raw (x:CR) (e:QposInf) : Q :=
match e with
| ∞ => approximate x e
| Qpos2QposInf e =>
let (n,d) := e in
match (Zsucc (Zdiv (2*d) n)) with
Zpos p => approximateQ (approximate x (Qpos2QposInf (1#p))) p
|_ => approximate x e
end
end.
Lemma compress_raw_prop : forall x e, ball e x (Cunit (compress_raw x e)).
Lemma compress_raw_prf : forall x, is_RegularFunction (compress_raw x).
Definition compress_fun (x:CR) : CR :=
Build_RegularFunction (compress_raw_prf x).
match e with
| ∞ => approximate x e
| Qpos2QposInf e =>
let (n,d) := e in
match (Zsucc (Zdiv (2*d) n)) with
Zpos p => approximateQ (approximate x (Qpos2QposInf (1#p))) p
|_ => approximate x e
end
end.
Lemma compress_raw_prop : forall x e, ball e x (Cunit (compress_raw x e)).
Lemma compress_raw_prf : forall x, is_RegularFunction (compress_raw x).
Definition compress_fun (x:CR) : CR :=
Build_RegularFunction (compress_raw_prf x).
Compress is equivalent to the identity function.
Lemma compress_fun_correct : forall x, (compress_fun x==x)%CR.
Lemma compress_uc : is_UniformlyContinuousFunction compress_fun Qpos2QposInf.
Definition compress : CR --> CR :=
Build_UniformlyContinuousFunction compress_uc.
Lemma compress_correct : forall x, (compress x==x)%CR.
Lemma compress_uc : is_UniformlyContinuousFunction compress_fun Qpos2QposInf.
Definition compress : CR --> CR :=
Build_UniformlyContinuousFunction compress_uc.
Lemma compress_correct : forall x, (compress x==x)%CR.