Manuscript Oai276-A@1 · Oai276-A.tex · lemma · 215068af

Lemma: Certified series identities

Stages 3 and 6: the explicit finite maximum certificate › Rational sums and explicit remainder bounds · lines 942–976 · proof included or linked

Oai276-A@1#lem:series, Oai276-A@1#eq:series-identities, Oai276-A@1#eq:fseries

Back to manuscript

For $0 \leq z < 1$ ,

0 \leq L (z) - L_{N} (z) \leq T_{N} (z), 0 \leq J (z) - J_{N} (z) \leq R_{N} (z) .

Also,

atanh r = r L (r^{2}), h_{e} (\frac{1 + r}{2}) = ln 2 - J (r^{2}) (∣ r ∣ < 1) .

Therefore

f (p) = J (q (p)) - J (x (p)^{2}) .

Proof. Expand $1/ (1 - r^{2})$ geometrically and integrate from zero to $r$ . This gives the $atanh$ series. The derivative of $ln 2 - h_{e} ((1 + r) /2)$ is $atanh r$ ; integrating again gives the $J$ series.

For each tail, replace every denominator by its first omitted denominator and sum the remaining geometric series. Equation (eq:fseries) follows because binary entropy is symmetric and $x (p) = 1 - 2 t (p)$ .

Displayed formulas in this passage

Oai276-A@1#eq:series-identities · line 951
$atanh r = r L (r^{2}), h_{e} (\frac{1 + r}{2}) = ln 2 - J (r^{2}) (∣ r ∣ < 1) .$
Oai276-A@1#eq:fseries · line 959
$f (p) = J (q (p)) - J (x (p)^{2}) .$
unlabeled · line 945
$0 \leq L (z) - L_{N} (z) \leq T_{N} (z), 0 \leq J (z) - J_{N} (z) \leq R_{N} (z) .$

Lemma: Certified series identities

Displayed formulas in this passage

Nearby in this section