\[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
Test:
Rosa's DopplerBench
Bits:
128 bits
Bits error versus u
Bits error versus v
Bits error versus t1
Time: 6.4 s
Input Error: 8.8
Output Error: 0.1
Log: ⚲
Profile: 🕒
\(\frac{t1}{\left|u + t1\right|} \cdot \frac{-v}{\left|u + t1\right|}\)
  1. Started with
    \[\frac{\left(-t1\right) \cdot v}{\left(t1 + u\right) \cdot \left(t1 + u\right)}\]
    8.8
  2. Using strategy rm
    8.8
  3. Applied add-sqr-sqrt to get
    \[\frac{\left(-t1\right) \cdot v}{\color{red}{\left(t1 + u\right) \cdot \left(t1 + u\right)}} \leadsto \frac{\left(-t1\right) \cdot v}{\color{blue}{{\left(\sqrt{\left(t1 + u\right) \cdot \left(t1 + u\right)}\right)}^2}}\]
    8.8
  4. Applied simplify to get
    \[\frac{\left(-t1\right) \cdot v}{{\color{red}{\left(\sqrt{\left(t1 + u\right) \cdot \left(t1 + u\right)}\right)}}^2} \leadsto \frac{\left(-t1\right) \cdot v}{{\color{blue}{\left(\left|t1 + u\right|\right)}}^2}\]
    5.4
  5. Applied taylor to get
    \[\frac{\left(-t1\right) \cdot v}{{\left(\left|t1 + u\right|\right)}^2} \leadsto \frac{\left(-t1\right) \cdot v}{{\left(\left|u + t1\right|\right)}^2}\]
    5.4
  6. Taylor expanded around 0 to get
    \[\frac{\left(-t1\right) \cdot v}{\color{red}{{\left(\left|u + t1\right|\right)}^2}} \leadsto \frac{\left(-t1\right) \cdot v}{\color{blue}{{\left(\left|u + t1\right|\right)}^2}}\]
    5.4
  7. Applied simplify to get
    \[\frac{\left(-t1\right) \cdot v}{{\left(\left|u + t1\right|\right)}^2} \leadsto \frac{t1}{\left|u + t1\right|} \cdot \frac{-v}{\left|u + t1\right|}\]
    0.1
  8. Applied final simplification

Original test:


(lambda ((u default) (v default) (t1 default))
  #:name "Rosa's DopplerBench"
  (/ (* (- t1) v) (* (+ t1 u) (+ t1 u))))