Fungrim entry: 75e692

\left|\operatorname{agm}\!\left(1, z\right) - a_{n}\right| \le \left|a_{n} - b_{n}\right|\; \text{ where } \left(a_{n}, b_{n}\right) = \operatorname{agm}_{n}\!\left(1, z\right)

Assumptions:

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \operatorname{Re}(z) \ge 0

TeX:

\left|\operatorname{agm}\!\left(1, z\right) - a_{n}\right| \le \left|a_{n} - b_{n}\right|\; \text{ where } \left(a_{n}, b_{n}\right) = \operatorname{agm}_{n}\!\left(1, z\right)

z \in \mathbb{C} \;\mathbin{\operatorname{and}}\; \operatorname{Re}(z) \ge 0

Definitions:

Fungrim symbol	Notation	Short description
`Abs`	$\left\|z\right\|$	Absolute value
`AGM`	$\operatorname{agm}\!\left(a, b\right)$	Arithmetic-geometric mean
`AGMSequence`	$\operatorname{agm}_{n}\!\left(a, b\right)$	Convergents in AGM iteration
`CC`	$\mathbb{C}$	Complex numbers
`Re`	$\operatorname{Re}(z)$	Real part

Source code for this entry:

Entry(ID("75e692"),
    Formula(Where(LessEqual(Abs(Sub(AGM(1, z), a_(n))), Abs(Sub(a_(n), b_(n)))), Def(Tuple(a_(n), b_(n)), AGMSequence(n, 1, z)))),
    Variables(z),
    Assumptions(And(Element(z, CC), GreaterEqual(Re(z), 0))))

Topics using this entry

Arithmetic-geometric mean