analysis.special_functions.trigonometric

source

theorem complex.has_strict_deriv_at_sin (x : ℂ) :

has_strict_deriv_at complex.sin (complex.cos x) x

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

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_strict_deriv_at_cos (x : ℂ) :

has_strict_deriv_at complex.cos (-complex.sin x) x

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

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_strict_deriv_at_sinh (x : ℂ) :

has_strict_deriv_at complex.sinh (complex.cosh x) x

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

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_strict_deriv_at_cosh (x : ℂ) :

has_strict_deriv_at complex.cosh (complex.sinh x) x

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

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

source

theorem measurable.ccos {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :

measurable (λ (x : α), complex.cos (f x))

source

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

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

source

theorem measurable.csin {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :

measurable (λ (x : α), complex.sin (f x))

source

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

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

source

theorem measurable.ccosh {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :

measurable (λ (x : α), complex.cosh (f x))

source

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

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

source

theorem measurable.csinh {α : Type u_1} [measurable_space α] {f : α → ℂ} (hf : measurable f) :

measurable (λ (x : α), complex.sinh (f x))

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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_strict_deriv_at_sin (x : ℝ) :

has_strict_deriv_at real.sin (real.cos x) 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.continuous_on_sin {s : set ℝ} :

continuous_on real.sin s

source

theorem real.measurable_sin :

measurable real.sin

source

theorem real.has_strict_deriv_at_cos (x : ℝ) :

has_strict_deriv_at real.cos (-real.sin x) x

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_strict_deriv_at_sinh (x : ℝ) :

has_strict_deriv_at real.sinh (real.cosh x) x

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_strict_deriv_at_cosh (x : ℝ) :

has_strict_deriv_at real.cosh (real.sinh x) x

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.

source

theorem measurable.cos {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), real.cos (f x))

source

theorem has_strict_deriv_at.cos {f : ℝ → ℝ} {f' x : ℝ} (hf : has_strict_deriv_at f f' x) :

has_strict_deriv_at (λ (x : ℝ), real.cos (f x)) ((-real.sin (f x)) * 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

source

theorem measurable.sin {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), real.sin (f x))

source

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

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

source

theorem measurable.cosh {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), real.cosh (f x))

source

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

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

source

theorem measurable.sinh {α : Type u_1} [measurable_space α] {f : α → ℝ} (hf : measurable f) :

measurable (λ (x : α), real.sinh (f x))

source

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

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

source

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

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

source

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

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

source

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

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

source

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

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

π = 2 * classical.some real.exists_cos_eq_zero

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

def nnreal.pi :

ℝ≥0

π considered as a nonnegative real.

Equations

nnreal.pi = ⟨π, nnreal.pi._proof_1⟩

source

@[simp]

theorem nnreal.coe_real_pi :

↑nnreal.pi = π

source

theorem nnreal.pi_pos :

0 < nnreal.pi

source

theorem nnreal.pi_ne_zero :

nnreal.pi ≠ 0

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_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.sin_add_pi (x : ℝ) :

real.sin (x + π) = -real.sin x

source

theorem real.sin_add_int_mul_two_pi (x : ℝ) (n : ℤ) :

real.sin (x + (↑n) * 2 * π) = real.sin x

source

theorem real.sin_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :

real.sin (x - (↑n) * 2 * π) = real.sin x

source

theorem real.sin_add_nat_mul_two_pi (x : ℝ) (n : ℕ) :

real.sin (x + (↑n) * 2 * π) = real.sin x

source

theorem real.sin_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :

real.sin (x - (↑n) * 2 * π) = real.sin x

source

theorem real.sin_add_two_pi (x : ℝ) :

real.sin (x + 2 * π) = real.sin x

source

theorem real.sin_sub_two_pi (x : ℝ) :

real.sin (x - 2 * π) = real.sin x

source

theorem real.cos_add_int_mul_two_pi (x : ℝ) (n : ℤ) :

real.cos (x + (↑n) * 2 * π) = real.cos x

source

theorem real.cos_sub_int_mul_two_pi (x : ℝ) (n : ℤ) :

real.cos (x - (↑n) * 2 * π) = real.cos x

source

theorem real.cos_add_nat_mul_two_pi (x : ℝ) (n : ℕ) :

real.cos (x + (↑n) * 2 * π) = real.cos x

source

theorem real.cos_sub_nat_mul_two_pi (x : ℝ) (n : ℕ) :

real.cos (x - (↑n) * 2 * π) = real.cos x

source

theorem real.cos_int_mul_two_pi_add_pi (n : ℤ) :

real.cos ((↑n) * 2 * π + π) = -1

source

theorem real.cos_int_mul_two_pi_sub_pi (n : ℤ) :

real.cos ((↑n) * 2 * π - π) = -1

source

theorem real.cos_nat_mul_two_pi_add_pi (n : ℕ) :

real.cos ((↑n) * 2 * π + π) = -1

source

theorem real.cos_nat_mul_two_pi_sub_pi (n : ℕ) :

real.cos ((↑n) * 2 * π - π) = -1

source

theorem real.cos_add_two_pi (x : ℝ) :

real.cos (x + 2 * π) = real.cos x

source

theorem real.cos_sub_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_sub_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_nonneg_of_neg_pi_div_two_le_of_le {x : ℝ} (hl : -(π / 2) ≤ x) (hu : x ≤ π / 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_eq_sqrt_one_sub_cos_sq {x : ℝ} (hl : 0 ≤ x) (hu : x ≤ π) :

real.sin x = real.sqrt (1 - real.cos x ^ 2)

source

theorem real.cos_eq_sqrt_one_sub_sin_sq {x : ℝ} (hl : -(π / 2) ≤ x) (hu : x ≤ π / 2) :

real.cos x = real.sqrt (1 - real.sin x ^ 2)

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

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

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

real.angle = quotient_add_group.quotient (add_subgroup.gmultiples (2 * π))

source

@[instance]

def real.angle.angle.add_comm_group :

add_comm_group real.angle

Equations

real.angle.angle.add_comm_group = quotient_add_group.add_comm_group (add_subgroup.gmultiples (2 * π))

source

@[instance]

def real.angle.inhabited :

inhabited real.angle

Equations

real.angle.inhabited = {default := 0}

source

@[instance]

def real.angle.angle.has_coe :

has_coe ℝ real.angle

Equations

real.angle.angle.has_coe = {coe := quotient.mk' (quotient_add_group.left_rel (add_subgroup.gmultiples (2 * π)))}

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

real.sin_order_iso = (strict_mono_incr_on.order_iso real.sin (set.Icc (-(π / 2)) (π / 2)) real.strict_mono_incr_on_sin).trans (order_iso.set_congr (real.sin '' set.Icc (-(π / 2)) (π / 2)) (set.Icc (-1) 1) real.sin_order_iso._proof_1)

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

real.arcsin = coe ∘ set.Icc_extend real.arcsin._proof_1 ⇑(real.sin_order_iso.symm)

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

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}

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_strict_deriv_at real.arcsin (1 / real.sqrt (1 - x ^ 2)) x ∧ times_cont_diff_at ℝ ⊤ real.arcsin x

source

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

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