feat(analysis/special_functions/arsinh): add lemmas, review API (#14668)

src/analysis/calculus/cont_diff.lean

@@ -2737,6 +2737,18 @@ begin
     exact Itop n (cont_diff_at_top.mp hf n) }
 end
 
+/-- If `f` is an `n` times continuously differentiable homeomorphism,
+and if the derivative of `f` at each point is a continuous linear equivalence,
+then `f.symm` is `n` times continuously differentiable.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+theorem homeomorph.cont_diff_symm [complete_space E] (f : E ≃ₜ F) {f₀' : E → E ≃L[𝕜] F}
+  (hf₀' : ∀ a, has_fderiv_at f (f₀' a : E →L[𝕜] F) a) (hf : cont_diff 𝕜 n (f : E → F)) :
+  cont_diff 𝕜 n (f.symm : F → E) :=
+cont_diff_iff_cont_diff_at.2 $ λ x,
+  f.to_local_homeomorph.cont_diff_at_symm (mem_univ x) (hf₀' _) hf.cont_diff_at
+
 /-- Let `f` be a local homeomorphism of a nondiscrete normed field, let `a` be a point in its
 target. if `f` is `n` times continuously differentiable at `f.symm a`, and if the derivative at
 `f.symm a` is nonzero, then `f.symm` is `n` times continuously differentiable at the point `a`.
@@ -2749,6 +2761,18 @@ theorem local_homeomorph.cont_diff_at_symm_deriv [complete_space 𝕜]
   cont_diff_at 𝕜 n f.symm a :=
 f.cont_diff_at_symm ha (hf₀'.has_fderiv_at_equiv h₀) hf
 
+/-- Let `f` be an `n` times continuously differentiable homeomorphism of a nondiscrete normed field.
+Suppose that the derivative of `f` is never equal to zero. Then `f.symm` is `n` times continuously
+differentiable.
+
+This is one of the easy parts of the inverse function theorem: it assumes that we already have
+an inverse function. -/
+theorem homeomorph.cont_diff_symm_deriv [complete_space 𝕜] (f : 𝕜 ≃ₜ 𝕜) {f' : 𝕜 → 𝕜}
+  (h₀ : ∀ x, f' x ≠ 0) (hf' : ∀ x, has_deriv_at f (f' x) x) (hf : cont_diff 𝕜 n (f : 𝕜 → 𝕜)) :
+  cont_diff 𝕜 n (f.symm : 𝕜 → 𝕜) :=
+cont_diff_iff_cont_diff_at.2 $ λ x,
+  f.to_local_homeomorph.cont_diff_at_symm_deriv (h₀ _) (mem_univ x) (hf' _) hf.cont_diff_at
+
 end function_inverse
 
 

src/analysis/special_functions/arsinh.lean

@@ -12,66 +12,222 @@ import analysis.special_functions.log.basic
 In this file we prove that sinh is bijective and hence has an
 inverse, arsinh.
 
+## Main definitions
+
+- `real.arsinh`: The inverse function of `real.sinh`.
+
+- `real.sinh_equiv`, `real.sinh_order_iso`, `real.sinh_homeomorph`: `real.sinh` as an `equiv`,
+  `order_iso`, and `homeomorph`, respectively.
+
 ## Main Results
 
-- `sinh_surjective`: The proof that `sinh` is surjective
-- `sinh_bijective`: The proof `sinh` is bijective
-- `arsinh`: The inverse function of `sinh`
+- `real.sinh_surjective`, `real.sinh_bijective`: `real.sinh` is surjective and bijective;
+
+- `real.arsinh_injective`, `real.arsinh_surjective`, `real.arsinh_bijective`: `real.arsinh` is
+  injective, surjective, and bijective;
+
+- `real.continuous_arsinh`, `real.differentiable_arsinh`, `real.cont_diff_arsinh`: `real.arsinh` is
+  continuous, differentiable, and continuously differentiable; we also provide dot notation
+  convenience lemmas like `filter.tendsto.arsinh` and `cont_diff_at.arsinh`.
 
 ## Tags
 
 arsinh, arcsinh, argsinh, asinh, sinh injective, sinh bijective, sinh surjective
 -/
 noncomputable theory
 
+open function filter set
+open_locale topological_space
+
 namespace real
 
+variables {x y : ℝ}
+
 /-- `arsinh` is defined using a logarithm, `arsinh x = log (x + sqrt(1 + x^2))`. -/
 @[pp_nodot] def arsinh (x : ℝ) := log (x + sqrt (1 + x^2))
 
-private lemma aux_lemma (x : ℝ) : 1 / (x + sqrt (1 + x ^ 2)) = -x + sqrt (1 + x ^ 2) :=
+lemma exp_arsinh (x : ℝ) : exp (arsinh x) = x + sqrt (1 + x^2) :=
 begin
-  refine (eq_one_div_of_mul_eq_one_right _).symm,
-  have : 0 ≤ 1 + x ^ 2 := add_nonneg zero_le_one (sq_nonneg x),
-  rw [add_comm, ← sub_eq_neg_add, ← mul_self_sub_mul_self,
-      mul_self_sqrt this, sq, add_sub_cancel]
+  apply exp_log,
+  rw [← neg_lt_iff_pos_add'],
+  calc -x ≤ sqrt (x ^ 2) : le_sqrt_of_sq_le (neg_pow_bit0 _ _).le
+  ... < sqrt (1 + x ^ 2) : sqrt_lt_sqrt (sq_nonneg _) (lt_one_add _)
 end
 
-private lemma b_lt_sqrt_b_one_add_sq (b : ℝ) : b < sqrt (1 + b ^ 2) :=
-calc  b
-    ≤ sqrt (b ^ 2)     : le_sqrt_of_sq_le le_rfl
-... < sqrt (1 + b ^ 2) : sqrt_lt_sqrt (sq_nonneg _) (lt_one_add _)
+@[simp] lemma arsinh_zero : arsinh 0 = 0 := by simp [arsinh]
 
-private lemma add_sqrt_one_add_sq_pos (b : ℝ) : 0 < b + sqrt (1 + b ^ 2) :=
-by { rw [← neg_neg b, ← sub_eq_neg_add, sub_pos, sq, neg_mul_neg, ← sq],
-  exact b_lt_sqrt_b_one_add_sq (-b) }
+@[simp] lemma arsinh_neg (x : ℝ) : arsinh (-x) = -arsinh x :=
+begin
+  rw [← exp_eq_exp, exp_arsinh, exp_neg, exp_arsinh],
+  apply eq_inv_of_mul_eq_one_left,
+  rw [neg_sq, neg_add_eq_sub, add_comm x, mul_comm, ← sq_sub_sq, sq_sqrt, add_sub_cancel],
+  exact add_nonneg zero_le_one (sq_nonneg _)
+end
 
 /-- `arsinh` is the right inverse of `sinh`. -/
-lemma sinh_arsinh (x : ℝ) : sinh (arsinh x) = x :=
-by rw [sinh_eq, arsinh, ← log_inv, exp_log (add_sqrt_one_add_sq_pos x),
-      exp_log (inv_pos.2 (add_sqrt_one_add_sq_pos x)),
-      inv_eq_one_div, aux_lemma x, sub_eq_add_neg, neg_add, neg_neg, ← sub_eq_add_neg,
-      add_add_sub_cancel, add_self_div_two]
+@[simp] lemma sinh_arsinh (x : ℝ) : sinh (arsinh x) = x :=
+by { rw [sinh_eq, ← arsinh_neg, exp_arsinh, exp_arsinh, neg_sq], field_simp }
+
+@[simp] lemma cosh_arsinh (x : ℝ) : cosh (arsinh x) = sqrt (1 + x^2) :=
+by rw [← sqrt_sq (cosh_pos _).le, cosh_sq', sinh_arsinh]
 
 /-- `sinh` is surjective, `∀ b, ∃ a, sinh a = b`. In this case, we use `a = arsinh b`. -/
-lemma sinh_surjective : function.surjective sinh := function.left_inverse.surjective sinh_arsinh
+lemma sinh_surjective : surjective sinh := left_inverse.surjective sinh_arsinh
 
 /-- `sinh` is bijective, both injective and surjective. -/
-lemma sinh_bijective : function.bijective sinh :=
-⟨sinh_injective, sinh_surjective⟩
+lemma sinh_bijective : bijective sinh := ⟨sinh_injective, sinh_surjective⟩
+
+/-- `arsinh` is the left inverse of `sinh`. -/
+@[simp] lemma arsinh_sinh (x : ℝ) : arsinh (sinh x) = x :=
+right_inverse_of_injective_of_left_inverse sinh_injective sinh_arsinh x
+
+/-- `real.sinh` as an `equiv`. -/
+@[simps] def sinh_equiv : ℝ ≃ ℝ :=
+{ to_fun := sinh,
+  inv_fun := arsinh,
+  left_inv := arsinh_sinh,
+  right_inv := sinh_arsinh }
+
+/-- `real.sinh` as an `order_iso`. -/
+@[simps { fully_applied := ff }] def sinh_order_iso : ℝ ≃o ℝ :=
+{ to_equiv := sinh_equiv,
+  map_rel_iff' := @sinh_le_sinh }
 
-/-- A rearrangement and `sqrt` of `real.cosh_sq_sub_sinh_sq`. -/
-lemma sqrt_one_add_sinh_sq (x : ℝ): sqrt (1 + sinh x ^ 2) = cosh x :=
+/-- `real.sinh` as a `homeomorph`. -/
+@[simps { fully_applied := ff }] def sinh_homeomorph : ℝ ≃ₜ ℝ := sinh_order_iso.to_homeomorph
+
+lemma arsinh_bijective : bijective arsinh := sinh_equiv.symm.bijective
+lemma arsinh_injective : injective arsinh := sinh_equiv.symm.injective
+lemma arsinh_surjective : surjective arsinh := sinh_equiv.symm.surjective
+
+lemma arsinh_strict_mono : strict_mono arsinh := sinh_order_iso.symm.strict_mono
+
+@[simp] lemma arsinh_inj : arsinh x = arsinh y ↔ x = y := arsinh_injective.eq_iff
+@[simp] lemma arsinh_le_arsinh : arsinh x ≤ arsinh y ↔ x ≤ y := sinh_order_iso.symm.le_iff_le
+@[simp] lemma arsinh_lt_arsinh : arsinh x < arsinh y ↔ x < y := sinh_order_iso.symm.lt_iff_lt
+
+@[simp] lemma arsinh_eq_zero_iff : arsinh x = 0 ↔ x = 0 :=
+arsinh_injective.eq_iff' arsinh_zero
+
+@[simp] lemma arsinh_nonneg_iff : 0 ≤ arsinh x ↔ 0 ≤ x :=
+by rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
+
+@[simp] lemma arsinh_nonpos_iff : arsinh x ≤ 0 ↔ x ≤ 0 :=
+by rw [← sinh_le_sinh, sinh_zero, sinh_arsinh]
+
+@[simp] lemma arsinh_pos_iff : 0 < arsinh x ↔ 0 < x :=
+lt_iff_lt_of_le_iff_le arsinh_nonpos_iff
+
+@[simp] lemma arsinh_neg_iff : arsinh x < 0 ↔ x < 0 :=
+lt_iff_lt_of_le_iff_le arsinh_nonneg_iff
+
+lemma has_strict_deriv_at_arsinh (x : ℝ) : has_strict_deriv_at arsinh (sqrt (1 + x ^ 2))⁻¹ x :=
 begin
-  have H := real.cosh_sq_sub_sinh_sq x,
-  have G : cosh x ^ 2 - sinh x ^ 2 + sinh x ^ 2 = 1 + sinh x ^ 2 := by rw H,
-  rw sub_add_cancel at G,
-  rw [←G, sqrt_sq],
-  exact le_of_lt (cosh_pos x),
+  convert sinh_homeomorph.to_local_homeomorph.has_strict_deriv_at_symm (mem_univ x)
+    (cosh_pos _).ne' (has_strict_deriv_at_sinh _),
+  exact (cosh_arsinh _).symm
 end
 
-/-- `arsinh` is the left inverse of `sinh`. -/
-lemma arsinh_sinh (x : ℝ) : arsinh (sinh x) = x :=
-function.right_inverse_of_injective_of_left_inverse sinh_injective sinh_arsinh x
+lemma has_deriv_at_arsinh (x : ℝ) : has_deriv_at arsinh (sqrt (1 + x ^ 2))⁻¹ x :=
+(has_strict_deriv_at_arsinh x).has_deriv_at
+
+lemma differentiable_arsinh : differentiable ℝ arsinh :=
+λ x, (has_deriv_at_arsinh x).differentiable_at
+
+lemma cont_diff_arsinh {n : with_top ℕ} : cont_diff ℝ n arsinh :=
+sinh_homeomorph.cont_diff_symm_deriv (λ x, (cosh_pos x).ne') has_deriv_at_sinh cont_diff_sinh
+
+@[continuity] lemma continuous_arsinh : continuous arsinh := sinh_homeomorph.symm.continuous
 
 end real
+
+open real
+
+lemma filter.tendsto.arsinh {α : Type*} {l : filter α} {f : α → ℝ} {a : ℝ}
+  (h : tendsto f l (𝓝 a)) : tendsto (λ x, arsinh (f x)) l (𝓝 (arsinh a)) :=
+(continuous_arsinh.tendsto _).comp h
+
+section continuous
+
+variables {X : Type*} [topological_space X] {f : X → ℝ} {s : set X} {a : X}
+
+lemma continuous_at.arsinh (h : continuous_at f a) : continuous_at (λ x, arsinh (f x)) a := h.arsinh
+
+lemma continuous_within_at.arsinh (h : continuous_within_at f s a) :
+  continuous_within_at (λ x, arsinh (f x)) s a :=
+h.arsinh
+
+lemma continuous_on.arsinh (h : continuous_on f s) : continuous_on (λ x, arsinh (f x)) s :=
+λ x hx, (h x hx).arsinh
+
+lemma continuous.arsinh (h : continuous f) : continuous (λ x, arsinh (f x)) :=
+continuous_arsinh.comp h
+
+end continuous
+
+section fderiv
+
+variables {E : Type*} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {s : set E} {a : E}
+  {f' : E →L[ℝ] ℝ} {n : with_top ℕ}
+
+lemma has_strict_fderiv_at.arsinh (hf : has_strict_fderiv_at f f' a) :
+  has_strict_fderiv_at (λ x, arsinh (f x)) ((sqrt (1 + (f a) ^ 2))⁻¹ • f') a :=
+(has_strict_deriv_at_arsinh _).comp_has_strict_fderiv_at a hf
+
+lemma has_fderiv_at.arsinh (hf : has_fderiv_at f f' a) :
+  has_fderiv_at (λ x, arsinh (f x)) ((sqrt (1 + (f a) ^ 2))⁻¹ • f') a :=
+(has_deriv_at_arsinh _).comp_has_fderiv_at a hf
+
+lemma has_fderiv_within_at.arsinh (hf : has_fderiv_within_at f f' s a) :
+  has_fderiv_within_at (λ x, arsinh (f x)) ((sqrt (1 + (f a) ^ 2))⁻¹ • f') s a :=
+(has_deriv_at_arsinh _).comp_has_fderiv_within_at a hf
+
+lemma differentiable_at.arsinh (h : differentiable_at ℝ f a) :
+  differentiable_at ℝ (λ x, arsinh (f x)) a :=
+(differentiable_arsinh _).comp a h
+
+lemma differentiable_within_at.arsinh (h : differentiable_within_at ℝ f s a) :
+  differentiable_within_at ℝ (λ x, arsinh (f x)) s a :=
+(differentiable_arsinh _).comp_differentiable_within_at a h
+
+lemma differentiable_on.arsinh (h : differentiable_on ℝ f s) :
+  differentiable_on ℝ (λ x, arsinh (f x)) s :=
+λ x hx, (h x hx).arsinh
+
+lemma differentiable.arsinh (h : differentiable ℝ f) :
+  differentiable ℝ (λ x, arsinh (f x)) :=
+differentiable_arsinh.comp h
+
+lemma cont_diff_at.arsinh (h : cont_diff_at ℝ n f a) :
+  cont_diff_at ℝ n (λ x, arsinh (f x)) a :=
+cont_diff_arsinh.cont_diff_at.comp a h
+
+lemma cont_diff_within_at.arsinh (h : cont_diff_within_at ℝ n f s a) :
+  cont_diff_within_at ℝ n (λ x, arsinh (f x)) s a :=
+cont_diff_arsinh.cont_diff_at.comp_cont_diff_within_at a h
+
+lemma cont_diff.arsinh (h : cont_diff ℝ n f) : cont_diff ℝ n (λ x, arsinh (f x)) :=
+cont_diff_arsinh.comp h
+
+lemma cont_diff_on.arsinh (h : cont_diff_on ℝ n f s) : cont_diff_on ℝ n (λ x, arsinh (f x)) s :=
+λ x hx, (h x hx).arsinh
+
+end fderiv
+
+section deriv
+
+variables {f : ℝ → ℝ} {s : set ℝ} {a f' : ℝ}
+
+lemma has_strict_deriv_at.arsinh (hf : has_strict_deriv_at f f' a) :
+  has_strict_deriv_at (λ x, arsinh (f x)) ((sqrt (1 + (f a) ^ 2))⁻¹ • f') a :=
+(has_strict_deriv_at_arsinh _).comp a hf
+
+lemma has_deriv_at.arsinh (hf : has_deriv_at f f' a) :
+  has_deriv_at (λ x, arsinh (f x)) ((sqrt (1 + (f a) ^ 2))⁻¹ • f') a :=
+(has_deriv_at_arsinh _).comp a hf
+
+lemma has_deriv_within_at.arsinh (hf : has_deriv_within_at f f' s a) :
+  has_deriv_within_at (λ x, arsinh (f x)) ((sqrt (1 + (f a) ^ 2))⁻¹ • f') s a :=
+(has_deriv_at_arsinh _).comp_has_deriv_within_at a hf
+
+end deriv