Quadratic bounds for the arithmetic-geometric mean

One arithmetic-geometric mean step bounds the new gap by the square of the old gap, divided by eight times the smaller input. For 0 < y ≤ x, iterating this estimate gives the bound (agmSequences x y n).2 - (agmSequences x y n).1 ≤ 8 * y * ((x - y) / (8 * y)) ^ (2 ^ (n + 1)). This upper bound decays to zero only when x < 9 * y, equivalently (x - y) / (8 * y) < 1. Mathlib's NNReal.agmSequences has its zeroth term already one step after the input pair.

We also show that the weighted differences of squares of the two means tend to zero. This controls the remainder in the AGM series for the second-kind elliptic integral.

The quadratic estimate follows Carlson.agmSeq_gap_succ from Bastiaan J Braams' lean-codes, adapted to Mathlib's existing AGM sequences and their indexing.

References

• J. M. Borwein and P. B. Borwein, Pi and the AGM, Wiley, 1987, Chapters 1–2.
• Bastiaan J Braams, Carlson/Elliptic/AGMSecondKind.lean in lean-codes: https://github.com/bjbraams/lean-codes/blob/2b8cba1/Carlson/Elliptic/AGMSecondKind.lean.

theorem Real.half_add_sub_sqrt_mul_le {x y : ℝ} (hy : 0 < y) (hxy : y ≤ x) : (x + y) / 2 - √(x * y) ≤ (x - y) ^ 2 / (8 * y)

The gap after one arithmetic-geometric mean step is bounded quadratically in the input gap, with the smaller positive input controlling the denominator.

theorem NNReal.agmSequences_fst_pos {x y : NNReal} (hx : 0 < x) (hy : 0 < y) (n : ℕ) : 0 < (x.agmSequences y n).1

Both positive inputs give a positive geometric mean at every AGM step.

theorem NNReal.half_add_sub_sqrt_mul_le {a b : NNReal} (hb : 0 < b) (hba : b ≤ a) : (a + b) / 2 - sqrt (a * b) ≤ (a - b) ^ 2 / (8 * b)

The gap after one arithmetic-geometric mean step is bounded quadratically in the input gap, with the smaller positive input controlling the denominator.

theorem NNReal.agmSequences_snd_sub_fst_le {x y : NNReal} (hy : 0 < y) (hxy : y ≤ x) (n : ℕ) : (x.agmSequences y n).2 - (x.agmSequences y n).1 ≤ 8 * y * ((x - y) / (8 * y)) ^ 2 ^ (n + 1)

For 0 < y ≤ x, the gap between the arithmetic and geometric AGM sequences is at most 8 * y * ((x - y) / (8 * y)) ^ (2 ^ (n + 1)). This upper bound decays to zero only when x < 9 * y, equivalently (x - y) / (8 * y) < 1. The index 0 already includes one AGM step.

theorem NNReal.agmSequences_fst_sq_le_snd_sq (x y : NNReal) (n m : ℕ) : ↑(x.agmSequences y n).1 ^ 2 ≤ ↑(x.agmSequences y m).2 ^ 2

The square of any geometric AGM mean is at most the square of any arithmetic AGM mean.

theorem NNReal.agmSequences_succ_snd_sq_sub_fst_sq (x y : NNReal) (n : ℕ) : ↑(x.agmSequences y (n + 1)).2 ^ 2 - ↑(x.agmSequences y (n + 1)).1 ^ 2 = (↑(x.agmSequences y n).2 - ↑(x.agmSequences y n).1) ^ 2 / 4

An AGM step turns the difference of squares into one quarter of the squared gap.

theorem NNReal.two_pow_mul_agmSequences_snd_sq_sub_fst_sq_le (x y : NNReal) (n : ℕ) : 2 ^ (n + 1) * (↑(x.agmSequences y (n + 1)).2 ^ 2 - ↑(x.agmSequences y (n + 1)).1 ^ 2) ≤ dist x y ^ 2 / 8 * (1 / 2) ^ n

The weighted difference of squares decays geometrically: 2ⁿ⁺¹ (aₙ₊₁² - gₙ₊₁²) ≤ dist x y ² / 8 · (1/2)ⁿ, where (gₙ₊₁, aₙ₊₁) = agmSequences x y (n + 1).

theorem NNReal.tendsto_two_pow_mul_agmSequences_snd_sq_sub_fst_sq (x y : NNReal) : Filter.Tendsto (fun (n : ℕ) => 2 ^ n * (↑(x.agmSequences y n).2 ^ 2 - ↑(x.agmSequences y n).1 ^ 2)) Filter.atTop (nhds 0)

The differences of squares of the AGM means tend to zero even after multiplication by 2ⁿ. This controls remainders in second-kind elliptic integral evaluation.