The constant κ for s close to one

Section 5 of the paper states that, for s close to one, κ ≈ (1 − s²)²/4 (sec5_kappa_proof). With u = s² − 1, κ = {u − log(1 + u)}/2 and (1 − s²)² = u², and the Taylor expansion log(1 + u) = u − u²/2 + O(u³) gives 2{u − log(1 + u)}/u² → 1 (tendsto_two_mul_sub_log_div_sq).

theorem LogOptimal.tendsto_two_mul_sub_log_div_sq : Filter.Tendsto (fun (u : ℝ) => 2 * (u - Real.log (1 + u)) / u ^ 2) (nhdsWithin 0 {0}ᶜ) (nhds 1)

2{u − log(1 + u)}/u² → 1 as u → 0, u ≠ 0.

theorem LogOptimal.sec5_kappa_proof : Filter.Tendsto (fun (s : ℝ) => kappa s / ((1 - s ^ 2) ^ 2 / 4)) (nhdsWithin 1 {1}ᶜ) (nhds 1)