Inverse of the cosh function

In this file we define an inverse of cosh as a function from [0, ∞) to [1, ∞).

Main definitions

• Real.arcosh: An inverse function of Real.cosh as a function from [0, ∞) to [1, ∞).

• Real.coshPartialEquiv: Real.cosh as a PartialEquiv.

Main Results

• Real.cosh_arcosh, Real.arcosh_cosh: cosh and arcosh are inverse in the appropriate domains.

Tags

arcosh, arccosh, argcosh, acosh

def Real.arcosh (x : ℝ) : ℝ

arcosh is defined using a logarithm, arcosh x = log (x + √(x ^ 2 - 1)).

Equations

• Real.arcosh x = Real.log (x + √(x ^ 2 - 1))

theorem Real.exp_arcosh {x : ℝ} (hx : 1 ≤ x) : exp (arcosh x) = x + √(x ^ 2 - 1)

@[simp]

theorem Real.arcosh_zero : arcosh 1 = 0

theorem Real.add_sqrt_self_sq_sub_one_inv {x : ℝ} (hx : 1 ≤ x) : (x + √(x ^ 2 - 1))⁻¹ = x - √(x ^ 2 - 1)

theorem Real.cosh_arcosh {x : ℝ} (hx : 1 ≤ x) : cosh (arcosh x) = x

arcosh is the right inverse of cosh over [1, ∞).

theorem Real.arcosh_eq_zero_iff {x : ℝ} (hx : 1 ≤ x) : arcosh x = 0 ↔ x = 1

theorem Real.sinh_arcosh {x : ℝ} (hx : 1 ≤ x) : sinh (arcosh x) = √(x ^ 2 - 1)

theorem Real.tanh_arcosh {x : ℝ} (hx : 1 ≤ x) : tanh (arcosh x) = √(x ^ 2 - 1) / x

theorem Real.arcosh_cosh {x : ℝ} (hx : 0 ≤ x) : arcosh (cosh x) = x

arcosh is the left inverse of cosh over [0, ∞).

theorem Real.arcosh_nonneg {x : ℝ} (hx : 1 ≤ x) : 0 ≤ arcosh x

theorem Real.arcosh_pos {x : ℝ} (hx : 1 < x) : 0 < arcosh x

theorem Real.strictMonoOn_arcosh : StrictMonoOn arcosh (Set.Ioi 0)

This holds for Ioi 0 instead of only Ici 1 due to junk values.

theorem Real.arcosh_le_arcosh {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : arcosh x ≤ arcosh y ↔ x ≤ y

This holds for 0 < x, y ≤ 1 due to junk values.

theorem Real.arcosh_lt_arcosh {x y : ℝ} (hx : 0 < x) (hy : 0 < y) : arcosh x < arcosh y ↔ x < y

This holds for 0 < x, y ≤ 1 due to junk values.

def Real.coshPartialEquiv : PartialEquiv ℝ ℝ

Real.cosh as a PartialEquiv.

Equations

• Real.coshPartialEquiv = { toFun := Real.cosh, invFun := Real.arcosh, source := Set.Ici 0, target := Set.Ici 1, map_source' := ⋯, map_target' := ⋯, left_inv' := ⋯, right_inv' := ⋯ }