mathlib3documentation

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_strict_deriv_at_tan {x : } (h : 0) :
(1 / ^ 2) x
theorem real.has_deriv_at_tan {x : } (h : 0) :
(1 / ^ 2) x
theorem real.tendsto_abs_tan_at_top (k : ) :
filter.tendsto (λ (x : ), ||) (nhds_within ((2 * k + 1) * real.pi / 2) {(2 * k + 1) * real.pi / 2}) filter.at_top
theorem real.continuous_at_tan {x : } :
0
@[simp]
theorem real.deriv_tan (x : ) :
= 1 / ^ 2
@[simp]
theorem real.cont_diff_at_tan {n : ℕ∞} {x : } :
0
theorem real.has_deriv_at_tan_of_mem_Ioo {x : } (h : x set.Ioo (-(real.pi / 2)) (real.pi / 2)) :
(1 / ^ 2) x
theorem real.has_strict_deriv_at_arctan (x : ) :
(1 / (1 + x ^ 2)) x
theorem real.has_deriv_at_arctan (x : ) :
(1 / (1 + x ^ 2)) x
@[simp]
theorem real.deriv_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 : 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 : 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 : 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 : x) (hxs : x) :
deriv_within (λ (x : ), real.arctan (f x)) s x = 1 / (1 + f x ^ 2) * s x
@[simp]
theorem deriv_arctan {f : } {x : } (hc : x) :
deriv (λ (x : ), real.arctan (f x)) x = 1 / (1 + f x ^ 2) * x
theorem has_strict_fderiv_at.arctan {E : Type u_1} [ E] {f : E } {f' : E →L[] } {x : E} (hf : 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} [ E] {f : E } {f' : E →L[] } {x : E} (hf : 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} [ E] {f : E } {f' : E →L[] } {x : E} {s : set E} (hf : 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} [ E] {f : E } {x : E} {s : set E} (hf : x) (hxs : x) :
(λ (x : E), real.arctan (f x)) s x = (1 / (1 + f x ^ 2)) s x
@[simp]
theorem fderiv_arctan {E : Type u_1} [ E] {f : E } {x : E} (hc : x) :
(λ (x : E), real.arctan (f x)) x = (1 / (1 + f x ^ 2)) f x
theorem differentiable_within_at.arctan {E : Type u_1} [ E] {f : E } {x : E} {s : set E} (hf : x) :
(λ (x : E), real.arctan (f x)) s x
@[simp]
theorem differentiable_at.arctan {E : Type u_1} [ E] {f : E } {x : E} (hc : x) :
(λ (x : E), real.arctan (f x)) x
theorem differentiable_on.arctan {E : Type u_1} [ E] {f : E } {s : set E} (hc : s) :
(λ (x : E), real.arctan (f x)) s
@[simp]
theorem differentiable.arctan {E : Type u_1} [ E] {f : E } (hc : f) :
(λ (x : E), real.arctan (f x))
theorem cont_diff_at.arctan {E : Type u_1} [ E] {f : E } {x : E} {n : ℕ∞} (h : f x) :
(λ (x : E), real.arctan (f x)) x
theorem cont_diff.arctan {E : Type u_1} [ E] {f : E } {n : ℕ∞} (h : f) :
(λ (x : E), real.arctan (f x))
theorem cont_diff_within_at.arctan {E : Type u_1} [ E] {f : E } {x : E} {s : set E} {n : ℕ∞} (h : s x) :
(λ (x : E), real.arctan (f x)) s x
theorem cont_diff_on.arctan {E : Type u_1} [ E] {f : E } {s : set E} {n : ℕ∞} (h : f s) :
(λ (x : E), real.arctan (f x)) s