Proof for the continued fraction of ln(2)

Stream: mathlib4

[Predrag Terzić]

I formalized in Lean 4 / mathlib a generalized continued fraction for ln(2).
The proof identifies the convergents with partial sums of the alternating harmonic series,
hence proving convergence to ln(2).

Gist: https://gist.github.com/formalista/da6dec10ea6fcd2fefdfda6ff2c07bc7

Any feedback or suggestions for simplification are welcome.

[Weiyi Wang]

Congrats on formalizing the proof of an interesting formula! (or teaching Aristotle to do so, which is still great)

I am a bit confused by all the repeating theorem with _final, _v2, _main, though. When doing a quick review of the proof, people likely want to check the statement first, so you should point out which is the main theorem. Here the last one limit_of_sum_term looks like a different formula from "continued fraction", so that added more confusion. I guessed that ln2_cf_converges is the one for continued fraction