An integral related to the arithmetic-geometric mean

For $a,b>0$ consider the improper integral $$I(a,b) = \int_0^\infty \frac{dx}{\sqrt{(x^2+a^2)(x^2+b^2)}}.$$ Then making the substitution $x = t+\sqrt{t^2+ab}$ yields, after rearranging, $$I(a,b) = \int_{-\infty}^\infty \frac{dx}{2\sqrt{(x^2+ab)(x^2+((a+b)/2)^2)}} = I(\sqrt{ab},(a+b)/2).$$ Iterating this transformation drives both arguments towards the arithmetic-geometric mean (AGM) of $a$ and $b$, by Mathlib.Analysis.SpecialFunctions.ArithmeticGeometricMean, so we have $$I(a,b)=I(\operatorname{agm}(a,b),\operatorname{agm}(a,b))=\frac{\pi/2}{\operatorname{agm}(a,b)}$$ where the second equality follows from an elementary integral. This establishes a link between the AGM and complete elliptic integrals.

TauCeti.lintegral_image_inv_sqrt_eq_agmIntegral turns a substitution x = f(t) with D(f t) = f′(t)² (t² + a²)(t² + b²) into an evaluation of ∫ D(x)^(-1/2) dx as I(a,b).

Adapted from Jeremy Tan's Mathlib PR #34397, commit 376352b6e080265bc0380074baaf9aafa0b70a80. The integral is finite for positive inputs; when either input is zero it diverges, and Lean's totalized Bochner integral returns zero.

noncomputable def TauCeti.agmIntegral (a b : ℝ) : ℝ

The elliptic integral related to the arithmetic-geometric mean. It is finite for positive inputs and has the totalized value zero if either input is zero.

theorem TauCeti.agmIntegral_def (a b : ℝ) : agmIntegral a b = ∫ (x : ℝ) in Set.Ioi 0, (√((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2)))⁻¹

theorem TauCeti.integrableOn_agmIntegrand_Ioi_of_pos {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : MeasureTheory.IntegrableOn (fun (x : ℝ) => (√((x ^ 2 + a ^ 2) * (x ^ 2 + b ^ 2)))⁻¹) (Set.Ioi 0) MeasureTheory.volume

The defining integrand is integrable on the positive half-line for positive inputs.

theorem TauCeti.agmIntegral_comm {a b : ℝ} : agmIntegral a b = agmIntegral b a

The AGM integral is symmetric in its arguments.

@[simp]

theorem TauCeti.agmIntegral_zero_left {b : ℝ} : agmIntegral 0 b = 0

The integral diverges (and thus takes the junk value of 0 in Lean) when a = 0.

@[simp]

theorem TauCeti.agmIntegral_zero_right {a : ℝ} : agmIntegral a 0 = 0

The integral diverges (and thus takes the junk value of 0 in Lean) when b = 0.

@[simp]

theorem TauCeti.agmIntegral_self {a : ℝ} (ha : 0 ≤ a) : agmIntegral a a = Real.pi / 2 / a

On the nonnegative diagonal the AGM integral is the elementary value π / 2 / a. At zero both sides take their totalized value zero.

theorem TauCeti.agmIntegral_eq_agmIntegral_gm_am {a b : ℝ} (ha : 0 ≤ a) (hb : 0 ≤ b) : agmIntegral a b = agmIntegral (√(a * b)) ((a + b) / 2)

Landen's transformation for agmIntegral.

theorem TauCeti.continuousOn_agmIntegral : ContinuousOn (fun (p : ℝ × ℝ) => agmIntegral p.1 p.2) (Set.Ioi 0 ×ˢ Set.Ioi 0)

The AGM integral depends continuously on its two positive arguments.

theorem TauCeti.agmIntegral_eq_agmIntegral_agmSequences {a b : NNReal} {n : ℕ} : agmIntegral ↑a ↑b = agmIntegral ↑(a.agmSequences b n).1 ↑(a.agmSequences b n).2

Every iterate of the arithmetic-geometric mean preserves the integral.

theorem TauCeti.agmIntegral_eq_pi_div_two_div_agm {a b : NNReal} : agmIntegral ↑a ↑b = Real.pi / 2 / ↑(a.agm b)

The fundamental relation between agmIntegral and NNReal.agm. For positive inputs this is the value of a convergent integral; if either input is zero both sides are totalized to zero.

theorem TauCeti.agmIntegral_pos {a b : ℝ} (ha : 0 < a) (hb : 0 < b) : 0 < agmIntegral a b

The AGM integral is strictly positive when both inputs are positive.

theorem TauCeti.agmIntegral_mul_left (c a b : ℝ) : agmIntegral (c * a) (c * b) = agmIntegral a b / |c|

The AGM integral is homogeneous of degree -1: scaling both axes by c divides it by |c|. For c = 0 both sides take the totalized value zero.

theorem TauCeti.lintegral_image_inv_sqrt_eq_agmIntegral {f f' D : ℝ → ℝ} {a b : ℝ} (ha : 0 < a) (hb : 0 < b) (hf : ∀ t ∈ Set.Ioi 0, HasDerivWithinAt f (f' t) (Set.Ioi 0) t) (hinj : Set.InjOn f (Set.Ioi 0)) (hf' : ∀ t ∈ Set.Ioi 0, f' t ≠ 0) (hD : ∀ t ∈ Set.Ioi 0, D (f t) = f' t ^ 2 * ((t ^ 2 + a ^ 2) * (t ^ 2 + b ^ 2))) : ∫⁻ (x : ℝ) in f '' Set.Ioi 0, ENNReal.ofReal (√(D x))⁻¹ = ENNReal.ofReal (agmIntegral a b)

If a substitution x = f(t) on t > 0 satisfies D(f t) = f′(t)² (t² + a²)(t² + b²) with f′(t) ≠ 0, then the integral of D(x)^(-1/2) over the image of f is the AGM integral of the axes a and b.