Average Error: 61.6 → 0.9
Time: 20.5s
Precision: binary64
Cost: 136708
\[-\frac{1}{\frac{\pi}{4}} \cdot \log \left(\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{e^{\frac{\pi}{4} \cdot f} - e^{-\frac{\pi}{4} \cdot f}}\right) \]
\[\begin{array}{l} t_0 := \frac{\pi}{4} \cdot f\\ \mathbf{if}\;t_0 \leq 20:\\ \;\;\;\;\log \left(\frac{{\left(e^{-0.25}\right)}^{\left(\pi \cdot f\right)} + e^{t_0}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, \mathsf{fma}\left({f}^{3}, {\pi}^{3} \cdot 0.005208333333333333, \left({\pi}^{7} \cdot 2.422030009920635 \cdot 10^{-8}\right) \cdot {f}^{7}\right)\right)\right)}\right) \cdot \frac{-4}{\pi}\\ \mathbf{else}:\\ \;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)\\ \end{array} \]
(FPCore (f)
 :precision binary64
 (-
  (*
   (/ 1.0 (/ PI 4.0))
   (log
    (/
     (+ (exp (* (/ PI 4.0) f)) (exp (- (* (/ PI 4.0) f))))
     (- (exp (* (/ PI 4.0) f)) (exp (- (* (/ PI 4.0) f)))))))))
(FPCore (f)
 :precision binary64
 (let* ((t_0 (* (/ PI 4.0) f)))
   (if (<= t_0 20.0)
     (*
      (log
       (/
        (+ (pow (exp -0.25) (* PI f)) (exp t_0))
        (fma
         (pow f 5.0)
         (* (pow PI 5.0) 1.6276041666666666e-5)
         (fma
          (* PI 0.5)
          f
          (fma
           (pow f 3.0)
           (* (pow PI 3.0) 0.005208333333333333)
           (* (* (pow PI 7.0) 2.422030009920635e-8) (pow f 7.0)))))))
      (/ -4.0 PI))
     (* (/ 0.0 PI) (* -4.0 (log (/ 2.0 f)))))))
double code(double f) {
	return -((1.0 / (((double) M_PI) / 4.0)) * log(((exp(((((double) M_PI) / 4.0) * f)) + exp(-((((double) M_PI) / 4.0) * f))) / (exp(((((double) M_PI) / 4.0) * f)) - exp(-((((double) M_PI) / 4.0) * f))))));
}
double code(double f) {
	double t_0 = (((double) M_PI) / 4.0) * f;
	double tmp;
	if (t_0 <= 20.0) {
		tmp = log(((pow(exp(-0.25), (((double) M_PI) * f)) + exp(t_0)) / fma(pow(f, 5.0), (pow(((double) M_PI), 5.0) * 1.6276041666666666e-5), fma((((double) M_PI) * 0.5), f, fma(pow(f, 3.0), (pow(((double) M_PI), 3.0) * 0.005208333333333333), ((pow(((double) M_PI), 7.0) * 2.422030009920635e-8) * pow(f, 7.0))))))) * (-4.0 / ((double) M_PI));
	} else {
		tmp = (0.0 / ((double) M_PI)) * (-4.0 * log((2.0 / f)));
	}
	return tmp;
}
function code(f)
	return Float64(-Float64(Float64(1.0 / Float64(pi / 4.0)) * log(Float64(Float64(exp(Float64(Float64(pi / 4.0) * f)) + exp(Float64(-Float64(Float64(pi / 4.0) * f)))) / Float64(exp(Float64(Float64(pi / 4.0) * f)) - exp(Float64(-Float64(Float64(pi / 4.0) * f))))))))
end
function code(f)
	t_0 = Float64(Float64(pi / 4.0) * f)
	tmp = 0.0
	if (t_0 <= 20.0)
		tmp = Float64(log(Float64(Float64((exp(-0.25) ^ Float64(pi * f)) + exp(t_0)) / fma((f ^ 5.0), Float64((pi ^ 5.0) * 1.6276041666666666e-5), fma(Float64(pi * 0.5), f, fma((f ^ 3.0), Float64((pi ^ 3.0) * 0.005208333333333333), Float64(Float64((pi ^ 7.0) * 2.422030009920635e-8) * (f ^ 7.0))))))) * Float64(-4.0 / pi));
	else
		tmp = Float64(Float64(0.0 / pi) * Float64(-4.0 * log(Float64(2.0 / f))));
	end
	return tmp
end
code[f_] := (-N[(N[(1.0 / N[(Pi / 4.0), $MachinePrecision]), $MachinePrecision] * N[Log[N[(N[(N[Exp[N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision]], $MachinePrecision] + N[Exp[(-N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision])], $MachinePrecision]), $MachinePrecision] / N[(N[Exp[N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision]], $MachinePrecision] - N[Exp[(-N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision])], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision]), $MachinePrecision])
code[f_] := Block[{t$95$0 = N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision]}, If[LessEqual[t$95$0, 20.0], N[(N[Log[N[(N[(N[Power[N[Exp[-0.25], $MachinePrecision], N[(Pi * f), $MachinePrecision]], $MachinePrecision] + N[Exp[t$95$0], $MachinePrecision]), $MachinePrecision] / N[(N[Power[f, 5.0], $MachinePrecision] * N[(N[Power[Pi, 5.0], $MachinePrecision] * 1.6276041666666666e-5), $MachinePrecision] + N[(N[(Pi * 0.5), $MachinePrecision] * f + N[(N[Power[f, 3.0], $MachinePrecision] * N[(N[Power[Pi, 3.0], $MachinePrecision] * 0.005208333333333333), $MachinePrecision] + N[(N[(N[Power[Pi, 7.0], $MachinePrecision] * 2.422030009920635e-8), $MachinePrecision] * N[Power[f, 7.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * N[(-4.0 / Pi), $MachinePrecision]), $MachinePrecision], N[(N[(0.0 / Pi), $MachinePrecision] * N[(-4.0 * N[Log[N[(2.0 / f), $MachinePrecision]], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]]]
-\frac{1}{\frac{\pi}{4}} \cdot \log \left(\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{e^{\frac{\pi}{4} \cdot f} - e^{-\frac{\pi}{4} \cdot f}}\right)
\begin{array}{l}
t_0 := \frac{\pi}{4} \cdot f\\
\mathbf{if}\;t_0 \leq 20:\\
\;\;\;\;\log \left(\frac{{\left(e^{-0.25}\right)}^{\left(\pi \cdot f\right)} + e^{t_0}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, \mathsf{fma}\left({f}^{3}, {\pi}^{3} \cdot 0.005208333333333333, \left({\pi}^{7} \cdot 2.422030009920635 \cdot 10^{-8}\right) \cdot {f}^{7}\right)\right)\right)}\right) \cdot \frac{-4}{\pi}\\

\mathbf{else}:\\
\;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)\\


\end{array}

Error

Derivation

  1. Split input into 2 regimes
  2. if (*.f64 (/.f64 (PI.f64) 4) f) < 20

    1. Initial program 61.6

      \[-\frac{1}{\frac{\pi}{4}} \cdot \log \left(\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{e^{\frac{\pi}{4} \cdot f} - e^{-\frac{\pi}{4} \cdot f}}\right) \]
    2. Simplified61.6

      \[\leadsto \color{blue}{\log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{e^{\frac{\pi \cdot f}{4}} - e^{-0.25 \cdot \left(\pi \cdot f\right)}}\right) \cdot \frac{-4}{\pi}} \]
      Proof
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 4)) (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 (*.f64 (PI.f64) f)))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 (PI.f64) f)) 4)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (PI.f64) f) 4))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 -1 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 4)) (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 (*.f64 (PI.f64) f)))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 (PI.f64) f)) 4)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (PI.f64) f) 4))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 -1 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (/.f64 (Rewrite<= metadata-eval (neg.f64 4)) (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 4 (PI.f64))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1 4)) (PI.f64)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (PI.f64)) 4)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 (PI.f64) 4))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (/.f64 1 (/.f64 (PI.f64) 4))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 (/.f64 (PI.f64) 4)) (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))))))): 0 points increase in error, 0 points decrease in error
    3. Taylor expanded in f around 0 0.7

      \[\leadsto \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{\color{blue}{{f}^{5} \cdot \left(8.138020833333333 \cdot 10^{-6} \cdot {\pi}^{5} - -8.138020833333333 \cdot 10^{-6} \cdot {\pi}^{5}\right) + \left(\left(0.25 \cdot \pi - -0.25 \cdot \pi\right) \cdot f + \left({f}^{3} \cdot \left(0.0026041666666666665 \cdot {\pi}^{3} - -0.0026041666666666665 \cdot {\pi}^{3}\right) + {f}^{7} \cdot \left(1.2110150049603175 \cdot 10^{-8} \cdot {\pi}^{7} - -1.2110150049603175 \cdot 10^{-8} \cdot {\pi}^{7}\right)\right)\right)}}\right) \cdot \frac{-4}{\pi} \]
    4. Applied egg-rr0.7

      \[\leadsto \color{blue}{\left(\log \left(e^{\frac{\pi}{\frac{4}{f}}} + {\left(e^{-0.25}\right)}^{\left(\pi \cdot f\right)}\right) - \log \left(\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, \mathsf{fma}\left({f}^{3}, {\pi}^{3} \cdot 0.005208333333333333, {f}^{7} \cdot \left({\pi}^{7} \cdot 2.422030009920635 \cdot 10^{-8}\right)\right)\right)\right)\right)\right)} \cdot \frac{-4}{\pi} \]
    5. Simplified0.7

      \[\leadsto \color{blue}{\log \left(\frac{{\left(e^{-0.25}\right)}^{\left(\pi \cdot f\right)} + e^{\frac{\pi}{4} \cdot f}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, \mathsf{fma}\left({f}^{3}, {\pi}^{3} \cdot 0.005208333333333333, \left({\pi}^{7} \cdot 2.422030009920635 \cdot 10^{-8}\right) \cdot {f}^{7}\right)\right)\right)}\right)} \cdot \frac{-4}{\pi} \]
      Proof
      (*.f64 (log.f64 (/.f64 (+.f64 (pow.f64 (exp.f64 -1/4) (*.f64 (PI.f64) f)) (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f))) (fma.f64 (pow.f64 f 5) (*.f64 (pow.f64 (PI.f64) 5) 1/61440) (fma.f64 (*.f64 (PI.f64) 1/2) f (fma.f64 (pow.f64 f 3) (*.f64 (pow.f64 (PI.f64) 3) 1/192) (*.f64 (*.f64 (pow.f64 (PI.f64) 7) 1/41287680) (pow.f64 f 7))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (pow.f64 (exp.f64 -1/4) (*.f64 (PI.f64) f)) (exp.f64 (Rewrite<= associate-/r/_binary64 (/.f64 (PI.f64) (/.f64 4 f))))) (fma.f64 (pow.f64 f 5) (*.f64 (pow.f64 (PI.f64) 5) 1/61440) (fma.f64 (*.f64 (PI.f64) 1/2) f (fma.f64 (pow.f64 f 3) (*.f64 (pow.f64 (PI.f64) 3) 1/192) (*.f64 (*.f64 (pow.f64 (PI.f64) 7) 1/41287680) (pow.f64 f 7))))))) (/.f64 -4 (PI.f64))): 1 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (Rewrite<= +-commutative_binary64 (+.f64 (exp.f64 (/.f64 (PI.f64) (/.f64 4 f))) (pow.f64 (exp.f64 -1/4) (*.f64 (PI.f64) f)))) (fma.f64 (pow.f64 f 5) (*.f64 (pow.f64 (PI.f64) 5) 1/61440) (fma.f64 (*.f64 (PI.f64) 1/2) f (fma.f64 (pow.f64 f 3) (*.f64 (pow.f64 (PI.f64) 3) 1/192) (*.f64 (*.f64 (pow.f64 (PI.f64) 7) 1/41287680) (pow.f64 f 7))))))) (/.f64 -4 (PI.f64))): 4 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (/.f64 (PI.f64) (/.f64 4 f))) (pow.f64 (exp.f64 -1/4) (*.f64 (PI.f64) f))) (fma.f64 (pow.f64 f 5) (*.f64 (pow.f64 (PI.f64) 5) 1/61440) (fma.f64 (*.f64 (PI.f64) 1/2) f (fma.f64 (pow.f64 f 3) (*.f64 (pow.f64 (PI.f64) 3) 1/192) (Rewrite<= *-commutative_binary64 (*.f64 (pow.f64 f 7) (*.f64 (pow.f64 (PI.f64) 7) 1/41287680)))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 5 points decrease in error
      (*.f64 (Rewrite=> log-div_binary64 (-.f64 (log.f64 (+.f64 (exp.f64 (/.f64 (PI.f64) (/.f64 4 f))) (pow.f64 (exp.f64 -1/4) (*.f64 (PI.f64) f)))) (log.f64 (fma.f64 (pow.f64 f 5) (*.f64 (pow.f64 (PI.f64) 5) 1/61440) (fma.f64 (*.f64 (PI.f64) 1/2) f (fma.f64 (pow.f64 f 3) (*.f64 (pow.f64 (PI.f64) 3) 1/192) (*.f64 (pow.f64 f 7) (*.f64 (pow.f64 (PI.f64) 7) 1/41287680)))))))) (/.f64 -4 (PI.f64))): 5 points increase in error, 0 points decrease in error

    if 20 < (*.f64 (/.f64 (PI.f64) 4) f)

    1. Initial program 62.2

      \[-\frac{1}{\frac{\pi}{4}} \cdot \log \left(\frac{e^{\frac{\pi}{4} \cdot f} + e^{-\frac{\pi}{4} \cdot f}}{e^{\frac{\pi}{4} \cdot f} - e^{-\frac{\pi}{4} \cdot f}}\right) \]
    2. Simplified62.2

      \[\leadsto \color{blue}{\log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{e^{\frac{\pi \cdot f}{4}} - e^{-0.25 \cdot \left(\pi \cdot f\right)}}\right) \cdot \frac{-4}{\pi}} \]
      Proof
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 4)) (*.f64 (PI.f64) f)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 (*.f64 (PI.f64) f)))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 (PI.f64) f)) 4)))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (PI.f64) f) 4))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 -1 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))) (-.f64 (exp.f64 (/.f64 (*.f64 (PI.f64) f) 4)) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))) (exp.f64 (*.f64 -1/4 (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 (Rewrite<= metadata-eval (/.f64 -1 4)) (*.f64 (PI.f64) f)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/r/_binary64 (/.f64 -1 (/.f64 4 (*.f64 (PI.f64) f)))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-/l*_binary64 (/.f64 (*.f64 -1 (*.f64 (PI.f64) f)) 4)))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= associate-*r/_binary64 (*.f64 -1 (/.f64 (*.f64 (PI.f64) f) 4))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (*.f64 -1 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 (PI.f64) 4) f))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (Rewrite<= neg-mul-1_binary64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))))) (/.f64 -4 (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (/.f64 (Rewrite<= metadata-eval (neg.f64 4)) (PI.f64))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (Rewrite<= distribute-neg-frac_binary64 (neg.f64 (/.f64 4 (PI.f64))))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1 4)) (PI.f64)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (Rewrite<= associate-*l/_binary64 (*.f64 (/.f64 1 (PI.f64)) 4)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (neg.f64 (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 (PI.f64) 4))))): 0 points increase in error, 0 points decrease in error
      (Rewrite<= distribute-rgt-neg-in_binary64 (neg.f64 (*.f64 (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))))) (/.f64 1 (/.f64 (PI.f64) 4))))): 0 points increase in error, 0 points decrease in error
      (neg.f64 (Rewrite<= *-commutative_binary64 (*.f64 (/.f64 1 (/.f64 (PI.f64) 4)) (log.f64 (/.f64 (+.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f)))) (-.f64 (exp.f64 (*.f64 (/.f64 (PI.f64) 4) f)) (exp.f64 (neg.f64 (*.f64 (/.f64 (PI.f64) 4) f))))))))): 0 points increase in error, 0 points decrease in error
    3. Taylor expanded in f around 0 63.4

      \[\leadsto \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{\color{blue}{\left(0.25 \cdot \pi - -0.25 \cdot \pi\right) \cdot f}}\right) \cdot \frac{-4}{\pi} \]
    4. Applied egg-rr63.4

      \[\leadsto \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\log \left(\frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f} + {\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{\pi \cdot \left(0.5 \cdot f\right)}\right)\right)\right)} \cdot \frac{-4}{\pi} \]
    5. Applied egg-rr64.0

      \[\leadsto \color{blue}{\frac{1}{\frac{\pi}{\log \left(\frac{0}{\pi \cdot 0} \cdot \frac{2}{f}\right) \cdot -4}}} \]
    6. Simplified9.0

      \[\leadsto \color{blue}{\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)} \]
      Proof
      (*.f64 (/.f64 0 (PI.f64)) (*.f64 -4 (log.f64 (/.f64 2 f)))): 0 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 (Rewrite<= div0_binary64 (/.f64 0 0)) (PI.f64)) (*.f64 -4 (log.f64 (/.f64 2 f)))): 2 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 (Rewrite=> *-inverses_binary64 1) (PI.f64)) (*.f64 -4 (log.f64 (/.f64 2 f)))): 1 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 1 (PI.f64)) (*.f64 -4 (log.f64 (/.f64 (Rewrite<= metadata-eval (*.f64 1 2)) f)))): 2 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 1 (PI.f64)) (*.f64 -4 (log.f64 (/.f64 (*.f64 (Rewrite<= *-inverses_binary64 (/.f64 0 0)) 2) f)))): 2 points increase in error, 1 points decrease in error
      (*.f64 (/.f64 1 (PI.f64)) (*.f64 -4 (log.f64 (/.f64 (*.f64 (/.f64 0 (Rewrite<= mul0-rgt_binary64 (*.f64 (PI.f64) 0))) 2) f)))): 1 points increase in error, 2 points decrease in error
      (*.f64 (/.f64 1 (PI.f64)) (*.f64 -4 (log.f64 (Rewrite<= associate-*r/_binary64 (*.f64 (/.f64 0 (*.f64 (PI.f64) 0)) (/.f64 2 f)))))): 1 points increase in error, 0 points decrease in error
      (*.f64 (/.f64 1 (PI.f64)) (Rewrite<= *-commutative_binary64 (*.f64 (log.f64 (*.f64 (/.f64 0 (*.f64 (PI.f64) 0)) (/.f64 2 f))) -4))): 0 points increase in error, 1 points decrease in error
      (Rewrite<= associate-/r/_binary64 (/.f64 1 (/.f64 (PI.f64) (*.f64 (log.f64 (*.f64 (/.f64 0 (*.f64 (PI.f64) 0)) (/.f64 2 f))) -4)))): 2 points increase in error, 1 points decrease in error
  3. Recombined 2 regimes into one program.
  4. Final simplification0.9

    \[\leadsto \begin{array}{l} \mathbf{if}\;\frac{\pi}{4} \cdot f \leq 20:\\ \;\;\;\;\log \left(\frac{{\left(e^{-0.25}\right)}^{\left(\pi \cdot f\right)} + e^{\frac{\pi}{4} \cdot f}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, \mathsf{fma}\left({f}^{3}, {\pi}^{3} \cdot 0.005208333333333333, \left({\pi}^{7} \cdot 2.422030009920635 \cdot 10^{-8}\right) \cdot {f}^{7}\right)\right)\right)}\right) \cdot \frac{-4}{\pi}\\ \mathbf{else}:\\ \;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)\\ \end{array} \]

Alternatives

Alternative 1
Error1.0
Cost45892
\[\begin{array}{l} \mathbf{if}\;\frac{\pi}{4} \cdot f \leq 20:\\ \;\;\;\;\mathsf{fma}\left(-4, \frac{\log \left(\frac{4}{\pi}\right) - \log f}{\pi}, -0.08333333333333333 \cdot \left(f \cdot \left(\pi \cdot f\right)\right)\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)\\ \end{array} \]
Alternative 2
Error1.3
Cost26180
\[\begin{array}{l} \mathbf{if}\;f \leq 1.25:\\ \;\;\;\;-4 \cdot \frac{\log \left(\frac{4}{\pi}\right) - \log f}{\pi}\\ \mathbf{else}:\\ \;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)\\ \end{array} \]
Alternative 3
Error1.4
Cost19780
\[\begin{array}{l} \mathbf{if}\;f \leq 1.25:\\ \;\;\;\;\frac{-4}{\pi} \cdot \log \left(\frac{\frac{4}{\pi}}{f}\right)\\ \mathbf{else}:\\ \;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)\\ \end{array} \]
Alternative 4
Error1.3
Cost19780
\[\begin{array}{l} \mathbf{if}\;f \leq 1.25:\\ \;\;\;\;\frac{\frac{\log \left(\frac{4}{\pi \cdot f}\right)}{\pi}}{-0.25}\\ \mathbf{else}:\\ \;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot \log \left(\frac{2}{f}\right)\right)\\ \end{array} \]
Alternative 5
Error42.6
Cost13444
\[\begin{array}{l} t_0 := \log \left(\frac{2}{f}\right)\\ \mathbf{if}\;f \leq 2:\\ \;\;\;\;\frac{4}{\frac{-\pi}{t_0}}\\ \mathbf{else}:\\ \;\;\;\;\frac{0}{\pi} \cdot \left(-4 \cdot t_0\right)\\ \end{array} \]
Alternative 6
Error43.8
Cost13248
\[\frac{4}{\frac{-\pi}{\log \left(\frac{2}{f}\right)}} \]
Alternative 7
Error43.8
Cost13184
\[\frac{\log \left(\frac{2}{f}\right)}{\pi \cdot -0.25} \]
Alternative 8
Error53.0
Cost6720
\[-4 \cdot \log \left(\frac{2}{f}\right) \]

Error

Reproduce

herbie shell --seed 2022343 
(FPCore (f)
  :name "VandenBroeck and Keller, Equation (20)"
  :precision binary64
  (- (* (/ 1.0 (/ PI 4.0)) (log (/ (+ (exp (* (/ PI 4.0) f)) (exp (- (* (/ PI 4.0) f)))) (- (exp (* (/ PI 4.0) f)) (exp (- (* (/ PI 4.0) f)))))))))