log_taylor_error_bound
plain-language theorem explainer
A concrete truncation error bound for the Taylor series of log(1 + x) on the real line when |x| < 1 is supplied by this lemma. Interval-arithmetic routines for computing log bounds on intervals inside (0, ∞) cite it to guarantee enclosure. The argument lifts the real input to complex, invokes the complex-norm version of the remainder estimate, extracts the real part, and reduces the norm back to the real absolute value.
Claim. For all real $x$ with $|x| < 1$ and natural number $n$, $|log(1 + x) - Re(logTaylor_{n+1}(x))| ≤ |x|^{n+1} / ((n+1)(1 - |x|))$, where logTaylor_k denotes the k-term Taylor polynomial for the logarithm.
background
The module develops interval bounds for the logarithm by combining monotonicity with Taylor remainders. For arguments of the form 1 + x with |x| < 1 the series log(1 + x) = sum (-1)^{k+1} x^k / k converges, and the remainder after n terms satisfies the displayed inequality. The key imported fact is the complex-norm remainder bound together with the identification of real and complex norms on the real line.
proof idea
The proof first converts the real absolute-value hypothesis into the complex norm bound via complex_norm_ofReal. It then applies the complex remainder lemma. A short calculation shows that the real logarithm equals the real part of the complex logarithm of the same argument, and that the real-part difference is bounded by the complex norm of the difference. The final simplification replaces the complex norm by the real absolute value.
why it matters
This lemma closes the error-control step required by the Taylor strategy in the logarithm interval module. It supports downstream constructions of rigorous bounds for log(φ) and related constants that appear in the phi-ladder. Because the bound is explicit and depends only on |x| and n, it can be instantiated inside interval-arithmetic decision procedures without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.