mathlib3 documentation

analysis.special_functions.trigonometric.arctan_deriv

Derivatives of the tan and arctan functions. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Continuity and derivatives of the tangent and arctangent functions.

theorem real.has_deriv_at_tan {x : } (h : real.cos x 0) :
@[simp]
theorem real.deriv_tan (x : ) :
@[simp]
theorem real.has_deriv_at_arctan (x : ) :
has_deriv_at real.arctan (1 / (1 + x ^ 2)) x
@[simp]
theorem real.deriv_arctan  :
deriv real.arctan = λ (x : ), 1 / (1 + x ^ 2)

Lemmas for derivatives of the composition of real.arctan with a differentiable function #

In this section we register lemmas for the derivatives of the composition of real.arctan with a differentiable function, for standalone use and use with simp.

theorem has_strict_deriv_at.arctan {f : } {f' x : } (hf : has_strict_deriv_at f f' x) :
has_strict_deriv_at (λ (x : ), real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
theorem has_deriv_at.arctan {f : } {f' x : } (hf : has_deriv_at f f' x) :
has_deriv_at (λ (x : ), real.arctan (f x)) (1 / (1 + f x ^ 2) * f') x
theorem has_deriv_within_at.arctan {f : } {f' x : } {s : set } (hf : has_deriv_within_at f f' s x) :
has_deriv_within_at (λ (x : ), real.arctan (f x)) (1 / (1 + f x ^ 2) * f') s x
theorem deriv_within_arctan {f : } {x : } {s : set } (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
deriv_within (λ (x : ), real.arctan (f x)) s x = 1 / (1 + f x ^ 2) * deriv_within f s x
@[simp]
theorem deriv_arctan {f : } {x : } (hc : differentiable_at f x) :
deriv (λ (x : ), real.arctan (f x)) x = 1 / (1 + f x ^ 2) * deriv f x
theorem has_strict_fderiv_at.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {f' : E →L[] } {x : E} (hf : has_strict_fderiv_at f f' x) :
has_strict_fderiv_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) f') x
theorem has_fderiv_at.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {f' : E →L[] } {x : E} (hf : has_fderiv_at f f' x) :
has_fderiv_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) f') x
theorem has_fderiv_within_at.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {f' : E →L[] } {x : E} {s : set E} (hf : has_fderiv_within_at f f' s x) :
has_fderiv_within_at (λ (x : E), real.arctan (f x)) ((1 / (1 + f x ^ 2)) f') s x
theorem fderiv_within_arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {s : set E} (hf : differentiable_within_at f s x) (hxs : unique_diff_within_at s x) :
fderiv_within (λ (x : E), real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) fderiv_within f s x
@[simp]
theorem fderiv_arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
fderiv (λ (x : E), real.arctan (f x)) x = (1 / (1 + f x ^ 2)) fderiv f x
theorem differentiable_within_at.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {s : set E} (hf : differentiable_within_at f s x) :
differentiable_within_at (λ (x : E), real.arctan (f x)) s x
@[simp]
theorem differentiable_at.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} (hc : differentiable_at f x) :
differentiable_at (λ (x : E), real.arctan (f x)) x
theorem differentiable_on.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} (hc : differentiable_on f s) :
differentiable_on (λ (x : E), real.arctan (f x)) s
@[simp]
theorem differentiable.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } (hc : differentiable f) :
differentiable (λ (x : E), real.arctan (f x))
theorem cont_diff_at.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {n : ℕ∞} (h : cont_diff_at n f x) :
cont_diff_at n (λ (x : E), real.arctan (f x)) x
theorem cont_diff.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {n : ℕ∞} (h : cont_diff n f) :
cont_diff n (λ (x : E), real.arctan (f x))
theorem cont_diff_within_at.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {x : E} {s : set E} {n : ℕ∞} (h : cont_diff_within_at n f s x) :
cont_diff_within_at n (λ (x : E), real.arctan (f x)) s x
theorem cont_diff_on.arctan {E : Type u_1} [normed_add_comm_group E] [normed_space E] {f : E } {s : set E} {n : ℕ∞} (h : cont_diff_on n f s) :
cont_diff_on n (λ (x : E), real.arctan (f x)) s