The algebra and the calculus of the inverse hyperbolic tangent

Mathlib's Analysis/SpecialFunctions/Artanh.lean introduces Real.artanh and proves that it inverts Real.tanh on (-1, 1), that it is strictly monotone there, and the closed forms Real.sinh_artanh, Real.cosh_artanh. It records neither the additive law of Real.artanh nor any of its analytic properties: no addition formula, no oddness, and no continuity or differentiability statement appears anywhere in the pinned Mathlib.

This file supplies both. The analytic half follows from the logarithmic formula Real.artanh_eq_half_log, artanh x = (1 / 2) * log ((1 + x) / (1 - x)), which is valid on the open interval (-1, 1); since that interval is open, the formula may be differentiated at each of its points and the result transported back to Real.artanh itself. The algebraic half follows from the inversion Real.tanh_artanh together with the addition formula for Real.tanh, which the pinned Mathlib does not state either and which is proved in TauCeti/Analysis/SpecialFunctions/Hyperbolic.lean.

Main declarations

The additive law

• Real.artanh_add and Real.artanh_sub — artanh a ± artanh b = artanh ((a ± b) / (1 ± a * b)) for a and b in (-1, 1): Real.artanh is an isomorphism from the Möbius addition of (-1, 1) onto (ℝ, +).
• Real.add_div_one_add_mul_mem_Ioo and Real.sub_div_one_sub_mul_mem_Ioo — that Möbius addition and Möbius subtraction are closed on (-1, 1), which is what lets the two formulae be applied again to their own right-hand sides.
• Real.artanh_neg_eq_neg_artanh and Real.artanh_abs — artanh (-x) = -artanh x and artanh |x| = |artanh x|, both for every real x, the values outside (-1, 1) being handled by Mathlib's Real.artanh_eq_zero_iff.

The calculus

• Real.hasDerivAt_artanh — Real.artanh has derivative (1 - x ^ 2)⁻¹ at each x of (-1, 1), with Real.deriv_artanh, Real.differentiableAt_artanh, Real.differentiableOn_artanh, Real.continuousAt_artanh and Real.continuousOn_artanh as companions, and HasDerivAt.artanh as the chain-rule form.
• Real.tendsto_artanh_div_nhdsNE_zero — artanh t / t tends to 1 as t tends to 0 through nonzero values: the derivative at the origin, read as a limit of slopes. This is what turns a closed-form hyperbolic distance into an infinitesimal one.
• Real.integral_one_sub_sq_inv_eq_artanh — artanh is the primitive of the density (1 - t ^ 2)⁻¹: ∫ t in (0)..r, (1 - t ^ 2)⁻¹ = artanh r for r ∈ (-1, 1).
• Real.self_le_artanh and Real.artanh_le_self_div_one_sub_sq — the two-sided comparison x ≤ artanh x ≤ x / (1 - x ^ 2) on [0, 1), obtained by bounding that integrand between its values at the two endpoints.

The motivation is the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md), whose layer L2 asks for the hyperbolic (Poincaré) metric on the unit disc. Tau Ceti's TauCeti.hyperbolicDist is Real.artanh of the pseudo-hyperbolic expression, so the additive law below is what makes it satisfy the triangle inequality (TauCeti.hyperbolicDist_triangle, in Conformal/Hyperbolic/Triangle.lean) and what measures hyperbolic arclength along a Euclidean diameter (TauCeti.hyperbolicDist_mul_ofReal_of_norm_eq_one, in Conformal/Poincare/Geodesic.lean), while its infinitesimal form — proved in TauCeti/Analysis/Complex/Conformal/Hyperbolic/Density.lean — is the derivative of Real.artanh at the origin transported along that expression. Nothing here is complex-analytic, so it is all stated for Real.artanh alone, at the natural generality of a real special function, rather than being buried in the disc files.

The additive law

@[simp]

theorem Real.artanh_neg_eq_neg_artanh (x : ℝ) : artanh (-x) = -artanh x

Real.artanh is odd, at every real number: artanh (-x) = -artanh x.

No hypothesis is needed. On (-1, 1) this is the logarithmic formula Real.artanh_eq_half_log read through Real.log_inv, and outside it both sides vanish by Real.artanh_eq_zero_iff — the junk value forced by the defining formula artanh x = log √((1 + x) / (1 - x)), whose argument is there nonpositive, or, at x = 1, the value 2 / 0 = 0 of Lean's division convention.

The name Real.artanh_neg, which the Mathlib convention for oddness would suggest (compare Real.arsinh_neg, Real.arctan_neg), is taken in Mathlib by the sign lemma artanh x < 0; the _eq_ form follows the precedent of Real.log_neg_eq_log, whose name is displaced by Real.log_neg for the same reason.

theorem Real.artanh_abs (x : ℝ) : artanh |x| = |artanh x|

The absolute value passes through Real.artanh, at every real number: artanh |x| = |artanh x|. Both sides are artanh of the larger of x and -x, by oddness and the sign lemmas Real.artanh_nonneg, Real.artanh_nonpos.

Not a simp lemma: neither side is a normal form for the other, and rewriting in either direction merely moves the absolute value across Real.artanh.

theorem Real.artanh_add {a b : ℝ} (ha : a ∈ Set.Ioo (-1) 1) (hb : b ∈ Set.Ioo (-1) 1) : artanh a + artanh b = artanh ((a + b) / (1 + a * b))

Addition formula for the inverse hyperbolic tangent. For a, b ∈ (-1, 1), artanh a + artanh b = artanh ((a + b) / (1 + a * b)): Real.artanh carries the Möbius addition of (-1, 1) — the one-dimensional relativistic velocity addition — to the addition of ℝ.

Both hypotheses are needed: outside (-1, 1) the left-hand side is a junk value while the right-hand side need not be. The proof applies Real.artanh_tanh to the sum, whose Real.tanh is computed by Real.tanh_add.

theorem Real.add_div_one_add_mul_mem_Ioo {a b : ℝ} (ha : a ∈ Set.Ioo (-1) 1) (hb : b ∈ Set.Ioo (-1) 1) : (a + b) / (1 + a * b) ∈ Set.Ioo (-1) 1

Möbius addition preserves the interval (-1, 1): for a, b ∈ (-1, 1) the Möbius sum (a + b) / (1 + a * b) again lies in (-1, 1), so that Real.artanh_add may be applied to it.

Elementary as the statement is, it is Real.tanh_add read backwards: the Möbius sum is tanh (artanh a + artanh b), and Real.tanh takes its values in (-1, 1).

theorem Real.artanh_sub {a b : ℝ} (ha : a ∈ Set.Ioo (-1) 1) (hb : b ∈ Set.Ioo (-1) 1) : artanh a - artanh b = artanh ((a - b) / (1 - a * b))

Subtraction formula for the inverse hyperbolic tangent. For a, b ∈ (-1, 1), artanh a - artanh b = artanh ((a - b) / (1 - a * b)): the addition formula Real.artanh_add with b negated, Real.artanh being odd.

theorem Real.sub_div_one_sub_mul_mem_Ioo {a b : ℝ} (ha : a ∈ Set.Ioo (-1) 1) (hb : b ∈ Set.Ioo (-1) 1) : (a - b) / (1 - a * b) ∈ Set.Ioo (-1) 1

Möbius subtraction preserves the interval (-1, 1): for a, b ∈ (-1, 1) the Möbius difference (a - b) / (1 - a * b) again lies in (-1, 1).

This is the closure statement that Real.artanh_sub needs, exactly as Real.add_div_one_add_mul_mem_Ioo is the one that Real.artanh_add needs: without it a consumer of the subtraction formula could not feed its right-hand side back into the interval-only Real.artanh API. It is the addition statement at -b.

Differentiability

theorem Real.hasDerivAt_artanh {x : ℝ} (hx : x ∈ Set.Ioo (-1) 1) : HasDerivAt artanh (1 - x ^ 2)⁻¹ x

The derivative of the inverse hyperbolic tangent. On the interval (-1, 1) where Real.artanh inverts Real.tanh, it has derivative (1 - x ^ 2)⁻¹.

Mathlib records no differentiability statement for Real.artanh; this is proved from the logarithmic formula Real.artanh_eq_half_log, which holds on all of (-1, 1) and hence on a neighbourhood of each of its points.

theorem Real.differentiableAt_artanh {x : ℝ} (hx : x ∈ Set.Ioo (-1) 1) : DifferentiableAt ℝ artanh x

Real.artanh is differentiable at each point of (-1, 1).

theorem Real.deriv_artanh {x : ℝ} (hx : x ∈ Set.Ioo (-1) 1) : deriv artanh x = (1 - x ^ 2)⁻¹

The derivative of Real.artanh on (-1, 1), in deriv form.

theorem Real.differentiableOn_artanh : DifferentiableOn ℝ artanh (Set.Ioo (-1) 1)

Real.artanh is differentiable on (-1, 1).

theorem Real.continuousAt_artanh {x : ℝ} (hx : x ∈ Set.Ioo (-1) 1) : ContinuousAt artanh x

Real.artanh is continuous at each point of (-1, 1).

theorem Real.continuousOn_artanh : ContinuousOn artanh (Set.Ioo (-1) 1)

Real.artanh is continuous on the interval (-1, 1) on which it inverts Real.tanh.

theorem HasDerivAt.artanh {f : ℝ → ℝ} {f' x : ℝ} (hf : HasDerivAt f f' x) (hx : f x ∈ Set.Ioo (-1) 1) : HasDerivAt (fun (y : ℝ) => Real.artanh (f y)) ((1 - f x ^ 2)⁻¹ * f') x

The chain rule for Real.artanh: composing with a function that is differentiable at x and takes a value in (-1, 1) there multiplies the derivative by (1 - f x ^ 2)⁻¹.

The derivative at the origin, as a limit of slopes

theorem Real.tendsto_artanh_div_nhdsNE_zero : Filter.Tendsto (fun (t : ℝ) => artanh t / t) (nhdsWithin 0 {0}ᶜ) (nhds 1)

The infinitesimal form of Real.artanh at the origin. Since artanh 0 = 0 and the derivative of Real.artanh at 0 is 1, the quotient artanh t / t tends to 1 as t tends to 0 through nonzero values.

This is the one-variable input to the infinitesimal Poincaré density: on the unit disc the hyperbolic distance is Real.artanh of the pseudo-hyperbolic expression, and near the diagonal the latter is small, so this limit converts the closed form into a density.

Real.artanh as the primitive of the Poincaré density

theorem Real.integral_one_sub_sq_inv_eq_artanh {r : ℝ} (hr : r ∈ Set.Ioo (-1) 1) : ∫ (t : ℝ) in 0..r, (1 - t ^ 2)⁻¹ = artanh r

Real.artanh is the primitive of (1 - t ^ 2)⁻¹. For r in (-1, 1), ∫ t in (0)..r, (1 - t ^ 2)⁻¹ = artanh r.

On the unit disc this says that the hyperbolic distance from the origin out to a point at Euclidean radius r is the length of that radius measured in the Poincaré density |dz| / (1 - |z| ^ 2).

theorem Real.self_le_artanh {x : ℝ} (hx : 0 ≤ x) (hx₁ : x < 1) : x ≤ artanh x

The elementary lower bound x ≤ artanh x on [0, 1): the Poincaré density (1 - t ^ 2)⁻¹ is at least 1, so the hyperbolic distance dominates the Euclidean one.

theorem Real.artanh_le_self_div_one_sub_sq {x : ℝ} (hx : 0 ≤ x) (hx₁ : x < 1) : artanh x ≤ x / (1 - x ^ 2)

The elementary upper bound artanh x ≤ x / (1 - x ^ 2) on [0, 1): the Poincaré density (1 - t ^ 2)⁻¹ is increasing, so on [0, x] it is at most its value at x.