The addition formula and the monotonicity of the hyperbolic tangent #
Mathlib's Analysis/Complex/Trigonometric.lean defines Real.sinh, Real.cosh and Real.tanh
and proves the two addition formulae Real.sinh_add and Real.cosh_add, but records none for
Real.tanh; Analysis/SpecialFunctions/Artanh.lean inverts Real.tanh on (-1, 1) and proves
that the inverse is strictly monotone, but does not state the monotonicity of Real.tanh
itself. This file supplies both.
Main declarations #
Real.tanh_add—tanh (a + b) = (tanh a + tanh b) / (1 + tanh a * tanh b): the hyperbolic tangent of a sum is the Möbius sum of the hyperbolic tangents.Real.tanh_strictMonoandReal.tanh_lt_tanh_iff—Real.tanhis strictly monotone, so it compares two real numbers exactly as they compare, and is positive on the positive reals.
The formula is the quotient of the other two, both sides carrying the factor
cosh a * cosh b, which is nonzero because Real.cosh is positive.
Where it is used: TauCeti/Analysis/SpecialFunctions/Artanh.lean inverts it into the additive
law of Real.artanh, which carries the Möbius addition of (-1, 1) to the addition of ℝ;
that law is in turn what makes the hyperbolic distance of the complex unit disc a metric, the
subject of layer L2 of the conformal-mapping roadmap
(TauCetiRoadmap/ConformalMapping/README.md).
Addition formula for the hyperbolic tangent. Real.tanh (a + b) is the Möbius sum
(tanh a + tanh b) / (1 + tanh a * tanh b).
The pinned Mathlib has Real.sinh_add and Real.cosh_add but no addition formula for
Real.tanh. This one is their quotient, both sides of which carry the same factor: by those two
formulae tanh a + tanh b = sinh (a + b) / (cosh a * cosh b) and
1 + tanh a * tanh b = cosh (a + b) / (cosh a * cosh b), and the right-hand denominator is
positive, so dividing cancels cosh a * cosh b and leaves tanh (a + b).
The hyperbolic tangent is strictly monotone. It is inverted on its range (-1, 1) by
the strictly monotone Real.artanh, so it cannot reverse a strict inequality.