Documentation

Mathlib.Analysis.SpecialFunctions.Arsinh

Inverse of the sinh function #

In this file we prove that sinh is bijective and hence has an inverse, arsinh.

Main definitions #

Main Results #

Tags #

arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective

def Real.arsinh (x : ) :

arsinh is defined using a logarithm, arsinh x = log (x + sqrt(1 + x^2)).

Instances For
    @[simp]
    @[simp]
    @[simp]

    arsinh is the right inverse of sinh.

    @[simp]
    theorem Real.cosh_arsinh (x : ) :

    sinh is surjective, ∀ b, ∃ a, sinh a = b. In this case, we use a = arsinh b.

    sinh is bijective, both injective and surjective.

    @[simp]

    arsinh is the left inverse of sinh.

    Real.sinh as an Equiv.

    Instances For
      @[simp]
      theorem Real.arsinh_inj {x : } {y : } :
      @[simp]
      @[simp]
      theorem Real.arsinh_lt_arsinh {x : } {y : } :
      @[simp]
      theorem Real.arsinh_eq_zero_iff {x : } :
      Real.arsinh x = 0 x = 0
      @[simp]
      @[simp]
      @[simp]
      theorem Real.arsinh_pos_iff {x : } :
      0 < Real.arsinh x 0 < x
      @[simp]
      theorem Real.arsinh_neg_iff {x : } :
      Real.arsinh x < 0 x < 0
      theorem Filter.Tendsto.arsinh {α : Type u_1} {l : Filter α} {f : α} {a : } (h : Filter.Tendsto f l (nhds a)) :
      Filter.Tendsto (fun x => Real.arsinh (f x)) l (nhds (Real.arsinh a))
      theorem ContinuousAt.arsinh {X : Type u_1} [TopologicalSpace X] {f : X} {a : X} (h : ContinuousAt f a) :
      ContinuousAt (fun x => Real.arsinh (f x)) a
      theorem ContinuousWithinAt.arsinh {X : Type u_1} [TopologicalSpace X] {f : X} {s : Set X} {a : X} (h : ContinuousWithinAt f s a) :
      ContinuousWithinAt (fun x => Real.arsinh (f x)) s a
      theorem ContinuousOn.arsinh {X : Type u_1} [TopologicalSpace X] {f : X} {s : Set X} (h : ContinuousOn f s) :
      ContinuousOn (fun x => Real.arsinh (f x)) s
      theorem Continuous.arsinh {X : Type u_1} [TopologicalSpace X] {f : X} (h : Continuous f) :
      Continuous fun x => Real.arsinh (f x)
      theorem HasStrictFDerivAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : E} {f' : E →L[] } (hf : HasStrictFDerivAt f f' a) :
      HasStrictFDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ f') a
      theorem HasFDerivAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : E} {f' : E →L[] } (hf : HasFDerivAt f f' a) :
      HasFDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ f') a
      theorem HasFDerivWithinAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {a : E} {f' : E →L[] } (hf : HasFDerivWithinAt f f' s a) :
      HasFDerivWithinAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ f') s a
      theorem DifferentiableAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : E} (h : DifferentiableAt f a) :
      DifferentiableAt (fun x => Real.arsinh (f x)) a
      theorem DifferentiableWithinAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {a : E} (h : DifferentiableWithinAt f s a) :
      theorem DifferentiableOn.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} (h : DifferentiableOn f s) :
      DifferentiableOn (fun x => Real.arsinh (f x)) s
      theorem ContDiffAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {a : E} {n : ℕ∞} (h : ContDiffAt n f a) :
      ContDiffAt n (fun x => Real.arsinh (f x)) a
      theorem ContDiffWithinAt.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {a : E} {n : ℕ∞} (h : ContDiffWithinAt n f s a) :
      ContDiffWithinAt n (fun x => Real.arsinh (f x)) s a
      theorem ContDiff.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {n : ℕ∞} (h : ContDiff n f) :
      ContDiff n fun x => Real.arsinh (f x)
      theorem ContDiffOn.arsinh {E : Type u_1} [NormedAddCommGroup E] [NormedSpace E] {f : E} {s : Set E} {n : ℕ∞} (h : ContDiffOn n f s) :
      ContDiffOn n (fun x => Real.arsinh (f x)) s
      theorem HasStrictDerivAt.arsinh {f : } {a : } {f' : } (hf : HasStrictDerivAt f f' a) :
      HasStrictDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ f') a
      theorem HasDerivAt.arsinh {f : } {a : } {f' : } (hf : HasDerivAt f f' a) :
      HasDerivAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ f') a
      theorem HasDerivWithinAt.arsinh {f : } {s : Set } {a : } {f' : } (hf : HasDerivWithinAt f f' s a) :
      HasDerivWithinAt (fun x => Real.arsinh (f x)) ((Real.sqrt (1 + f a ^ 2))⁻¹ f') s a