The geometric mean of two positive elements #
For a strictly positive element a of a unital algebra carrying a continuous functional calculus
and a nonnegative element b, the geometric mean
geometricMean a b = √a * √(√a⁻¹ * b * √a⁻¹) * √a
is the unique nonnegative solution x of the Riccati equation x * a⁻¹ * x = b. For positive
definite matrices, and for positive operators on a real Hilbert space, this is the classical
geometric mean. The element geometricMean a⁻¹ b, characterised here as the unique nonnegative
solution of x * a * x = b, is the linear map transporting a centred Gaussian law of covariance
a to one of covariance b, that is, the linear Brenier map from a nondegenerate source Gaussian
to a possibly degenerate target Gaussian.
The definition is phrased through Mathlib's CFC.conjSqrt, so all of the identities below reduce
to associativity together with CFC.sqrt_mul_sqrt_self and the uniqueness of nonnegative square
roots (CFC.sqrt_unique).
Main declarations #
TauCeti.geometricMean: the geometric mean of two elements.TauCeti.geometricMean_eq_sqrt_mul_mul: the explicit square-root formula.TauCeti.geometricMean_mul_ringInverse_mul_geometricMean: it solvesx * a⁻¹ * x = b.TauCeti.eq_geometricMean_of_mul_ringInverse_mul: it is the only nonnegative solution.TauCeti.geometricMean_eq_iff: the resulting characterisation.TauCeti.geometricMean_comm: the geometric mean is symmetric in its two arguments.TauCeti.geometricMean_ringInverse_ringInverse: it commutes with inversion.TauCeti.geometricMean_add_geometricMean_le: the arithmetic--geometric mean inequality.TauCeti.eq_geometricMean_ringInverse_of_mul_mul: the transport formx * a * x = b.
References #
- T. Ando, Topics on operator inequalities, Hokkaido University, 1978.
- W. Pusz and S. L. Woronowicz, Functional calculus for sesquilinear forms and the purification map, Rep. Math. Phys. 8 (1975), 159--170.
Conjugation by a square root preserves nonnegativity.
A factor between two square-root conjugations by c moves inside a single conjugation by
c, where it is itself conjugated by c.
The geometric mean geometricMean a b = √a * √(√a⁻¹ * b * √a⁻¹) * √a of two elements of a
unital algebra with a continuous functional calculus. The intended range of the definition is a
strictly positive and b nonnegative; the value is 0 whenever a fails to be nonnegative.
Equations
- TauCeti.geometricMean a b = (CFC.conjSqrt a) (CFC.sqrt ((CFC.conjSqrt (Ring.inverse a)) b))
Instances For
Outside the intended range, the geometric mean takes the junk value 0.
The geometric mean written out through square roots rather than through CFC.conjSqrt.
The geometric mean of a and b solves the Riccati equation x * a⁻¹ * x = b.
The Riccati equation x * a⁻¹ * x = b has at most one nonnegative solution.
The geometric mean of a and b is characterised as the nonnegative solution of the Riccati
equation x * a⁻¹ * x = b.
The geometric mean of two strictly positive elements is strictly positive.
The geometric mean is symmetric in its two arguments.
The geometric mean commutes with inversion.
The arithmetic--geometric mean inequality for positive elements:
geometricMean a b + geometricMean a b ≤ a + b.
The transport identity: geometricMean a⁻¹ b solves x * a * x = b. Read through the
covariances of two centred Gaussian laws, this is the linear Brenier map from the first to the
second.
The equation x * a * x = b has at most one nonnegative solution.