Trigonometric functions #
Main definitions #
This file contains the following definitions:
- π, arcsin, arccos, arctan
- argument of a complex number
- logarithm on complex numbers
Main statements #
Many basic inequalities on trigonometric functions are established.
The continuity and differentiability of the usual trigonometric functions are proved, and their derivatives are computed.
polynomial.chebyshev.T_complex_cos: then-th Chebyshev polynomial evaluates oncomplex.cos θto the valuen * complex.cos θ.
Tags #
log, sin, cos, tan, arcsin, arccos, arctan, angle, argument
The complex sine function is everywhere strictly differentiable, with the derivative cos x.
The complex sine function is everywhere differentiable, with the derivative cos x.
The complex cosine function is everywhere strictly differentiable, with the derivative
-sin x.
The complex cosine function is everywhere differentiable, with the derivative -sin x.
The complex hyperbolic sine function is everywhere strictly differentiable, with the derivative
cosh x.
The complex hyperbolic sine function is everywhere differentiable, with the derivative
cosh x.
The complex hyperbolic cosine function is everywhere strictly differentiable, with the
derivative sinh x.
The complex hyperbolic cosine function is everywhere differentiable, with the derivative
sinh x.
Simp lemmas for derivatives of λ x, complex.cos (f x) etc., f : ℂ → ℂ #
theorem
measurable.ccos
{α : Type u_1}
[measurable_space α]
{f : α → ℂ}
(hf : measurable f) :
measurable (λ (x : α), complex.cos (f x))
theorem
has_strict_deriv_at.ccos
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℂ), complex.cos (f x)) ((-complex.sin (f x)) * f') x
theorem
has_deriv_at.ccos
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℂ), complex.cos (f x)) ((-complex.sin (f x)) * f') x
theorem
has_deriv_within_at.ccos
{f : ℂ → ℂ}
{f' x : ℂ}
{s : set ℂ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℂ), complex.cos (f x)) ((-complex.sin (f x)) * f') s x
theorem
deriv_within_ccos
{f : ℂ → ℂ}
{x : ℂ}
{s : set ℂ}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
deriv_within (λ (x : ℂ), complex.cos (f x)) s x = (-complex.sin (f x)) * deriv_within f s x
@[simp]
theorem
deriv_ccos
{f : ℂ → ℂ}
{x : ℂ}
(hc : differentiable_at ℂ f x) :
deriv (λ (x : ℂ), complex.cos (f x)) x = (-complex.sin (f x)) * deriv f x
theorem
measurable.csin
{α : Type u_1}
[measurable_space α]
{f : α → ℂ}
(hf : measurable f) :
measurable (λ (x : α), complex.sin (f x))
theorem
has_strict_deriv_at.csin
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℂ), complex.sin (f x)) ((complex.cos (f x)) * f') x
theorem
has_deriv_at.csin
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℂ), complex.sin (f x)) ((complex.cos (f x)) * f') x
theorem
has_deriv_within_at.csin
{f : ℂ → ℂ}
{f' x : ℂ}
{s : set ℂ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℂ), complex.sin (f x)) ((complex.cos (f x)) * f') s x
theorem
deriv_within_csin
{f : ℂ → ℂ}
{x : ℂ}
{s : set ℂ}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
deriv_within (λ (x : ℂ), complex.sin (f x)) s x = (complex.cos (f x)) * deriv_within f s x
@[simp]
theorem
deriv_csin
{f : ℂ → ℂ}
{x : ℂ}
(hc : differentiable_at ℂ f x) :
deriv (λ (x : ℂ), complex.sin (f x)) x = (complex.cos (f x)) * deriv f x
theorem
measurable.ccosh
{α : Type u_1}
[measurable_space α]
{f : α → ℂ}
(hf : measurable f) :
measurable (λ (x : α), complex.cosh (f x))
theorem
has_strict_deriv_at.ccosh
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℂ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x
theorem
has_deriv_at.ccosh
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℂ), complex.cosh (f x)) ((complex.sinh (f x)) * f') x
theorem
has_deriv_within_at.ccosh
{f : ℂ → ℂ}
{f' x : ℂ}
{s : set ℂ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℂ), complex.cosh (f x)) ((complex.sinh (f x)) * f') s x
theorem
deriv_within_ccosh
{f : ℂ → ℂ}
{x : ℂ}
{s : set ℂ}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
deriv_within (λ (x : ℂ), complex.cosh (f x)) s x = (complex.sinh (f x)) * deriv_within f s x
@[simp]
theorem
deriv_ccosh
{f : ℂ → ℂ}
{x : ℂ}
(hc : differentiable_at ℂ f x) :
deriv (λ (x : ℂ), complex.cosh (f x)) x = (complex.sinh (f x)) * deriv f x
theorem
measurable.csinh
{α : Type u_1}
[measurable_space α]
{f : α → ℂ}
(hf : measurable f) :
measurable (λ (x : α), complex.sinh (f x))
theorem
has_strict_deriv_at.csinh
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℂ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x
theorem
has_deriv_at.csinh
{f : ℂ → ℂ}
{f' x : ℂ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℂ), complex.sinh (f x)) ((complex.cosh (f x)) * f') x
theorem
has_deriv_within_at.csinh
{f : ℂ → ℂ}
{f' x : ℂ}
{s : set ℂ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℂ), complex.sinh (f x)) ((complex.cosh (f x)) * f') s x
theorem
deriv_within_csinh
{f : ℂ → ℂ}
{x : ℂ}
{s : set ℂ}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
deriv_within (λ (x : ℂ), complex.sinh (f x)) s x = (complex.cosh (f x)) * deriv_within f s x
@[simp]
theorem
deriv_csinh
{f : ℂ → ℂ}
{x : ℂ}
(hc : differentiable_at ℂ f x) :
deriv (λ (x : ℂ), complex.sinh (f x)) x = (complex.cosh (f x)) * deriv f x
Simp lemmas for derivatives of λ x, complex.cos (f x) etc., f : E → ℂ #
theorem
has_strict_fderiv_at.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) • f') x
theorem
has_fderiv_at.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) • f') x
theorem
has_fderiv_within_at.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.cos (f x)) (-complex.sin (f x) • f') s x
theorem
differentiable_within_at.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x) :
differentiable_within_at ℂ (λ (x : E), complex.cos (f x)) s x
@[simp]
theorem
differentiable_at.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
differentiable_at ℂ (λ (x : E), complex.cos (f x)) x
theorem
differentiable_on.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
(hc : differentiable_on ℂ f s) :
differentiable_on ℂ (λ (x : E), complex.cos (f x)) s
@[simp]
theorem
differentiable.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
(hc : differentiable ℂ f) :
differentiable ℂ (λ (x : E), complex.cos (f x))
theorem
fderiv_within_ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
fderiv_within ℂ (λ (x : E), complex.cos (f x)) s x = -complex.sin (f x) • fderiv_within ℂ f s x
@[simp]
theorem
fderiv_ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
fderiv ℂ (λ (x : E), complex.cos (f x)) x = -complex.sin (f x) • fderiv ℂ f x
theorem
times_cont_diff.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{n : with_top ℕ}
(h : times_cont_diff ℂ n f) :
times_cont_diff ℂ n (λ (x : E), complex.cos (f x))
theorem
times_cont_diff_at.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℂ n f x) :
times_cont_diff_at ℂ n (λ (x : E), complex.cos (f x)) x
theorem
times_cont_diff_on.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℂ n f s) :
times_cont_diff_on ℂ n (λ (x : E), complex.cos (f x)) s
theorem
times_cont_diff_within_at.ccos
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℂ n f s x) :
times_cont_diff_within_at ℂ n (λ (x : E), complex.cos (f x)) s x
theorem
has_strict_fderiv_at.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) • f') x
theorem
has_fderiv_at.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) • f') x
theorem
has_fderiv_within_at.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.sin (f x)) (complex.cos (f x) • f') s x
theorem
differentiable_within_at.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x) :
differentiable_within_at ℂ (λ (x : E), complex.sin (f x)) s x
@[simp]
theorem
differentiable_at.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
differentiable_at ℂ (λ (x : E), complex.sin (f x)) x
theorem
differentiable_on.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
(hc : differentiable_on ℂ f s) :
differentiable_on ℂ (λ (x : E), complex.sin (f x)) s
@[simp]
theorem
differentiable.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
(hc : differentiable ℂ f) :
differentiable ℂ (λ (x : E), complex.sin (f x))
theorem
fderiv_within_csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
fderiv_within ℂ (λ (x : E), complex.sin (f x)) s x = complex.cos (f x) • fderiv_within ℂ f s x
@[simp]
theorem
fderiv_csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
fderiv ℂ (λ (x : E), complex.sin (f x)) x = complex.cos (f x) • fderiv ℂ f x
theorem
times_cont_diff.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{n : with_top ℕ}
(h : times_cont_diff ℂ n f) :
times_cont_diff ℂ n (λ (x : E), complex.sin (f x))
theorem
times_cont_diff_at.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℂ n f x) :
times_cont_diff_at ℂ n (λ (x : E), complex.sin (f x)) x
theorem
times_cont_diff_on.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℂ n f s) :
times_cont_diff_on ℂ n (λ (x : E), complex.sin (f x)) s
theorem
times_cont_diff_within_at.csin
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℂ n f s x) :
times_cont_diff_within_at ℂ n (λ (x : E), complex.sin (f x)) s x
theorem
has_strict_fderiv_at.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) • f') x
theorem
has_fderiv_at.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) • f') x
theorem
has_fderiv_within_at.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.cosh (f x)) (complex.sinh (f x) • f') s x
theorem
differentiable_within_at.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x) :
differentiable_within_at ℂ (λ (x : E), complex.cosh (f x)) s x
@[simp]
theorem
differentiable_at.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
differentiable_at ℂ (λ (x : E), complex.cosh (f x)) x
theorem
differentiable_on.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
(hc : differentiable_on ℂ f s) :
differentiable_on ℂ (λ (x : E), complex.cosh (f x)) s
@[simp]
theorem
differentiable.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
(hc : differentiable ℂ f) :
differentiable ℂ (λ (x : E), complex.cosh (f x))
theorem
fderiv_within_ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
fderiv_within ℂ (λ (x : E), complex.cosh (f x)) s x = complex.sinh (f x) • fderiv_within ℂ f s x
@[simp]
theorem
fderiv_ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
fderiv ℂ (λ (x : E), complex.cosh (f x)) x = complex.sinh (f x) • fderiv ℂ f x
theorem
times_cont_diff.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{n : with_top ℕ}
(h : times_cont_diff ℂ n f) :
times_cont_diff ℂ n (λ (x : E), complex.cosh (f x))
theorem
times_cont_diff_at.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℂ n f x) :
times_cont_diff_at ℂ n (λ (x : E), complex.cosh (f x)) x
theorem
times_cont_diff_on.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℂ n f s) :
times_cont_diff_on ℂ n (λ (x : E), complex.cosh (f x)) s
theorem
times_cont_diff_within_at.ccosh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℂ n f s x) :
times_cont_diff_within_at ℂ n (λ (x : E), complex.cosh (f x)) s x
theorem
has_strict_fderiv_at.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) • f') x
theorem
has_fderiv_at.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) • f') x
theorem
has_fderiv_within_at.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), complex.sinh (f x)) (complex.cosh (f x) • f') s x
theorem
differentiable_within_at.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x) :
differentiable_within_at ℂ (λ (x : E), complex.sinh (f x)) s x
@[simp]
theorem
differentiable_at.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
differentiable_at ℂ (λ (x : E), complex.sinh (f x)) x
theorem
differentiable_on.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
(hc : differentiable_on ℂ f s) :
differentiable_on ℂ (λ (x : E), complex.sinh (f x)) s
@[simp]
theorem
differentiable.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
(hc : differentiable ℂ f) :
differentiable ℂ (λ (x : E), complex.sinh (f x))
theorem
fderiv_within_csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℂ f s x)
(hxs : unique_diff_within_at ℂ s x) :
fderiv_within ℂ (λ (x : E), complex.sinh (f x)) s x = complex.cosh (f x) • fderiv_within ℂ f s x
@[simp]
theorem
fderiv_csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(hc : differentiable_at ℂ f x) :
fderiv ℂ (λ (x : E), complex.sinh (f x)) x = complex.cosh (f x) • fderiv ℂ f x
theorem
times_cont_diff.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{n : with_top ℕ}
(h : times_cont_diff ℂ n f) :
times_cont_diff ℂ n (λ (x : E), complex.sinh (f x))
theorem
times_cont_diff_at.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℂ n f x) :
times_cont_diff_at ℂ n (λ (x : E), complex.sinh (f x)) x
theorem
times_cont_diff_on.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℂ n f s) :
times_cont_diff_on ℂ n (λ (x : E), complex.sinh (f x)) s
theorem
times_cont_diff_within_at.csinh
{E : Type u_1}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℂ n f s x) :
times_cont_diff_within_at ℂ n (λ (x : E), complex.sinh (f x)) s x
theorem
measurable.cos
{α : Type u_1}
[measurable_space α]
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), real.cos (f x))
theorem
has_deriv_within_at.cos
{f : ℝ → ℝ}
{f' x : ℝ}
{s : set ℝ}
(hf : has_deriv_within_at f f' s x) :
theorem
deriv_within_cos
{f : ℝ → ℝ}
{x : ℝ}
{s : set ℝ}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), real.cos (f x)) s x = (-real.sin (f x)) * deriv_within f s x
theorem
measurable.sin
{α : Type u_1}
[measurable_space α]
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), real.sin (f x))
theorem
has_strict_deriv_at.sin
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℝ), real.sin (f x)) ((real.cos (f x)) * f') x
theorem
has_deriv_at.sin
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℝ), real.sin (f x)) ((real.cos (f x)) * f') x
theorem
has_deriv_within_at.sin
{f : ℝ → ℝ}
{f' x : ℝ}
{s : set ℝ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℝ), real.sin (f x)) ((real.cos (f x)) * f') s x
theorem
deriv_within_sin
{f : ℝ → ℝ}
{x : ℝ}
{s : set ℝ}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), real.sin (f x)) s x = (real.cos (f x)) * deriv_within f s x
theorem
measurable.cosh
{α : Type u_1}
[measurable_space α]
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), real.cosh (f x))
theorem
has_strict_deriv_at.cosh
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℝ), real.cosh (f x)) ((real.sinh (f x)) * f') x
theorem
has_deriv_at.cosh
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℝ), real.cosh (f x)) ((real.sinh (f x)) * f') x
theorem
has_deriv_within_at.cosh
{f : ℝ → ℝ}
{f' x : ℝ}
{s : set ℝ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℝ), real.cosh (f x)) ((real.sinh (f x)) * f') s x
theorem
deriv_within_cosh
{f : ℝ → ℝ}
{x : ℝ}
{s : set ℝ}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), real.cosh (f x)) s x = (real.sinh (f x)) * deriv_within f s x
theorem
measurable.sinh
{α : Type u_1}
[measurable_space α]
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), real.sinh (f x))
theorem
has_strict_deriv_at.sinh
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℝ), real.sinh (f x)) ((real.cosh (f x)) * f') x
theorem
has_deriv_at.sinh
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℝ), real.sinh (f x)) ((real.cosh (f x)) * f') x
theorem
has_deriv_within_at.sinh
{f : ℝ → ℝ}
{f' x : ℝ}
{s : set ℝ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℝ), real.sinh (f x)) ((real.cosh (f x)) * f') s x
theorem
deriv_within_sinh
{f : ℝ → ℝ}
{x : ℝ}
{s : set ℝ}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), real.sinh (f x)) s x = (real.cosh (f x)) * deriv_within f s x
theorem
has_strict_fderiv_at.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.cos (f x)) (-real.sin (f x) • f') x
theorem
has_fderiv_at.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.cos (f x)) (-real.sin (f x) • f') x
theorem
has_fderiv_within_at.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.cos (f x)) (-real.sin (f x) • f') s x
theorem
differentiable_within_at.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (x : E), real.cos (f x)) s x
@[simp]
theorem
differentiable_at.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (x : E), real.cos (f x)) x
theorem
differentiable_on.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
(hc : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (x : E), real.cos (f x)) s
@[simp]
theorem
differentiable.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
(hc : differentiable ℝ f) :
differentiable ℝ (λ (x : E), real.cos (f x))
theorem
fderiv_within_cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
fderiv_within ℝ (λ (x : E), real.cos (f x)) s x = -real.sin (f x) • fderiv_within ℝ f s x
@[simp]
theorem
fderiv_cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
theorem
times_cont_diff.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : with_top ℕ}
(h : times_cont_diff ℝ n f) :
times_cont_diff ℝ n (λ (x : E), real.cos (f x))
theorem
times_cont_diff_at.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℝ n f x) :
times_cont_diff_at ℝ n (λ (x : E), real.cos (f x)) x
theorem
times_cont_diff_on.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℝ n f s) :
times_cont_diff_on ℝ n (λ (x : E), real.cos (f x)) s
theorem
times_cont_diff_within_at.cos
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℝ n f s x) :
times_cont_diff_within_at ℝ n (λ (x : E), real.cos (f x)) s x
theorem
has_strict_fderiv_at.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.sin (f x)) (real.cos (f x) • f') x
theorem
has_fderiv_at.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.sin (f x)) (real.cos (f x) • f') x
theorem
has_fderiv_within_at.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.sin (f x)) (real.cos (f x) • f') s x
theorem
differentiable_within_at.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (x : E), real.sin (f x)) s x
@[simp]
theorem
differentiable_at.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (x : E), real.sin (f x)) x
theorem
differentiable_on.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
(hc : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (x : E), real.sin (f x)) s
@[simp]
theorem
differentiable.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
(hc : differentiable ℝ f) :
differentiable ℝ (λ (x : E), real.sin (f x))
theorem
fderiv_within_sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
fderiv_within ℝ (λ (x : E), real.sin (f x)) s x = real.cos (f x) • fderiv_within ℝ f s x
@[simp]
theorem
fderiv_sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
theorem
times_cont_diff.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : with_top ℕ}
(h : times_cont_diff ℝ n f) :
times_cont_diff ℝ n (λ (x : E), real.sin (f x))
theorem
times_cont_diff_at.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℝ n f x) :
times_cont_diff_at ℝ n (λ (x : E), real.sin (f x)) x
theorem
times_cont_diff_on.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℝ n f s) :
times_cont_diff_on ℝ n (λ (x : E), real.sin (f x)) s
theorem
times_cont_diff_within_at.sin
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℝ n f s x) :
times_cont_diff_within_at ℝ n (λ (x : E), real.sin (f x)) s x
theorem
has_strict_fderiv_at.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) • f') x
theorem
has_fderiv_at.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) • f') x
theorem
has_fderiv_within_at.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.cosh (f x)) (real.sinh (f x) • f') s x
theorem
differentiable_within_at.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (x : E), real.cosh (f x)) s x
@[simp]
theorem
differentiable_at.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (x : E), real.cosh (f x)) x
theorem
differentiable_on.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
(hc : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (x : E), real.cosh (f x)) s
@[simp]
theorem
differentiable.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
(hc : differentiable ℝ f) :
differentiable ℝ (λ (x : E), real.cosh (f x))
theorem
fderiv_within_cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
fderiv_within ℝ (λ (x : E), real.cosh (f x)) s x = real.sinh (f x) • fderiv_within ℝ f s x
@[simp]
theorem
fderiv_cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
theorem
times_cont_diff.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : with_top ℕ}
(h : times_cont_diff ℝ n f) :
times_cont_diff ℝ n (λ (x : E), real.cosh (f x))
theorem
times_cont_diff_at.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℝ n f x) :
times_cont_diff_at ℝ n (λ (x : E), real.cosh (f x)) x
theorem
times_cont_diff_on.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℝ n f s) :
times_cont_diff_on ℝ n (λ (x : E), real.cosh (f x)) s
theorem
times_cont_diff_within_at.cosh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℝ n f s x) :
times_cont_diff_within_at ℝ n (λ (x : E), real.cosh (f x)) s x
theorem
has_strict_fderiv_at.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) • f') x
theorem
has_fderiv_at.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) • f') x
theorem
has_fderiv_within_at.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.sinh (f x)) (real.cosh (f x) • f') s x
theorem
differentiable_within_at.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (x : E), real.sinh (f x)) s x
@[simp]
theorem
differentiable_at.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (x : E), real.sinh (f x)) x
theorem
differentiable_on.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
(hc : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (x : E), real.sinh (f x)) s
@[simp]
theorem
differentiable.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
(hc : differentiable ℝ f) :
differentiable ℝ (λ (x : E), real.sinh (f x))
theorem
fderiv_within_sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
fderiv_within ℝ (λ (x : E), real.sinh (f x)) s x = real.cosh (f x) • fderiv_within ℝ f s x
@[simp]
theorem
fderiv_sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
theorem
times_cont_diff.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : with_top ℕ}
(h : times_cont_diff ℝ n f) :
times_cont_diff ℝ n (λ (x : E), real.sinh (f x))
theorem
times_cont_diff_at.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{n : with_top ℕ}
(hf : times_cont_diff_at ℝ n f x) :
times_cont_diff_at ℝ n (λ (x : E), real.sinh (f x)) x
theorem
times_cont_diff_on.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_on ℝ n f s) :
times_cont_diff_on ℝ n (λ (x : E), real.sinh (f x)) s
theorem
times_cont_diff_within_at.sinh
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{n : with_top ℕ}
(hf : times_cont_diff_within_at ℝ n f s x) :
times_cont_diff_within_at ℝ n (λ (x : E), real.sinh (f x)) s x
@[protected]
The number π = 3.14159265... Defined here using choice as twice a zero of cos in [1,2], from
which one can derive all its properties. For explicit bounds on π, see data.real.pi.
Equations
@[simp]
the series sqrt_two_add_series x n is sqrt(2 + sqrt(2 + ... )) with n square roots,
starting with x. We define it here because cos (pi / 2 ^ (n+1)) = sqrt_two_add_series 0 n / 2
Equations
- real.sqrt_two_add_series x (n + 1) = real.sqrt (2 + real.sqrt_two_add_series x n)
- real.sqrt_two_add_series x 0 = x
theorem
real.sqrt_two_add_series_nonneg
{x : ℝ}
(h : 0 ≤ x)
(n : ℕ) :
0 ≤ real.sqrt_two_add_series x n
theorem
real.sqrt_two_add_series_succ
(x : ℝ)
(n : ℕ) :
real.sqrt_two_add_series x (n + 1) = real.sqrt_two_add_series (real.sqrt (2 + x)) n
The type of angles
Equations
@[protected, instance]
@[protected, instance]
Equations
- real.angle.inhabited = {default := 0}
@[protected, instance]
Equations
Inverse of the sin function, returns values in the range -π / 2 ≤ arcsin x ≤ π / 2.
It defaults to -π / 2 on (-∞, -1) and to π / 2 to (1, ∞).
Equations
- real.arcsin = coe ∘ set.Icc_extend real.arcsin._proof_1 ⇑(real.sin_order_iso.symm)
theorem
real.arcsin_inj
{x y : ℝ}
(hx₁ : -1 ≤ x)
(hx₂ : x ≤ 1)
(hy₁ : -1 ≤ y)
(hy₂ : y ≤ 1) :
real.arcsin x = real.arcsin y ↔ x = y
@[simp]
real.sin as a local_homeomorph between (-π / 2, π / 2) and (-1, 1).
Equations
- real.sin_local_homeomorph = {to_local_equiv := {to_fun := real.sin, inv_fun := real.arcsin, source := set.Ioo (-(π / 2)) (π / 2), target := set.Ioo (-1) 1, map_source' := real.maps_to_sin_Ioo, map_target' := real.sin_local_homeomorph._proof_1, left_inv' := real.sin_local_homeomorph._proof_2, right_inv' := real.sin_local_homeomorph._proof_3}, open_source := real.sin_local_homeomorph._proof_4, open_target := real.sin_local_homeomorph._proof_5, continuous_to_fun := real.sin_local_homeomorph._proof_6, continuous_inv_fun := real.sin_local_homeomorph._proof_7}
theorem
real.deriv_arcsin_aux
{x : ℝ}
(h₁ : x ≠ -1)
(h₂ : x ≠ 1) :
has_strict_deriv_at real.arcsin (1 / real.sqrt (1 - x ^ 2)) x ∧ times_cont_diff_at ℝ ⊤ real.arcsin x
theorem
real.has_strict_deriv_at_arcsin
{x : ℝ}
(h₁ : x ≠ -1)
(h₂ : x ≠ 1) :
has_strict_deriv_at real.arcsin (1 / real.sqrt (1 - x ^ 2)) x
theorem
real.has_deriv_at_arcsin
{x : ℝ}
(h₁ : x ≠ -1)
(h₂ : x ≠ 1) :
has_deriv_at real.arcsin (1 / real.sqrt (1 - x ^ 2)) x
theorem
real.has_deriv_within_at_arcsin_Ici
{x : ℝ}
(h : x ≠ -1) :
has_deriv_within_at real.arcsin (1 / real.sqrt (1 - x ^ 2)) (set.Ici x) x
theorem
real.has_deriv_within_at_arcsin_Iic
{x : ℝ}
(h : x ≠ 1) :
has_deriv_within_at real.arcsin (1 / real.sqrt (1 - x ^ 2)) (set.Iic x) x
theorem
real.differentiable_within_at_arcsin_Ici
{x : ℝ} :
differentiable_within_at ℝ real.arcsin (set.Ici x) x ↔ x ≠ -1
theorem
real.differentiable_within_at_arcsin_Iic
{x : ℝ} :
differentiable_within_at ℝ real.arcsin (set.Iic x) x ↔ x ≠ 1
theorem
real.times_cont_diff_on_arcsin
{n : with_top ℕ} :
times_cont_diff_on ℝ n real.arcsin {-1, 1}ᶜ
theorem
real.times_cont_diff_at_arcsin_iff
{x : ℝ}
{n : with_top ℕ} :
times_cont_diff_at ℝ n real.arcsin x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
Inverse of the cos function, returns values in the range 0 ≤ arccos x and arccos x ≤ π.
If the argument is not between -1 and 1 it defaults to π / 2
Equations
- real.arccos x = π / 2 - real.arcsin x
theorem
real.arccos_inj
{x y : ℝ}
(hx₁ : -1 ≤ x)
(hx₂ : x ≤ 1)
(hy₁ : -1 ≤ y)
(hy₂ : y ≤ 1) :
real.arccos x = real.arccos y ↔ x = y
theorem
real.has_strict_deriv_at_arccos
{x : ℝ}
(h₁ : x ≠ -1)
(h₂ : x ≠ 1) :
has_strict_deriv_at real.arccos (-(1 / real.sqrt (1 - x ^ 2))) x
theorem
real.has_deriv_at_arccos
{x : ℝ}
(h₁ : x ≠ -1)
(h₂ : x ≠ 1) :
has_deriv_at real.arccos (-(1 / real.sqrt (1 - x ^ 2))) x
theorem
real.has_deriv_within_at_arccos_Ici
{x : ℝ}
(h : x ≠ -1) :
has_deriv_within_at real.arccos (-(1 / real.sqrt (1 - x ^ 2))) (set.Ici x) x
theorem
real.has_deriv_within_at_arccos_Iic
{x : ℝ}
(h : x ≠ 1) :
has_deriv_within_at real.arccos (-(1 / real.sqrt (1 - x ^ 2))) (set.Iic x) x
theorem
real.differentiable_within_at_arccos_Ici
{x : ℝ} :
differentiable_within_at ℝ real.arccos (set.Ici x) x ↔ x ≠ -1
theorem
real.differentiable_within_at_arccos_Iic
{x : ℝ} :
differentiable_within_at ℝ real.arccos (set.Iic x) x ↔ x ≠ 1
theorem
real.times_cont_diff_on_arccos
{n : with_top ℕ} :
times_cont_diff_on ℝ n real.arccos {-1, 1}ᶜ
theorem
real.times_cont_diff_at_arccos_iff
{x : ℝ}
{n : with_top ℕ} :
times_cont_diff_at ℝ n real.arccos x ↔ n = 0 ∨ x ≠ -1 ∧ x ≠ 1
arg returns values in the range (-π, π], such that for x ≠ 0,
sin (arg x) = x.im / x.abs and cos (arg x) = x.re / x.abs,
arg 0 defaults to 0
Equations
- x.arg = ite (0 ≤ x.re) (real.arcsin (x.im / complex.abs x)) (ite (0 ≤ x.im) (real.arcsin ((-x).im / complex.abs x) + π) (real.arcsin ((-x).im / complex.abs x) - π))
theorem
complex.ext_abs_arg
{x y : ℂ}
(h₁ : complex.abs x = complex.abs y)
(h₂ : x.arg = y.arg) :
x = y
Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π.
log 0 = 0
Equations
- complex.log x = ↑(real.log (complex.abs x)) + (↑(x.arg)) * complex.I
theorem
complex.log_exp
{x : ℂ}
(hx₁ : -π < x.im)
(hx₂ : x.im ≤ π) :
complex.log (complex.exp x) = x
theorem
complex.exp_eq_exp_iff_exp_sub_eq_one
{x y : ℂ} :
complex.exp x = complex.exp y ↔ complex.exp (x - y) = 1
complex.exp as a local_homeomorph with source = {z | -π < im z < π} and
target = {z | 0 < re z} ∪ {z | im z ≠ 0}. This definition is used to prove that complex.log
is complex differentiable at all points but the negative real semi-axis.
Equations
- complex.exp_local_homeomorph = local_homeomorph.of_continuous_open {to_fun := complex.exp, inv_fun := complex.log, source := {z : ℂ | z.im ∈ set.Ioo (-π) π}, target := {z : ℂ | 0 < z.re} ∪ {z : ℂ | z.im ≠ 0}, map_source' := complex.exp_local_homeomorph._proof_1, map_target' := complex.exp_local_homeomorph._proof_2, left_inv' := complex.exp_local_homeomorph._proof_3, right_inv' := complex.exp_local_homeomorph._proof_4} complex.exp_local_homeomorph._proof_5 complex.is_open_map_exp complex.exp_local_homeomorph._proof_6
theorem
complex.sin_eq_zero_iff_cos_eq
{z : ℂ} :
complex.sin z = 0 ↔ complex.cos z = 1 ∨ complex.cos z = -1
theorem
complex.tan_two_mul
{z : ℂ} :
complex.tan (2 * z) = 2 * complex.tan z / (1 - complex.tan z ^ 2)
theorem
complex.tan_add_mul_I
{x y : ℂ}
(h : ((∀ (k : ℤ), x ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), y * complex.I ≠ (2 * ↑l + 1) * ↑π / 2) ∨ (∃ (k : ℤ), x = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ (l : ℤ), y * complex.I = (2 * ↑l + 1) * ↑π / 2) :
complex.tan (x + y * complex.I) = (complex.tan x + (complex.tanh y) * complex.I) / (1 - ((complex.tan x) * complex.tanh y) * complex.I)
theorem
complex.tan_eq
{z : ℂ}
(h : ((∀ (k : ℤ), ↑(z.re) ≠ (2 * ↑k + 1) * ↑π / 2) ∧ ∀ (l : ℤ), (↑(z.im)) * complex.I ≠ (2 * ↑l + 1) * ↑π / 2) ∨ (∃ (k : ℤ), ↑(z.re) = (2 * ↑k + 1) * ↑π / 2) ∧ ∃ (l : ℤ), (↑(z.im)) * complex.I = (2 * ↑l + 1) * ↑π / 2) :
complex.tan z = (complex.tan ↑(z.re) + (complex.tanh ↑(z.im)) * complex.I) / (1 - ((complex.tan ↑(z.re)) * complex.tanh ↑(z.im)) * complex.I)
theorem
complex.has_strict_deriv_at_tan
{x : ℂ}
(h : complex.cos x ≠ 0) :
has_strict_deriv_at complex.tan (1 / complex.cos x ^ 2) x
theorem
complex.has_deriv_at_tan
{x : ℂ}
(h : complex.cos x ≠ 0) :
has_deriv_at complex.tan (1 / complex.cos x ^ 2) x
theorem
complex.tendsto_abs_tan_of_cos_eq_zero
{x : ℂ}
(hx : complex.cos x = 0) :
filter.tendsto (λ (x : ℂ), complex.abs (complex.tan x)) (𝓝[{x}ᶜ] x) filter.at_top
@[simp]
@[simp]
theorem
complex.differentiable_at_tan
{x : ℂ} :
differentiable_at ℂ complex.tan x ↔ complex.cos x ≠ 0
@[continuity]
@[simp]
theorem
complex.times_cont_diff_at_tan
{x : ℂ}
{n : with_top ℕ} :
times_cont_diff_at ℂ n complex.tan x ↔ complex.cos x ≠ 0
theorem
complex.cos_eq_iff_quadratic
{z w : ℂ} :
complex.cos z = w ↔ complex.exp (z * complex.I) ^ 2 - (2 * w) * complex.exp (z * complex.I) + 1 = 0
theorem
measurable.carg
{α : Type u_1}
[measurable_space α]
{f : α → ℂ}
(h : measurable f) :
measurable (λ (x : α), (f x).arg)
theorem
measurable.clog
{α : Type u_1}
[measurable_space α]
{f : α → ℂ}
(h : measurable f) :
measurable (λ (x : α), complex.log (f x))
theorem
filter.tendsto.clog
{α : Type u_1}
{l : filter α}
{f : α → ℂ}
{x : ℂ}
(h : filter.tendsto f l (𝓝 x))
(hx : 0 < x.re ∨ x.im ≠ 0) :
filter.tendsto (λ (t : α), complex.log (f t)) l (𝓝 (complex.log x))
theorem
continuous_at.clog
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{x : α}
(h₁ : continuous_at f x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
continuous_at (λ (t : α), complex.log (f t)) x
theorem
continuous_within_at.clog
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{s : set α}
{x : α}
(h₁ : continuous_within_at f s x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
continuous_within_at (λ (t : α), complex.log (f t)) s x
theorem
continuous_on.clog
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
{s : set α}
(h₁ : continuous_on f s)
(h₂ : ∀ (x : α), x ∈ s → 0 < (f x).re ∨ (f x).im ≠ 0) :
continuous_on (λ (t : α), complex.log (f t)) s
theorem
continuous.clog
{α : Type u_1}
[topological_space α]
{f : α → ℂ}
(h₁ : continuous f)
(h₂ : ∀ (x : α), 0 < (f x).re ∨ (f x).im ≠ 0) :
continuous (λ (t : α), complex.log (f t))
theorem
has_strict_fderiv_at.clog
{E : Type u_2}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(h₁ : has_strict_fderiv_at f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
has_strict_fderiv_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ • f') x
theorem
has_strict_deriv_at.clog
{f : ℂ → ℂ}
{f' x : ℂ}
(h₁ : has_strict_deriv_at f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
has_strict_deriv_at (λ (t : ℂ), complex.log (f t)) (f' / f x) x
theorem
has_fderiv_at.clog
{E : Type u_2}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{x : E}
(h₁ : has_fderiv_at f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
has_fderiv_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ • f') x
theorem
has_deriv_at.clog
{f : ℂ → ℂ}
{f' x : ℂ}
(h₁ : has_deriv_at f f' x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
has_deriv_at (λ (t : ℂ), complex.log (f t)) (f' / f x) x
theorem
differentiable_at.clog
{E : Type u_2}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{x : E}
(h₁ : differentiable_at ℂ f x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
differentiable_at ℂ (λ (t : E), complex.log (f t)) x
theorem
has_fderiv_within_at.clog
{E : Type u_2}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{f' : E →L[ℂ] ℂ}
{s : set E}
{x : E}
(h₁ : has_fderiv_within_at f f' s x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
has_fderiv_within_at (λ (t : E), complex.log (f t)) ((f x)⁻¹ • f') s x
theorem
has_deriv_within_at.clog
{f : ℂ → ℂ}
{f' x : ℂ}
{s : set ℂ}
(h₁ : has_deriv_within_at f f' s x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
has_deriv_within_at (λ (t : ℂ), complex.log (f t)) (f' / f x) s x
theorem
differentiable_within_at.clog
{E : Type u_2}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
{x : E}
(h₁ : differentiable_within_at ℂ f s x)
(h₂ : 0 < (f x).re ∨ (f x).im ≠ 0) :
differentiable_within_at ℂ (λ (t : E), complex.log (f t)) s x
theorem
differentiable_on.clog
{E : Type u_2}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
{s : set E}
(h₁ : differentiable_on ℂ f s)
(h₂ : ∀ (x : E), x ∈ s → 0 < (f x).re ∨ (f x).im ≠ 0) :
differentiable_on ℂ (λ (t : E), complex.log (f t)) s
theorem
differentiable.clog
{E : Type u_2}
[normed_group E]
[normed_space ℂ E]
{f : E → ℂ}
(h₁ : differentiable ℂ f)
(h₂ : ∀ (x : E), 0 < (f x).re ∨ (f x).im ≠ 0) :
differentiable ℂ (λ (t : E), complex.log (f t))
theorem
polynomial.chebyshev.T_complex_cos
(θ : ℂ)
(n : ℕ) :
polynomial.eval (complex.cos θ) (polynomial.chebyshev.T ℂ n) = complex.cos ((↑n) * θ)
The n-th Chebyshev polynomial of the first kind evaluates on cos θ to the
value cos (n * θ).
theorem
polynomial.chebyshev.cos_nat_mul
(n : ℕ)
(θ : ℂ) :
complex.cos ((↑n) * θ) = polynomial.eval (complex.cos θ) (polynomial.chebyshev.T ℂ n)
cos (n * θ) is equal to the n-th Chebyshev polynomial of the first kind evaluated
on cos θ.
theorem
polynomial.chebyshev.U_complex_cos
(θ : ℂ)
(n : ℕ) :
(polynomial.eval (complex.cos θ) (polynomial.chebyshev.U ℂ n)) * complex.sin θ = complex.sin ((↑n + 1) * θ)
The n-th Chebyshev polynomial of the second kind evaluates on cos θ to the
value sin ((n+1) * θ) / sin θ.
theorem
polynomial.chebyshev.sin_nat_succ_mul
(n : ℕ)
(θ : ℂ) :
complex.sin ((↑n + 1) * θ) = (polynomial.eval (complex.cos θ) (polynomial.chebyshev.U ℂ n)) * complex.sin θ
sin ((n + 1) * θ) is equal to sin θ multiplied with the n-th Chebyshev polynomial of the
second kind evaluated on cos θ.
theorem
real.has_strict_deriv_at_tan
{x : ℝ}
(h : real.cos x ≠ 0) :
has_strict_deriv_at real.tan (1 / real.cos x ^ 2) x
theorem
real.has_deriv_at_tan
{x : ℝ}
(h : real.cos x ≠ 0) :
has_deriv_at real.tan (1 / real.cos x ^ 2) x
theorem
real.tendsto_abs_tan_of_cos_eq_zero
{x : ℝ}
(hx : real.cos x = 0) :
filter.tendsto (λ (x : ℝ), abs (real.tan x)) (𝓝[{x}ᶜ] x) filter.at_top
@[continuity]
theorem
real.tendsto_tan_pi_div_two
:
filter.tendsto real.tan (𝓝[set.Iio (π / 2)] (π / 2)) filter.at_top
real.tan as an order_iso between (-(π / 2), π / 2) and ℝ.
Equations
- real.tan_order_iso = (strict_mono_incr_on.order_iso real.tan (set.Ioo (-(π / 2)) (π / 2)) real.strict_mono_incr_on_tan).trans ((order_iso.set_congr (real.tan '' set.Ioo (-(π / 2)) (π / 2)) set.univ real.image_tan_Ioo).trans order_iso.set.univ)
Inverse of the tan function, returns values in the range -π / 2 < arctan x and
arctan x < π / 2
Equations
- real.arctan x = ↑(⇑(real.tan_order_iso.symm) x)
theorem
real.arcsin_eq_arctan
{x : ℝ}
(h : x ∈ set.Ioo (-1) 1) :
real.arcsin x = real.arctan (x / real.sqrt (1 - x ^ 2))
real.tan as a local_homeomorph between (-(π / 2), π / 2) and the whole line.
Equations
- real.tan_local_homeomorph = {to_local_equiv := {to_fun := real.tan, inv_fun := real.arctan, source := set.Ioo (-(π / 2)) (π / 2), target := set.univ ℝ, map_source' := real.tan_local_homeomorph._proof_1, map_target' := real.tan_local_homeomorph._proof_2, left_inv' := real.tan_local_homeomorph._proof_3, right_inv' := real.tan_local_homeomorph._proof_4}, open_source := real.tan_local_homeomorph._proof_5, open_target := real.tan_local_homeomorph._proof_6, continuous_to_fun := real.continuous_on_tan_Ioo, continuous_inv_fun := real.tan_local_homeomorph._proof_7}
@[simp]
theorem
real.has_strict_deriv_at_arctan
(x : ℝ) :
has_strict_deriv_at real.arctan (1 / (1 + x ^ 2)) x
Lemmas for derivatives of the composition of real.arctan with a differentiable function #
In this section we register lemmas for the derivatives of the composition of real.arctan with a
differentiable function, for standalone use and use with simp.
theorem
measurable.arctan
{α : Type u_1}
[measurable_space α]
{f : α → ℝ}
(hf : measurable f) :
measurable (λ (x : α), real.arctan (f x))
theorem
has_strict_deriv_at.arctan
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ℝ), real.arctan (f x)) ((1 / (1 + f x ^ 2)) * f') x
theorem
has_deriv_at.arctan
{f : ℝ → ℝ}
{f' x : ℝ}
(hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℝ), real.arctan (f x)) ((1 / (1 + f x ^ 2)) * f') x
theorem
has_deriv_within_at.arctan
{f : ℝ → ℝ}
{f' x : ℝ}
{s : set ℝ}
(hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℝ), real.arctan (f x)) ((1 / (1 + f x ^ 2)) * f') s x
theorem
deriv_within_arctan
{f : ℝ → ℝ}
{x : ℝ}
{s : set ℝ}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
deriv_within (λ (x : ℝ), real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) * deriv_within f s x
theorem
has_strict_fderiv_at.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
theorem
has_fderiv_at.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
(hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
theorem
has_fderiv_within_at.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{f' : E →L[ℝ] ℝ}
{x : E}
{s : set E}
(hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') s x
theorem
fderiv_within_arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x)
(hxs : unique_diff_within_at ℝ s x) :
fderiv_within ℝ (λ (x : E), real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) • fderiv_within ℝ f s x
@[simp]
theorem
fderiv_arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
theorem
differentiable_within_at.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
(hf : differentiable_within_at ℝ f s x) :
differentiable_within_at ℝ (λ (x : E), real.arctan (f x)) s x
@[simp]
theorem
differentiable_at.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
(hc : differentiable_at ℝ f x) :
differentiable_at ℝ (λ (x : E), real.arctan (f x)) x
theorem
differentiable_on.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
(hc : differentiable_on ℝ f s) :
differentiable_on ℝ (λ (x : E), real.arctan (f x)) s
@[simp]
theorem
differentiable.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
(hc : differentiable ℝ f) :
differentiable ℝ (λ (x : E), real.arctan (f x))
theorem
times_cont_diff_at.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{n : with_top ℕ}
(h : times_cont_diff_at ℝ n f x) :
times_cont_diff_at ℝ n (λ (x : E), real.arctan (f x)) x
theorem
times_cont_diff.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{n : with_top ℕ}
(h : times_cont_diff ℝ n f) :
times_cont_diff ℝ n (λ (x : E), real.arctan (f x))
theorem
times_cont_diff_within_at.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{x : E}
{s : set E}
{n : with_top ℕ}
(h : times_cont_diff_within_at ℝ n f s x) :
times_cont_diff_within_at ℝ n (λ (x : E), real.arctan (f x)) s x
theorem
times_cont_diff_on.arctan
{E : Type u_1}
[normed_group E]
[normed_space ℝ E]
{f : E → ℝ}
{s : set E}
{n : with_top ℕ}
(h : times_cont_diff_on ℝ n f s) :
times_cont_diff_on ℝ n (λ (x : E), real.arctan (f x)) s