Documentation

Mathlib.Analysis.SpecialFunctions.Artanh

Inverse of the tanh function #

In this file we define an inverse of tanh as a function from ℝ to (-1, 1).

Main definitions #

Real.artanh: An inverse function of Real.tanh as a function from ℝ to (-1, 1).
Real.tanhPartialEquiv: Real.tanh and Real.artanh bundled as a PartialEquiv from ℝ to (-1, 1).

Main Results #

Real.tanh_artanh, Real.artanh_tanh: tanh and artanh are inverse in the appropriate domains.
Real.tanh_bijOn, Real.tanh_injective, Real.tanh_surjOn: Real.tanh is bijective, injective and surjective as a function from ℝ to (-1, 1)
Real.artanh_bijOn, Real.artanh_injOn, Real.artanh_surjOn: Real.artanh is bijective, injective and surjective as a function from (-1, 1) to ℝ

Tags #

artanh, arctanh, argtanh, atanh

noncomputable def Real.artanh (x : ℝ) :

artanh is defined using a logarithm, artanh x = log √((1 + x) / (1 - x)).

Equations

Real.artanh x = Real.log √((1 + x) / (1 - x))

Instances For

theorem Real.artanh_eq_half_log {x : ℝ} (hx : x ∈ Set.Icc (-1) 1) :

artanh x = 1 / 2 * log ((1 + x) / (1 - x))

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

exp (artanh x) = √((1 + x) / (1 - x))

@[simp]

theorem Real.artanh_zero :

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

sinh (artanh x) = x / √(1 - x ^ 2)

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

cosh (artanh x) = 1 / √(1 - x ^ 2)

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

tanh (artanh x) = x

artanh is the right inverse of tanh over (-1, 1).

theorem Real.artanh_tanh (x : ℝ) :

artanh (tanh x) = x

artanh is the left inverse of tanh.

theorem Real.strictMonoOn_one_add_div_one_sub :

StrictMonoOn (fun (x : ℝ) => (1 + x) / (1 - x)) (Set.Ioo (-1) 1)

theorem Real.strictMonoOn_artanh :

StrictMonoOn artanh (Set.Ioo (-1) 1)

theorem Real.artanh_le_artanh_iff {x y : ℝ} (hx : x ∈ Set.Ioo (-1) 1) (hy : y ∈ Set.Ioo (-1) 1) :

artanh x ≤ artanh y ↔ x ≤ y

theorem Real.artanh_lt_artanh_iff {x y : ℝ} (hx : x ∈ Set.Ioo (-1) 1) (hy : y ∈ Set.Ioo (-1) 1) :

artanh x < artanh y ↔ x < y

theorem Real.artanh_le_artanh {x y : ℝ} (hx : -1 < x) (hy : y < 1) (hxy : x ≤ y) :

artanh x ≤ artanh y

theorem Real.artanh_lt_artanh {x y : ℝ} (hx : -1 < x) (hy : y < 1) (hxy : x < y) :

artanh x < artanh y

theorem Real.artanh_eq_zero_iff {x : ℝ} :

artanh x = 0 ↔ x ≤ -1 ∨ x = 0 ∨ 1 ≤ x

theorem Real.artanh_pos {x : ℝ} (hx : x ∈ Set.Ioo 0 1) :

theorem Real.artanh_neg {x : ℝ} (hx : x ∈ Set.Ioo (-1) 0) :

theorem Real.artanh_nonneg {x : ℝ} (hx : 0 ≤ x) :

theorem Real.artanh_nonpos {x : ℝ} (hx : x ≤ 0) :

noncomputable def Real.tanhPartialEquiv :

PartialEquiv ℝ ℝ

Real.tanh as a PartialEquiv.

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Real.tanh_bijOn :

Set.BijOn tanh Set.univ (Set.Ioo (-1) 1)

theorem Real.tanh_injective :

Function.Injective tanh

theorem Real.tanh_surjOn :

Set.SurjOn tanh Set.univ (Set.Ioo (-1) 1)

theorem Real.artanh_bijOn :

Set.BijOn artanh (Set.Ioo (-1) 1) Set.univ

theorem Real.artanh_injOn :

Set.InjOn artanh (Set.Ioo (-1) 1)

theorem Real.artanh_surjOn :

Set.SurjOn artanh (Set.Ioo (-1) 1) Set.univ