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 and Real.arcosh bundled as a PartialEquiv from [0, ∞) to [1, ∞).

• Real.coshOpenPartialHomeomorph: Real.cosh as an OpenPartialHomeomorph from (0, ∞) to (1, ∞).

Main Results

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

• Real.cosh_bijOn, Real.cosh_injOn, Real.cosh_surjOn: Real.cosh is bijective, injective and surjective as a function from [0, ∞) to [1, ∞)

• Real.arcosh_bijOn, Real.arcosh_injOn, Real.arcosh_surjOn: Real.arcosh is bijective, injective and surjective as a function from [1, ∞) to [0, ∞)

• Real.continuousOn_arcosh: arcosh is continuous on [1, ∞)

• Real.differentiableOn_arcosh, Real.contDiffOn_arcosh: Real.arcosh is differentiable, and continuously differentiable on (1, ∞)

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 from [0, ∞) to [1, ∞).

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' := ⋯ }

theorem Real.continuousOn_arcosh : ContinuousOn arcosh (Set.Ici 1)

def Real.coshOpenPartialHomeomorph : OpenPartialHomeomorph ℝ ℝ

Real.cosh as an OpenPartialHomemorph from (0, ∞) to (1, ∞).

Equations

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

theorem Real.hasStrictDerivAt_arcosh {x : ℝ} (hx : x ∈ Set.Ioi 1) : HasStrictDerivAt arcosh (√(x ^ 2 - 1))⁻¹ x

theorem Real.hasDerivAt_arcosh {x : ℝ} (hx : x ∈ Set.Ioi 1) : HasDerivAt arcosh (√(x ^ 2 - 1))⁻¹ x

theorem Real.differentiableAt_arcosh {x : ℝ} (hx : x ∈ Set.Ioi 1) : DifferentiableAt ℝ arcosh x

theorem Real.differentiableOn_arcosh : DifferentiableOn ℝ arcosh (Set.Ioi 1)

theorem Real.contDiffAt_arcosh {n : WithTop ℕ∞} {x : ℝ} (hx : x ∈ Set.Ioi 1) : ContDiffAt ℝ n arcosh x

theorem Real.contDiffOn_arcosh {n : WithTop ℕ∞} : ContDiffOn ℝ n arcosh (Set.Ioi 1)

theorem Real.analyticAt_arcosh {x : ℝ} (hx : x ∈ Set.Ioi 1) : AnalyticAt ℝ arcosh x

The function Real.arcosh is real analytic.

theorem Real.analyticWithinAt_arcosh {s : Set ℝ} {x : ℝ} (hx : x ∈ Set.Ioi 1) : AnalyticWithinAt ℝ arcosh s x

The function Real.arcosh is real analytic.

theorem Real.analyticOnNhd_arcosh {s : Set ℝ} (hs : s ⊆ Set.Ioi 1) : AnalyticOnNhd ℝ arcosh s

The function Real.arcosh is real analytic.

theorem Real.analyticOn_arcosh {s : Set ℝ} (hs : s ⊆ Set.Ioi 1) : AnalyticOn ℝ arcosh s

The function Real.arcosh is real analytic.

theorem Real.cosh_bijOn : Set.BijOn cosh (Set.Ici 0) (Set.Ici 1)

theorem Real.cosh_injOn : Set.InjOn cosh (Set.Ici 0)

theorem Real.cosh_surjOn : Set.SurjOn cosh (Set.Ici 0) (Set.Ici 1)

theorem Real.arcosh_bijOn : Set.BijOn arcosh (Set.Ici 1) (Set.Ici 0)

theorem Real.arcosh_injOn : Set.InjOn arcosh (Set.Ici 1)

theorem Real.arcosh_surjOn : Set.SurjOn arcosh (Set.Ici 1) (Set.Ici 0)