Average Error: 61.8 → 1.0
Time: 20.4s
Precision: binary64
Cost: 110788
\[-\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} \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}{\frac{4}{f}}}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, {\pi}^{3} \cdot \left(0.005208333333333333 \cdot {f}^{3}\right)\right)\right)}\right) \cdot \frac{-4}{\pi}\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \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
 (if (<= (* (/ PI 4.0) f) 20.0)
   (*
    (log
     (/
      (+ (pow (exp -0.25) (* PI f)) (exp (/ PI (/ 4.0 f))))
      (fma
       (pow f 5.0)
       (* (pow PI 5.0) 1.6276041666666666e-5)
       (fma
        (* PI 0.5)
        f
        (* (pow PI 3.0) (* 0.005208333333333333 (pow f 3.0)))))))
    (/ -4.0 PI))
   (* -4.0 (/ 0.0 PI))))
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 tmp;
	if (((((double) M_PI) / 4.0) * f) <= 20.0) {
		tmp = log(((pow(exp(-0.25), (((double) M_PI) * f)) + exp((((double) M_PI) / (4.0 / f)))) / fma(pow(f, 5.0), (pow(((double) M_PI), 5.0) * 1.6276041666666666e-5), fma((((double) M_PI) * 0.5), f, (pow(((double) M_PI), 3.0) * (0.005208333333333333 * pow(f, 3.0))))))) * (-4.0 / ((double) M_PI));
	} else {
		tmp = -4.0 * (0.0 / ((double) M_PI));
	}
	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)
	tmp = 0.0
	if (Float64(Float64(pi / 4.0) * f) <= 20.0)
		tmp = Float64(log(Float64(Float64((exp(-0.25) ^ Float64(pi * f)) + exp(Float64(pi / Float64(4.0 / f)))) / fma((f ^ 5.0), Float64((pi ^ 5.0) * 1.6276041666666666e-5), fma(Float64(pi * 0.5), f, Float64((pi ^ 3.0) * Float64(0.005208333333333333 * (f ^ 3.0))))))) * Float64(-4.0 / pi));
	else
		tmp = Float64(-4.0 * Float64(0.0 / pi));
	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_] := If[LessEqual[N[(N[(Pi / 4.0), $MachinePrecision] * f), $MachinePrecision], 20.0], N[(N[Log[N[(N[(N[Power[N[Exp[-0.25], $MachinePrecision], N[(Pi * f), $MachinePrecision]], $MachinePrecision] + N[Exp[N[(Pi / N[(4.0 / f), $MachinePrecision]), $MachinePrecision]], $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[Pi, 3.0], $MachinePrecision] * N[(0.005208333333333333 * N[Power[f, 3.0], $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]), $MachinePrecision]], $MachinePrecision] * N[(-4.0 / Pi), $MachinePrecision]), $MachinePrecision], N[(-4.0 * N[(0.0 / Pi), $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}
\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}{\frac{4}{f}}}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, {\pi}^{3} \cdot \left(0.005208333333333333 \cdot {f}^{3}\right)\right)\right)}\right) \cdot \frac{-4}{\pi}\\

\mathbf{else}:\\
\;\;\;\;-4 \cdot \frac{0}{\pi}\\


\end{array}

Error

Derivation

  1. Split input into 2 regimes

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

    1. Initial program 61.8

      \[-\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.8

      \[\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

      [Start]61.8

      \[ -\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) \]

      *-commutative [=>]61.8

      \[ -\color{blue}{\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) \cdot \frac{1}{\frac{\pi}{4}}} \]

      distribute-rgt-neg-in [=>]61.8

      \[ \color{blue}{\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) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right)} \]

      associate-*l/ [=>]61.8

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

      neg-mul-1 [=>]61.8

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

      associate-*l/ [=>]61.8

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

      associate-*r/ [=>]61.8

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

      associate-/l* [=>]61.8

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

      associate-/r/ [=>]61.8

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

      metadata-eval [=>]61.8

      \[ \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{\color{blue}{-0.25} \cdot \left(\pi \cdot f\right)}}{e^{\frac{\pi}{4} \cdot f} - e^{-\frac{\pi}{4} \cdot f}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-*l/ [=>]61.8

      \[ \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{e^{\color{blue}{\frac{\pi \cdot f}{4}}} - e^{-\frac{\pi}{4} \cdot f}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      neg-mul-1 [=>]61.8

      \[ \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^{\color{blue}{-1 \cdot \left(\frac{\pi}{4} \cdot f\right)}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-*l/ [=>]61.8

      \[ \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^{-1 \cdot \color{blue}{\frac{\pi \cdot f}{4}}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-*r/ [=>]61.8

      \[ \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^{\color{blue}{\frac{-1 \cdot \left(\pi \cdot f\right)}{4}}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-/l* [=>]61.8

      \[ \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^{\color{blue}{\frac{-1}{\frac{4}{\pi \cdot f}}}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-/r/ [=>]61.8

      \[ \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^{\color{blue}{\frac{-1}{4} \cdot \left(\pi \cdot f\right)}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      metadata-eval [=>]61.8

      \[ \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^{\color{blue}{-0.25} \cdot \left(\pi \cdot f\right)}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      distribute-neg-frac [=>]61.8

      \[ \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 \color{blue}{\frac{-1}{\frac{\pi}{4}}} \]

      metadata-eval [=>]61.8

      \[ \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{\color{blue}{-1}}{\frac{\pi}{4}} \]

      associate-/r/ [=>]61.8

      \[ \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 \color{blue}{\left(\frac{-1}{\pi} \cdot 4\right)} \]

      associate-*l/ [=>]61.8

      \[ \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 \color{blue}{\frac{-1 \cdot 4}{\pi}} \]

      metadata-eval [=>]61.8

      \[ \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{\color{blue}{-4}}{\pi} \]

    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 + {f}^{3} \cdot \left(0.0026041666666666665 \cdot {\pi}^{3} - -0.0026041666666666665 \cdot {\pi}^{3}\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, {f}^{3} \cdot \left({\pi}^{3} \cdot 0.005208333333333333\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}{\frac{4}{f}}}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, {\pi}^{3} \cdot \left(0.005208333333333333 \cdot {f}^{3}\right)\right)\right)}\right)} \cdot \frac{-4}{\pi} \]
      Proof

      [Start]0.7

      \[ \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, {f}^{3} \cdot \left({\pi}^{3} \cdot 0.005208333333333333\right)\right)\right)\right)\right) \cdot \frac{-4}{\pi} \]

      log-div [<=]0.7

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

      +-commutative [=>]0.7

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

      *-commutative [=>]0.7

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

      associate-*l* [=>]0.7

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

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

    1. Initial program 62.7

      \[-\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.7

      \[\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

      [Start]62.7

      \[ -\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) \]

      *-commutative [=>]62.7

      \[ -\color{blue}{\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) \cdot \frac{1}{\frac{\pi}{4}}} \]

      distribute-rgt-neg-in [=>]62.7

      \[ \color{blue}{\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) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right)} \]

      associate-*l/ [=>]62.7

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

      neg-mul-1 [=>]62.7

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

      associate-*l/ [=>]62.7

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

      associate-*r/ [=>]62.7

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

      associate-/l* [=>]62.7

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

      associate-/r/ [=>]62.7

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

      metadata-eval [=>]62.7

      \[ \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{\color{blue}{-0.25} \cdot \left(\pi \cdot f\right)}}{e^{\frac{\pi}{4} \cdot f} - e^{-\frac{\pi}{4} \cdot f}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-*l/ [=>]62.7

      \[ \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{e^{\color{blue}{\frac{\pi \cdot f}{4}}} - e^{-\frac{\pi}{4} \cdot f}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      neg-mul-1 [=>]62.7

      \[ \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^{\color{blue}{-1 \cdot \left(\frac{\pi}{4} \cdot f\right)}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-*l/ [=>]62.7

      \[ \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^{-1 \cdot \color{blue}{\frac{\pi \cdot f}{4}}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-*r/ [=>]62.7

      \[ \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^{\color{blue}{\frac{-1 \cdot \left(\pi \cdot f\right)}{4}}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-/l* [=>]62.7

      \[ \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^{\color{blue}{\frac{-1}{\frac{4}{\pi \cdot f}}}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      associate-/r/ [=>]62.7

      \[ \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^{\color{blue}{\frac{-1}{4} \cdot \left(\pi \cdot f\right)}}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      metadata-eval [=>]62.7

      \[ \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^{\color{blue}{-0.25} \cdot \left(\pi \cdot f\right)}}\right) \cdot \left(-\frac{1}{\frac{\pi}{4}}\right) \]

      distribute-neg-frac [=>]62.7

      \[ \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 \color{blue}{\frac{-1}{\frac{\pi}{4}}} \]

      metadata-eval [=>]62.7

      \[ \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{\color{blue}{-1}}{\frac{\pi}{4}} \]

      associate-/r/ [=>]62.7

      \[ \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 \color{blue}{\left(\frac{-1}{\pi} \cdot 4\right)} \]

      associate-*l/ [=>]62.7

      \[ \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 \color{blue}{\frac{-1 \cdot 4}{\pi}} \]

      metadata-eval [=>]62.7

      \[ \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{\color{blue}{-4}}{\pi} \]

    3. Taylor expanded in f around 0 63.1

      \[\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-rr64.0

      \[\leadsto \color{blue}{e^{\mathsf{log1p}\left(\log \left({\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)}^{\left(\frac{-4}{\pi}\right)}\right)\right)} - 1} \]

    5. Simplified63.1

      \[\leadsto \color{blue}{-4 \cdot \frac{\log \left(\frac{4}{\pi} \cdot \frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{f}\right)}{\pi}} \]
      Proof

      [Start]64.0

      \[ e^{\mathsf{log1p}\left(\log \left({\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)}^{\left(\frac{-4}{\pi}\right)}\right)\right)} - 1 \]

      expm1-def [=>]64.0

      \[ \color{blue}{\mathsf{expm1}\left(\mathsf{log1p}\left(\log \left({\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)}^{\left(\frac{-4}{\pi}\right)}\right)\right)\right)} \]

      expm1-log1p [=>]63.1

      \[ \color{blue}{\log \left({\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)}^{\left(\frac{-4}{\pi}\right)}\right)} \]

      log-pow [=>]63.1

      \[ \color{blue}{\frac{-4}{\pi} \cdot \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)} \]

      associate-*l/ [=>]63.1

      \[ \color{blue}{\frac{-4 \cdot \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)}{\pi}} \]

      *-commutative [<=]63.1

      \[ \frac{\color{blue}{\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) \cdot -4}}{\pi} \]

      /-rgt-identity [<=]63.1

      \[ \frac{\color{blue}{\frac{\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) \cdot -4}{1}}}{\pi} \]

      associate-/l* [=>]63.1

      \[ \frac{\color{blue}{\frac{\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)}{\frac{1}{-4}}}}{\pi} \]

      metadata-eval [=>]63.1

      \[ \frac{\frac{\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)}{\color{blue}{-0.25}}}{\pi} \]

      associate-/r* [<=]63.1

      \[ \color{blue}{\frac{\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)}{-0.25 \cdot \pi}} \]

      *-lft-identity [<=]63.1

      \[ \frac{\color{blue}{1 \cdot \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)}}{-0.25 \cdot \pi} \]

      times-frac [=>]63.1

      \[ \color{blue}{\frac{1}{-0.25} \cdot \frac{\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)}{\pi}} \]

      metadata-eval [=>]63.1

      \[ \color{blue}{-4} \cdot \frac{\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)}{\pi} \]

      count-2 [=>]63.1

      \[ -4 \cdot \frac{\log \left(\frac{\color{blue}{2 \cdot {\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}}{\pi \cdot \left(0.5 \cdot f\right)}\right)}{\pi} \]

      associate-*r* [=>]63.1

      \[ -4 \cdot \frac{\log \left(\frac{2 \cdot {\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{\color{blue}{\left(\pi \cdot 0.5\right) \cdot f}}\right)}{\pi} \]

      metadata-eval [<=]63.1

      \[ -4 \cdot \frac{\log \left(\frac{2 \cdot {\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{\left(\pi \cdot \color{blue}{\left(0.25 - -0.25\right)}\right) \cdot f}\right)}{\pi} \]

      distribute-rgt-out-- [<=]63.1

      \[ -4 \cdot \frac{\log \left(\frac{2 \cdot {\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{\color{blue}{\left(0.25 \cdot \pi - -0.25 \cdot \pi\right)} \cdot f}\right)}{\pi} \]

      times-frac [=>]63.1

      \[ -4 \cdot \frac{\log \color{blue}{\left(\frac{2}{0.25 \cdot \pi - -0.25 \cdot \pi} \cdot \frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{f}\right)}}{\pi} \]

      distribute-rgt-out-- [=>]63.1

      \[ -4 \cdot \frac{\log \left(\frac{2}{\color{blue}{\pi \cdot \left(0.25 - -0.25\right)}} \cdot \frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{f}\right)}{\pi} \]

      metadata-eval [=>]63.1

      \[ -4 \cdot \frac{\log \left(\frac{2}{\pi \cdot \color{blue}{0.5}} \cdot \frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{f}\right)}{\pi} \]

      *-commutative [=>]63.1

      \[ -4 \cdot \frac{\log \left(\frac{2}{\color{blue}{0.5 \cdot \pi}} \cdot \frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{f}\right)}{\pi} \]

      associate-/r* [=>]63.1

      \[ -4 \cdot \frac{\log \left(\color{blue}{\frac{\frac{2}{0.5}}{\pi}} \cdot \frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{f}\right)}{\pi} \]

      metadata-eval [=>]63.1

      \[ -4 \cdot \frac{\log \left(\frac{\color{blue}{4}}{\pi} \cdot \frac{{\left({\left(e^{0.25}\right)}^{\pi}\right)}^{f}}{f}\right)}{\pi} \]

    6. Taylor expanded in f around 0 61.5

      \[\leadsto -4 \cdot \frac{\log \color{blue}{\left(1 + 4 \cdot \frac{1}{f \cdot \pi}\right)}}{\pi} \]

    7. Simplified61.5

      \[\leadsto -4 \cdot \frac{\log \color{blue}{\left(1 + \frac{\frac{4}{\pi}}{f}\right)}}{\pi} \]
      Proof

      [Start]61.5

      \[ -4 \cdot \frac{\log \left(1 + 4 \cdot \frac{1}{f \cdot \pi}\right)}{\pi} \]

      *-commutative [<=]61.5

      \[ -4 \cdot \frac{\log \left(1 + 4 \cdot \frac{1}{\color{blue}{\pi \cdot f}}\right)}{\pi} \]

      associate-*r/ [=>]61.5

      \[ -4 \cdot \frac{\log \left(1 + \color{blue}{\frac{4 \cdot 1}{\pi \cdot f}}\right)}{\pi} \]

      metadata-eval [=>]61.5

      \[ -4 \cdot \frac{\log \left(1 + \frac{\color{blue}{4}}{\pi \cdot f}\right)}{\pi} \]

      associate-/r* [=>]61.5

      \[ -4 \cdot \frac{\log \left(1 + \color{blue}{\frac{\frac{4}{\pi}}{f}}\right)}{\pi} \]

    8. Taylor expanded in f around inf 13.1

      \[\leadsto -4 \cdot \frac{\log \color{blue}{1}}{\pi} \]
  3. Recombined 2 regimes into one program.

  4. Final simplification1.0

    \[\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}{\frac{4}{f}}}}{\mathsf{fma}\left({f}^{5}, {\pi}^{5} \cdot 1.6276041666666666 \cdot 10^{-5}, \mathsf{fma}\left(\pi \cdot 0.5, f, {\pi}^{3} \cdot \left(0.005208333333333333 \cdot {f}^{3}\right)\right)\right)}\right) \cdot \frac{-4}{\pi}\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]

Alternatives

Alternative 1
Error1.1
Cost91908
\[\begin{array}{l} t_0 := {\pi}^{3} \cdot -0.0026041666666666665\\ \mathbf{if}\;\frac{\pi}{4} \cdot f \leq 20:\\ \;\;\;\;\frac{-4}{\pi} \cdot \log \left(\frac{e^{\frac{\pi \cdot f}{4}} + e^{-0.25 \cdot \left(\pi \cdot f\right)}}{f \cdot \left(\pi \cdot 0.25 + \pi \cdot 0.25\right) - {f}^{3} \cdot \left(t_0 + t_0\right)}\right)\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]
Alternative 2
Error1.1
Cost72068
\[\begin{array}{l} \mathbf{if}\;\frac{\pi}{4} \cdot f \leq 20:\\ \;\;\;\;\mathsf{fma}\left(-4, \frac{\log \left(\frac{\frac{4}{f}}{\pi}\right)}{\pi}, \mathsf{fma}\left(-2, \frac{f \cdot f}{\pi} \cdot \mathsf{fma}\left(0.5, {\pi}^{2} \cdot 0.08333333333333333, 0\right), f \cdot \frac{0}{\pi}\right)\right)\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]
Alternative 3
Error1.0
Cost52676
\[\begin{array}{l} \mathbf{if}\;f \leq 225:\\ \;\;\;\;\frac{-4}{\pi} \cdot \left(\left(\log \left(\frac{4}{\pi}\right) - \log f\right) + \mathsf{fma}\left(0.5 \cdot \left(f \cdot f\right), \mathsf{fma}\left(0.5, {\pi}^{2} \cdot 0.08333333333333333, 0\right), f \cdot 0\right)\right)\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]
Alternative 4
Error1.3
Cost39428
\[\begin{array}{l} \mathbf{if}\;f \leq 225:\\ \;\;\;\;\frac{-4}{\pi} \cdot \log \left(\frac{\frac{4}{\pi}}{f} + 0.125 \cdot \frac{f \cdot {\pi}^{2}}{\pi}\right)\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]
Alternative 5
Error1.3
Cost19780
\[\begin{array}{l} \mathbf{if}\;f \leq 1.3:\\ \;\;\;\;-4 \cdot \frac{\log \left(\frac{\frac{4}{\pi}}{f}\right)}{\pi}\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]
Alternative 6
Error42.7
Cost13316
\[\begin{array}{l} \mathbf{if}\;f \leq 2:\\ \;\;\;\;\frac{\log \left(\frac{2}{f}\right)}{\pi \cdot -0.25}\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]
Alternative 7
Error51.8
Cost6852
\[\begin{array}{l} \mathbf{if}\;f \leq 2:\\ \;\;\;\;-4 \cdot \log \left(\frac{2}{f}\right)\\ \mathbf{else}:\\ \;\;\;\;-4 \cdot \frac{0}{\pi}\\ \end{array} \]
Alternative 8
Error53.0
Cost6720
\[-4 \cdot \log \left(\frac{2}{f}\right) \]
Alternative 9
Error60.6
Cost320
\[-4 \cdot \left(f \cdot 0.25\right) \]

Error

Reproduce

herbie shell --seed 2022356 
(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)))))))))