mathlib documentation

analysis.special_functions.trigonometric

Trigonometric functions

Main definitions

This file contains the following definitions:

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.

Tags

log, sin, cos, tan, arcsin, arccos, arctan, angle, argument

source
theorem complex.has_deriv_at_sin (x : ℂ) :
has_deriv_at complex.sin (complex.cos x) x

The complex sine function is everywhere differentiable, with the derivative cos x.

source
theorem complex.times_cont_diff_sin {n : with_top ℕ} :
times_cont_diff ℂ n complex.sin

source
theorem complex.differentiable_sin  :
differentiable ℂ complex.sin

source
theorem complex.differentiable_at_sin {x : ℂ} :
differentiable_at ℂ complex.sin x

source
@[simp]
theorem complex.deriv_sin  :
deriv complex.sin = complex.cos

source
theorem complex.continuous_sin  :
continuous complex.sin

source
theorem complex.continuous_on_sin {s : set ℂ} :
continuous_on complex.sin s

source
theorem complex.measurable_sin  :
measurable complex.sin

source
theorem complex.has_deriv_at_cos (x : ℂ) :
has_deriv_at complex.cos (-complex.sin x) x

The complex cosine function is everywhere differentiable, with the derivative -sin x.

source
theorem complex.times_cont_diff_cos {n : with_top ℕ} :
times_cont_diff ℂ n complex.cos

source
theorem complex.differentiable_cos  :
differentiable ℂ complex.cos

source
theorem complex.differentiable_at_cos {x : ℂ} :
differentiable_at ℂ complex.cos x

source
theorem complex.deriv_cos {x : ℂ} :
deriv complex.cos x = -complex.sin x

source
@[simp]
theorem complex.deriv_cos'  :
deriv complex.cos = λ (x : ℂ), -complex.sin x

source
theorem complex.continuous_cos  :
continuous complex.cos

source
theorem complex.continuous_on_cos {s : set ℂ} :
continuous_on complex.cos s

source
theorem complex.measurable_cos  :
measurable complex.cos

source
theorem complex.has_deriv_at_sinh (x : ℂ) :
has_deriv_at complex.sinh (complex.cosh x) x

The complex hyperbolic sine function is everywhere differentiable, with the derivative cosh x.

source
theorem complex.times_cont_diff_sinh {n : with_top ℕ} :
times_cont_diff ℂ n complex.sinh

source
theorem complex.differentiable_sinh  :
differentiable ℂ complex.sinh

source
theorem complex.differentiable_at_sinh {x : ℂ} :
differentiable_at ℂ complex.sinh x

source
@[simp]
theorem complex.deriv_sinh  :
deriv complex.sinh = complex.cosh

source
theorem complex.continuous_sinh  :
continuous complex.sinh

source
theorem complex.measurable_sinh  :
measurable complex.sinh

source
theorem complex.has_deriv_at_cosh (x : ℂ) :
has_deriv_at complex.cosh (complex.sinh x) x

The complex hyperbolic cosine function is everywhere differentiable, with the derivative sinh x.

source
theorem complex.times_cont_diff_cosh {n : with_top ℕ} :
times_cont_diff ℂ n complex.cosh

source
theorem complex.differentiable_cosh  :
differentiable ℂ complex.cosh

source
theorem complex.differentiable_at_cosh {x : ℂ} :
differentiable_at ℂ complex.cos x

source
@[simp]
theorem complex.deriv_cosh  :
deriv complex.cosh = complex.sinh

source
theorem complex.continuous_cosh  :
continuous complex.cosh

source
theorem complex.measurable_cosh  :
measurable complex.cosh

Simp lemmas for derivatives of λ x, complex.cos (f x) etc., f : ℂ → ℂ

complex.cos

source
theorem measurable.ccos {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :
measurable (λ (x : α), complex.cos (f x))

source
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

source
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

source
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

source
@[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

complex.sin

source
theorem measurable.csin {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :
measurable (λ (x : α), complex.sin (f x))

source
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

source
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

source
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

source
@[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

complex.cosh

source
theorem measurable.ccosh {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :
measurable (λ (x : α), complex.cosh (f x))

source
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

source
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

source
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

source
@[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

complex.sinh

source
theorem measurable.csinh {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :
measurable (λ (x : α), complex.sinh (f x))

source
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

source
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

source
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

source
@[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 → ℂ

complex.cos

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[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

source
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))

source
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

source
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

source
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

complex.sin

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[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

source
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))

source
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

source
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

source
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

complex.cosh

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[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

source
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))

source
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

source
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

source
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

complex.sinh

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[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

source
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))

source
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

source
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

source
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

source
theorem real.has_deriv_at_sin (x : ℝ) :
has_deriv_at real.sin (real.cos x) x

source
theorem real.times_cont_diff_sin {n : with_top ℕ} :
times_cont_diff ℝ n real.sin

source
theorem real.differentiable_sin  :
differentiable ℝ real.sin

source
theorem real.differentiable_at_sin {x : ℝ} :
differentiable_at ℝ real.sin x

source
@[simp]
theorem real.deriv_sin  :
deriv real.sin = real.cos

source
theorem real.continuous_sin  :
continuous real.sin

source
theorem real.measurable_sin  :
measurable real.sin

source
theorem real.has_deriv_at_cos (x : ℝ) :
has_deriv_at real.cos (-real.sin x) x

source
theorem real.times_cont_diff_cos {n : with_top ℕ} :
times_cont_diff ℝ n real.cos

source
theorem real.differentiable_cos  :
differentiable ℝ real.cos

source
theorem real.differentiable_at_cos {x : ℝ} :
differentiable_at ℝ real.cos x

source
theorem real.deriv_cos {x : ℝ} :
deriv real.cos x = -real.sin x

source
@[simp]
theorem real.deriv_cos'  :
deriv real.cos = λ (x : ℝ), -real.sin x

source
theorem real.continuous_cos  :
continuous real.cos

source
theorem real.continuous_on_cos {s : set ℝ} :
continuous_on real.cos s

source
theorem real.measurable_cos  :
measurable real.cos

source
theorem real.has_deriv_at_sinh (x : ℝ) :
has_deriv_at real.sinh (real.cosh x) x

source
theorem real.times_cont_diff_sinh {n : with_top ℕ} :
times_cont_diff ℝ n real.sinh

source
theorem real.differentiable_sinh  :
differentiable ℝ real.sinh

source
theorem real.differentiable_at_sinh {x : ℝ} :
differentiable_at ℝ real.sinh x

source
@[simp]
theorem real.deriv_sinh  :
deriv real.sinh = real.cosh

source
theorem real.continuous_sinh  :
continuous real.sinh

source
theorem real.measurable_sinh  :
measurable real.sinh

source
theorem real.has_deriv_at_cosh (x : ℝ) :
has_deriv_at real.cosh (real.sinh x) x

source
theorem real.times_cont_diff_cosh {n : with_top ℕ} :
times_cont_diff ℝ n real.cosh

source
theorem real.differentiable_cosh  :
differentiable ℝ real.cosh

source
theorem real.differentiable_at_cosh {x : ℝ} :
differentiable_at ℝ real.cosh x

source
@[simp]
theorem real.deriv_cosh  :
deriv real.cosh = real.sinh

source
theorem real.continuous_cosh  :
continuous real.cosh

source
theorem real.measurable_cosh  :
measurable real.cosh

source
theorem real.sinh_strict_mono  :
strict_mono real.sinh

sinh is strictly monotone.

Simp lemmas for derivatives of λ x, real.cos (f x) etc., f : ℝ → ℝ

real.cos

source
theorem measurable.cos {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
measurable (λ (x : α), real.cos (f x))

source
theorem has_deriv_at.cos {f : ℝ → ℝ} {f' x : ℝ} (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ℝ), real.cos (f x)) ((-real.sin (f x)) * f') x

source
theorem has_deriv_within_at.cos {f : ℝ → ℝ} {f' x : ℝ} {s : set ℝ} (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ℝ), real.cos (f x)) ((-real.sin (f x)) * f') s x

source
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

source
@[simp]
theorem deriv_cos {f : ℝ → ℝ} {x : ℝ} (hc : differentiable_at ℝ f x) :
deriv (λ (x : ℝ), real.cos (f x)) x = (-real.sin (f x)) * deriv f x

real.sin

source
theorem measurable.sin {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
measurable (λ (x : α), real.sin (f x))

source
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

source
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

source
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

source
@[simp]
theorem deriv_sin {f : ℝ → ℝ} {x : ℝ} (hc : differentiable_at ℝ f x) :
deriv (λ (x : ℝ), real.sin (f x)) x = (real.cos (f x)) * deriv f x

real.cosh

source
theorem measurable.cosh {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
measurable (λ (x : α), real.cosh (f x))

source
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

source
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

source
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

source
@[simp]
theorem deriv_cosh {f : ℝ → ℝ} {x : ℝ} (hc : differentiable_at ℝ f x) :
deriv (λ (x : ℝ), real.cosh (f x)) x = (real.sinh (f x)) * deriv f x

real.sinh

source
theorem measurable.sinh {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :
measurable (λ (x : α), real.sinh (f x))

source
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

source
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

source
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

source
@[simp]
theorem deriv_sinh {f : ℝ → ℝ} {x : ℝ} (hc : differentiable_at ℝ f x) :
deriv (λ (x : ℝ), real.sinh (f x)) x = (real.cosh (f x)) * deriv f x

Simp lemmas for derivatives of λ x, real.cos (f x) etc., f : E → ℝ

real.cos

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[simp]
theorem fderiv_cos {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hc : differentiable_at ℝ f x) :
fderiv ℝ (λ (x : E), real.cos (f x)) x = -real.sin (f x) • fderiv ℝ f x

source
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))

source
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

source
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

source
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

real.sin

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[simp]
theorem fderiv_sin {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hc : differentiable_at ℝ f x) :
fderiv ℝ (λ (x : E), real.sin (f x)) x = real.cos (f x) • fderiv ℝ f x

source
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))

source
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

source
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

source
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

real.cosh

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[simp]
theorem fderiv_cosh {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hc : differentiable_at ℝ f x) :
fderiv ℝ (λ (x : E), real.cosh (f x)) x = real.sinh (f x) • fderiv ℝ f x

source
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))

source
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

source
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

source
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

real.sinh

source
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

source
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

source
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

source
@[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

source
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

source
@[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))

source
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

source
@[simp]
theorem fderiv_sinh {E : Type u_1} [normed_group E] [normed_space ℝ E] {f : E → ℝ} {x : E} (hc : differentiable_at ℝ f x) :
fderiv ℝ (λ (x : E), real.sinh (f x)) x = real.cosh (f x) • fderiv ℝ f x

source
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))

source
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

source
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

source
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

source
theorem real.exists_cos_eq_zero  :
0 ∈ real.cos '' set.Icc 1 2

source
def real.pi  :
ℝ

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
source
@[simp]
theorem real.cos_pi_div_two  :
real.cos (π / 2) = 0

source
theorem real.one_le_pi_div_two  :
1 ≤ π / 2

source
theorem real.pi_div_two_le_two  :
π / 2 ≤ 2

source
theorem real.two_le_pi  :
2 ≤ π

source
theorem real.pi_le_four  :
π ≤ 4

source
theorem real.pi_pos  :
0 < π

source
theorem real.pi_ne_zero  :
π ≠ 0

source
theorem real.pi_div_two_pos  :
0 < π / 2

source
theorem real.two_pi_pos  :
0 < 2 * π

source
@[simp]
theorem real.sin_pi  :
real.sin π = 0

source
@[simp]
theorem real.cos_pi  :
real.cos π = -1

source
@[simp]
theorem real.sin_two_pi  :
real.sin (2 * π) = 0

source
@[simp]
theorem real.cos_two_pi  :
real.cos (2 * π) = 1

source
theorem real.sin_add_pi (x : ℝ) :
real.sin (x + π) = -real.sin x

source
theorem real.sin_add_two_pi (x : ℝ) :
real.sin (x + 2 * π) = real.sin x

source
theorem real.cos_add_two_pi (x : ℝ) :
real.cos (x + 2 * π) = real.cos x

source
theorem real.sin_pi_sub (x : ℝ) :
real.sin (π - x) = real.sin x

source
theorem real.cos_add_pi (x : ℝ) :
real.cos (x + π) = -real.cos x

source
theorem real.cos_pi_sub (x : ℝ) :
real.cos (π - x) = -real.cos x

source
theorem real.sin_pos_of_pos_of_lt_pi {x : ℝ} (h0x : 0 < x) (hxp : x < π) :
0 < real.sin x

source
theorem real.sin_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ set.Ioo 0 π) :
0 < real.sin x

source
theorem real.sin_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ set.Icc 0 π) :
0 ≤ real.sin x

source
theorem real.sin_nonneg_of_nonneg_of_le_pi {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ π) :
0 ≤ real.sin x

source
theorem real.sin_neg_of_neg_of_neg_pi_lt {x : ℝ} (hx0 : x < 0) (hpx : -π < x) :
real.sin x < 0

source
theorem real.sin_nonpos_of_nonnpos_of_neg_pi_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -π ≤ x) :
real.sin x ≤ 0

source
@[simp]
theorem real.sin_pi_div_two  :
real.sin (π / 2) = 1

source
theorem real.sin_add_pi_div_two (x : ℝ) :
real.sin (x + π / 2) = real.cos x

source
theorem real.sin_sub_pi_div_two (x : ℝ) :
real.sin (x - π / 2) = -real.cos x

source
theorem real.sin_pi_div_two_sub (x : ℝ) :
real.sin (π / 2 - x) = real.cos x

source
theorem real.cos_add_pi_div_two (x : ℝ) :
real.cos (x + π / 2) = -real.sin x

source
theorem real.cos_sub_pi_div_two (x : ℝ) :
real.cos (x - π / 2) = real.sin x

source
theorem real.cos_pi_div_two_sub (x : ℝ) :
real.cos (π / 2 - x) = real.sin x

source
theorem real.cos_pos_of_mem_Ioo {x : ℝ} (hx : x ∈ set.Ioo (-(π / 2)) (π / 2)) :
0 < real.cos x

source
theorem real.cos_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ set.Icc (-(π / 2)) (π / 2)) :
0 ≤ real.cos x

source
theorem real.cos_neg_of_pi_div_two_lt_of_lt {x : ℝ} (hx₁ : π / 2 < x) (hx₂ : x < π + π / 2) :
real.cos x < 0

source
theorem real.cos_nonpos_of_pi_div_two_le_of_le {x : ℝ} (hx₁ : π / 2 ≤ x) (hx₂ : x ≤ π + π / 2) :
real.cos x ≤ 0

source
theorem real.sin_nat_mul_pi (n : ℕ) :
real.sin ((↑n) * π) = 0

source
theorem real.sin_int_mul_pi (n : ℤ) :
real.sin ((↑n) * π) = 0

source
theorem real.cos_nat_mul_two_pi (n : ℕ) :
real.cos ((↑n) * 2 * π) = 1

source
theorem real.cos_int_mul_two_pi (n : ℤ) :
real.cos ((↑n) * 2 * π) = 1

source
theorem real.cos_int_mul_two_pi_add_pi (n : ℤ) :
real.cos ((↑n) * 2 * π + π) = -1

source
theorem real.sin_eq_zero_iff_of_lt_of_lt {x : ℝ} (hx₁ : -π < x) (hx₂ : x < π) :
real.sin x = 0 ↔ x = 0

source
theorem real.sin_eq_zero_iff {x : ℝ} :
real.sin x = 0 ↔ ∃ (n : ℤ), (↑n) * π = x

source
theorem real.sin_ne_zero_iff {x : ℝ} :
real.sin x ≠ 0 ↔ ∀ (n : ℤ), (↑n) * π ≠ x

source
theorem real.sin_eq_zero_iff_cos_eq {x : ℝ} :
real.sin x = 0 ↔ real.cos x = 1 ∨ real.cos x = -1

source
theorem real.cos_eq_one_iff (x : ℝ) :
real.cos x = 1 ↔ ∃ (n : ℤ), (↑n) * 2 * π = x

source
theorem real.cos_eq_one_iff_of_lt_of_lt {x : ℝ} (hx₁ : -2 * π < x) (hx₂ : x < 2 * π) :
real.cos x = 1 ↔ x = 0

source
theorem real.cos_lt_cos_of_nonneg_of_le_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π / 2) (hxy : x < y) :
real.cos y < real.cos x

source
theorem real.cos_lt_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π) (hxy : x < y) :
real.cos y < real.cos x

source
theorem real.strict_mono_decr_on_cos  :
strict_mono_decr_on real.cos (set.Icc 0 π)

source
theorem real.cos_le_cos_of_nonneg_of_le_pi {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y ≤ π) (hxy : x ≤ y) :
real.cos y ≤ real.cos x

source
theorem real.sin_lt_sin_of_lt_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hy₂ : y ≤ π / 2) (hxy : x < y) :
real.sin x < real.sin y

source
theorem real.strict_mono_incr_on_sin  :
strict_mono_incr_on real.sin (set.Icc (-(π / 2)) (π / 2))

source
theorem real.sin_le_sin_of_le_of_le_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) ≤ x) (hy₂ : y ≤ π / 2) (hxy : x ≤ y) :
real.sin x ≤ real.sin y

source
theorem real.inj_on_sin  :
set.inj_on real.sin (set.Icc (-(π / 2)) (π / 2))

source
theorem real.inj_on_cos  :
set.inj_on real.cos (set.Icc 0 π)

source
theorem real.surj_on_sin  :
set.surj_on real.sin (set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)

source
theorem real.surj_on_cos  :
set.surj_on real.cos (set.Icc 0 π) (set.Icc (-1) 1)

source
theorem real.sin_mem_Icc (x : ℝ) :
real.sin x ∈ set.Icc (-1) 1

source
theorem real.cos_mem_Icc (x : ℝ) :
real.cos x ∈ set.Icc (-1) 1

source
theorem real.maps_to_sin (s : set ℝ) :
set.maps_to real.sin s (set.Icc (-1) 1)

source
theorem real.maps_to_cos (s : set ℝ) :
set.maps_to real.cos s (set.Icc (-1) 1)

source
theorem real.bij_on_sin  :
set.bij_on real.sin (set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1)

source
theorem real.bij_on_cos  :
set.bij_on real.cos (set.Icc 0 π) (set.Icc (-1) 1)

source
@[simp]
theorem real.range_cos  :
set.range real.cos = set.Icc (-1) 1

source
@[simp]
theorem real.range_sin  :
set.range real.sin = set.Icc (-1) 1

source
theorem real.range_cos_infinite  :
(set.range real.cos).infinite

source
theorem real.range_sin_infinite  :
(set.range real.sin).infinite

source
theorem real.sin_lt {x : ℝ} (h : 0 < x) :
real.sin x < x

source
theorem real.sin_gt_sub_cube {x : ℝ} (h : 0 < x) (h' : x ≤ 1) :
x - x ^ 3 / 4 < real.sin x

source
@[simp]
def real.sqrt_two_add_series (x : ℝ) :
ℕ → ℝ

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
source
theorem real.sqrt_two_add_series_zero (x : ℝ) :
real.sqrt_two_add_series x 0 = x

source
theorem real.sqrt_two_add_series_one  :
real.sqrt_two_add_series 0 1 = real.sqrt 2

source
theorem real.sqrt_two_add_series_two  :
real.sqrt_two_add_series 0 2 = real.sqrt (2 + real.sqrt 2)

source
theorem real.sqrt_two_add_series_zero_nonneg (n : ℕ) :
0 ≤ real.sqrt_two_add_series 0 n

source
theorem real.sqrt_two_add_series_nonneg {x : ℝ} (h : 0 ≤ x) (n : ℕ) :
0 ≤ real.sqrt_two_add_series x n

source
theorem real.sqrt_two_add_series_lt_two (n : ℕ) :
real.sqrt_two_add_series 0 n < 2

source
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

source
theorem real.sqrt_two_add_series_monotone_left {x y : ℝ} (h : x ≤ y) (n : ℕ) :
real.sqrt_two_add_series x n ≤ real.sqrt_two_add_series y n

source
@[simp]
theorem real.cos_pi_over_two_pow (n : ℕ) :
real.cos (π / 2 ^ (n + 1)) = real.sqrt_two_add_series 0 n / 2

source
theorem real.sin_square_pi_over_two_pow (n : ℕ) :
real.sin (π / 2 ^ (n + 1)) ^ 2 = 1 - (real.sqrt_two_add_series 0 n / 2) ^ 2

source
theorem real.sin_square_pi_over_two_pow_succ (n : ℕ) :
real.sin (π / 2 ^ (n + 2)) ^ 2 = 1 / 2 - real.sqrt_two_add_series 0 n / 4

source
@[simp]
theorem real.sin_pi_over_two_pow_succ (n : ℕ) :
real.sin (π / 2 ^ (n + 2)) = real.sqrt (2 - real.sqrt_two_add_series 0 n) / 2

source
@[simp]
theorem real.cos_pi_div_four  :
real.cos (π / 4) = real.sqrt 2 / 2

source
@[simp]
theorem real.sin_pi_div_four  :
real.sin (π / 4) = real.sqrt 2 / 2

source
@[simp]
theorem real.cos_pi_div_eight  :
real.cos (π / 8) = real.sqrt (2 + real.sqrt 2) / 2

source
@[simp]
theorem real.sin_pi_div_eight  :
real.sin (π / 8) = real.sqrt (2 - real.sqrt 2) / 2

source
@[simp]
theorem real.cos_pi_div_sixteen  :
real.cos (π / 16) = real.sqrt (2 + real.sqrt (2 + real.sqrt 2)) / 2

source
@[simp]
theorem real.sin_pi_div_sixteen  :
real.sin (π / 16) = real.sqrt (2 - real.sqrt (2 + real.sqrt 2)) / 2

source
@[simp]
theorem real.cos_pi_div_thirty_two  :
real.cos (π / 32) = real.sqrt (2 + real.sqrt (2 + real.sqrt (2 + real.sqrt 2))) / 2

source
@[simp]
theorem real.sin_pi_div_thirty_two  :
real.sin (π / 32) = real.sqrt (2 - real.sqrt (2 + real.sqrt (2 + real.sqrt 2))) / 2

source
@[simp]
theorem real.cos_pi_div_three  :
real.cos (π / 3) = 1 / 2

The cosine of π / 3 is 1 / 2.

source
theorem real.square_cos_pi_div_six  :
real.cos (π / 6) ^ 2 = 3 / 4

The square of the cosine of π / 6 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

source
@[simp]
theorem real.cos_pi_div_six  :
real.cos (π / 6) = real.sqrt 3 / 2

The cosine of π / 6 is √3 / 2.

source
@[simp]
theorem real.sin_pi_div_six  :
real.sin (π / 6) = 1 / 2

The sine of π / 6 is 1 / 2.

source
theorem real.square_sin_pi_div_three  :
real.sin (π / 3) ^ 2 = 3 / 4

The square of the sine of π / 3 is 3 / 4 (this is sometimes more convenient than the result for cosine itself).

source
@[simp]
theorem real.sin_pi_div_three  :
real.sin (π / 3) = real.sqrt 3 / 2

The sine of π / 3 is √3 / 2.

source
def real.angle  :
Type

The type of angles

Equations
source
@[instance]
def real.angle.angle.add_comm_group  :
add_comm_group real.angle

Equations
source
@[instance]
def real.angle.inhabited  :
inhabited real.angle

Equations
source
@[instance]
def real.angle.angle.has_coe  :
has_coe ℝ real.angle

Equations
source
@[simp]
theorem real.angle.coe_zero  :
↑0 = 0

source
@[simp]
theorem real.angle.coe_add (x y : ℝ) :
↑(x + y) = ↑x + ↑y

source
@[simp]
theorem real.angle.coe_neg (x : ℝ) :
↑-x = -↑x

source
@[simp]
theorem real.angle.coe_sub (x y : ℝ) :
↑(x - y) = ↑x - ↑y

source
@[simp]
theorem real.angle.coe_nat_mul_eq_nsmul (x : ℝ) (n : ℕ) :
↑(↑n) * x = n •ℕ ↑x

source
@[simp]
theorem real.angle.coe_int_mul_eq_gsmul (x : ℝ) (n : ℤ) :
↑(↑n) * x = n •ℤ ↑x

source
@[simp]
theorem real.angle.coe_two_pi  :
↑2 * π = 0

source
theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} :
↑θ = ↑ψ ↔ ∃ (k : ℤ), θ - ψ = (2 * π) * ↑k

source
theorem real.angle.cos_eq_iff_eq_or_eq_neg {θ ψ : ℝ} :
real.cos θ = real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

source
theorem real.angle.sin_eq_iff_eq_or_add_eq_pi {θ ψ : ℝ} :
real.sin θ = real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑π

source
theorem real.angle.cos_sin_inj {θ ψ : ℝ} (Hcos : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :
↑θ = ↑ψ

source
def real.sin_order_iso  :
↥(set.Icc (-(π / 2)) (π / 2)) ≃o ↥(set.Icc (-1) 1)

real.sin as an order_iso between [-(π / 2), π / 2] and [-1, 1].

Equations
source
@[simp]
theorem real.coe_sin_order_iso_apply (x : ↥(set.Icc (-(π / 2)) (π / 2))) :
↑(⇑real.sin_order_iso x) = real.sin ↑x

source
theorem real.sin_order_iso_apply (x : ↥(set.Icc (-(π / 2)) (π / 2))) :
⇑real.sin_order_iso x = ⟨real.sin ↑x, _⟩

source
def real.arcsin  :
ℝ → ℝ

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
source
theorem real.arcsin_mem_Icc (x : ℝ) :
real.arcsin x ∈ set.Icc (-(π / 2)) (π / 2)

source
@[simp]
theorem real.range_arcsin  :
set.range real.arcsin = set.Icc (-(π / 2)) (π / 2)

source
theorem real.arcsin_le_pi_div_two (x : ℝ) :
real.arcsin x ≤ π / 2

source
theorem real.neg_pi_div_two_le_arcsin (x : ℝ) :
-(π / 2) ≤ real.arcsin x

source
theorem real.arcsin_proj_Icc (x : ℝ) :
real.arcsin ↑(set.proj_Icc (-1) 1 _ x) = real.arcsin x

source
theorem real.sin_arcsin' {x : ℝ} (hx : x ∈ set.Icc (-1) 1) :
real.sin (real.arcsin x) = x

source
theorem real.sin_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
real.sin (real.arcsin x) = x

source
theorem real.arcsin_sin' {x : ℝ} (hx : x ∈ set.Icc (-(π / 2)) (π / 2)) :
real.arcsin (real.sin x) = x

source
theorem real.arcsin_sin {x : ℝ} (hx₁ : -(π / 2) ≤ x) (hx₂ : x ≤ π / 2) :
real.arcsin (real.sin x) = x

source
theorem real.strict_mono_incr_on_arcsin  :
strict_mono_incr_on real.arcsin (set.Icc (-1) 1)

source
theorem real.monotone_arcsin  :
monotone real.arcsin

source
theorem real.inj_on_arcsin  :
set.inj_on real.arcsin (set.Icc (-1) 1)

source
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

source
theorem real.continuous_arcsin  :
continuous real.arcsin

source
theorem real.continuous_at_arcsin {x : ℝ} :
continuous_at real.arcsin x

source
theorem real.arcsin_eq_of_sin_eq {x y : ℝ} (h₁ : real.sin x = y) (h₂ : x ∈ set.Icc (-(π / 2)) (π / 2)) :
real.arcsin y = x

source
@[simp]
theorem real.arcsin_zero  :
real.arcsin 0 = 0

source
@[simp]
theorem real.arcsin_one  :
real.arcsin 1 = π / 2

source
theorem real.arcsin_of_one_le {x : ℝ} (hx : 1 ≤ x) :
real.arcsin x = π / 2

source
theorem real.arcsin_neg_one  :
real.arcsin (-1) = -(π / 2)

source
theorem real.arcsin_of_le_neg_one {x : ℝ} (hx : x ≤ -1) :
real.arcsin x = -(π / 2)

source
@[simp]
theorem real.arcsin_neg (x : ℝ) :
real.arcsin (-x) = -real.arcsin x

source
theorem real.arcsin_le_iff_le_sin {x y : ℝ} (hx : x ∈ set.Icc (-1) 1) (hy : y ∈ set.Icc (-(π / 2)) (π / 2)) :
real.arcsin x ≤ y ↔ x ≤ real.sin y

source
theorem real.arcsin_le_iff_le_sin' {x y : ℝ} (hy : y ∈ set.Ico (-(π / 2)) (π / 2)) :
real.arcsin x ≤ y ↔ x ≤ real.sin y

source
theorem real.le_arcsin_iff_sin_le {x y : ℝ} (hx : x ∈ set.Icc (-(π / 2)) (π / 2)) (hy : y ∈ set.Icc (-1) 1) :
x ≤ real.arcsin y ↔ real.sin x ≤ y

source
theorem real.le_arcsin_iff_sin_le' {x y : ℝ} (hx : x ∈ set.Ioc (-(π / 2)) (π / 2)) :
x ≤ real.arcsin y ↔ real.sin x ≤ y

source
theorem real.arcsin_lt_iff_lt_sin {x y : ℝ} (hx : x ∈ set.Icc (-1) 1) (hy : y ∈ set.Icc (-(π / 2)) (π / 2)) :
real.arcsin x < y ↔ x < real.sin y

source
theorem real.arcsin_lt_iff_lt_sin' {x y : ℝ} (hy : y ∈ set.Ioc (-(π / 2)) (π / 2)) :
real.arcsin x < y ↔ x < real.sin y

source
theorem real.lt_arcsin_iff_sin_lt {x y : ℝ} (hx : x ∈ set.Icc (-(π / 2)) (π / 2)) (hy : y ∈ set.Icc (-1) 1) :
x < real.arcsin y ↔ real.sin x < y

source
theorem real.lt_arcsin_iff_sin_lt' {x y : ℝ} (hx : x ∈ set.Ico (-(π / 2)) (π / 2)) :
x < real.arcsin y ↔ real.sin x < y

source
theorem real.arcsin_eq_iff_eq_sin {x y : ℝ} (hy : y ∈ set.Ioo (-(π / 2)) (π / 2)) :
real.arcsin x = y ↔ x = real.sin y

source
@[simp]
theorem real.arcsin_nonneg {x : ℝ} :
0 ≤ real.arcsin x ↔ 0 ≤ x

source
@[simp]
theorem real.arcsin_nonpos {x : ℝ} :
real.arcsin x ≤ 0 ↔ x ≤ 0

source
@[simp]
theorem real.arcsin_eq_zero_iff {x : ℝ} :
real.arcsin x = 0 ↔ x = 0

source
@[simp]
theorem real.zero_eq_arcsin_iff {x : ℝ} :
0 = real.arcsin x ↔ x = 0

source
@[simp]
theorem real.arcsin_pos {x : ℝ} :
0 < real.arcsin x ↔ 0 < x

source
@[simp]
theorem real.arcsin_lt_zero {x : ℝ} :
real.arcsin x < 0 ↔ x < 0

source
@[simp]
theorem real.arcsin_lt_pi_div_two {x : ℝ} :
real.arcsin x < π / 2 ↔ x < 1

source
@[simp]
theorem real.neg_pi_div_two_lt_arcsin {x : ℝ} :
-(π / 2) < real.arcsin x ↔ -1 < x

source
@[simp]
theorem real.arcsin_eq_pi_div_two {x : ℝ} :
real.arcsin x = π / 2 ↔ 1 ≤ x

source
@[simp]
theorem real.pi_div_two_eq_arcsin {x : ℝ} :
π / 2 = real.arcsin x ↔ 1 ≤ x

source
@[simp]
theorem real.pi_div_two_le_arcsin {x : ℝ} :
π / 2 ≤ real.arcsin x ↔ 1 ≤ x

source
@[simp]
theorem real.arcsin_eq_neg_pi_div_two {x : ℝ} :
real.arcsin x = -(π / 2) ↔ x ≤ -1

source
@[simp]
theorem real.neg_pi_div_two_eq_arcsin {x : ℝ} :
-(π / 2) = real.arcsin x ↔ x ≤ -1

source
@[simp]
theorem real.arcsin_le_neg_pi_div_two {x : ℝ} :
real.arcsin x ≤ -(π / 2) ↔ x ≤ -1

source
theorem real.maps_to_sin_Ioo  :
set.maps_to real.sin (set.Ioo (-(π / 2)) (π / 2)) (set.Ioo (-1) 1)

source
@[simp]
def real.sin_local_homeomorph  :
local_homeomorph ℝ ℝ

real.sin as a local_homeomorph between (-π / 2, π / 2) and (-1, 1).

Equations
source
theorem real.cos_arcsin_nonneg (x : ℝ) :
0 ≤ real.cos (real.arcsin x)

source
theorem real.cos_arcsin {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
real.cos (real.arcsin x) = real.sqrt (1 - x ^ 2)

source
theorem real.deriv_arcsin_aux {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) :
has_deriv_at real.arcsin (1 / real.sqrt (1 - x ^ 2)) x ∧ times_cont_diff_at ℝ ⊤ real.arcsin x

source
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

source
theorem real.times_cont_diff_at_arcsin {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} :
times_cont_diff_at ℝ n real.arcsin x

source
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

source
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

source
theorem real.differentiable_within_at_arcsin_Ici {x : ℝ} :
differentiable_within_at ℝ real.arcsin (set.Ici x) x ↔ x ≠ -1

source
theorem real.differentiable_within_at_arcsin_Iic {x : ℝ} :
differentiable_within_at ℝ real.arcsin (set.Iic x) x ↔ x ≠ 1

source
theorem real.differentiable_at_arcsin {x : ℝ} :
differentiable_at ℝ real.arcsin x ↔ x ≠ -1 ∧ x ≠ 1

source
@[simp]
theorem real.deriv_arcsin  :
deriv real.arcsin = λ (x : ℝ), 1 / real.sqrt (1 - x ^ 2)

source
theorem real.differentiable_on_arcsin  :
differentiable_on ℝ real.arcsin {-1, 1}ᶜ

source
theorem real.times_cont_diff_on_arcsin {n : with_top ℕ} :
times_cont_diff_on ℝ n real.arcsin {-1, 1}ᶜ

source
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

source
theorem real.measurable_arcsin  :
measurable real.arcsin

source
def real.arccos (x : ℝ) :
ℝ

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
source
theorem real.arccos_eq_pi_div_two_sub_arcsin (x : ℝ) :
real.arccos x = π / 2 - real.arcsin x

source
theorem real.arcsin_eq_pi_div_two_sub_arccos (x : ℝ) :
real.arcsin x = π / 2 - real.arccos x

source
theorem real.arccos_le_pi (x : ℝ) :
real.arccos x ≤ π

source
theorem real.arccos_nonneg (x : ℝ) :
0 ≤ real.arccos x

source
theorem real.cos_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
real.cos (real.arccos x) = x

source
theorem real.arccos_cos {x : ℝ} (hx₁ : 0 ≤ x) (hx₂ : x ≤ π) :
real.arccos (real.cos x) = x

source
theorem real.strict_mono_decr_on_arccos  :
strict_mono_decr_on real.arccos (set.Icc (-1) 1)

source
theorem real.arccos_inj_on  :
set.inj_on real.arccos (set.Icc (-1) 1)

source
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

source
@[simp]
theorem real.arccos_zero  :
real.arccos 0 = π / 2

source
@[simp]
theorem real.arccos_one  :
real.arccos 1 = 0

source
@[simp]
theorem real.arccos_neg_one  :
real.arccos (-1) = π

source
@[simp]
theorem real.arccos_eq_zero {x : ℝ} :
real.arccos x = 0 ↔ 1 ≤ x

source
@[simp]
theorem real.arccos_eq_pi_div_two {x : ℝ} :
real.arccos x = π / 2 ↔ x = 0

source
@[simp]
theorem real.arccos_eq_pi {x : ℝ} :
real.arccos x = π ↔ x ≤ -1

source
theorem real.arccos_neg (x : ℝ) :
real.arccos (-x) = π - real.arccos x

source
theorem real.sin_arccos {x : ℝ} (hx₁ : -1 ≤ x) (hx₂ : x ≤ 1) :
real.sin (real.arccos x) = real.sqrt (1 - x ^ 2)

source
theorem real.continuous_arccos  :
continuous real.arccos

source
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

source
theorem real.times_cont_diff_at_arccos {x : ℝ} (h₁ : x ≠ -1) (h₂ : x ≠ 1) {n : with_top ℕ} :
times_cont_diff_at ℝ n real.arccos x

source
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

source
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

source
theorem real.differentiable_within_at_arccos_Ici {x : ℝ} :
differentiable_within_at ℝ real.arccos (set.Ici x) x ↔ x ≠ -1

source
theorem real.differentiable_within_at_arccos_Iic {x : ℝ} :
differentiable_within_at ℝ real.arccos (set.Iic x) x ↔ x ≠ 1

source
theorem real.differentiable_at_arccos {x : ℝ} :
differentiable_at ℝ real.arccos x ↔ x ≠ -1 ∧ x ≠ 1

source
@[simp]
theorem real.deriv_arccos  :
deriv real.arccos = λ (x : ℝ), -(1 / real.sqrt (1 - x ^ 2))

source
theorem real.differentiable_on_arccos  :
differentiable_on ℝ real.arccos {-1, 1}ᶜ

source
theorem real.times_cont_diff_on_arccos {n : with_top ℕ} :
times_cont_diff_on ℝ n real.arccos {-1, 1}ᶜ

source
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

source
theorem real.measurable_arccos  :
measurable real.arccos

source
@[simp]
theorem real.tan_pi_div_four  :
real.tan (π / 4) = 1

source
@[simp]
theorem real.tan_pi_div_two  :
real.tan (π / 2) = 0

source
theorem real.tan_pos_of_pos_of_lt_pi_div_two {x : ℝ} (h0x : 0 < x) (hxp : x < π / 2) :
0 < real.tan x

source
theorem real.tan_nonneg_of_nonneg_of_le_pi_div_two {x : ℝ} (h0x : 0 ≤ x) (hxp : x ≤ π / 2) :
0 ≤ real.tan x

source
theorem real.tan_neg_of_neg_of_pi_div_two_lt {x : ℝ} (hx0 : x < 0) (hpx : -(π / 2) < x) :
real.tan x < 0

source
theorem real.tan_nonpos_of_nonpos_of_neg_pi_div_two_le {x : ℝ} (hx0 : x ≤ 0) (hpx : -(π / 2) ≤ x) :
real.tan x ≤ 0

source
theorem real.tan_lt_tan_of_nonneg_of_lt_pi_div_two {x y : ℝ} (hx₁ : 0 ≤ x) (hy₂ : y < π / 2) (hxy : x < y) :
real.tan x < real.tan y

source
theorem real.tan_lt_tan_of_lt_of_lt_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) < x) (hy₂ : y < π / 2) (hxy : x < y) :
real.tan x < real.tan y

source
theorem real.strict_mono_incr_on_tan  :
strict_mono_incr_on real.tan (set.Ioo (-(π / 2)) (π / 2))

source
theorem real.inj_on_tan  :
set.inj_on real.tan (set.Ioo (-(π / 2)) (π / 2))

source
theorem real.tan_inj_of_lt_of_lt_pi_div_two {x y : ℝ} (hx₁ : -(π / 2) < x) (hx₂ : x < π / 2) (hy₁ : -(π / 2) < y) (hy₂ : y < π / 2) (hxy : real.tan x = real.tan y) :
x = y

source
def complex.arg (x : ℂ) :
ℝ

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
source
theorem complex.arg_le_pi (x : ℂ) :
x.arg ≤ π

source
theorem complex.neg_pi_lt_arg (x : ℂ) :
-π < x.arg

source
theorem complex.arg_eq_arg_neg_add_pi_of_im_nonneg_of_re_neg {x : ℂ} (hxr : x.re < 0) (hxi : 0 ≤ x.im) :
x.arg = (-x).arg + π

source
theorem complex.arg_eq_arg_neg_sub_pi_of_im_neg_of_re_neg {x : ℂ} (hxr : x.re < 0) (hxi : x.im < 0) :
x.arg = (-x).arg - π

source
@[simp]
theorem complex.arg_zero  :
0.arg = 0

source
@[simp]
theorem complex.arg_one  :
1.arg = 0

source
@[simp]
theorem complex.arg_neg_one  :
(-1).arg = π

source
@[simp]
theorem complex.arg_I  :
complex.I.arg = π / 2

source
@[simp]
theorem complex.arg_neg_I  :
(-complex.I).arg = -(π / 2)

source
theorem complex.sin_arg (x : ℂ) :
real.sin x.arg = x.im / complex.abs x

source
theorem complex.cos_arg {x : ℂ} (hx : x ≠ 0) :
real.cos x.arg = x.re / complex.abs x

source
theorem complex.tan_arg {x : ℂ} :
real.tan x.arg = x.im / x.re

source
theorem complex.arg_cos_add_sin_mul_I {x : ℝ} (hx₁ : -π < x) (hx₂ : x ≤ π) :
(complex.cos ↑x + (complex.sin ↑x) * complex.I).arg = x

source
theorem complex.arg_eq_arg_iff {x y : ℂ} (hx : x ≠ 0) (hy : y ≠ 0) :
x.arg = y.arg ↔ (↑(complex.abs y) / ↑(complex.abs x)) * x = y

source
theorem complex.arg_real_mul (x : ℂ) {r : ℝ} (hr : 0 < r) :
((↑r) * x).arg = x.arg

source
theorem complex.ext_abs_arg {x y : ℂ} (h₁ : complex.abs x = complex.abs y) (h₂ : x.arg = y.arg) :
x = y

source
theorem complex.arg_of_real_of_nonneg {x : ℝ} (hx : 0 ≤ x) :
↑x.arg = 0

source
theorem complex.arg_of_real_of_neg {x : ℝ} (hx : x < 0) :
↑x.arg = π

source
def complex.log (x : ℂ) :
ℂ

Inverse of the exp function. Returns values such that (log x).im > - π and (log x).im ≤ π. log 0 = 0

Equations