The lemniscate constant

This file defines Gauss's lemniscate constant ϖ = 2 ∫₀¹ (1 - t⁴)^(-1/2) dt ≈ 2.62206, half the arc length of the lemniscate of Bernoulli (x² + y²)² = x² - y², and evaluates it by Euler's beta function, by the Gamma function, by the complete elliptic integral of the first kind at the modulus 1/√2, and by the arithmetic-geometric mean.

The substitution u = t⁴ turns the defining integral into the beta integral Β(1/4, 1/2) / 4, so ϖ = Β(1/4, 1/2) / 2. The reflection formula Γ(1/4) Γ(3/4) = π / sin (π / 4) = π √2 and Γ(1/2) = √π then give the classical closed form ϖ = Γ(1/4)² / (2 √(2π)).

The substitution t = sin θ turns the defining integral into ∫₀^{π/2} (1 + sin² θ)^(-1/2) dθ, and the imaginary-modulus transformation identifies this with K(1/√2) / √2, so ϖ = √2 K(1/√2). Together with the Gamma evaluation this gives K(1/√2) = Γ(1/4)² / (4 √π), and together with Gauss's theorem K(k) = π / (2 M(1, √(1 - k²))) it gives Gauss's identity ϖ = π / M(1, √2), where M = NNReal.agm.

Main definitions

• TauCeti.Real.lemniscateConstant — the lemniscate constant ϖ = 2 ∫₀¹ (1 - t⁴)^(-1/2) dt.

Main results

• TauCeti.Real.lemniscateConstant_def — the defining equation of ϖ as an integral;
• TauCeti.Real.intervalIntegrable_one_sub_pow_four_rpow — the defining integrand is interval integrable on [0, 1], so the integral is a genuine (improper) integral and not a junk value;
• TauCeti.Real.lemniscateConstant_eq_beta — ϖ = Β(1/4, 1/2) / 2;
• TauCeti.Real.lemniscateConstant_pos — 0 < ϖ;
• TauCeti.Real.lemniscateConstant_eq_Gamma — ϖ = Γ(1/4)² / (2 √(2π));
• TauCeti.Real.lemniscateConstant_eq_sqrt_two_mul_legendreK — ϖ = √2 K(1/√2);
• TauCeti.Real.legendreK_one_div_sqrt_two — K(1/√2) = Γ(1/4)² / (4 √π);
• TauCeti.Real.lemniscateConstant_eq_pi_div_agm — Gauss's identity ϖ = π / M(1, √2).

References

• J. M. Borwein and P. B. Borwein, Pi and the AGM, Wiley, 1987, Chapter 1.
• NIST Digital Library of Mathematical Functions, §19.20(i), https://dlmf.nist.gov/19.20.
• J. Todd, The lemniscate constants, Comm. ACM 18 (1975), 14–19.

noncomputable def TauCeti.Real.lemniscateConstant : ℝ

Gauss's lemniscate constant ϖ = 2 ∫₀¹ (1 - t⁴)^(-1/2) dt.

theorem TauCeti.Real.lemniscateConstant_def : lemniscateConstant = 2 * ∫ (t : ℝ) in 0..1, (1 - t ^ 4) ^ (-1 / 2)

The defining equation ϖ = 2 ∫₀¹ (1 - t⁴)^(-1/2) dt of the lemniscate constant.

theorem TauCeti.Real.intervalIntegrable_one_sub_pow_four_rpow : IntervalIntegrable (fun (t : ℝ) => (1 - t ^ 4) ^ (-1 / 2)) MeasureTheory.volume 0 1

The integrand (1 - t⁴)^(-1/2) defining the lemniscate constant is interval integrable on [0, 1], despite its singularity at t = 1.

theorem TauCeti.Real.lemniscateConstant_eq_beta : lemniscateConstant = ProbabilityTheory.beta (1 / 4) (1 / 2) / 2

The lemniscate constant is half the beta value Β(1/4, 1/2).

theorem TauCeti.Real.lemniscateConstant_pos : 0 < lemniscateConstant

The lemniscate constant is positive.

theorem TauCeti.Real.lemniscateConstant_eq_Gamma : lemniscateConstant = Real.Gamma (1 / 4) ^ 2 / (2 * √(2 * Real.pi))

The Gamma evaluation of the lemniscate constant: ϖ = Γ(1/4)² / (2 √(2π)).

theorem TauCeti.Real.lemniscateConstant_eq_sqrt_two_mul_legendreK : lemniscateConstant = √2 * legendreK (1 / √2)

The lemniscate constant is √2 times the complete elliptic integral of the first kind at the modulus 1/√2: ϖ = √2 K(1/√2).

theorem TauCeti.Real.legendreK_one_div_sqrt_two : legendreK (1 / √2) = Real.Gamma (1 / 4) ^ 2 / (4 * √Real.pi)

The Gamma evaluation of the complete elliptic integral of the first kind at the modulus 1/√2: K(1/√2) = Γ(1/4)² / (4 √π).

theorem TauCeti.Real.lemniscateConstant_eq_pi_div_agm : lemniscateConstant = Real.pi / ↑(NNReal.agm 1 (NNReal.sqrt 2))

Gauss's identity: the lemniscate constant is ϖ = π / M(1, √2), where M is the arithmetic-geometric mean NNReal.agm.