Initial program 29.4
\[\log \left(N + 1\right) - \log N
\]
Simplified29.4
\[\leadsto \color{blue}{\mathsf{log1p}\left(N\right) - \log N}
\]
Proof
(-.f64 (log1p.f64 N) (log.f64 N)): 0 points increase in error, 0 points decrease in error
(-.f64 (Rewrite<= log1p-def_binary64 (log.f64 (+.f64 1 N))) (log.f64 N)): 0 points increase in error, 0 points decrease in error
(-.f64 (log.f64 (Rewrite<= +-commutative_binary64 (+.f64 N 1))) (log.f64 N)): 0 points increase in error, 0 points decrease in error
Applied egg-rr29.2
\[\leadsto \color{blue}{\log \left(\frac{N + 1}{N}\right)}
\]
Taylor expanded in N around 0 29.3
\[\leadsto \log \color{blue}{\left(1 + \frac{1}{N}\right)}
\]
Applied egg-rr0.0
\[\leadsto \color{blue}{\mathsf{log1p}\left(\frac{1}{N}\right)}
\]
Final simplification0.0
\[\leadsto \mathsf{log1p}\left(\frac{1}{N}\right)
\]